LeanDojo es una plataforma de código abierto para demostrar teoremas matemáticos utilizando modelos lingüísticos.

La demostración automatizada de teoremas (ATP) es una tarea que genera pruebas de teoremas formulados en lógica formal. Es útil para las matemáticas formales y sirve de apoyo a la verificación formal, que garantiza la corrección y la seguridad de las aplicaciones de alto riesgo.

Sin embargo, ATP es un reto debido a su gran espacio de búsqueda. Por ello, la Prueba Interactiva de Teoremas (PTI) ha surgido como alternativa. En ITP, las pruebas son generadas por matemáticos que interactúan con herramientas de software denominadas asistentes de pruebas.

El aprendizaje automático podría automatizar este proceso y abrir una nueva forma de demostrar teoremas.

Los grandes modelos lingüísticos pueden automatizar la demostración de teoremas

Los grandes modelos de lenguaje combinados con asistentes de demostración, como Lean, son candidatos para este proceso.

Sin embargo, según un equipo de investigadores de Caltech, Nvidia, MIT, UC Santa Barbara y UT Austin, los métodos existentes son difíciles de reproducir o evolucionar debido al código propietario, los datos y los elevados requisitos computacionales.

Para solucionar este problema, crearon LeanDojo, una plataforma de código abierto para demostrar teoremas matemáticos utilizando modelos lingüísticos.

LeanDojo y ReProver abren la puerta a nuevas investigaciones

LeanDojo ofrece dos características principales para la demostración de teoremas basada en el aprendizaje: la extracción de datos y la interacción programática de modelos con Lean, un asistente de demostración ampliamente utilizado. Según los investigadores, LeanDojo es la primera herramienta capaz de interactuar de forma fiable con Lean, lo que debería reducir significativamente los errores de demostración.

LeanDojo también aborda un importante cuello de botella en la demostración de teoremas: la selección de premisas. El equipo lo demuestra con ReProver (Retrieval-Augmented Prover), un probador basado en un modelo de lenguaje que genera una estrategia de demostración basada en algunas premisas recuperadas de la biblioteca matemática de Lean.

Según el equipo, ReProver supera a otros métodos, demostrando un porcentaje significativo de teoremas en la prueba comparativa LeanDojo, así como en dos conjuntos de datos existentes, MiniF2F y ProofNet. ReProver también puede demostrar teoremas para los que aún no existe una demostración en Lean, lo que lo convierte en una herramienta útil para ampliar las bibliotecas matemáticas existentes en Lean.

¿Los modelos lingüísticos serán coautores de las matemáticas en 2026?
El equipo también está publicando un benchmark construido con LeanDojo, que incluye casi 97.000 teoremas de Mathlib, así como un plugin para ChatGPT.

El matemático Terence Tao predijo recientemente que los modelos lingüísticos que utilizan herramientas externas podrían convertirse en coautores de confianza en matemáticas y otras ciencias para 2026. LeanDojo y ReProver muestran cómo podrían ser esas herramientas y ofrecen ahora a otros investigadores una base para mejorarlas.

Más información en el sitio web de LeanDojo.