Axiom usa enxames de agentes de IA para verificar no Lean a maior prova da matemática

A matemática tem a sua própria «obra gigante», e não é um mangá de cem volumes. A Classificação dos Grupos Simples Finitos, apelidada de «teorema enorme», ocupa cerca de 15 mil páginas espalhadas por mais de 500 artigos escritos por uns cem matemáticos ao longo de décadas. Agora a empresa Axiom anunciou que conseguiu reescrever essa prova inteira no Lean, uma linguagem em que cada passo de um raciocínio é conferido por computador.

Como foi feito

Segundo a Axiom, o trabalho levou 24 dias. Engenheiros e matemáticos da empresa coordenaram enxames de dezenas de agentes de IA, que dividiram o projeto em 108 grandes etapas e cerca de 380 tarefas menores. Uns agentes quebravam os argumentos difíceis em partes, outros procuravam resultados já existentes e outros escreviam as provas em Lean. As pessoas entravam quando havia um obstáculo matemático de verdade. O resultado tem aproximadamente 43,1 milhões de linhas de código, e o repositório foi aberto ao público.

O que apareceu no caminho

O mais interessante para mim não é o tamanho, e sim o que a revisão encontrou. A maioria dos problemas eram deslizes pequenos, como erros de digitação, tabelas erradas ou hipóteses esquecidas. Mas a empresa diz ter achado 34 desvios relevantes em relação ao que estava publicado, o mais sério ligado ao chamado Teorema do Grupo Desequilibrado, com um contraexemplo a uma afirmação usada num dos caminhos da prova. A classificação em si continua de pé, e o trabalho ainda rendeu um resultado novo em teoria dos grupos.

Minha opinião

É um daqueles anúncios que dão vontade de comemorar e de esperar ao mesmo tempo. O Lean garante que os passos fecham, mas ainda falta gente de fora reconstruir a prova e especialistas confirmarem que o enunciado formal diz exatamente o que o teorema diz, algo que a própria Axiom pede à comunidade. Se isso se confirmar, é um marco enorme para a IA a serviço da ciência, e não só para gerar imagens ou texto.

Fonte: anúncio oficial da Axiom