OpenAI Publica Dez Avanços em Matemática Gerados pelo Astra — com Provas Verificadas por Máquina

A OpenAI publicou em 1º de agosto uma seleção de dez resultados que resolvem ou avançam substancialmente problemas em aberto na matemática e na ciência da computação teórica. Todos os argumentos foram gerados por uma versão interna do Astra, o próximo modelo principal da empresa — e cada um foi formalizado em certificados Lean, verificáveis por máquina.

Os problemas atravessam geometria de altas dimensões, teoria da codificação, complexidade de circuitos aritméticos, teoria dos grupos, álgebra de operadores, complexidade quântica, criptografia de reticulados e combinatória extremal. Segundo a OpenAI, os problemas selecionados não registravam progresso em seu resultado principal há pelo menos uma década — e, na maioria, muito mais.

O custo de computação é um dos dados mais impressionantes: o total de tokens necessários para encontrar as soluções custaria cerca de US$ 2.000 às tarifas da API Sol. Os manuscritos foram preparados por humanos com o mesmo modelo, que depois formalizou cada argumento em Lean. A OpenAI também liberou, para cada solução, uma narrativa do processo de raciocínio do modelo.

Os Dez Resultados

Destaques: da Geometria à Teoria dos Grupos

O primeiro capítulo determina a força assintótica do programa linear de Cohn–Elkies para empacotamento de esferas em altas dimensões. O resultado melhora o expoente geral de empacotamento de cerca de 0,5991 para 0,6044 — descrito no manuscrito como a primeira melhoria desde 1978 — e ainda mostra que o método de Cohn–Elkies não pode superar o novo expoente.

O pacote inclui um manuscrito de 249 páginas, uma narrativa de 62 páginas sobre os caminhos de descoberta e certificados Lean públicos

No capítulo de teoria dos grupos, o Astra construiu um grupo não-sofic explícito e finitamente apresentado usando expansores de propriedade-(T) e a álgebra de Leavitt binária — resolvendo, se aceito, a questão central de saber se todo grupo contável admite aproximações por permutações finitas. Já o capítulo da conjectura de rigidez de Connes constrói infinitos grupos de propriedade-(T) não isomorfos com álgebras de von Neumann de grupo isomorfas, contradizendo a conjectura e respondendo a uma questão de Sorin Popa.

Há ainda um dado de independência notável: a OpenAI relata trabalho concorrente independente de Shuoxing Zhou, que chegou a um contraexemplo para a conjectura de Connes com a assistência do GPT-5.6 Sol — apoio separado para a conclusão principal, embora não uma verificação da construção específica da OpenAI.

Lean: a Prova que a Máquina Confere

A peça que diferencia essa publicação de um anúncio convencional é a formalização em Lean 4. Em vez de pedir que um leitor humano siga uma prova em prosa persuasiva, o Lean exige que a afirmação e a demonstração sejam expressas numa linguagem formal — e seu pequeno kernel verifica se o termo de prova segue das definições, hipóteses e axiomas.

O repositório público openai/ten-proofs no GitHub contém um arquivo Lean para cada resultado. O manifesto de formalização reporta zero ocorrências de "sorry" (o escape usado para deixar lacunas de prova) e lista apenas axiomas lógicos padrão — propext, Classical.choice e Quot.sound. O projeto compila com Lean 4.32.0 e mathlib, e inclui configurações de Comparator para permitir a checagem das provas exportadas com outro kernel.

Mas uma verificação bem-sucedida do kernel estabelece apenas que a conclusão codificada segue das definições e hipóteses codificadas. Ela não determina por si mesma se a afirmação formal captura fielmente a conjectura histórica, se uma definição enfraqueceu o problema ou se o manuscrito descreve corretamente a importância do teorema. Essas são questões de revisão matemática, não de type-checking.

Os certificados Lean elevam a barra de evidência — mas matemáticos independentes ainda precisam julgar a novidade e a significância de cada resultado

O que Ainda Falta: Revisão por Pares

O pacote não equivale a revisão por pares concluída. O manifesto de formalização descreve o código como "agent-reviewed", e os agradecimentos mostram que especialistas externos comentaram o manuscrito sobre grupos não-sofic e leram cuidadosamente o capítulo da rigidez de Connes — escrutínio pré-publicação significativo, mas a coleção não reporta aceite em revista ou conferência formal.

Especialistas destacam cinco pontos de atenção antes de qualquer celebração:

1. O Lean verifica o teorema como formalizado, não a manchete
2. Humanos precisam confirmar que as definições capturam os objetos matemáticos pretendidos
3. Especialistas devem confirmar que o teorema formal é equivalente, ou forte o suficiente, para resolver o problema histórico
4. Um provador de teoremas não julga novidade, precedência ou importância
5. Metadados de repositório e compilação reproduzível não substituem a revisão independente do pacote completo

A própria OpenAI adota uma declaração de atribuição incomumente direta: os argumentos matemáticos foram gerados pelo Astra, enquanto humanos ajudaram a preparar os manuscritos e o modelo formalizou cada argumento em Lean. Para a empresa, afirmar autoria humana de uma prova gerada inteiramente por IA distorceria a contribuição do sistema e a natureza do trabalho intelectual genuíno.

O Significado para a Pesquisa

O anúncio é o passo seguinte de uma trajetória: em maio, a OpenAI já havia compartilhado uma disprova gerada por IA da conjectura da distância unitária de Erdős, que inspirou novos desenvolvimentos em matemática e ciência da computação. O pacote de agosto, porém, é qualitativamente diferente — não é um benchmark, mas um dossiê de pesquisa com dez resultados nomeados, manuscritos completos e artefatos formais que especialistas podem atacar linha por linha.

Há, ainda, o contexto da iniciativa ChatGPT for Academic Researchers, que dá acesso gratuito aos melhores modelos da empresa a 100 mil cientistas e matemáticos. O movimento sugere que a avaliação de modelos frontier está deixando os testes de resposta curta e caminhando para resultados de pesquisa originais e auditáveis.

A conclusão equilibrada, como resumem os analistas: não é "a IA resolveu definitivamente dez problemas famosos" nem "nada disso importa". É que a OpenAI publicou dez afirmações matemáticas concretas com substancialmente mais material de verificação do que um anúncio de laboratório normalmente oferece — e deixou o veredito para os matemáticos. O teste real será o que vem depois: se as provas sobreviverem ao escrutínio e produzirem novas ideias, o impacto será medido pela pesquisa humana que elas inspirarem.