Axiom Math levanta US$ 200 mi para base matemática da IA segura

Tecnologia

Startup converte extenso projeto matemático em código para aprimorar a segurança em IA e software.

Leia também: Meta compra startup de IA Conductor e encerra serviço em 20/11

A Axiom Math anunciou nesta semana que concluiu a formalização computacional do Stacks Project, traduzindo 7.654 páginas de um dos maiores corpos de conhecimento matemático do mundo em cerca de 16 milhões de linhas de código na linguagem Lean, verificadas linha a linha por um assistente de provas. A façanha, liderada pela CEO Carina Hong e pela equipe técnica que inclui Ashvin Swaminathan, cria uma base matemática rigorosa pensada para sustentar a próxima geração de agentes de inteligência artificial e de software crítico.

Startup bilionária aposta em matemática como infraestrutura

Fundada em março de 2025, a Axiom Math já é avaliada em US$ 1,6 bilhão e levantou uma rodada Series A de US$ 200 milhões, liderada pelo fundo Menlo Ventures. A empresa nasceu da decisão de Carina Hong de abandonar um doutorado em matemática em Stanford para atacar um problema que ela vê como estrutural na era da IA: como impedir que provas matemáticas e códigos gerados por máquinas deslizem para erros difíceis de detectar.

“Things that are big and things that are delicate in life just don’t go together”, disse Hong, ao explicar o desafio de levar um projeto gigantesco e delicado como o Stacks para dentro de um sistema formal. Para ela, o objetivo é garantir que o acervo, que funciona como fundação para boa parte da matemática moderna, não esconda contradições. “Você quer [os teoremas] consistentes e não, tipo, paradoxais. Quer as definições sem brigar entre si”, afirmou.

O Stacks Project foi iniciado por Johan de Jong como uma referência aberta para temas que vão de álgebra de graduação a tópicos avançados em geometria e teoria dos números. Ao formalizar esse material, a Axiom Math tenta transformar o que hoje é um texto humano altamente sofisticado em uma biblioteca de blocos lógicos que programas podem reutilizar com segurança.

Como a Axiom ia traduziu 7.654 páginas em Lean

A formalização usa Lean, uma linguagem de programação voltada a provas matemáticas, em que cada passo lógico é escrito como código e validado automaticamente por um assistente de provas. O procedimento, conhecido como verificação formal, já é comum em projetos de chips e em softwares altamente sensíveis, mas nunca tinha sido aplicado nessa escala a um corpus tão entrelaçado quanto o Stacks.

O desafio não estava apenas em checar cada teorema, mas em preservar a teia de dependências entre definições e resultados. “Com o Stacks, impusemos uma hierarquia… [mas] não era, tipo, uma hierarquia completa ditando o que cada agente fazia”, contou Ashvin Swaminathan, da equipe técnica da Axiom Math. “The agents were finding tasks for themselves and identified things that they could work on in parallel”, disse.

Para isso, a Axiom co treinou agentes próprios de IA, especializados em matemática, que aprenderam a escrever em Lean e a navegar pela estrutura do projeto. Inicialmente, especialistas humanos em Lean serviram de tutores, transmitindo um certo “senso de gosto” matemático. Com o tempo, relata a empresa, os agentes passaram a refinar esse gosto sozinhos, escolhendo que partes atacar e como decompor problemas complexos em subtarefas paralelas.

O cuidado, diz Hong, incluía uma preocupação estética. “We were not sure if vibe coding would be able to preserve the beauty of Stacks”, afirmou, em referência à tendência de deixar que modelos generativos improvisem. A ideia da Axiom ia foi combinar autonomia dos agentes com uma estrutura rígida o suficiente para que cada linha de código formal correspondesse fielmente às ideias originais do Stacks Project.

Entenda o contexto

Nos últimos meses, grandes laboratórios de IA passaram a divulgar aos montes manuscritos com supostas soluções para problemas difíceis em matemática, muitas vezes apoiados em verificações automáticas. Mesmo assim, erros têm escapado. Em paralelo, cresce o uso de agentes de IA para escrever partes significativas do código que roda em sistemas financeiros, de infraestrutura e até ciência.

