Georges Gonthier es un informático canadiense y uno de los principales profesionales de las matemáticas formales . Dirigió la formalización del teorema de los cuatro colores y la demostración de Feit-Thompson del teorema de orden impar . (Ambos fueron escritos usando el asistente de pruebas Coq .)
Ver también
- A prueba de moscas dirigidas por Thomas Callister Hales
Referencias
- Página personal en Microsoft Research
- Documento que describe la prueba del teorema de los cuatro colores
- Artículo de noticias de phys.org que describe la prueba de Feit-Thompson
- Comunicado de prensa de INRIA con enlaces al código Coq de Feit-Thompson Proof