Asistente de pruebas Lean e IA: cómo las demostraciones se vuelven verificables por máquina

Once días, un enjambre de agentes, 13 millones de líneas de código: una IA ha hecho verificable por máquina la demostración del último teorema de Fermat. Lo decisivo no fue tanto la potencia de cálculo como un verificador que no deja pasar ningún error.

Hacia 1637, Pierre de Fermat anotó en el margen de un libro una afirmación para la que supuestamente tenía una demostración. Nunca se encontró. Tuvieron que pasar hasta 1995 para que Andrew Wiles publicara una demostración completa. El 4 de septiembre de 2026, Anthropic comunicó que un enjambre de agentes Claude ha formalizado por completo esa demostración en el lenguaje de pruebas Lean. Lo hizo posible el asistente de pruebas Lean, que comprueba por máquina cada paso de una demostración.

Este artículo sitúa ese anuncio en contexto. Explica qué es un asistente de pruebas y por qué un resultado de Lean se considera fiable. Describe cómo colaboraron los agentes y compara el anuncio con los problemas de olimpiadas y los problemas de Erdős. Para ello se separan las cifras documentadas, las declaraciones del fabricante y las cuestiones abiertas. La tesis: lo nuevo no es solo que una IA trabaje en matemáticas. Lo nuevo es la combinación de un modelo que puede probar libremente y un programa que da por buenos, sin concesiones, todos los pasos.

El último teorema de Fermat: qué ha comunicado realmente Anthropic

El teorema afirma que la ecuación aⁿ + bⁿ = cⁿ no tiene solución en números enteros mayores que cero con un exponente n mayor que 2. El enunciado es fácil de entender y durante siglos fue extremadamente difícil de demostrar. En 1908 se ofreció un premio de 100.000 marcos de oro y, según Anthropic, en el primer año llegaron 621 demostraciones erróneas. Wiles presentó una demostración en 1993, encontró una laguna y la cerró junto con Richard Taylor. La publicación llegó en mayo de 1995.

El anuncio más reciente se refiere a cuán segura es esa demostración cuando una máquina comprueba cada paso. Los datos principales de la publicación de Anthropic figuran en la tabla.

Un token es un pequeño fragmento de texto que genera un modelo de lenguaje, por ejemplo una parte de una palabra. La fuente no indica costes en dinero. Todos los datos proceden del fabricante y no se han recontado de forma independiente.

Es importante delimitar bien el alcance. Se trata de una formalización, no de una demostración nueva. El teorema estaba demostrado desde 1995. Según Anthropic, los agentes partieron de una versión simplificada de la demostración de Wiles elaborada por Darmon, Diamond y Taylor, y aprovecharon partes del proyecto de formalización del Imperial College y del proyecto flt-regular. Quien lea que una IA ha resuelto el teorema de Fermat no debería pensar en un nuevo descubrimiento matemático, sino en una verificación. Anthropic distingue expresamente este resultado del trabajo de IA sobre la hipótesis de Riemann, en el que, según afirma, se descubrió algo nuevo.

Qué es el asistente de pruebas Lean: un sistema que no omite ningún paso

El asistente de pruebas Lean es un lenguaje de programación de código abierto con el que se pueden escribir demostraciones matemáticas de forma que un ordenador pueda comprobarlas. La página del proyecto lean-lang.org describe Lean como un lenguaje de programación y asistente de pruebas con un núcleo mínimo y de confianza que garantiza la corrección. Lean fue desarrollado por Leonardo de Moura y publicado como código abierto en 2013, según informa la Simons Foundation. Desde 2023, la organización sin ánimo de lucro Lean FRO trabaja en su desarrollo, con el apoyo, entre otros, de 5 millones de dólares de la Simons Foundation International.

El principio puede expresarse con palabras cotidianas. Una demostración en Lean es un programa. El núcleo de Lean comprueba paso a paso si cada conclusión se sigue de los axiomas y de teoremas ya verificados. Los axiomas son las suposiciones básicas de las matemáticas, que se aceptan sin demostración. Un paso que no se sigue es rechazado, por convincente que suene. Donde aún falta una demostración, Lean muestra el marcador «sorry». Una demostración con esos marcadores se considera incompleta.

Precisamente eso hace que Lean sea tan útil para los modelos de IA. Los modelos de lenguaje pueden expresarse de forma convincente y, aun así, cometer errores. En matemáticas eso es un problema, porque un error en el paso 400 puede invalidar todo lo que viene después. Con un asistente de pruebas como Lean desaparece la pregunta de si hay que creer al modelo.

