Axiom lança formalização completa do Stacks Project em Lean

A Axiom publicou uma formalização em Lean de todo o Stacks Project, a referência open-source de cerca de 7.500 páginas que organiza as fundações da geometria algébrica moderna. A empresa fala em aproximadamente 16 milhões de linhas de código e classifica o resultado como a maior biblioteca integrada e reutilizável de matemática formalizada já construída. Trata-se de lançamento disponível, com código aberto e uma interface em stacks.axiommath.ai que mostra o texto original ao lado do código Lean e o grafo de dependências.

O ponto técnico central é a coerência. Segundo a Axiom, se milhares de agentes formalizam teoremas em paralelo sem coordenação, o kernel do Lean aceita cada arquivo isolado, mas as definições podem ficar incompatíveis ou duplicar o que já existe na Mathlib. Por isso a empresa montou um sistema hierárquico de agentes com papéis específicos e protocolos de coordenação. Eles traduziam enunciados, buscavam abstrações na Mathlib, construíam provas e mantinham interfaces alinhadas entre capítulos. A fidelidade dos enunciados é checada por auditoria multiagente, verificações semânticas contra o texto-fonte e pela exigência de que cada definição se encaixe nos teoremas que dependem dela. Cada declaração Lean mantém as tags permanentes do Stacks.

A Axiom também afirma que o processo expôs dezenas de enunciados do Stacks que precisavam de ajuste, como hipóteses ausentes, casos de borda em característica positiva e afirmações que não valiam na generalidade declarada. Nesses casos, os agentes construíram contraexemplos e formalizaram versões corrigidas. Esses achados são relato da própria empresa. A formalização é um projeto independente mantido pela Axiom, e o texto cita que Johan de Jong pediu, em 21 de outubro de 2026, que comentários e pull requests gerados por IA não sejam enviados ao repositório principal do Stacks por enquanto. A Axiom diz respeitar o pedido e mantém correções e contraexemplos no próprio repositório.

Este é o segundo grande lançamento de formalização da Axiom em poucos dias. Em 28 de outubro de 2026, o CEVIU noticiou "Axiom Math divulga primeira prova formal verificada por computador da Classificação dos Grupos Simples Finitos", uma prova que, na versão humana, tem cerca de 15 mil páginas. Segundo a Axiom, o CFSG gira em torno de um único teorema monumental. O Stacks Project é diferente: é uma biblioteca de definições, construções e lemas feita para ser reaproveitada em provas futuras. A empresa passa de um grande resultado isolado para infraestrutura que outros podem importar.

Para quem trabalha com agentes de prova, a leitura é que o gargalo se desloca. Gerar scripts Lean curtos já é rápido. O difícil é manter milhões de linhas coerentes e importáveis. Se a biblioteca se sustentar fora do ambiente da Axiom, agentes de terceiros ganham uma base verificada para geometria algébrica, algo que essa área não tinha em Lean. Ainda falta ver como a comunidade vai auditar a fidelidade dos enunciados em escala.