Uma startup fundada por um estudante que deixou Stanford há menos de 15 meses afirma ter feito algo que normalmente leva décadas a matemáticos humanos: resolver múltiplos problemas não resolvidos em matemática usando um sistema de IA e conseguir que o trabalho seja aceito pela comunidade acadêmica.
Axiom Math, uma empresa sediada em Palo Alto liderada pela fundadora Carina Hong, afirma que seu sistema AxiomProver resolveu pelo menos quatro problemas matemáticos anteriormente não resolvidos. As provas foram publicadas no arXiv em fevereiro de 2026, mas, até o final de maio de 2026, nenhuma publicação em revista revisada por pares foi confirmada — uma distinção que o enquadramento do artigo oculta.
O que o Axiom realmente resolveu
Os problemas abordados pelo AxiomProver não são exercícios triviais. Entre os resultados estão soluções para conjecturas significativas na geometria algébrica e a Conjectura de Fel, um problema ligado ao trabalho de Srinivasa Ramanujan. Um dos problemas resolvidos envolve uma conjectura da teoria dos números com 20 anos.
Pelo menos uma das provas resultou da colaboração com matemáticos estabelecidos, não de saída pura de máquina.
A empresa utiliza verificação formal por meio do assistente de prova Lean. Em vez de gerar texto que parece ser uma prova e esperar que esteja correta, o AxiomProver produz provas que são verificadas mecanicamente quanto à validade lógica em cada etapa. Essa camada de verificação formal é o que confere credibilidade ao trabalho, algo que as saídas típicas de grandes modelos de linguagem não possuem.
O dinheiro e a equipe por trás dele
Axiom Math arrecadou US$200 milhões em financiamento da Série A liderado pela Menlo Ventures, elevando sua avaliação pós-negócio para US$1,6 bilhão. Isso somou-se aos US$64 milhões em investimentos anteriores, trazendo o total de financiamento conhecido para US$264 milhões. Hong deixou um programa conjunto de J.D./Ph.D. em Stanford para iniciar a empresa em março de 2025.
Ken Ono, um renomado teórico dos números conhecido por seu trabalho sobre o legado de Ramanujan e formas modulares, juntou-se à Axiom Math como matemático fundador.
A visão geral para IA e matemática
Axiom Math não está operando em um vácuo. O DeepMind do Google tem avançado na raciocínio matemático, mais notavelmente com seu sistema AlphaProof.
É prática padrão para matemáticos publicar preprints no arXiv enquanto os artigos passam por revisão por pares, um processo que pode levar meses ou até anos. As postagens do arXiv de fevereiro de 2026 estão atualmente sob escrutínio de especialistas, e nenhuma publicação revisada por pares foi confirmada até final de maio de 2026.