Una revisión humana funciona de otra manera. Especialistas leen una demostración, la consideran plausible y confían en su experiencia. Eso es valioso, pero cuesta tiempo y deja margen para pasar algo por alto. Ya en 2021, un proyecto colaborativo validó en Lean una demostración compleja de Peter Scholze, como relata la Simons Foundation. La comprobación mediante el asistente de pruebas no sustituye la comprensión matemática, pero aporta certeza sobre la corrección.

El esquema de la figura 1 muestra el reparto de tareas: el modelo hace propuestas y el núcleo de Lean dicta sentencia. Para el veredicto da igual que una propuesta provenga de una persona, de un modelo o de un generador aleatorio.

Mathlib y la pregunta de quién comprueba lo comprobado

Lean por sí solo todavía no contiene matemáticas. Estas residen en Mathlib, la biblioteca desarrollada de forma colaborativa sobre la que se apoyan casi todas las formalizaciones. La página de Lean habla de más de un millón de líneas. La página de estadísticas de la comunidad indicaba en el momento de la consulta 139.391 definiciones, 290.502 teoremas y 772 colaboradores. Quien demuestra algo en Lean puede recurrir a estos bloques ya verificados en lugar de empezar desde cero.

Como comparación: según Anthropic, la demostración de Fermat tiene unos 13 millones de líneas y es, por tanto, más de cinco veces mayor que Mathlib. Parece una obra nueva enorme, pero también muestra cuánto cuesta la verificación formal de teoremas profundos, incluso cuando Mathlib proporciona la base. La demostración depende de lo que ya está formalizado en Mathlib.

Hay que plantear dos preguntas de verificación por separado. Primera: ¿es correcta la demostración? Eso lo responde Lean. Anthropic indica que solo se utilizan los tres axiomas estándar. Segunda: ¿se ha demostrado realmente el teorema de Fermat y no un enunciado modificado? Aquí se empleó una herramienta comparadora que confirmó que el enunciado formalizado coincide con la formulación de Mathlib. Esta separación es decisiva. Una demostración sin errores de un enunciado falso no valdría nada.

Según Anthropic, la demostración completa, junto con una explicación escrita, está en GitHub y puede consultarse allí. Lo único que no es público es el modelo utilizado.

Kevin Buzzard, del Imperial College de Londres, que dirige el proyecto de formalización desde 2024, revisó la demostración. Según Anthropic, señala que el teorema se demuestra sin más supuestos que los axiomas de las matemáticas. Queda un límite: Lean comprueba la corrección, no el significado. La herramienta no valora si un resultado es interesante, elegante o importante. La Simons Foundation recoge valoraciones en este sentido de Alex Kontorovich.

IA agéntica: por qué funcionó el enjambre

Varias decenas de agentes trabajaron en paralelo. En este contexto, un agente es un modelo de lenguaje que no solo responde, sino que utiliza herramientas de forma autónoma, edita archivos y comprueba resultados intermedios. La estructura multiagente se basaba en Claude Code. Los agentes definieron conceptos, demostraron resultados intermedios y los utilizaron para enunciados más difíciles. Una introducción general ofrece el artículo La era de los agentes de IA.

Según Anthropic, el avance no lo trajo un modelo más potente, sino una mejor organización. La plataforma Prove2Me, una plataforma abierta de colaboración de Tianyi Peng y colegas de la Universidad de Columbia, ofrecía tres características:

• Un grafo acíclico dirigido de los enunciados de los teoremas servía de orientación: cada enunciado muestra de qué depende y no hay ciclos.
• Los enunciados y las demostraciones estaban en archivos separados. Eso acelera la compilación de Lean, porque no hay que volver a comprobarlo todo con cada cambio.
• Los teoremas ya demostrados podían buscarse y reutilizarse mediante descripciones en lenguaje natural.

Los intentos anteriores sin esta estructura fracasaron porque los agentes perdían el estado del proyecto. Resulta instructivo que, aun así, esos intentos aportaron alrededor del 7 % de las líneas no triviales de la demostración final. La lección: en tareas grandes, la estructura gana a la potencia bruta del modelo. Quien utiliza muchos agentes necesita un plan común, un almacenamiento compartido y responsabilidades claras. Los desarrolladores viven la misma experiencia en cualquier proyecto de agentes de cierto tamaño.

