Parece que a inteligência artificial está resolvendo um novo problema matemático quase toda semana. No mês passado, apenas a OpenAI publicou 719 manuscritos alegando resolver alguns dos problemas mais difíceis do campo. Mesmo a verificação por computador pode estar errada. Após anos de conteúdo lixo de IA, não se pode deixar de perguntar se a matemática será o próximo campo afetado.
AxiomMath pode evitar esse destino não desacelerando, mas construindo uma base mais sólida. Esta startup avaliada em 1,6 bilhões de dólares espera criar uma camada de base verificada, sobre a qual agentes de IA possam confiar para escrever software e, eventualmente, realizar pesquisas científicas.
Na quarta-feira, a empresa anunciou que havia verificado oficialmente o Stacks Project, um dos maiores resultados matemáticos já escritos por humanos. Os matemáticos geralmente avaliam os Stacks de forma muito elevada. O matemático da Universidade de Columbia Peter Woit já o descreveu como “quase nada mais pode ser comparado a ele” e comparou o projeto à “famosa série Bourbaki” — a coleção de obras que, no século XX, reconstruiu a matemática a partir dos fundamentos.
O colega colombiano de Woit, Johan de Jong, lançou o Stacks Project em 2005 como uma referência de código aberto. Desde então, matemáticos têm contribuído com conteúdo, expandindo desde álgebra de nível universitário até as ideias mais avançadas em álgebra, geometria e teoria dos números.
O grupo de agentes de IA da empresa traduziu esse banco de dados de aproximadamente 7.654 páginas em cerca de 16 milhões de linhas de código verificáveis por computador.
O objetivo da matemática formalizada é garantir que sua estrutura subjacente seja confiável. Matemáticos reescrevem provas como código usando uma linguagem de programação chamada Lean, e um programa chamado assistente de prova verifica esse código linha por linha. Se a prova for aprovada, os matemáticos podem confiar que ela é logicamente válida.
Engenheiros também usam a mesma abordagem, chamada verificação formal, para confirmar se o design de um chip é viável; pesquisadores franceses a utilizaram para descobrir uma vulnerabilidade no software de cálculo de subsídios familiares.
Para um repositório como o Stacks Project, verificar teoremas um a um é apenas parte do trabalho. Os teoremas e definições no Stacks estão interligados, cada um construindo sobre os anteriores. Assim como um genealogia, muitos resultados no Stacks podem ser rastreados até resultados mais antigos.
Essa interdependência deixou o Axiom incerto no início sobre a viabilidade do projeto. A equipe precisava manter todas as conexões intactas em cerca de 16 milhões de linhas de código Lean.
A diretora executiva da Axiom, Carina Hong, disse à TechCrunch: “Grande escala e precisão, na realidade, geralmente não são compatíveis. [Stacks] é um conjunto de resultados matemáticos que constituem a base matemática. Você deseja que os [teoremas] sejam consistentes entre si, e não contraditórios como paradoxos. Você também deseja que essas definições não entrem em conflito entre si.”
Este CEO de 25 anos deixou o programa de doutorado em matemática da Stanford University e fundou esta empresa em março de 2025. Em março deste ano, a Axiom concluiu um financiamento da série A de 200 milhões de dólares liderado pelo Menlo Ventures.
Hong disse: "Na época, não tínhamos certeza se o vibe coding conseguiria manter a estética do Stacks."
Para concluir este projeto, a equipe estabeleceu uma estrutura flexível para os agentes e os executou em paralelo. Ashvin Swaminathan, membro da equipe técnica da Axiom, disse: “Para o Stacks, definimos uma hierarquia... mas não uma hierarquia que especifique exatamente o que cada agente deve fazer. Os agentes procuram tarefas por conta própria e identificam o que pode ser processado em paralelo.”
Axiom também treinou seus próprios modelos para se tornarem proficientes em matemática. Hong disse que essa abordagem não é adotada pela maioria das outras startups de validação. Inicialmente, a equipe dependia de um especialista interno em Lean para ensinar os agentes a formar critérios de julgamento semelhantes aos humanos. Com o tempo, Hong disse que esses agentes aprenderam sozinhos esse julgamento.
Essa conquista preenche uma das maiores lacunas da matemática formalizada. Swaminathan disse: “Quando você olha para o conteúdo matemático já formalizado, percebe que há um enorme buraco negro. E esse buraco negro abrange a geometria algébrica.”
Swaminathan disse que, até agora, pesquisadores que queriam usar o Lean para verificar novos trabalhos em geometria algébrica tinham pouquíssimas bases prontas disponíveis. “Agora eles têm.”
Axiom acredita que cada resultado verificado se torna um bloco de construção, permitindo que provas futuras se baseiem na matemática já verificada, sem precisar começar do zero. O matemático da UCLA e ganhador da Medalha Fields, Terence Tao, resumiu isso de forma mais concisa: "Quanto mais provas formalizadas você tiver, mais provas formalizadas poderá fazer."
O público-alvo da Axiom não é apenas matemáticos. Desenvolvedores há muito tempo se esforçam para garantir que seu código esteja livre de falhas e vulnerabilidades de segurança. Com agentes de IA escrevendo cada vez mais software, esse problema só ficará maior.
Axiom betting, o software do futuro precisa ser construído sobre bases comprovadas, assim como o Stacks atualmente.
Swaminathan disse: "Acreditamos que a matemática é o campo em que você começa a construir essas coisas, e essa é uma habilidade transferível. Os agentes podem ler nosso código, compreendê-lo e construir nova infraestrutura sobre ele. A formalização que fizemos com o Lean agora serve como a base subjacente sobre a qual os agentes podem construir."
A maneira como os agentes do Axiom constroem o Stacks — trabalhando em paralelo e escolhendo suas próprias tarefas — é exatamente o que Hong espera que seja o futuro de muitos trabalhos de IA. Ela acredita que agentes de IA precisam de uma base de conhecimento bem estruturada e reutilizável para evitar gerar conteúdo de baixa qualidade.
Hong disse: "Você quer que [o agente] tenha um repositório reutilizável no qual possa continuar construindo e empurrando constantemente os limites. Se você começar enchendo-o com más escolhas de engenharia, será muito difícil expandir esse limite."
Hong tem muita confiança nesse método e até lançou um desafio público. Ela disse: "Desafio publicamente todas as empresas de programação a realizarem esse tipo de trabalho formal nessa escala."