Proof assistants (Coq, Lean) and AI mathematics (AlphaProof)
Asistentes de demostración (Coq, Lean) y matemáticas con IA (AlphaProof)
- Date
- 1989-2024 · confidence high
- Place
- INRIA, Rocquencourt, France (Coq, 1989); Microsoft Research, Redmond (Lean, 2013); Google DeepMind, London (AlphaProof, 2024)
- Credited to
- Thierry Coquand and Gérard Huet (Coq); Leonardo de Moura (Lean); Kevin Buzzard (formalisation); DeepMind (AlphaProof, silver medal at the 2024 IMO; gold-level in 2025)
- People
- 👤 Gérard Huet1947–👤 Kevin Buzzard1968–👤 Leonardo de Moura👤 Thierry Coquand1961–
- Field
- Knowledge & symbols
What it is
Languages that mechanically verify every step of a proof and AI systems that solve olympiad problems and help formalise theorems. They are changing the way mathematics is done and verified.
What it led to
- The formalisation of major theorems and collaborative libraries (mathlib)
- AI as a mathematical collaborator and the verification of critical software
- The debate over the future of human mathematical research
Built on
Made possible
- formal software verification
- Olympiad-level mathematical AI