Start-ups dos EUA correm para criar superinteligência matemática com IA verificável

Start-ups do Vale do Silício estão investindo centenas de milhões de dólares para desenvolver sistemas de inteligência artificial capazes de resolver problemas matemáticos complexos e comprovar a exatidão de suas respostas.

A Axiom Math e a Harmonic lideram essa corrida, atraindo matemáticos renomados como Ken Ono, que deixou a Universidade de Emory em 2025 para integrar a equipe da Axiom. Ono descreve a experiência como um choque, comparando-a à surpresa de um agricultor ao ver um motor de combustão pela primeira vez.

O êxodo de acadêmicos para o setor privado reflete a crença de que a matemática é o ingrediente secreto para aprimorar a inteligência artificial. A Axiom Math já publicou cinco artigos científicos produzidos inteiramente por suas ferramentas de IA, aceitos em periódicos de geometria algébrica e teoria dos números.

Segundo reportagem da New Scientist, essas empresas miram também o mercado de verificação de software. A Harmonic e a Axiom Math apostam que a checagem automática e matematicamente garantida se tornará um serviço bilionário, à medida que a IA assume a escrita de código.

O mecanismo de verificação utiliza linguagens formais como o Lean, que traduzem demonstrações manuais em formatos verificáveis por computador em segundos. Essa lógica pode ser aplicada a programas de computador, provando que estão livres de falhas sem necessidade de revisão humana.

Gigantes da tecnologia também entraram na disputa. Jakub Pachocki, cientista-chefe da OpenAI, destaca que a matemática é ideal para desenvolver IA por ser altamente mensurável. Modelos recentes da empresa já conquistaram medalha de ouro na Olimpíada Internacional de Matemática.

A OpenAI busca uma inteligência geral com habilidades matemáticas surpreendentes, enquanto a Axiom Math e a Harmonic treinam modelos especializados. Sébastien Bubeck, da Microsoft Research, classifica o progresso dos últimos seis meses como chocante, com a IA refutando uma conjectura de 80 anos considerada intocável.

A rápida injeção de capital gera incertezas entre matemáticos. Ravi Vakil, da Universidade de Stanford, alerta que o dinheiro fácil pode desaparecer tão rápido quanto chegou. Ele questiona se há realmente ganhos em resolver problemas como a hipótese de Riemann.

Outra preocupação é a possível privatização do conhecimento matemático. Embora as ferramentas da Axiom Math sejam gratuitas atualmente, a empresa admite que poderá cobrar pelo serviço no futuro. A Harmonic defende que serviços úteis têm custo, mas o avanço do conhecimento deve permanecer acessível.

Ono recorda uma conversa com seu pai, falecido em janeiro, que comparou o momento ao surgimento de Srinivasa Ramanujan, o gênio indiano cujas intuições revolucionaram a matemática no século 20. Para ele, testemunhar um computador criando algo que parece mágica é uma experiência compartilhada por todos os envolvidos.

Enquanto bilhões são investidos, o futuro da pesquisa matemática é reescrito em escritórios discretos de Palo Alto, batizados com nomes de Gauss e Ada Lovelace. Para alguns, essa é a aurora de uma era em que a criação matemática se acelera de décadas para dias.

Com informações de NEWSCIENTIST.