Nesse cenário, a Axiom Math tenta se diferenciar ao tratar a matemática como infraestrutura, não apenas como um campo de aplicação. “We believe that mathematics is the domain where you start building these things, and that it’s a transferable skill”, resumiu Swaminathan. A aposta é que uma base formal confiável reduza tanto o risco de “IA torta” produzindo provas falsas quanto o de softwares com falhas lógicas difíceis de rastrear.

Geometria algébrica deixa de ser um “buraco negro”

Para a comunidade acadêmica, o movimento tem um impacto particular em áreas em que a formalização ainda engatinha. “When you look at what has been formalized in mathematics, there’s this huge black hole. And that black hole covers algebraic geometry”, afirmou Swaminathan. O Stacks Project é justamente um grande compêndio de geometria algébrica, o que torna sua formalização uma peça inédita nesse quebra-cabeça.

Até agora, pesquisadores interessados em checar novos resultados em geometria algébrica com Lean tinham pouco material formalizado de base. “Well, now they do”, disse Swaminathan. Com o Stacks verificado, teoremas futuros podem se apoiar em um alicerce já checado por máquina, em vez de reconstituir desde o início cada definição ou lema intermediário.

O matemático Terence Tao, ganhador da Medalha Fields e um dos nomes mais respeitados da área, resume o efeito cumulativo desse tipo de trabalho: “The more formalized proofs you have, the more formalized proofs you can make”. Em outras palavras, cada resultado verificado aumenta o alcance do que é possível formalizar a seguir.

Base para software e IA mais confiáveis

A ambição da Axiom Math, porém, vai além dos departamentos de matemática. A empresa mira diretamente o problema de segurança de software em um mundo em que agentes de IA escrevem volumes crescentes de código. A visão é que a formalização do Stacks sirva como “substrato” lógico sobre o qual esses agentes possam raciocinar ao projetar novas infraestruturas digitais.

Segundo Swaminathan, a biblioteca em Lean que nasce da formalização permite que agentes leiam o código, entendam as estruturas matemáticas por trás dos algoritmos e construam sistemas com provas embutidas de correção. “Agents can read our code, understand it, and build new infrastructure on top of it. Our Lean formalization is now the substrate that agents can build upon”, afirmou.

Hong argumenta que, sem uma biblioteca reutilizável e bem construída, agentes de IA tendem a “empilhar gambiarra sobre gambiarra”, acumulando escolhas ruins de engenharia desde o começo. “Você quer [agentes] com uma biblioteca reutilizável para construir e seguir empurrando a fronteira”, disse. Na avaliação dela, quem ignorar a formalização hoje corre o risco de carregar, por anos, bugs lógicos difíceis de erradicar.

Próximos passos da Axiom Math team

Com o Stacks Project formalizado, a Axiom Math indica que o plano é avançar para outras áreas da matemática ainda pouco cobertas por verificações formais e, em paralelo, aproximar essa base dos fluxos de trabalho de desenvolvedores de software e pesquisadores em IA. A ideia é que, no futuro, ferramentas de programação assistida consigam não apenas sugerir trechos de código, mas também produzir provas formais de que aquele código se comporta como esperado.

A CEO da Axiom co chegou a lançar um desafio público para que outras empresas de código se aventurem em formalizações de escala semelhante. A expectativa é que o movimento estimule parcerias entre startups, universidades e a indústria de tecnologia, e acabe influenciando padrões de segurança em IA e em sistemas críticos.

Para a comunidade matemática, a formalização do Stacks impõe uma nova referência de rigor e abre espaço para que jovens pesquisadores se apoiem em uma base já verificada. Para o setor de tecnologia, representa um sinal de que a próxima fase da corrida da IA pode ser menos sobre velocidade de geração de resultados e mais sobre a solidez das fundações em que eles se apoiam.