AxiomMath usa agentes de IA para verificar o Stacks Project em Lean

A startup AxiomMath anunciou na quarta-feira a verificação formal do Stacks Project, um dos maiores acervos de matemática escritos por humanos. Segundo a empresa, uma frota de agentes de inteligência artificial foi empregada para traduzir cerca de 7.654 páginas do projeto em aproximadamente 16 milhões de linhas de código auditáveis por computador na linguagem Lean.

De acordo com reportagem do TechCrunch, a iniciativa visa estabelecer uma base matemática rigorosamente auditada para orientar a criação de novos softwares e pesquisas científicas. Avaliada em US$ 1,6 bilhão, a AxiomMath foi fundada em março de 2025 pela ex-aluna de doutorado em matemática de Stanford, Carina Hong, de 25 anos. Em março, a empresa captou US$ 200 milhões em uma rodada de investimentos Series A liderada pela Menlo Ventures.

Como funciona a verificação matemática com Lean

A formalização matemática é um método em que pesquisadores reescrevem demonstrações como código em uma linguagem específica, como o Lean. Em seguida, um programa denominado assistente de prova verifica a construção linha por linha. Se o código for aprovado, confirma-se que a lógica do teorema está correta.

O Stacks Project começou em 2005 por iniciativa do matemático Johan de Jong, da Universidade Columbia, como uma referência em código aberto. A compilação abrange desde tópicos de álgebra universitária até estudos avançados em geometria algébrica e teoria dos números. O matemático Peter Woit, também de Columbia, comparou o alcance do projeto aos livros da coleção Bourbaki do século XX.

Como os conceitos dentro do Stacks Project dependem encadeadamente uns dos outros, a AxiomMath informou ter enfrentado o desafio de preservar todas as interconexões ao longo das 16 milhões de linhas de código. A CEO da startup, Carina Hong, relatou que a equipe temia que o processo não conseguisse manter a integridade das dependências lógicas da obra.

Autonomia dos agentes e treinamento de modelos

Para realizar a tradução do acervo, a equipe da AxiomMath atribuiu aos agentes de IA uma estrutura geral sem impor uma hierarquia rígida sobre cada ação. Segundo Ashvin Swaminathan, membro da equipe técnica da startup, os agentes identificaram tarefas por conta própria e trabalharam em paralelo.

A AxiomMath declarou ter treinado modelos próprios voltados para matemática. Hong afirmou que, inicialmente, a empresa utilizou a orientação de um especialista humano na linguagem Lean para repassar padrões de rigor aos agentes, e que os sistemas passaram a assimilar esses critérios ao longo do tempo.

Aplicações em software e pesquisas futuras

De acordo com Swaminathan, a verificação do Stacks Project preenche uma lacuna relevante ao fornecer uma base auditada para estudos em geometria algébrica. O matemático Terence Tao, da UCLA e vencedor da Medalha Fields, pontuou que quanto maior a quantidade de provas formalizadas disponíveis, mais fácil se torna a criação de novas demonstrações auditadas.

Além do impacto na matemática pura, a empresa defende que a formalização é aplicável ao desenvolvimento de softwares. A AxiomMath sustenta que, à medida que agentes de IA passam a gerar mais código, será necessário contar com bases auditadas para evitar falhas de lógica e vulnerabilidades de segurança nos programas do futuro.