Formalización en Lean: Liquid Tensor Experiment y mathlib
Lean formalization: Liquid Tensor Experiment
- Fecha
- 2022 · fiabilidad alta
- Lugar
- Bonn (Alemania) y Londres (Imperial College)
- Autoría
- Peter Scholze (desafío), Johan Commelin y comunidad de mathlib (Kevin Buzzard y otros)
- Personas
- 👤 Peter Scholze1987–
- Ámbito
- Saber y símbolos
Qué se descubrió
Verificación completa en el asistente de pruebas Lean de un teorema de vanguardia de Clausen y Scholze sobre matemática condensada, en 18 meses. Mostró que la matemática de investigación actual puede formalizarse y disparó la biblioteca mathlib.
El proyecto Flyspeck y la prueba de Gonthier del teorema de Feit-Thompson en Coq (2012) fueron los precedentes de gran escala.
A qué dio paso
- formalización sistemática de la matemática
- proyectos de formalización del teorema de Fermat (2024-) y del teorema de los números primos
- IA para demostración automática (AlphaProof)
Se apoya en
- Paradoja de Russell y Principia Mathematica1901
- Coq (cuatro colores, 2005)
- Flyspeck (2014)
- teoría de tipos de Martin-Löf
Hizo posible
- Demostración matemática por inteligencia artificial a nivel de Olimpiada (AlphaProof, FunSearch)2024-2025
- asistentes de prueba integrados en la investigación