Interesujące algorytmy w formalizacji twierdzenia Feit-Thompson?

Wygląda na to, że George Gonthier i jego współpracownicy zakończyli formalizację Twierdzenia o nieparzystym porządku .

We wcześniejszej pracy nad twierdzeniem o czterech kolorach Gonthier wynalazł szereg nowych algorytmów (głównie wariantów BDD i algorytmów grafowych), które były szczególnie podatne na formalną weryfikację. Ponieważ powiedział, że nadal stosuje ten weryfikacyjny styl weryfikacji na małą skalę w pracy nad teorią grup skończonych, zastanawiam się, jakie nowe sztuczki algorytmiczne opracowano podczas tego rozwoju?

(Przekształcanie komentarza w odpowiedź i rozwijanie go)

Od rozmowy z kimś, kto nad tym pracował: nie. Wynalazł różnego rodzaju sprytne udoskonalenia wielu dowodów i zrestrukturyzował wiele opracowań teorii, z których oba są niezwykle cenne, ale zastosowane algorytmy nie są interesujące - w rzeczywistości wiele z nich jest głupią brutalną siłą, co jest przeciwieństwem interesujących.

Zasadniczo poszukiwano bezpośredniego linku do dowodu Feita Thompsona, nie martwiąc się o „zawartość obliczeniową” po drodze (a nawet nie przejmując się zbytnio możliwością ponownego użycia niektórych modułów). Było to już niezwykle ambitne, biorąc pod uwagę ramy czasowe. Na szczęście kilka osób zaangażowanych w projekt przeredagowało wiele części dowodów

• bardziej wielokrotnego użytku do szerszego zestawu aplikacji
• bardziej znaczący pod względem obliczeniowym