O número que importa e 460.000: linhas de prova formalmente verificável que a OpenAI depositou num repositório público do GitHub em 1o de agosto para respaldar dez avanços reivindicados em matemática e ciência da computação teórica. O artigo que os anuncia, datado da mesma manhã, diz que os resultados vieram de uma versão interna do Astra, 'nosso próximo modelo principal'. Cada um dos dez resultados vem com um certificado Lean, uma prova formal verificável por máquina, no repositório github.com/openai/ten-proofs sob licença Apache-2.0. Verificamos os arquivos: os dez compilam com Lean 4.32 e mathlib, e nenhum contem um 'sorry' nem um axioma sob medida, as duas saídas de emergência habituais.
Os dez, como a OpenAI os enuncia: novas cotas superiores para empacotamento de esferas em alta dimensão ate o limiar de Cohn-Elkies; cotas exponencialmente melhoradas para códigos binários e esfericos; uma construcao de grupos não soficos; um contraexemplo que refuta a conjectura de rigidez de Connes; cotas inferiores para o permanente, incluindo uma cota de formula aritmética de ordem n a quarta sobre log n; um teorema de repeticao paralela exponencial para jogos quânticos; dureza de aproximacao de fator polinomial para o problema do vetor mais próximo; uma resposta precisa a conjectura do volume de Ehrhart; uma cota inferior superexponencial para os números de Ramsey multicoloridos do triangulo, que resolveria o problema 183 de Erdos; e contraexemplos as conjecturas de compacidade e degenerescencia, resolvendo os problemas 146 e 180 de Erdos. O enquadramento da OpenAI e que cada problema estava parado ha pelo menos uma década. Esse enquadramento e dela, como a cifra de cerca de US$ 2.000 de computação nas tarifas Sol da API.
Eis o que e verificável de forma independente hoje, e e mais que nada e menos que uma prova. Verificável: o repositório existe, os dez arquivos Lean estão la, o conteudo e o descrito, dois PDFs companheiros (o artigo e as narracoes de raciocínio do modelo) baixam, e o repositório inclui configurações para verificação com um núcleo independente. Ainda não verificável: ninguem fora da OpenAI disse ter reconstruído as provas; nenhum matematico humano as revisou; e nenhum especialista confirma que os enunciados formalizados dizem o que os teoremas informais dizem, a etapa em que a formalizacao pode quebrar em silêncio. O sinal mais forte de não ratificacao: o erdosproblems.com, o rastreador de referencia, ainda lista o problema 183 como aberto com premio de US$ 250, enquanto um rastreador menor ja o marcou como resolvido em 1o de agosto. Thomas Bloom, que mantem esse site, chamou de 'grande notícia' e de 'grande' para as construções, em mensagens citadas pelo The Decoder; não conseguimos recupera-las diretamente.
No nome, a precisão importa porque este e o artigo que as pessoas vao citar. O blog diz 'uma versão interna do Astra, nosso próximo modelo principal'. A frase 'próxima grande familia de modelos' e do pesquisador da OpenAI Noam Brown, que acrescentou 'infelizmente nenhum problema do Milenio (ainda)', e notou que o modelo falhou em outros grandes problemas. Todo o resto e reportado, não confirmado: o The Information, via The Decoder, coloca o Astra como uma nova classe ao lado de Sol, Terra e Luna, com a decisão GPT-6 contra GPT-5.7 em aberto e sem data de lançamento. A nota de ética da OpenAI merece ser citada inteira: 'reivindicar autoria humana de uma prova gerada inteiramente por um sistema de IA detortaria tanto a contribuição do sistema quanto a natureza do trabalho intelectual humano genuino', e a empresa diz assumir a responsabilidade pela correção enquanto os argumentos foram gerados pelo modelo. Essa e a frase a que segura-los quando as reconstrucoes chegarem.