Axiom Math quer tirar a matemática produzida por IA da zona cinzenta
Startup avaliada em US$ 1,6 bilhão verificou formalmente as 7.654 páginas do Stacks Project usando agentes de IA e a linguagem Lean. A aposta é virar a infraestrutura de confiança para provas matemáticas geradas por máquinas.
Por Marina Sato · Repórter de IA
Sete mil páginas, 16 milhões de linhas de código
A startup Axiom Math, avaliada em US$ 1,6 bilhão, anunciou em 5 de novembro a verificação formal completa do Stacks Project, biblioteca de matemática de código aberto com cerca de 7.654 páginas sobre álgebra, geometria algébrica e teoria dos números. O processo converteu o material em aproximadamente 16 milhões de linhas de código verificável, segundo a TechCrunch.
O Stacks Project foi iniciado em 2005 pelo matemático Johan de Jong, da Universidade Columbia, e é frequentemente comparado ao Bourbaki, a série de livros que tentou reconstruir as bases da matemática no século 20. Até agora, nenhuma biblioteca dessa escala havia sido formalizada por completo.
Como funciona a verificação
A Axiom Math, empresa fundada em março de 2025, usa agentes de IA para traduzir provas matemáticas escritas em linguagem natural para Lean, uma linguagem de programação ligada a um assistente de prova. Cada etapa lógica é checada automaticamente pelo kernel do Lean, linha por linha — diferente de um texto matemático tradicional, que depende da revisão humana por pares.
Segundo a cobertura da TechCrunch, o trabalho de formalização também expôs falhas no material original: declarações sem hipóteses completas, casos de borda em característica positiva e afirmações que não se sustentavam na generalidade em que haviam sido escritas.
A CEO Carina Hong, de 25 anos, deixou o doutorado em matemática de Stanford para fundar a empresa. "Você quer que os agentes tenham uma biblioteca reutilizável para construir sobre ela", disse ela à publicação. Ashvin Swaminathan, do time técnico, descreveu o resultado como o preenchimento de "um vazio enorme" em geometria algébrica formalizada.
Capital para apostar em matemática verificada
Em março de 2026, a Axiom Math levantou uma rodada Série A de US$ 200 milhões liderada pela Menlo Ventures, elevando sua avaliação a mais de US$ 1,6 bilhão. Entre os investidores também aparecem Madrona, Greycroft, B Capital, Toyota Ventures e Triatomic Capital, segundo reportagens que acompanharam a rodada.
A proposta da empresa é oferecer uma camada de verificação formal para provas geradas por IA, num momento em que modelos de linguagem produzem cada vez mais conteúdo matemático sem garantia de correção — o chamado "AI slop" citado no título da reportagem original.
O que ainda falta responder
Resta saber se a verificação formal escala para além de bibliotecas já consolidadas como o Stacks Project, e se pesquisadores e empresas de IA vão de fato adotar Lean como padrão de checagem. Também não está claro quem, na prática, vai pagar pela verificação de provas novas geradas por modelos — ou se esse custo será absorvido pelas próprias companhias de IA que produzem o volume de conteúdo que a Axiom Math diz querer filtrar.