Biography:Georges Gonthier

Short description: Canadian computer scientist

Georges Gonthier is a Canadian computer scientist and one of the leading practitioners in formal mathematics. He led the formalization of the four color theorem and Feit–Thompson proof of the odd-order theorem. (Both were written using the proof assistant Coq.)

See also

• Flyspeck proof led by Thomas Callister Hales

References

• Personal Page at Microsoft Research
• Paper describing proof of the Four color theorem
• phys.org news article describing Feit-Thompson proof
• Press release from INRIA with links to Coq code of Feit-Thompson Proof