The Coq mailing list

[Florent Hivert <Florent.Hivert AT lri.fr>]

> The reason it happened with the odd order theorem was that mathematicians
> wrote a good roadmap (two essentially self-contained books, by
> Bender--Glauberman and Peterfalvi) which mathematically-inclined computer
> scientists could follow, and it probably helped that the odd order theorem
> was a statement whose proof (not just the statement, but the proof too)
> mostly involved finite objects and hence LEM/AC were not an issue (some
> parts of it use representation theory and hence the complex numbers,
> although the use was not "serious" enough to require non- constructive
> arguments).

Actually complex number are not required. You need only the algebraic closure
of Q, the elements of which can be represented by a finite data-structure and
whose theory is completely computable.

A++

Florent