Axiom Math quer manter a porcaria de IA fora da matemática

Parece que a IA está resolvendo um novo problema de matemática toda semana. No mês passado, a OpenAI lançou 719 manuscritos alegando soluções para alguns dos problemas mais difíceis da área. Até mesmo as verificações de computadores podem falhar. Após anos de conteúdo gerado por IA de baixa qualidade, é justo questionar se a matemática será a próxima.

Axiom Math está apostando que a matemática pode evitar esse destino, não desacelerando, mas se apoiando em bases mais firmes. A startup avaliada em US$ 1,6 bilhão quer construir uma fundação verificada na qual agentes de IA possam confiar para escrever software e, eventualmente, fazer ciência.

Na quarta-feira, a empresa anunciou que verificou formalmente o Stacks Project, um dos maiores corpos da matemática já escritos por humanos. Matemáticos frequentemente nutrem uma consideração rara pelo Stacks — o matemático de Columbia Peter Woit afirmou que “não há realmente nada comparável”, comparando o projeto aos “famosos livros de Bourbaki”, uma série que reconstrói a matemática a partir de suas bases no século XX. 

O colega de Woit em Columbia, Johan de Jong, iniciou o Stacks Project em 2005 como uma referência de código aberto. Matemáticos têm contribuído para ele desde então, desenvolvendo 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 aproximadamente 16 milhões de linhas de código verificadas por computador.

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

Engenheiros usam a mesma ideia, chamada de verificação formal, para confirmar que seus projetos de chips funcionam, enquanto pesquisadores na França a usaram para encontrar 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 no Stacks são interconectados, e cada um se baseia naqueles que vieram antes dele. Assim como em uma árvore genealógica, muitos resultados no Stacks remontam aos que os precederam.

Essa interconexão deixou a Axiom incerta se o projeto funcionaria no início. A equipe teve que manter cada conexão intacta ao longo de cerca de 16 milhões de linhas de código Lean.

“Coisas que são grandes e coisas que são delicadas na vida simplesmente não combinam”, disse a CEO da Axiom, Carina Hong, ao TechCrunch. “[O Stacks] é uma coleção de resultados matemáticos que é a fundação da matemática. Você quer que os [teoremas] sejam consistentes e não, tipo, paradoxais. Você quer que as definições não entrem em conflito umas com as outras.”

A CEO de 25 anos abandonou o programa de doutorado em matemática de Stanford e 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 por vibração seria capaz de preservar a beleza do Stacks”, disse Hong.

Para concretizar o projeto, a equipe deu aos seus agentes uma estrutura flexível e permitiu que eles rodassem em paralelo. “Com o Stacks, impusemos uma hierarquia … [mas] não era, tipo, uma hierarquia completa ditando o que cada agente individual estava fazendo”, disse Ashvin Swaminathan, membro da equipe técnica da Axiom. “Os agentes estavam encontrando tarefas por si mesmos e identificavam coisas em que podiam trabalhar em paralelo.”

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

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

Até agora, pesquisadores que queriam verificar novos trabalhos em geometria algébrica com o Lean tinham pouco sobre o que construir, disse Swaminathan. “Bem, agora eles têm.”

A Axiom argumenta que cada resultado verificado se torna um bloco de construção, para que futuras demonstrações possam se apoiar na matemática verificada em vez de começar do zero. Terence Tao, matemático da UCLA e ganhador da Medalha Fields, resumiu o caso geral de forma mais simples: “Quanto mais demonstrações formalizadas você tem, mais demonstrações formalizadas você pode fazer.”

Os matemáticos não são o único público-alvo da Axiom. Desenvolvedores lutam há muito tempo para garantir que seus códigos estejam livres de bugs e falhas de segurança. Esse problema cresce à medida que agentes de IA escrevem mais códigos do mundo. 

A Axiom está apostando que o software do futuro precisará se apoiar em fundações verificadas, da mesma forma que o Stacks faz agora.

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

A maneira como os agentes da Axiom construíram o Stacks, trabalhando em paralelo e escolhendo suas próprias tarefas, é como Hong espera que gran parte do trabalho futuro da IA aconteça. Agentes de IA, argumenta ela, precisarão de um corpo de conhecimento bem construído e reutilizável para evitar a produção de conteúdo de baixa qualidade.

“Você quer que os [agentes] tenham uma biblioteca reutilizável para construir em cima e continuar empurrando a fronteira”, disse Hong. “Se você despejar conteúdo de má qualidade com escolhas de engenharia ruins no início, fica muito difícil para eles expandirem essa fronteira.”

Hong está confiante o suficiente nessa abordagem para lançar um desafio. “Eu desafio abertamente todas as empresas de código a trabalharem na formalização nessa escala.”