Las dos versiones están alineadas bloque a bloque, en el orden del texto: titular, lo esencial y después párrafo a párrafo. Cuando la traducción ha fusionado o dividido un párrafo, la casilla correspondiente queda vacía — nunca emparejamos dos pasajes a ojo.
Der entscheidende Moment dieses Fermat-Projekts ist unspektakulär: In Lean kompiliert ein Beweis – oder er tut es nicht. Im GitHub-Repository von Anthropic liegt nach Angaben des Unternehmens nun eine vollständig computergeprüfte Fassung von Fermats letztem Satz. Der Mathematiker Kevin Buzzard hat den Code inzwischen selbst kompiliert und den zugehörigen Komparator ausgeführt.
El momento decisivo de este proyecto sobre Fermat no tiene nada de espectacular: en Lean, una demostración compila o no compila. En el repositorio de GitHub de Anthropic hay ahora, según la empresa, una versión completamente verificada por ordenador del último teorema de Fermat. El matemático Kevin Buzzard ya ha compilado personalmente el código y ejecutado el comparador correspondiente.
Mathematisch ist der Satz nicht neu. Andrew Wiles bewies 1995 auf 129 Seiten, dass die Gleichung xⁿ + yⁿ = zⁿ für ganzzahlige Exponenten n > 2 keine ganzzahligen Lösungen hat. Neu ist die Formalisierung: Der Beweis wird so in Code übersetzt, dass ein Computer jeden einzelnen Schritt kontrollieren kann, statt sich auf übersprungene, für Menschen offensichtliche Zwischenschritte zu verlassen.
Desde el punto de vista matemático, el teorema no es nuevo. Andrew Wiles demostró en 1995, en 129 páginas, que la ecuación xⁿ + yⁿ = zⁿ no tiene soluciones enteras para exponentes enteros n > 2. Lo novedoso es la formalización: la demostración se traduce a código de modo que un ordenador pueda controlar cada paso, en lugar de confiar en pasos intermedios omitidos por resultar evidentes para los seres humanos.
Lean ist dabei Programmiersprache und Prüfsystem zugleich. Mathematische Aussagen und ihre Herleitungen werden gegen ein festes logisches Regelwerk geprüft; wenn auch nur eine Lücke bleibt, kompiliert der Beweis nicht. Vertrauen muss dann vor allem dem kleinen Kern von Lean und seinen Axiomen gelten. Die verfügbare Bibliothek Mathlib begrenzt den Spielraum allerdings auf den Teil der Mathematik, der bereits formalisiert wurde.
Lean es a la vez lenguaje de programación y sistema de verificación. Las afirmaciones matemáticas y sus demostraciones se comprueban con arreglo a un conjunto fijo de reglas lógicas; si queda siquiera un vacío, la demostración no compila. Por tanto, la confianza debe depositarse sobre todo en el pequeño núcleo de Lean y sus axiomas. Sin embargo, la biblioteca disponible Mathlib limita el margen de acción a la parte de las matemáticas que ya ha sido formalizada.
Anthropic zufolge arbeiteten Dutzende Claude-Agenten elf Tage lang an einer vereinfachten Fassung von Wiles’ Beweis nach Darmon, Diamond und Taylor. Heraus kamen 13 Millionen Zeilen Lean-Code und rund 29.500 Zwischentheoreme. Erste Teams scheiterten laut dem Unternehmen am Projektüberblick; vorangekommen sei die Arbeit erst mit Prove2Me, einer von Tianyi Pengs Gruppe an der Columbia University entwickelten Plattform, die nächste Beweisschritte in einem gerichteten azyklischen Graphen verwaltet. Der Aufwand lag laut Anthropic bei rund sechs Milliarden Output-Token; daraus lassen sich Kosten zwischen 100.000 und 300.000 US-Dollar hochrechnen.
Según Anthropic, docenas de agentes de Claude trabajaron durante once días en una versión simplificada de la demostración de Wiles basada en el trabajo de Darmon, Diamond y Taylor. El resultado fueron 13 millones de líneas de código Lean y unas 29.500 teorías intermedias. Según la empresa, los primeros equipos fracasaron a la hora de mantener una visión general del proyecto; el trabajo solo avanzó con Prove2Me, una plataforma desarrollada por el grupo de Tianyi Peng en la Universidad de Columbia que gestiona los siguientes pasos de la demostración en un grafo dirigido acíclico. Según Anthropic, el esfuerzo ascendió a unos seis mil millones de tokens de salida; a partir de esa cifra pueden calcularse unos costes de entre 100.000 y 300.000 dólares estadounidenses.
Konkret ändert sich damit schon jetzt etwas für die Formalisierung mathematischer Literatur: Dritte können den offengelegten Code kompilieren und die logische Kette prüfen. Das schafft eine technisch reproduzierbare Kontrolle, ersetzt aber keine unabhängige Bewertung, die bislang weitgehend aussteht. Buzzard hält die Formalisierung für einen großen Schritt hin zur automatischen Formalisierung moderner Mathematik; zugleich folgt sie der frühen Literatur und liefert keine neue mathematische Aussage über Fermats letzten Satz.
Esto ya cambia algo concreto para la formalización de la literatura matemática: terceros pueden compilar el código publicado y comprobar la cadena lógica. Esto permite una verificación técnicamente reproducible, pero no sustituye una evaluación independiente, que hasta ahora sigue pendiente en gran medida. Buzzard considera que la formalización supone un gran paso hacia la formalización automática de las matemáticas modernas; al mismo tiempo, sigue la literatura temprana y no aporta ninguna afirmación matemática nueva sobre el último teorema de Fermat.