26
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ for reference en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem (every finite group of odd order is solvable) $\endgroup$ – Radu GRIGore Sep 26 '12 at 8:01
  • 4
    $\begingroup$ It should be possible to get Gonthier to answer this questions. Someone who is close to his office, please point him here. Tell him we're great fans of his. $\endgroup$ – Andrej Bauer Sep 26 '12 at 13:41
  • 4
    $\begingroup$ From talking to someone who worked on this: no. He invented all sorts of clever refinements to many proofs, and restructured many theory developments, but the algorithms involved are not interesting -- in fact, many of them are dumb brute force, the very opposite of interesting. $\endgroup$ – Jacques Carette Dec 2 '12 at 4:01
  • $\begingroup$ @JacquesCarette: I think that should be an answer, seeing as nothing has changed on it in a few years... $\endgroup$ – Joshua Grochow Aug 15 '15 at 4:28
10
$\begingroup$

(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
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.