A Axiom Math anunciou que seus agentes de inteligência artificial verificaram formalmente o Stacks Project, uma extensa referência matemática de código aberto. O trabalho converteu cerca de 7.654 páginas em aproximadamente 16 milhões de linhas de código Lean verificadas por computador. A empresa vê o acervo como uma base que poderá ser reutilizada em provas futuras e, mais adiante, no desenvolvimento de software por agentes de IA.
Criado em 2005 pelo matemático Johan de Jong, o Stacks Project reúne contribuições de pesquisadores e cobre temas que vão da álgebra ensinada na universidade a áreas avançadas de álgebra, geometria e teoria dos números. A coleção é interligada: definições e teoremas dependem de resultados anteriores. Por isso, a equipe precisou manter essas relações coerentes ao formalizar todo o material.
Na verificação formal descrita pela empresa, uma prova matemática é reescrita como código na linguagem Lean. Um assistente de provas confere o código linha a linha; se ele passar pela checagem, a prova tem sua consistência lógica confirmada nesse sistema. A técnica também é usada em engenharia para verificar projetos de chips e, segundo o texto, já ajudou pesquisadores na França a encontrar erros em um programa de cálculo de benefícios familiares.
O projeto foi conduzido por agentes que trabalharam em paralelo. A Axiom estabeleceu uma hierarquia geral, sem determinar a tarefa de cada agente: eles próprios identificavam atividades que podiam executar ao mesmo tempo. Ashvin Swaminathan, integrante da equipe técnica, descreveu a organização como flexível, mas condicionada à preservação das conexões entre os resultados matemáticos.
A empresa também treinou modelos próprios para trabalhar com matemática. No começo, um especialista interno em Lean orientava os agentes sobre como avaliar a qualidade do trabalho. Com o tempo, afirmou a diretora-executiva Carina Hong, eles passaram a desenvolver essa capacidade gradualmente.
Segundo Swaminathan, a formalização preenche uma lacuna importante em geometria algébrica. Antes do trabalho, pesquisadores que quisessem conferir novos resultados dessa área com Lean tinham pouco material formalizado para usar como base. Agora, argumenta ele, há mais conteúdo disponível para esse fim.
A Axiom defende que resultados verificados podem funcionar como blocos reutilizáveis: provas futuras poderiam partir de matemática já conferida, em vez de recomeçar do zero. O matemático Terence Tao, da Universidade da Califórnia em Los Angeles e vencedor da Medalha Fields, resumiu a ideia dizendo que, quanto mais provas forem formalizadas, mais provas formalizadas poderão ser produzidas.
A aposta da empresa vai além da pesquisa matemática. Axiom afirma que fundamentos verificados também podem ajudar agentes de IA a escrever software com mais confiabilidade, num cenário em que esses sistemas produzem uma parcela crescente do código. A empresa aponta que desenvolvedores enfrentam dificuldades para garantir que programas estejam livres de erros e falhas de segurança, e espera que bibliotecas reutilizáveis de conhecimento verificado sirvam de apoio para esse trabalho. Trata-se de uma perspectiva defendida pela companhia, não de um resultado já demonstrado pelo projeto do Stacks.
Fundada por Hong em março de 2025, após ela deixar um doutorado em matemática em Stanford, a Axiom captou US$ 200 milhões em uma rodada Série A liderada pela Menlo Ventures, também em março. A fonte descreve a empresa como avaliada em US$ 1,6 bilhão. Ao apresentar o trabalho, Hong afirmou que a equipe não sabia inicialmente se a abordagem de programação com agentes conseguiria preservar a estrutura do acervo. A executiva também desafiou empresas de programação a realizar projetos de formalização nessa escala.
