A Anthropic abriu o código, sob licença Apache 2.0, de uma prova completa e verificada por máquina do Último Teorema de Fermat em Lean 4, construída sobre a biblioteca matemática Mathlib. A afirmação formal apresentada no repositório é: para todo n ≥ 3 e inteiros positivos a, b, c, a^n + b^n ≠ c^n. Essa frase foi escrita em Lean como um teorema que o kernel pode conferir passo a passo, sem deixar nenhuma lacuna.
A escala é a parte mais evidente deste trabalho. O repositório contabiliza 60.475 módulos, 29.511 teoremas, 1.450 módulos de definições; a verificação de exportação cobriu 1.052.234 declarações. A documentação HTML gerada tem cerca de 390 MB, e o arquivo de exportação completo, 37,8 GB. Para rodar tudo localmente, são necessários mais de 300 GB de disco e um pico de memória de cerca de 153 GB.
Três verificações, todas registradas
O repositório não se contenta em dizer apenas "compilou com sucesso". A primeira verificação é a compilação completa pelo próprio kernel do Lean 4.33.1, que levou 5 horas e 32 minutos numa máquina de 96 núcleos. A segunda usa a ferramenta oficial comparator do leanprover (v4.33.0) para conferir de novo, levando cerca de 14 horas e 46 minutos. A terceira troca para o kernel independente escrito em Rust, o nanoda 0.4.13, que com 16 threads levou cerca de 30 minutos e produziu a saída "Your solution is okay!".
Além das três verificações, há uma restrição rígida: em nenhum módulo pode aparecer `axiom`, `sorry`, `native_decide`, `unsafe`, `extern`, `implemented_by`, `partial def` ou `#eval`. Essas palavras-chave são reconhecidas na comunidade Lean como portas de entrada para falhas — `sorry` representa diretamente "isto ainda não foi provado", enquanto `native_decide` delega parte do julgamento a código de máquina não verificado pelo kernel. Excluir todas elas equivale a admitir que a credibilidade dessa prova está apostada apenas no kernel do Lean e nas ferramentas de verificação — o próprio README diz isso.
Quanto a IA escreveu, o repositório não diz
Segundo o README, o código-fonte em Lean foi "produzido por agentes de IA sobre código Lean de código aberto escrito por humanos, com o Lean atuando como árbitro". A proporção exata não é revelada: quais módulos foram escritos por humanos e quais foram gerados pelo modelo e depois barrados pelo kernel para serem refeitos não aparece detalhado no material público.
A base humana também está registrada com relativa clareza. 106 arquivos de dependências vêm de projetos acadêmicos já existentes, principalmente o projeto de formalização do FLT liderado por Kevin Buzzard no Imperial College e o flt-regular, que trata do teorema de Kummer; outros 23 módulos reprovam conteúdos já presentes no Mathlib.
Vista na trajetória da matemática formalizada, essa mudança de escala é bem visível. O Teorema das Quatro Cores foi formalizado por Georges Gonthier em Coq em 2005, e o projeto Flyspeck, sobre a conjectura de Kepler, foi declarado concluído em 2014 — ambos medidos em pessoas-ano. Quando o projeto FLT de Buzzard foi lançado, a expectativa também era de um prazo de vários anos. O quanto este repositório antecipou essa linha de chegada depende da real proporção entre trabalho humano e trabalho de máquina — e esse é justamente o único número que ainda não pode ser verificado.
Fontes: README público e registros de verificação da Anthropic, CocoLoop, projeto Mathlib, materiais públicos do projeto FLT do Imperial College; número de módulos, número de teoremas e a duração das três verificações foram conferidos conforme os dados do repositório.