La participación humana fue reducida, pero no nula. Tianyi Peng daba de vez en cuando instrucciones de nivel superior, por ejemplo priorizar la variedad jacobiana como esquema o cerrar pronto el teorema de Mazur. Según la salida de agente citada, el sistema comunicó el resultado raíz como demostrado el 18 de agosto a las 02:00:57 UTC.

De las olimpiadas a los problemas de Erdős: demostraciones de IA desde 2024

El anuncio sobre Fermat no está solo. Desde 2024, varios resultados muestran que la IA puede demostrar matemáticas, y se diferencian en si se usó Lean o no.

En julio de 2024, AlphaProof junto con AlphaGeometry 2 resolvió cuatro de los seis problemas de la Olimpiada Matemática Internacional y alcanzó 28 de 42 puntos, nivel de plata. El umbral del oro era de 29 puntos. AlphaProof demuestra en Lean y resolvió, entre otros, el problema más difícil de la competición. Sin embargo, los problemas se tradujeron antes a mano a lenguaje formal, y el tiempo de cálculo fue de hasta tres días por problema. Los participantes disponen de dos veces 4,5 horas.

En julio de 2025, Gemini Deep Think alcanzó 35 de 42 puntos, nivel de oro, evaluado oficialmente por los coordinadores de la olimpiada. El sistema trabajó en lenguaje natural, dentro del límite de tiempo y sin Lean. Es un contraste deliberado: la IA se vuelve potente incluso sin verificación formal, pero entonces los resultados no están verificados por máquina, sino que deben ser leídos por personas. La empresa Harmonic describe en una publicación en arXiv su sistema Aristotle, que combina la búsqueda de demostraciones basada en Lean con el razonamiento informal y un resolutor de geometría y, según el resumen, alcanza un rendimiento de nivel de oro en los problemas de 2025.

A principios de 2026 los problemas de Erdős pasaron a primer plano, una gran colección de cuestiones abiertas del matemático Paul Erdős. Un ejemplo es el problema 728, cuya demostración por Aristotle en Lean está documentada como elaboración en arXiv. Según la Simons Foundation, además, un joven de 23 años resolvió a principios de 2026 el problema 1196 con ChatGPT y Lean.

La valoración es prudente. La wiki de Terence Tao sobre contribuciones de la IA a los problemas de Erdős se presenta expresamente como algo distinto de un banco de pruebas. Menciona un sesgo de selección, porque los éxitos se documentan con más facilidad que los fracasos. Señala que la falta de avances previos suele indicar desconocimiento y no dificultad, que a posteriori a menudo aparecía bibliografía ya existente y que un problema resuelto no es automáticamente un trabajo listo para publicar. Al mismo tiempo, la wiki recomienda comprobar formalmente en Lean las demostraciones de IA.

El campo de las demostraciones de IA en matemáticas abarca desde problemas de competición hasta problemas marginales y grandes formalizaciones. El desarrollo avanza rápido; si cada anuncio cumple lo que promete el titular debe comprobarse caso por caso. Para eso mismo está pensada una herramienta de verificación como Lean.

Cuánto valen 11 días: una comparación temporal sin exageraciones

Las cifras invitan a comparaciones grandilocuentes. Fermat formuló el teorema en 1637 y Wiles lo demostró en 1995, es decir, 358 años después. El proyecto de formalización del Imperial College se inició en 2024, con un blueprint de 86 páginas, y estaba concebido originalmente para varios años. La formalización por IA duró 11 días.

Esta comparación cojea por varias razones:

• Los 11 días son el tiempo de ejecución de un enjambre de agentes, no el tiempo de cálculo de un solo modelo.
• La demostración era conocida. La IA no tenía que encontrar una idea nueva, sino traducir a Lean una estructura de demostración existente.
• Hubo trabajo previo: Mathlib, material del proyecto del Imperial College y de flt-regular, y un blueprint.
• El esfuerzo de unos seis mil millones de tokens de salida de un modelo interno es considerable. No se indican costes en dinero.

Equiparar 11 días de trabajo de una IA con siglos de trabajo humano sobre el problema es, por tanto, solo una comparación retórica. Lo correcto es esto: un trabajo que un proyecto colaborativo había planificado para varios años se completó en lo esencial en pocos días.

Un experimento paralelo acerca el asunto a la vida cotidiana. Según Anthropic, tres suscripciones personales de Claude Max formalizaron en tres días el teorema de los tres primos de Vinogradov. Los autores consideran posible una formalización colaborativa con suscripciones de consumo si la estructura es adecuada. Es una valoración de los autores y no un resultado confirmado de forma independiente.

