AxiomMath, uma startup avaliada em US$ 1,6 bilhão, está buscando garantir a precisão matemática em uma era dominada pela inteligência artificial (IA). A empresa anunciou recentemente a verificação formal do Projeto Stacks, um dos maiores corpos de matemática escrita por humanos.

Objetivo e método

A ideia é criar uma base matemática verificada que os agentes de IA possam usar para escrever software e, eventualmente, realizar ciência. Para isso, a empresa traduz cerca de 7,654 páginas do Projeto Stacks em código de computador, passando por um processo de verificação formal.

O Projeto Stacks foi iniciado em 2005 por Johan de Jong, um matemático da Columbia University, como um referencial aberto. Desde então, matemáticos contribuem para ele, construindo resultados desde álgebra básica até ideias avançadas em álgebra, geometria e teoria dos números.

Tecnologia e desafios

A verificação formal é um processo que garante a consistência lógica das provas. Os matemáticos reescrevem as provas em um idioma de programação chamado Lean, e um assistente de prova verifica cada linha. Se a prova passar, os matemáticos podem confiar na sua lógica.

A equipe de AxiomMath enfrentou desafios significativos ao manter todas as conexões intactas em cerca de 16 milhões de linhas de código Lean. A CEO Carina Hong, uma ex-doutoranda em matemática da Stanford University, explicou que a consistência e a coerença são cruciais para evitar paradoxos.