As duas versões estão alinhadas bloco a bloco, pela ordem do texto: título, o essencial e depois parágrafo a parágrafo. Quando a tradução fundiu ou dividiu um parágrafo, a casa correspondente fica vazia — nunca aproximamos duas passagens a olho.
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.
O momento decisivo deste projeto sobre Fermat é pouco espetacular: no Lean, uma demonstração é compilada — ou não é. No repositório do Anthropic no GitHub encontra-se agora, segundo a empresa, uma versão totalmente verificada por computador do Último Teorema de Fermat. O matemático Kevin Buzzard já compilou pessoalmente o código e executou o comparador correspondente.
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.
Do ponto de vista matemático, o teorema não é novo. Andrew Wiles provou, em 1995, ao longo de 129 páginas, que a equação xⁿ + yⁿ = zⁿ não tem soluções inteiras para expoentes inteiros n > 2. A novidade está na formalização: a demonstração é traduzida para código de modo a que um computador possa controlar cada passo, em vez de depender de etapas intermédias omitidas por serem evidentes para os 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.
O Lean é simultaneamente uma linguagem de programação e um sistema de verificação. As afirmações matemáticas e as respetivas demonstrações são verificadas com base num conjunto fixo de regras lógicas; se existir sequer uma lacuna, a demonstração não é compilada. A confiança tem de ser depositada sobretudo no pequeno núcleo do Lean e nos seus axiomas. A biblioteca disponível Mathlib limita, contudo, o campo de aplicação à parte da matemática que já foi 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.
Segundo a Anthropic, dezenas de agentes Claude trabalharam durante onze dias numa versão simplificada da demonstração de Wiles, baseada no trabalho de Darmon, Diamond e Taylor. O resultado foram 13 milhões de linhas de código Lean e cerca de 29 500 teoremas intermédios. Segundo a empresa, as primeiras equipas falharam na gestão global do projeto; o trabalho só avançou com o Prove2Me, uma plataforma desenvolvida pelo grupo de Tianyi Peng na Columbia University, que gere os passos seguintes da demonstração num grafo acíclico dirigido. Segundo a Anthropic, o esforço ascendeu a cerca de seis mil milhões de tokens de saída; a partir desse valor, é possível calcular custos entre 100 000 e 300 000 dólares americanos.
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.
Na prática, isto já altera algo na formalização da literatura matemática: terceiros podem compilar o código disponibilizado e verificar a cadeia lógica. Isto cria um controlo tecnicamente reprodutível, mas não substitui uma avaliação independente, que continua, até agora, em grande medida por realizar. Buzzard considera a formalização um grande passo rumo à formalização automática da matemática moderna; ao mesmo tempo, segue a literatura inicial e não apresenta nenhuma nova afirmação matemática sobre o Último Teorema de Fermat.