--- service: "Publicasta" schema_version: "1.0" article_id: 508 title: "Una IA formaliza en Lean 4 la demostración del último teorema de Fermat" language: "es" default_language: "en" canonical_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked?lang=es" json_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.json?lang=es" api_url: "https://publicasta.com/api/public/v1/channels/good_tech_news/articles/claude_fermat_last_theorem_lean_machine_checked?lang=es" channel_url: "https://publicasta.com/api/public/v1/channels/good_tech_news" channel_articles: "https://publicasta.com/api/public/v1/channels/good_tech_news/articles" search_url: "https://publicasta.com/api/public/v1/search" documentation_url: "https://publicasta.com/api-docs#reading-publicasta" openapi_url: "https://publicasta.com/api-docs/openapi.json" published_at: "2026-09-05T18:26:23+00:00" updated_at: "2026-09-05T18:26:23+00:00" translations: - language: "ar" html_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked?lang=ar" markdown_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.md?lang=ar" json_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.json?lang=ar" - language: "de" html_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked?lang=de" markdown_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.md?lang=de" json_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.json?lang=de" - language: "en" html_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked?lang=en" markdown_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.md?lang=en" json_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.json?lang=en" - language: "es" html_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked?lang=es" markdown_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.md?lang=es" json_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.json?lang=es" - language: "fr" html_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked?lang=fr" markdown_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.md?lang=fr" json_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.json?lang=fr" - language: "pl" html_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked?lang=pl" markdown_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.md?lang=pl" json_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.json?lang=pl" - language: "ru" html_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked?lang=ru" markdown_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.md?lang=ru" json_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.json?lang=ru" - language: "zh" html_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked?lang=zh" markdown_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.md?lang=zh" json_url: "https://publicasta.com/good_tech_news/claude_fermat_last_theorem_lean_machine_checked.json?lang=zh" --- # Una IA formaliza en Lean 4 la demostración del último teorema de Fermat > Agentes de Claude formalizaron en Lean 4, en unos once días, una vía clásica para demostrar el teorema. El logro no resuelve un problema nuevo, pero muestra cómo la IA puede acelerar un trabajo matemático exhaustivo sin renunciar a la comprobación formal. El último teorema de Fermat quedó demostrado en la década de 1990; la novedad anunciada ahora es de otra naturaleza. Anthropic comunicó el 4 de septiembre de 2026 que varios agentes de Claude habían formalizado en Lean 4 una demostración ya conocida. La empresa presenta el resultado como la primera formalización completa del teorema comprobada por ordenador y afirma que el trabajo se produjo durante una ejecución en gran medida autónoma de unos once días. Conviene mantener esas dos afirmaciones —la primacía y el grado de autonomía— claramente atribuidas a Anthropic. No se ha resuelto un problema que permaneciera abierto ni se ha descubierto una demostración matemática nueva. Lo que se ha hecho es expresar con precisión formal una extensa argumentación aceptada desde hace décadas, de modo que el núcleo de Lean pueda comprobar cada paso lógico. La formulación publicada se refiere a números naturales: para todo n mayor o igual que 3 y para a, b y c positivos, a^n + b^n no puede ser igual a c^n. Según el repositorio, la demostración recorre la vía clásica vinculada a Frey, Serre, Ribet, Wiles y Taylor–Wiles, siguiendo la exposición de Darmon, Diamond y Taylor. Por tanto, el resultado descansa en matemáticas creadas por personas y también aprovecha resultados disponibles en bibliotecas formales. ## De una demostración para especialistas a una formulación comprobable Una demostración matemática habitual se dirige a lectores expertos. Puede omitir pasos rutinarios, apoyarse en convenciones compartidas y confiar en que quien la estudie reconstruirá determinadas conexiones. Un asistente de demostración exige algo diferente: hay que declarar los objetos, precisar las hipótesis y justificar las transiciones con detalle suficiente para que el sistema decida si cada conclusión se deriva de lo anterior. Esa exigencia no sustituye la comprensión matemática ni la revisión de especialistas. Añade una forma distinta y reproducible de comprobación: dada una formulación concreta, unas definiciones y unos axiomas declarados, el núcleo verifica que la conclusión se obtiene de ellos. El alcance es estricto. La máquina comprueba el argumento codificado, no que los nombres elegidos sean esclarecedores, que la exposición resulte pedagógica o que cada definición represente exactamente la intención informal de sus autores. Formalizar tampoco equivale a copiar símbolos de un texto. Es necesario representar estructuras matemáticas, conectar teorías distribuidas entre numerosos módulos y hacer explícitos los resultados intermedios que en una exposición convencional podrían resumirse en una frase. En una demostración de esta magnitud, buena parte del esfuerzo consiste precisamente en construir y ensamblar esa infraestructura. Por eso los once días comunicados por Anthropic deben entenderse dentro de un marco concreto. Los agentes no partieron de cero: siguieron una estrategia matemática conocida, utilizaron Lean y Mathlib, e incorporaron trabajo formal previo. La aportación que se evalúa es la capacidad de completar y enlazar una formalización enorme con un alto grado de automatización, no la creación autónoma de las ideas que hicieron posible la demostración original. ## La escala del trabajo Las cifras comunicadas ayudan a entender por qué el resultado es relevante como obra de ingeniería formal. Anthropic informa de 13 millones de líneas de Lean y de unos seis mil millones de fragmentos de salida generados, medidos en tokens. También cifra en 30.300 los resultados intermedios demostrados y señala que aproximadamente 29.500 de ellos se emplearon en la demostración final. El inventario del repositorio ofrece otros recuentos, definidos de manera distinta: 29.511 páginas de teoremas, 1.450 módulos de definiciones y 60.475 módulos construidos. No son medidas intercambiables, de modo que no deben sumarse ni presentarse como si describieran una sola categoría. En conjunto muestran la dimensión del artefacto, pero cada número responde a una unidad propia. El volumen de salida tampoco permite deducir por sí solo el coste económico ni el consumo energético. No se ha publicado una contabilidad completa que autorice ese cálculo. La cifra sí ilustra la cantidad de generación empleada, pero convertirla en dinero o energía exigiría datos adicionales sobre infraestructura, precios, duración efectiva y condiciones de ejecución. La magnitud importa además por una razón práctica. En una formalización extensa, no basta con demostrar el enunciado final de una vez. Antes hay que disponer de definiciones adecuadas y establecer miles de lemas que permitan pasar de una parte de la teoría a otra. El resultado final depende de esa red de trabajo intermedio; de ahí que el repositorio distinga entre resultados producidos, resultados utilizados y módulos construidos. ## Qué se comprobó El artefacto fija Lean 4.33.1 y Mathlib v4.33.0. Su comprobación predeterminada exige que el teorema final dependa exactamente de `propext`, `Classical.choice` y `Quot.sound`. Según el inventario publicado, ningún módulo del proyecto usa `axiom`, `sorry`, `native_decide`, `unsafe`, `extern`, `implemented_by`, `partial def` ni `#eval`. El archivo separado que plantea el reto sí contiene deliberadamente `sorry`, pero queda fuera del paquete comprobado. Estas restricciones son importantes porque delimitan cómo llega Lean a aceptar el resultado. En especial, impiden que la demostración principal se dé por terminada mediante marcadores de trabajo pendiente o mecanismos excluidos por las reglas del proyecto. Aun así, se trata de declaraciones del repositorio y de salvaguardas de construcción, no de una auditoría humana e independiente, línea por línea, de los 13 millones de líneas. El repositorio informa también de que `comparator` v4.33.0 confirmó tres propiedades: la identidad del enunciado con el reto, la restricción de axiomas y la repetición de la comprobación por el núcleo de Lean. La ejecución concluyó con el mensaje “Your solution is okay!”. Esto aporta una prueba concreta de que el artefacto satisface las condiciones técnicas definidas para el reto, siempre dentro de las versiones y del procedimiento indicados. La identidad del enunciado merece atención. Una demostración formal puede ser internamente válida y, sin embargo, responder a una formulación distinta de la que se pretendía estudiar. Comparar de forma explícita el teorema final con el enunciado del reto reduce ese riesgo específico. No elimina la necesidad de interpretar correctamente las definiciones, pero evita que el éxito dependa de una mera semejanza verbal entre dos formulaciones. ## Comprobaciones adicionales y sus límites El matemático Kevin Buzzard aportó una corroboración independiente poco después del anuncio. Explicó que había compilado el código y ejecutado `comparator`, y resumió el resultado con la frase “it checks out”. Su prueba confirma que el repositorio se puede compilar y que supera ese procedimiento de comparación en manos de una persona ajena a Anthropic. Es una comprobación sólida, pero no debe ampliarse más allá de lo que acredita. Buzzard no afirmó haber revisado manualmente cada línea, cada nombre o cada interpretación matemática del proyecto. Compilar el artefacto y obtener la aceptación de `comparator` demuestra algo preciso; no convierte automáticamente todos sus aspectos editoriales, conceptuales o de mantenimiento en objeto de una revisión humana exhaustiva. Anthropic comunica una segunda prueba mediante `nanoda` 0.4.13, una implementación independiente del núcleo de Lean escrita en Rust. Según el proyecto, este núcleo aceptó sin errores una exportación con 1.052.234 declaraciones. La utilidad de la prueba radica en que no repite exactamente la misma implementación utilizada en la comprobación ordinaria de Lean: proporciona otra vía para revisar las reglas de tipado aplicadas al material exportado. También aquí hay una reserva explícita. Anthropic aplicó cuatro parches a `nanoda` y sostiene que modifican la información de progreso y el rendimiento de las búsquedas, no las reglas de tipado. El resultado del segundo núcleo sigue siendo un dato comunicado por el propio proyecto, y esos cambios son un objeto razonable de examen independiente. Presentarlo con esa salvedad es más exacto que describirlo como una certificación absoluta. ## Lo que significa «comprobado por ordenador» En este contexto, la expresión indica que el enunciado exacto de Lean se deriva de las definiciones y los axiomas declarados dentro de una base informática de confianza. La comprobación puede repetirse y obliga a explicitar muchos pasos que una demostración escrita para especialistas deja sobreentendidos. Esa combinación ofrece una garantía valiosa sobre la coherencia deductiva del objeto formal. No significa que el resultado sea infalible ni que quede fuera de toda duda imaginable. La cadena de confianza incluye implementaciones, compiladores, sistema operativo y equipo físico, además de la correspondencia entre las matemáticas informales y su representación formal. La prueba con otro núcleo reduce la dependencia de una única implementación, pero no hace desaparecer todos los posibles fallos del entorno. Tampoco establece novedad matemática. El teorema, la vía argumental y los ingredientes esenciales ya existían. Ni la comprobación del núcleo decide si un nombre describe bien el contenido de un lema, ni determina si las abstracciones son sensatas, si el código será fácil de mantener o si la exposición ayuda a aprender las matemáticas. El propio repositorio reconoce que las herramientas no pueden garantizar que un teorema intermedio signifique lo que su nombre sugiere. Estas distinciones no rebajan el logro; permiten decir con claridad en qué consiste. La aportación está en haber llevado una demostración de enorme extensión hasta una formulación que supera controles formales concretos, con una intervención automatizada que Anthropic describe como mayoritaria. Evaluarla bien exige conservar a la vez el valor de esa comprobación y los límites de aquello que se comprobó. ## Un artefacto de investigación, no una biblioteca mantenida El repositorio se distribuye con licencia Apache-2.0 y se presenta expresamente como un artefacto de investigación. Anthropic advierte que no lo mantiene y que no acepta contribuciones. Esa condición importa para valorar su uso futuro: una obra puede compilarse, superar sus controles y ser valiosa como demostración experimental sin estar organizada para evolucionar como parte de una biblioteca comunitaria. El proyecto reconoce además material derivado del proyecto sobre el último teorema de Fermat del Imperial College London, de `flt-regular` y de Mathlib. Los créditos refuerzan una idea central: la automatización se construyó sobre una base acumulada de matemáticas y formalización humanas. La ejecución de los agentes enlazó y amplió esa base a gran escala; no la sustituyó. El proyecto del Imperial College London persigue un propósito diferente y continúa siendo pertinente. Una biblioteca concebida para ofrecer código legible, explicaciones y componentes reutilizables no es equivalente a un artefacto autónomo de gran tamaño cuya finalidad inmediata es completar y comprobar una demostración. Buzzard ha señalado que el trabajo del Imperial conserva esa función de construcción de biblioteca y exposición, aunque Anthropic haya terminado antes este otro tipo de formalización. La diferencia afecta a lo que puede hacerse con el resultado. Incorporar material a Mathlib requiere algo más que lograr que el núcleo lo acepte: también cuentan la arquitectura de las definiciones, la claridad de las interfaces, la posibilidad de reutilizar resultados y el mantenimiento continuado. El repositorio de Anthropic no afirma cumplir ese cometido. Su valor principal está en mostrar que un sistema de agentes puede producir un objeto formal completo de una escala extraordinaria y someterlo a verificaciones reproducibles. ## Por qué es una noticia positiva, con cautela El resultado ofrece una muestra concreta de cómo la inteligencia artificial puede agilizar labores matemáticas exhaustivas sin eliminar la comprobación formal. En lugar de pedir al lector que confíe únicamente en una respuesta generada, el producto del trabajo está escrito en un lenguaje que el núcleo de Lean puede revisar. Además, el repositorio expone versiones, restricciones, inventarios y procedimientos de comprobación que permiten repetir partes esenciales de la evaluación. Ese modelo puede ser útil allí donde el coste de detallar cada paso frena la formalización de matemáticas ya conocidas. Los agentes pueden encargarse de una parte considerable de la elaboración y del enlace de resultados intermedios, mientras que el sistema formal rechaza las transiciones que no se justifican conforme a sus reglas. Lo demostrado aquí es la viabilidad de ese proceso en un caso excepcionalmente grande, no una garantía automática para cualquier proyecto matemático. La noticia era muy reciente en el momento de la comprobación: tanto el anuncio de Anthropic como el relato independiente de Buzzard llevan fecha del 4 de septiembre de 2026, aproximadamente un día antes de la revisión de las fuentes. Esa actualidad corresponde al artefacto y al método empleado. El último teorema de Fermat, por supuesto, no volvió a resolverse en 2026; su demostración pertenece a los años noventa. Quedan abiertas tareas razonables para la comunidad: examinar los parches de `nanoda`, estudiar la calidad y el significado de las abstracciones, valorar cuánto material puede reutilizarse y comparar el artefacto con formalizaciones orientadas a una biblioteca mantenida. Ninguna de ellas invalida las comprobaciones ya descritas, pero todas ayudan a evitar una lectura triunfalista. La conclusión más sólida es, por tanto, limitada y relevante. Anthropic ha publicado una formalización de una vía conocida para demostrar el último teorema de Fermat; el proyecto afirma que fue producida en gran medida por agentes durante unos once días, y los controles documentados incluyen la repetición por el núcleo de Lean, restricciones explícitas sobre axiomas, una prueba independiente de compilación y comparación, y la aceptación comunicada por un segundo núcleo. No es matemática nueva ni una garantía de perfección absoluta. Sí es un avance verificable en la automatización de una tarea formal extensa. ![Representación de una demostración matemática conectada a un sistema de verificación formal](https://publicasta.com/storage/projects/16/pages/508/2026/09/ec5c6f07-85e3-40dc-be1d-ebdc927d43b8.webp)