<p>(Turning a comment into an answer, and expanding on it)</p>

<p>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.</p>

<p>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</p>

<ul>
<li>more reusable for a wider set of applications</li>
<li>more computationally meaningful</li>
</ul>

CC BY-SA 3.0
2015-08-15T13:35:50.357Z
2015-08-15T13:35:50.357Z
Jacques Carette
<p>It looks like George Gonthier and his collaborators have <a href="http://www.msr-inria.inria.fr/events-news/feit-thompson-proved-in-coq">finished formalizing the Odd Order Theorem</a>. </p>

<p>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 <a href="http://www.msr-inria.inria.fr/Projects/math-components">small-scale reflection</a> style of verification in the work on finite group theory, I wonder what new algorithmic tricks were developed during this development?</p>

CC BY-SA 3.0
2012-09-26T08:01:57.903Z
for reference http://en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem (every finite group of odd order is solvable)
Radu GRIGore
CC BY-SA 3.0
2012-09-26T13:41:43.807Z
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.
Andrej Bauer
CC BY-SA 3.0
2012-12-02T04:01:10.250Z
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.
Jacques Carette
CC BY-SA 3.0
2015-08-15T04:28:29.380Z
@JacquesCarette: I think that should be an answer, seeing as nothing has changed on it in a few years...
Joshua Grochow
<lo.logic><proof-assistants>
Interesting algorithms in the formalization of the Feit-Thompson theorem?
Neel Krishnaswami
# Interesting algorithms in the formalization of the Feit-Thompson theorem?

(Asked by: username_0 on 2012-09-25)

It looks like George Gonthier and his collaborators have [finished formalizing the Odd Order Theorem](http://www.msr-inria.inria.fr/events-news/feit-thompson-proved-in-coq).

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](http://www.msr-inria.inria.fr/Projects/math-components) style of verification in the work on finite group theory, I wonder what new algorithmic tricks were developed during this development?

**Tags:** lo.logic, proof-assistants

> **Comments:**
> **username_1**: for reference http://en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem (every finite group of odd order is solvable)  
> **username_2**: 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.  
> **username_3**: 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.  
> **username_4**: @JacquesCarette: I think that should be an answer, seeing as nothing has changed on it in a few years...  

---

## 1 answers

### Answer by username_3 on 2015-08-15. Score: 11 | Accepted answer

(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


---

