Anthropic ha publicado en abierto, bajo licencia Apache 2.0, una prueba completa verificada por máquina del Último Teorema de Fermat en Lean 4, construida sobre la biblioteca matemática Mathlib. El enunciado formal que ofrece el repositorio es: para todo n ≥ 3 y enteros positivos a, b, c, a^n + b^n ≠ c^n. Esta frase se escribió en Lean como un teorema que el núcleo puede comprobar paso a paso, sin dejar ningún hueco.
La escala es la parte más evidente de este trabajo. El repositorio contabiliza 60.475 módulos, 29.511 teoremas, 1.450 módulos de definiciones; la verificación de exportación cubrió 1.052.234 declaraciones. La documentación HTML generada pesa unos 390 MB, y el archivo de exportación completo, 37,8 GB. Para ejecutarlo todo en local hacen falta más de 300 GB de disco y un pico de memoria de unos 153 GB.
Tres verificaciones, todas registradas
El repositorio no se conforma con decir simplemente "compiló correctamente". La primera verificación es la compilación completa por el propio núcleo de Lean 4.33.1, que tardó 5 horas y 32 minutos en una máquina de 96 núcleos. La segunda usa la herramienta oficial comparator de leanprover (v4.33.0) para volver a comprobarlo, con una duración de unas 14 horas y 46 minutos. La tercera cambia al núcleo independiente escrito en Rust nanoda 0.4.13, que con 16 hilos tardó unos 30 minutos y produjo la salida "Your solution is okay!".
Además de las tres verificaciones hay una restricción estricta: en ningún módulo puede aparecer `axiom`, `sorry`, `native_decide`, `unsafe`, `extern`, `implemented_by`, `partial def` ni `#eval`. Estas palabras clave están reconocidas en la comunidad de Lean como puertas de entrada a fallos: `sorry` representa directamente "esto todavía no está demostrado", mientras que `native_decide` delega parte del juicio a código máquina que el núcleo no verifica. Excluirlas todas equivale a admitir que la credibilidad de esta prueba se juega únicamente en el núcleo de Lean y en las herramientas de verificación, tal como reconoce el propio README.
Cuánto escribió la IA, el repositorio no lo dice
Según el README, el código fuente en Lean fue "producido por agentes de IA sobre código Lean de código abierto escrito por humanos, con Lean actuando de árbitro". La proporción concreta no se revela: qué módulos escribieron personas y cuáles generó el modelo para luego ser rechazados por el núcleo y rehechos no aparece desglosado en el material público.
La base humana, en cambio, está registrada con bastante claridad. 106 archivos de dependencias proceden de proyectos académicos ya existentes, principalmente el proyecto de formalización del FLT dirigido por Kevin Buzzard en el Imperial College y flt-regular, que trata el teorema de Kummer; otros 23 módulos vuelven a demostrar contenidos que ya existían en Mathlib.
Situado en la trayectoria de las matemáticas formalizadas, el salto de escala resulta bastante evidente. El teorema de los cuatro colores fue formalizado por Georges Gonthier en Coq en 2005, y el proyecto Flyspeck sobre la conjetura de Kepler se dio por concluido en 2014; ambos se midieron en personas-año. Cuando arrancó el proyecto FLT, el propio equipo de Buzzard también preveía un plazo de varios años. Cuánto ha adelantado este repositorio esa meta depende de la proporción real entre trabajo humano y trabajo de máquina, y esa es precisamente la única cifra que hoy no se puede consultar.
Fuentes: README público y registros de verificación de Anthropic, CocoLoop, proyecto Mathlib, materiales públicos del proyecto FLT del Imperial College; el número de módulos, el número de teoremas y la duración de las tres verificaciones se han cotejado con los datos del repositorio.