Límites y puntos abiertos: lo que el anuncio no demuestra

Anthropic menciona por sí misma algunas limitaciones. La demostración es probablemente bastante más larga de lo necesario, pues Mathlib es más compacta y está mejor revisada. Depende de lo que ya esté formalizado en Mathlib. El modelo utilizado es un modelo de investigación interno y no público, de modo que el resultado no puede repetirse desde fuera con los mismos medios.

Quedan otros puntos abiertos:

• No se ha generado matemática nueva. La formalización aumenta la certeza, no el conocimiento.
• Una demostración en Lean no es automáticamente comprensible. Nadie lee 13 millones de líneas de principio a fin.
• Lean no dice nada sobre la importancia de un teorema, solo sobre su corrección.
• Del anuncio no se desprende hasta qué punto es independiente la verificación más allá de la valoración de Buzzard.

Sobre otros anuncios aislados, por ejemplo mejoras en la hipótesis de Riemann o agentes de autoformalización de empresas concretas, en esta investigación no hay fuentes primarias que se puedan comprobar por uno mismo. Por eso estos anuncios quedan aquí sin cifras. Tampoco se recogen valoraciones de especialistas concretos salvo que se disponga de la declaración original.

Qué significa el enfoque de Lean más allá de las matemáticas

El patrón detrás del proyecto de Fermat es generalizable: prueba libre por un lado, aceptación estricta por el otro. Encaja allí donde un resultado se puede comprobar por máquina. La página de Lean menciona como aplicaciones fuera de las matemáticas la verificación de ArkLib, una biblioteca sobre SNARK (pruebas criptográficas compactas), y de Cedar, el lenguaje de autorización de AWS. En el desarrollo de software el principio es conocido: un compilador y una ejecución de pruebas también dan por bueno, o no, lo que ha escrito una persona o una IA.

De ello se deduce una regla práctica para tratar los resultados de la IA. Cuanto mejor pueda comprobarse automáticamente un resultado, con mayor seguridad puede trabajar un modelo con libertad. En textos, valoraciones y recomendaciones suele faltar esa aceptación estricta. Ahí el verificador sigue siendo la persona.

La misma lógica vale para la seguridad y la protección de datos: las propiedades demostrables cuentan más que las meras afirmaciones. Si un sitio web carga rastreadores o establece cabeceras de seguridad, por ejemplo, puede medirse de forma automatizada. Para ello ofrece una posibilidad la comprobación de sitios web de Dr. DSGVO, y las propiedades técnicas de seguridad pueden comprobarse con los Security-Checks. Ninguna de las dos es una demostración formal en el sentido de Lean, pero siguen la misma idea: medir en lugar de creer.

Experimentos de Dr. DSGVO

Con ayuda de IA se ha elaborado (probablemente) la demostración matemática, y se ha formalizado, de que los hexágonos mágicos existen, según una determinada regla de construcción, para cualquier n (n = longitud del lado de un hexágono en celdas de panal).

El tiempo total de cálculo de la IA fue de casi 9 horas. De ese tiempo, el sistema trabajó de forma autónoma durante casi el 99,9 % y no necesitó ninguna entrada. ¡El tamaño de los archivos de la demostración fue de 173 MB! La formalización con Lean, incluidas las bibliotecas, consumió casi 8 GB de espacio en disco – ¡en pasos intermedios! La demostración completa se prolongó durante un período de 5 días. Se interrumpió por límites de uso o similares.

Próximamente se publicará aquí la demostración. Si es correcta lo tendrán que juzgar personas competentes que entiendan más de matemáticas que el autor, que utilizó la IA 😉

Conclusión: la revolución es la verificabilidad

La IA no ha demostrado de nuevo el último teorema de Fermat, sino que ha formalizado por completo en Lean la demostración de Wiles, según Anthropic en 11 días y con varias decenas de agentes en paralelo. El éxito se basa en dos cosas: una organización que mantiene visible el estado del proyecto y el asistente de pruebas Lean, que solo acepta lo que se sigue.

La evolución desde 2024 muestra que la IA aporta cada vez más demostraciones matemáticas. Cuánto hay de nuevo y cuánto de material conocido debe valorarse caso por caso, y también la wiki de Tao lo advierte. Donde interviene Lean, la corrección sigue siendo verificable. Ese es el verdadero avance: ya no afirmaciones, sino certeza verificada por máquina.