Axiom Math quer manter o desperdício de IA fora da matemática

Parece que a IA está resolvendo um novo problema de matemática toda semana. No mês passado, só a OpenAI divulgou 719 manuscritos alegando soluções para alguns dos problemas mais difíceis da área. Até mesmo as verificações do computador podem falhar. Depois de anos de desperdício de IA, é justo imaginar se a matemática será a próxima.

A AxiomMath aposta que a matemática pode evitar esse destino, não desacelerando, mas permanecendo em terreno mais firme. A startup de US$ 1,6 bilhão quer construir uma base verificada na qual os agentes de IA possam confiar para escrever software e, eventualmente, fazer ciência.

Na quarta-feira, a empresa anunciou que verificou formalmente o Projeto Stacks, um dos maiores corpos matemáticos já escritos por humanos. Os matemáticos muitas vezes têm Stacks com rara consideração – o matemático de Columbia, Peter Woit, afirmou que não há “nada mais realmente comparável”, comparando o projeto aos “famosos livros de Bourbaki”, uma série que reconstruiu a matemática desde seus fundamentos no século XX.

O colega de Woit na Columbia, Johan de Jong, iniciou o Stacks Project em 2005 como uma referência de código aberto. Os matemáticos têm contribuído para isso desde então, construindo resultados desde a álgebra de nível universitário até as ideias mais avançadas da área em álgebra, geometria e teoria dos números.

A frota de agentes de IA da empresa traduz as cerca de 7.654 páginas da biblioteca em cerca de 16 milhões de linhas de código verificado por computador.

Formalizar a matemática é uma forma de garantir que a estrutura subjacente seja sólida. Os matemáticos reescrevem a prova como código em uma linguagem de programação chamada Lean, e um programa chamado assistente de prova verifica o código linha por linha. Se a prova for aprovada, os matemáticos podem confiar que ela é logicamente correta.

Os engenheiros usam a mesma ideia, chamada de verificação formal, para confirmar o funcionamento de seus projetos de chips, enquanto pesquisadores na França a usam para detectar bugs em softwares que calculam benefícios familiares.

Para uma biblioteca como o Stacks Project, verificar cada teorema é apenas parte do trabalho. Os teoremas e definições em Stacks estão interconectados e cada um se baseia nos anteriores. Como uma árvore genealógica, muitos resultados nas pilhas remontam aos anteriores.

Essa interconectividade deixou a Axiom insegura de que o projeto funcionaria inicialmente. A equipe teve que manter todas as conexões intactas em cerca de 16 milhões de linhas de código Lean.

“Coisas grandes e delicadas na vida simplesmente não combinam”, disse Carina Hong, CEO da Axiom, ao TechCrunch. “(Stacks) é uma coleção de resultados matemáticos que é a base da matemática. Você quer que (os teoremas) sejam consistentes e não paradoxais. Você quer que as definições não briguem entre si.”

O CEO de 25 anos abandonou o doutorado em matemática de Stanford. O programa nd fundou a empresa em março de 2025. Em março, a Axiom levantou uma Série A de US$ 200 milhões liderada pela Menlo Ventures.

“Não tínhamos certeza se a codificação vibratória seria capaz de preservar a beleza das Stacks”, disse Hong.

Para levar adiante o projeto, a equipe deu aos seus agentes uma estrutura flexível e os deixou trabalhar em paralelo. “Com Stacks, impusemos uma hierarquia… (mas) não era uma hierarquia completa que ditasse o que cada agente estava fazendo”, disse Ashvin Swaminathan, membro da equipe técnica da Axiom. “Os agentes estavam encontrando tarefas para si próprios e identificando coisas nas quais poderiam trabalhar em paralelo.”

A Axiom também treinou seus próprios modelos para serem bons em matemática, uma abordagem que Hong disse que a maioria das outras startups de verificação não adotam. No início, a equipe contou com um de seus especialistas Lean internos para ensinar aos agentes o sentido humano do paladar. Com o tempo, disse Hong, os agentes adquiriram o gosto por conta própria.

O resultado preenche uma das maiores lacunas da matemática formalizada. “Quando você olha para o que foi formalizado em matemática, existe um enorme buraco negro. E esse buraco negro cobre a geometria algébrica”, disse Swaminathan.

Até agora, os pesquisadores que queriam verificar novos trabalhos em geometria algébrica com Lean tinham pouco em que se basear, disse Swaminathan. “Bem, agora eles fazem.”

A Axiom argumenta que cada resultado verificado se torna um alicerce, de modo que as provas futuras podem basear-se na matemática verificada em vez de começar do zero. Terence Tao, o matemático da UCLA e vencedor da Medalha Fields, tornou o caso geral mais simples: “Quanto mais provas formalizadas você tiver, mais provas formalizadas você poderá fazer”.

Os matemáticos não são o único público-alvo da Axiom. Os desenvolvedores há muito lutam para garantir que seu código esteja livre de bugs e falhas de segurança. Esse problema aumenta à medida que os agentes de IA escrevem mais códigos do mundo.

A Axiom aposta que o software do futuro precisará se basear em bases verificadas, como o Stacks faz agora.

“Acreditamos que a matemática é o domínio onde você começa a construir essas coisas e que é uma habilidade transferível”, disse Swaminathan. “Os agentes podem ler nosso código, entendê-lo e construir uma nova infraestrutura sobre ele. Nossa formalização Lean é agora o substrato sobre o qual os agentes podem construir.”

A forma como os agentes da Axiom construíram Stacks, trabalhando em paralelo e escolhendo suas próprias tarefas, é como Hong espera que grande parte do trabalho futuro da IA ​​aconteça. Os agentes de IA, argumenta ela, precisarão de um corpo de conhecimento bem construído e reutilizável para não produzir resíduos.

“Você deseja que (os agentes) tenham uma biblioteca reutilizável para que possam desenvolver e continuar avançando além das fronteiras”, disse Hong. “Se você cair de uma forma que seja uma má escolha de engenharia no início, será muito difícil para eles aumentar esse limite.”

Hong está suficientemente confiante nessa abordagem para lançar um desafio. “Desafio abertamente todas as empresas de codificação a trabalharem na formalização nesta escala.”