A IA da Axiom Math Verifica o Teorema dos 246 Intervalos entre Primos no Lean

A Axiom Math afirma que seu sistema AxiomProver produziu uma prova verificada por máquina em Lean 4 do resultado mais forte conhecido sobre lacunas entre números primos: o teorema de que infinitos pares de primos diferem em no máximo 246. A empresa publicou o resultado em 17 de agosto de 2026 como um plano de formalização interativo creditado a 41 colaboradores nomeados — matemáticos, engenheiros e investigadores‑principais —, com IEEE Spectrum primeiro a relatar a conquista.

O limite de 246 é a fronteira atual do conhecimento humano na longa investida contra a conjectura dos primos gêmeos, a hipótese do século XIX de que primos separados exatamente por dois ocorrem indefinidamente. Página do projeto da Axiom Math descreve o trabalho como uma formalização unificada do artigo de James Maynard de 2013 “Small gaps between primes” juntamente com a parte do seguimento da colaboração Polymath8b que reduziu o limite de Maynard de 600 para 246. As provas verificadas por máquina são organizadas em uma biblioteca pública de Lean, PrimeGapsLib, com o teorema de 246 como seu resultado principal.

“Este teorema representa atualmente o limite do conhecimento humano sobre números primos”, disse Ken Ono, matemático fundador da Axiom Math.

A verificação formal consiste em traduzir uma prova para uma linguagem que um pequeno programa confiável, chamado kernel, pode checar linha por linha. O resultado não é uma garantia absoluta — a própria afirmação precisa ser traduzida corretamente, e o verificador deve ser sólido — mas elimina a falibilidade do árbitro humano da cadeia. Até agora, os sistemas de IA que competem em benchmarks de matemática foram medidos principalmente em problemas de competição com provas curtas e autocontidas; a diferença entre esses resultados e a formalização em nível de pesquisa tem sido grande, um padrão visível em sistemas anteriores que se destacaram em geometria olímpica enquanto deixavam a matemática de pesquisa em grande parte intocada.

De 70 Milhões a 246

A própria conjectura, formulada precisamente por Alphonse de Polignac no século XIX, continua sem prova. O primeiro limite finito de qualquer tipo surgiu em 2013, quando Yitang Zhang demonstrou que infinitos pares de primos estão a no máximo 70 milhões uns dos outros. Meses depois, Maynard introduziu um método de crivo refinado e reduziu o limite para 600 — trabalho que contribuiu para sua Medalha Fields de 2022 — e a colaboração Polymath8b, que incluiu Maynard e Terence Tao, o reduziu para 246. O plano da Axiom Math apresenta essa progressão como o projeto que se propôs a formalizar.

A formalização segue um fluxo de trabalho que a empresa descreve em três etapas. Os pesquisadores primeiro escreveram a prova como um plano — cada definição, lema e teorema recebeu um rótulo, uma declaração precisa e uma lista dos resultados dos quais depende — produzindo um grafo de dependências que ordenou o trabalho. O AxiomProver, o sistema multiagente da empresa para pesquisa matemática por meio de prova formal, então gerou provas Lean 4 verificáveis por máquina, construídas sobre o Mathlib, a biblioteca comunitária de matemática, e sobre o PrimeNumberTheoremAnd, o projeto de formalização existente liderado por Alex Kontorovich e Tao. A equipe da Axiom revisou o código gerado e o organizou na PrimeGapsLib.

Os principais resultados declarados da biblioteca vão um pouco além do teorema de destaque. Além do limite de 246, ela formaliza o limite de 600 de Maynard e inclui um desafio de verificação autônomo — construído apenas sobre o Mathlib, com a seção de prova deixada vazia — que permite a qualquer pessoa com a ferramenta de comparação Lean confirmar independentemente que as provas da biblioteca correspondem aos teoremas declarados. A empresa alerta que a verificação completa pode levar horas; uma versão reduzida que cobre os outros dois resultados é executada em minutos.

Onde Isso Se Encaixa Entre as Alegações de Formalização por IA

O resultado surge em um ano de alegações crescentes sobre sistemas de IA realizando matemática de nível de pesquisa, a maioria delas baseada em pontuações de competições ou provas curtas. A Axiom Math tem sido uma das reclamantes mais agressivas: o AxiomProver é creditado por resolver problemas anteriormente em aberto, incluindo trabalhos que a empresa publicou em periódicos revisados por pares, e sistemas de IA já resolveram vários problemas de Erdős de longa data. A formalização de 246 é um tipo diferente de resultado — não um novo teorema, mas uma reconstrução verificada por máquina de uma das provas mais tecnicamente exigentes da teoria dos números moderna.

A comparação mais próxima ocorreu no início deste ano, quando Math, Inc. utilizou seu agente Gauss para concluir a prova formal dos resultados de empacotamento de esferas de Maryna Viazovska, vencedora da Medalha Fields, nas dimensões 8 e 24. Sidharth Hariharan, estudante de doutorado da Carnegie Mellon que liderou o esforço humano de plano nessa formalização e que agora é estagiário na Axiom Math e colaborador matemático nomeado no projeto de 246, argumenta que o novo resultado é a conquista mais abrangente. Seu raciocínio, como ele descreveu, é que a Axiom foi construída para reutilização: em vez de uma formalização única de uma única prova, a PrimeGapsLib é uma biblioteca mantida de resultados sobre lacunas entre primos, destinada a apoiar trabalhos e pesquisas de formalização futuros.

Essa distinção é importante para a forma como o resultado deve ser interpretado. Uma verificação pontual demonstra que um sistema pode lidar com uma prova difícil. Uma biblioteca demonstra algo mais próximo de infraestrutura — maquinaria formal reutilizável que outros resultados podem aproveitar — que é a direção dos sistemas de prova formal têm avançado à medida que passam de resolver exercícios para checar matemática real. A alegação de capacidade aqui se baseia em artefatos que são públicos e reexecutáveis, em vez de uma pontuação de benchmark: o plano, o código Lean e um desafio de comparação projetado para que pesquisadores externos possam verificar as provas por si mesmos.

Ono apresenta a matemática como um campo de testes para uma ambição maior. Se propriedades de software — como se um programa termina ou se sua saída está correta para toda entrada — podem ser expressas como declarações matemáticas precisas, então os sistemas derivados do AxiomProver poderiam prová‑las formalmente, argumenta ele, apontando para a verificação do código gerado por IA que começa a operar em infraestruturas, finanças e sistemas de segurança.

“O mundo está prestes a operar com código de computador que ninguém leu”, disse Ono. “A IA está aqui e não podemos mais desviar o olhar — a formalização de provas é um campo de testes para resolver o que eu acredito ser o desafio mais importante que enfrentaremos da IA.”

Por enquanto, o entregável é mais restrito e verificável: um plano com 41 autores, uma biblioteca pública Lean e uma prova verificada por máquina de que primos a até 246 de distância nunca se esgotam — o vizinho mais próximo verificado da conjectura dos primos gêmeos, e a mais profunda peça de matemática de pesquisa que um sistema de IA verificou de ponta a ponta.