Asistentes de demostración (Coq, Lean) y matemáticas con IA (AlphaProof)
Proof assistants (Coq, Lean) and AI mathematics (AlphaProof)
- Fecha
- 1989-2024 · fiabilidad alta
- Lugar
- INRIA, Rocquencourt, Francia (Coq, 1989); Microsoft Research, Redmond (Lean, 2013); Google DeepMind, Londres (AlphaProof, 2024)
- Autoría
- Thierry Coquand y Gérard Huet (Coq); Leonardo de Moura (Lean); Kevin Buzzard (formalización); DeepMind (AlphaProof, medalla de plata en la IMO 2024; nivel oro en 2025)
- Personas
- 👤 Gérard Huet1947–👤 Kevin Buzzard1968–👤 Leonardo de Moura👤 Thierry Coquand1961–
- Ámbito
- Saber y símbolos
Qué es
Lenguajes que verifican mecánicamente cada paso de una demostración y sistemas de IA que resuelven problemas de olimpiada y ayudan a formalizar teoremas. Cambian la manera de hacer y verificar matemáticas.
A qué dio paso
- La formalización de grandes teoremas y las bibliotecas colaborativas (mathlib)
- La IA como colaborador matemático y la verificación de software crítico
- El debate sobre el futuro de la investigación matemática humana
Se apoya en
Hizo posible
- verificación formal de software
- IA matemática de nivel olímpico