A Axiom Math anunciou a formalização do Stacks Project, uma das maiores bibliotecas de matemática produzidas por humanos. Segundo a startup, agentes de inteligência artificial converteram o conteúdo da obra, que tem cerca de 7.654 páginas, em aproximadamente 16 milhões de linhas de código verificadas por computador.
O trabalho busca criar uma base matemática que possa ser usada por outros sistemas de IA para desenvolver software e, futuramente, apoiar pesquisas científicas. A empresa afirma que resultados submetidos ao processo de verificação podem servir como blocos de construção para novas provas, reduzindo a necessidade de recomeçar cada demonstração do zero.
Como funciona a verificação
Na formalização, matemáticos traduzem uma prova para a linguagem de programação Lean. Um programa chamado assistente de provas examina o código linha por linha. Quando o código é aprovado, o sistema confirma que a estrutura lógica apresentada é consistente dentro das regras usadas na verificação.
No caso do Stacks Project, o desafio não era apenas conferir teoremas isolados. As definições e os resultados da biblioteca são interdependentes, e muitos deles se baseiam em conteúdos apresentados anteriormente. A Axiom Math precisou preservar essas relações ao longo das cerca de 16 milhões de linhas de código.
O Stacks Project foi iniciado em 2005 por Johan de Jong, da Universidade Columbia, como uma referência de código aberto. Ao longo dos anos, matemáticos contribuíram com conteúdos que vão da álgebra estudada na graduação a conceitos avançados de álgebra, geometria e teoria dos números.
Aplicações para matemática e software
De acordo com a Axiom Math, a formalização preenche uma lacuna especialmente relevante na geometria algébrica. Até agora, pesquisadores interessados em verificar novos trabalhos dessa área com Lean tinham uma base limitada para aproveitar. A empresa afirma que o Stacks Project oferece um ponto de partida mais amplo.
A tecnologia de verificação formal também é usada por engenheiros para conferir projetos de chips e por pesquisadores para identificar falhas em programas. A startup relaciona esse tipo de controle ao avanço de agentes de IA capazes de escrever cada vez mais código, argumentando que bibliotecas verificadas podem reduzir erros e decisões técnicas inadequadas desde o início dos projetos.
Para realizar a tarefa, os agentes da empresa trabalharam em paralelo, seguindo uma estrutura geral, mas identificando por conta própria atividades que poderiam ser executadas simultaneamente. A Axiom Math também treinou modelos próprios para tarefas matemáticas e contou inicialmente com especialistas em Lean para orientar a qualidade das soluções produzidas.
Fundada em março de 2025 por Carina Hong, de 25 anos, a Axiom Math é descrita como uma startup de US$ 1,6 bilhão. Em março, a empresa anunciou uma rodada Série A de US$ 200 milhões liderada pela Menlo Ventures. A companhia pretende aplicar a mesma lógica de conhecimento reutilizável à criação de software e sustenta que bases verificadas podem ajudar a evitar a produção de conteúdo de IA sem controle suficiente.
