Theoretical Computer Science
- lo.logic proof-assistants
- Updated Sat, 28 May 2022 06:38:58 GMT
-
Interesting algorithms in the formalization of the Feit-Thompson theorem?
It looks like George Gonthier and his collaborators have finished formalizing the Odd Order Theorem.
In his earlier work on the Four Color Theorem, Gonthier invented a bunch of new algorithms (mostly variants of BDDs and graph algorithms) which were especially amenable to formal verification. Since he has said that he was continuing to use this small-scale reflection style of verification in the work on finite group theory, I wonder what new algorithmic tricks were developed during this development?
Solution
(Turning a comment into an answer, and expanding on it)
From talking to someone who worked on this: no. He invented all sorts of clever refinements to many proofs, and restructured many theory developments, both of which are extremely valuable, but the algorithms involved are not interesting -- in fact, many of them are dumb brute force, the very opposite of interesting.
Basically what was sought was as direct a line to the proof of Feit Thompson, without worrying about 'computational content' along the way (and even not overly worrying about reusability of some of the modules). This was already extremely ambitious given the timelines. Luckily, several of the people involved in the project have gone on to refactor many parts of the proofs to be
- more reusable for a wider set of applications
- more computationally meaningful
External Links
External links referenced by this document: