A Axiom Math lançou uma versão verificada por máquina do Stacks Project, uma importante referência de código aberto em geometria algébrica. A formalização traduz a matemática do projeto em cerca de 16 milhões de linhas de código Lean, verificadas passo a passo por um programa de checagem de provas. Segundo a Axiom, pesquisadores e agentes de IA podem usar os resultados como uma biblioteca integrada para desenvolver novas provas formais.
As fontes apresentam números ligeiramente diferentes de páginas: a TechCrunch informa cerca de 7.654 páginas, enquanto a Axiom descreve o projeto como tendo aproximadamente 7.500. A referência original foi iniciada em 2005 pelo matemático Johan de Jong, da Universidade Columbia, e ampliada por matemáticos ao longo de duas décadas. O trabalho da Axiom formaliza esse conhecimento já existente; não significa que os agentes de IA tenham descoberto a matemática subjacente por conta própria.
Por que uma biblioteca integrada é importante?
Uma biblioteca de provas é útil não apenas porque seus teoremas foram verificados individualmente, mas também porque provas posteriores podem reutilizá-los e aproveitar suas dependências. A Axiom afirma ter preservado as etiquetas permanentes do Stacks Project, ligando as declarações em Lean às partes correspondentes do texto original. Em seu site, a empresa também permite que os leitores vejam o texto e o código lado a lado e explorem as dependências entre os resultados.
Isso é especialmente importante na geometria algébrica, em que uma prova pode depender de uma longa cadeia de ideias de áreas como álgebra comutativa, esquemas, feixes e cohomologia. A Axiom diz que, antes desse lançamento, os pesquisadores dispunham de uma infraestrutura Lean bem mais limitada para formalizar a geometria algébrica moderna. A biblioteca da empresa oferece um ponto de partida, sem exigir que esses fundamentos sejam formalizados novamente em cada projeto.
Uma base para futuras provas — e softwares
Segundo a Axiom, seus agentes trabalharam em paralelo para traduzir, provar e integrar milhares de teoremas. A TechCrunch informa que a empresa forneceu aos agentes uma estrutura flexível para que identificassem tarefas e trabalhassem nelas, e que a Axiom também treinou seus próprios modelos especializados em matemática. A empresa afirma que a biblioteca concluída é a maior biblioteca integrada e reutilizável de matemática formalizada; essa é a caracterização da Axiom para o lançamento.
O mesmo tipo de verificação é usado em áreas como projeto de chips e validação de software. A Axiom argumenta que fundamentos verificados e reutilizáveis podem ajudar agentes de IA a criar sistemas mais confiáveis à medida que escrevem mais código. Mas o lançamento verifica a formalização do Stacks Project, não toda nova afirmação matemática ou todo software que um sistema de IA possa produzir.
Por que importa
Para matemáticos que trabalham com geometria algébrica, a biblioteca oferece resultados verificados que podem ser reutilizados, em vez de reconstruir os mesmos fundamentos em Lean. Ela confirma a formalização dessa referência, mas não garante que futuras provas ou códigos gerados por IA sejam confiáveis sem verificação.
