Terence Tao escribe para matemáticos sobre la fiabilidad de Lean y el papel de la IA

El 9 de octubre de 2026, Terence Tao publicó en su blog el post «What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI». El título deja claro a quién se dirige: matemáticos profesionales que se interesan por la verificación formal y por los sistemas de IA que escriben demostraciones. En Hacker News la entrada sumó 53 puntos y 7 comentarios. A nuestro feed solo llegó el enlace, sin texto, por lo que no resumimos los argumentos del autor. A continuación analizamos el contexto en el que aparece una publicación así y por qué es importante.

Por qué la fiabilidad se ha vuelto una cuestión práctica

Lean nació como un proyecto de Leonardo de Moura en Microsoft Research en 2013. Hoy es una herramienta de trabajo para grandes proyectos colectivos. El propio Tao participó a finales de 2023 en la formalización de la conjetura PFR, que llevó unas tres semanas. En 2024 coordinó el Equational Theories Project, cuyo objetivo era determinar 22 028 942 implicaciones entre 4694 identidades sobre magmas. Sin automatización ni verificación formal, ni las personas ni los revisores habrían podido con un volumen así.

En paralelo, los modelos de lenguaje empezaron a trabajar con Lean. En julio de 2024, AlphaProof, de Google DeepMind, resolvió cuatro de los seis problemas de la IMO y obtuvo 28 puntos de 42. Entregaba las demostraciones en Lean. Desde entonces, la pregunta «¿se puede confiar en lo que sale de una cadena así?» ya no pertenece a la filosofía de las matemáticas, sino al trabajo cotidiano.

Dónde está el límite de la confianza

Lean tiene un pequeño núcleo que comprueba cada término de la demostración. Las tácticas, la automatización y el código generado por un modelo quedan fuera del núcleo. Si cometen un error, el núcleo simplemente rechaza el resultado. Eso es lo que hace atractiva la combinación con la IA: una alucinación en la demostración se detecta de forma mecánica.

Quedan puntos en los que la confianza hay que evaluarla por separado:

• Enunciado del teorema. El núcleo confirma que se ha demostrado lo que está escrito. Que coincida con lo que se pretendía lo decide una persona.
• Definiciones. Una definición imprecisa en una biblioteca o en un archivo deja sin contenido el teorema demostrado.
• Axiomas. Lean se apoya en `propext`, `Classical.choice` y `Quot.sound`. El comando `#print axioms` muestra cuáles se han usado.
• `sorry`. Es un marcador que ocupa el lugar de la demostración. Un archivo que lo contiene compila, pero el teorema no está demostrado.
• `native_decide`. Esta táctica añade el compilador a la base de confianza, y en la lista de axiomas aparece `Lean.ofReduceBool`.
• Implementación del núcleo. Existen verificadores independientes, como lean4checker y revisiones de terceros, que reducen el riesgo de error en el propio núcleo.

Qué cambia la IA

Antes de los modelos, el principal límite era el trabajo del formalizador. El modelo alivia parte de esa carga, porque produce cientos de candidatos a demostración. La comprobación por el núcleo sigue siendo barata. En cambio, pasa a primer plano una segunda tarea: asegurarse de que el enunciado formal dice realmente lo que el autor tenía en mente. Esa labor no la hace el núcleo, y un modelo que ajusta la demostración al enunciado puede encontrar resquicios en el propio enunciado. Un ejemplo típico: la afirmación se cumple de forma trivial por un conjunto vacío o por una división por cero mal definida.

De ahí se deriva una conclusión práctica: la auditoría se desplaza de los pasos de la demostración a las condiciones del problema. Para los matemáticos, esto supone más un cambio de habilidad que una pérdida de control.

Cómo trabajar con esto

Si va a usar Lean o un asistente de IA en su investigación, conviene seguir un orden de pasos breve:

• Escriba o relea usted mismo los enunciados de los teoremas, aunque la demostración la haya generado un modelo.
• Antes de publicar, ejecute `#print axioms` y busque `sorry`.
• Compruebe que las definiciones de Mathlib que utiliza coinciden con su comprensión. En los casos no estándar, escriba contraejemplos y lemas de comprobación.
• Para los resultados críticos, pase el archivo por una herramienta de verificación independiente.
• Lea el post original de Tao. Aquí hemos aportado contexto, pero sus argumentos y recomendaciones es mejor tomarlos de la fuente primaria.