Axiom Math conclui verificação formal da Stacks Project, com 16 milhões de linhas em Lean

A Stacks Project agora é matemática verificada por máquina

Na quarta-feira, 4 de novembro de 2026, a startup Axiom Math anunciou que concluiu a verificação formal da Stacks Project, uma das maiores obras de matemática já escritas por humanos (TechCrunch). O projeto, iniciado em 2005 pelo matemático da Columbia Johan de Jong como referência aberta, reúne cerca de 7.654 páginas que vão da álgebra de nível universitário até resultados avançados em geometria algébrica e teoria dos números.

Para fazer a verificação, a frota de agentes de IA da Axiom traduziu o conteúdo da Stacks Project em cerca de 16 milhões de linhas de código escrito em Lean, uma linguagem de programação criada para registrar demonstrações matemáticas de um jeito que um programa, chamado de assistente de provas, consegue checar linha por linha. Se o código passa na checagem, a demonstração está logicamente correta, sem espaço para o tipo de erro sutil que às vezes escapa até de revisores humanos.

Por que verificação formal interessa a quem escreve código, não só a matemáticos

Verificação formal não é novidade só da matemática. Fabricantes de chips usam a técnica para confirmar que o desenho de um processador funciona antes de ir para a linha de produção, e pesquisadores na França já a usaram para encontrar bugs em um software que calcula benefícios sociais do governo. A lógica é a mesma: em vez de testar um programa rodando casos de exemplo, você prova matematicamente que ele faz o que deveria fazer, para todo caso possível.

A Axiom escolheu a matemática como terreno de teste porque ela funciona como base reutilizável. Ashvin Swaminathan, do time técnico da empresa, afirma que a formalização da Stacks Project preenche uma lacuna na geometria algébrica, área em que praticamente não havia nada verificado em Lean até agora.

Antes disso, segundo Swaminathan, pesquisadores que queriam checar novos resultados em geometria algébrica com Lean tinham pouco material para se apoiar.

Bom, agora há.

Well, now they do.Ashvin Swaminathan, membro do time técnico da Axiom Math

O desafio técnico: manter 16 milhões de linhas consistentes entre si

A dificuldade não foi só o tamanho. Na Stacks Project, cada teorema depende de outros que vieram antes, como uma árvore genealógica: mudar uma definição pode derrubar uma cadeia inteira de resultados que dependem dela. A CEO da Axiom, Carina Hong, disse à TechCrunch que esse acoplamento quase inviabilizou o projeto no início.

Coisas grandes e coisas delicadas, na vida, simplesmente não combinam.

Things that are big and things that are delicate in life just don't go together.Carina Hong, CEO da Axiom Math

Para resolver isso sem travar o trabalho, a equipe não escreveu um roteiro fixo para cada agente. Deu uma hierarquia solta de prioridades e deixou que os próprios agentes encontrassem tarefas para rodar em paralelo, identificando o que podiam resolver sem esperar instrução.

Não tínhamos certeza se o vibe coding seria capaz de preservar a beleza da Stacks.

We were not sure if vibe coding would be able to preserve the beauty of Stacks.Carina Hong, CEO da Axiom Math

Vibe coding é o termo usado para descrever o processo de deixar um agente de IA escrever código, ou neste caso provas, de forma mais autônoma, com pouca supervisão linha a linha. A diferença, segundo a Axiom, é que aqui cada linha gerada passa pelo crivo do assistente de provas em Lean antes de entrar na biblioteca: o agente pode improvisar o caminho, mas não pode errar o resultado.

O que muda para quem constrói ou treina agentes de IA

A Axiom não está construindo isso só para matemáticos. A empresa é avaliada em US$ 1,6 bilhão e levantou uma rodada Série A de US$ 200 milhões liderada pela Menlo Ventures em março, segundo a TechCrunch, que não especifica o ano da rodada. Hong, então com 25 anos, largou o doutorado em matemática em Stanford para fundar a startup em março de 2025.

A tese de negócio é que agentes de IA vão precisar de bibliotecas verificadas e reutilizáveis para não empilhar erro sobre erro, o problema que o mercado já apelidou de lixo de IA (no original em inglês, AI slop): conteúdo gerado em volume, sem garantia de qualidade, que vira ruído difícil de filtrar. Hong argumenta que, sem uma base confiável, cada novo agente reinventa a roda com as próprias falhas.

Você quer que os agentes tenham uma biblioteca reutilizável para construir em cima e continuar empurrando a fronteira. Se você faz um despejo de lixo de IA com más escolhas de engenharia no começo, fica muito difícil para eles expandirem esse limite depois.

You want [agents] to have a reusable library for them to build on and keep pushing the frontier. If you slop drop in a way that's bad engineering choices in the beginning, then it's very hard for them to grow that boundary.Carina Hong, CEO da Axiom Math

Para quem desenvolve software com ajuda de agentes de IA, o recorte prático é este: a Axiom trata a Stacks Project verificada como uma camada de infraestrutura, parecida com uma biblioteca padrão que outros agentes podem importar, ler e estender sem reconstruir a lógica do zero. Swaminathan descreve o resultado como um substrato.

Agentes conseguem ler nosso código, entender e construir nova infraestrutura em cima dele. Nossa formalização em Lean agora é o substrato sobre o qual os agentes podem construir.

Agents can read our code, understand it, and build new infrastructure on top of it. Our Lean formalization is now the substrate that agents can build upon.Ashvin Swaminathan, membro do time técnico da Axiom Math

O pano de fundo: a corrida da IA contra provas duvidosas

O anúncio chega num momento em que o campo da matemática lida com um volume inédito de resultados gerados por IA. Só em outubro de 2026, a OpenAI publicou 719 manuscritos alegando soluções para problemas considerados entre os mais difíceis da área, segundo a reportagem da TechCrunch. O problema é que nem toda checagem automática pega tudo: já houve provas aprovadas por verificadores de computador que continham falhas que passaram despercebidas.

Esse cenário é o que chama a atenção de matemáticos como Peter Woit, da Columbia, que compara o porte da Stacks Project aos livros de Bourbaki, a coleção que reconstruiu a matemática a partir de suas fundações no século XX, dizendo que não há "nada realmente comparável" a esse volume de trabalho coordenado. O matemático Terence Tao, da UCLA e vencedor da Medalha Fields, resume por que mais provas formalizadas importam para o campo como um todo.

Quanto mais provas formalizadas você tem, mais provas formalizadas você consegue fazer.

The more formalized proofs you have, the more formalized proofs you can make.Terence Tao, matemático da UCLA

O que ainda está em aberto

A Axiom formalizou uma biblioteca de matemática pura, não um sistema de produção com usuários reais, e a promessa de aplicar a mesma lógica ao software do futuro ainda depende de ferramentas, custo e adoção que a empresa não detalhou publicamente.

Hong lançou um desafio aberto a outras empresas de IA voltadas a código para reproduzir o feito em escala, mas não divulgou prazo nem quantos agentes ou quanto tempo o processo levou. Para times de TI que avaliam incorporar Lean ou verificação formal ao próprio pipeline, o caso da Stacks Project funciona, por enquanto, como prova de conceito de escala, não como produto pronto para uso fora do domínio matemático.

Fonte: TechCrunch AI