OpenAI publica 719 provas e esconde modelo

O modelo que ninguém pode usar resolveu 719 problemas

Modelo de fronteira da OpenAI que ninguém fora do laboratório pode acessar acabou de assinar 719 manuscritos matemáticos de uma vez. Não é demo, não é benchmark vazado, é matemática publicável, com prova, formalização em Lean em boa parte dos casos e repositório público para a comunidade revisar. O detalhe incômodo é óbvio: o modelo que fez isso continua fechado.

Se você constrói com LLMs, sabe o peso disso. A gente passou dois anos discutindo se modelo de linguagem sabia raciocinar ou só completava padrão com boa lábia. Agora temos um sistema interno gerando volume de produção matemática que um departamento inteiro levaria anos para produzir. E não dá para testar, não dá para chamar via API, não dá para medir latência ou custo real. Só dá para ler o resultado final.

O fato: 719 manuscritos, 372 famílias e um modelo invisível

No dia 6 de outubro de 2026, a OpenAI publicou um repositório com 719 manuscritos cobrindo 372 famílias de tópicos, que são agrupamentos de artigos relacionados. Junto vieram formalizações em Lean para muitos das provas, 10 resumos do raciocínio do modelo, estatísticas sobre problemas tentados e estimativas de computação expressas em uso equivalente ao ChatGPT Pro.

É o mesmo modelo não lançado que, cerca de um mês antes, produziu um resultado ligado a Navier-Stokes, um dos sete Problemas do Milênio do Clay Mathematics Institute. O líder de pesquisa Dan Roberts tratou as provas como um subproduto de testes internos para construir ferramentas melhores. A OpenAI disse que consultou o Advisory Group on Mathematics and Artificial Intelligence, do Institute for Advanced Study, sobre como compartilhar o trabalho, e criou protocolos para revisão e citação dos artigos.

Até aqui, parece ciência aberta. Mas o grupo consultivo publicou recomendações em 29 de setembro pedindo exatamente o contrário do que foi feito em um ponto central: divulgar nomes de modelos, prompts e custos de computação, evitar transformar resultado matemático em peça de marketing e parar de testar problemas avançados em modelos proprietários que a comunidade científica não pode acessar. Esse último ponto, pelo visto, não foi seguido.

Como funciona: o que dá para inferir sem acesso à API

Sem pesos, sem endpoint e sem log completo, o que resta é inferência de operador. E dá para inferir bastante. Para gerar 719 manuscritos com coerência formal, esse sistema provavelmente não é só um LLM gigante respondendo em zero-shot. O fluxo mais plausível envolve geração massiva de candidatos, filtragem por verificador formal em Lean, e loops de revisão com crítica interna antes de consolidar a prova final.

Na prática, isso significa arquitetura de agentes para matemática: um gerador propõe passos, um verificador tenta quebrar, outro módulo traduz para Lean e só o que passa na checagem formal vai para o repositório. Esse tipo de pipeline explica por que a OpenAI fala em custo medido em uso de ChatGPT Pro. Não é só o custo de um forward pass, é o custo de centenas ou milhares de tentativas por teorema, com re-tentativas, buscas em árvore e formalização. Barato por token, caro por prova.

Latência aqui importa menos que throughput de verificação. Em matemática formal, você pode paralelizar tentativas, mas a formalização em Lean é o gargalo. Ela exige precisão sintática total, e qualquer alucinação quebra a compilação. O fato de muitas provas já virem com formalização sugere que o modelo aprendeu a escrever Lean compilável de primeira ou quase, o que é um salto enorme em relação aos modelos públicos que ainda sofrem para fechar provas simples sem ajuda humana.

O que isso muda na prática

Para quem pesquisa, o repositório é útil de verdade. São 372 famílias de tópicos para minerar, testar contra seus próprios provadores e usar como dataset de treino para verificação. Para quem constrói produto com IA, o recado é outro: raciocínio verificável está virando diferencial, e quem dominar o loop entre linguagem natural e verificador formal vai cobrar mais caro por tarefa resolvida, não por token gerado.

• Se você trabalha com agentes: estude o padrão geração mais verificação formal. Troque avaliação por vibe por checagem executável, seja em código, em Lean ou em testes unitários.
• Se você pesquisa: baixe uma família de tópicos próxima da sua área e tente reproduzir uma prova com modelos abertos. Documente onde quebra, esse delta é o seu roadmap.
• Se você lidera time: reveja custo por tarefa resolvida. Estimativa em uso de ChatGPT Pro soa amigável, mas esconde milhares de tentativas. Faça conta de inferência total antes de prometer automação matemática para cliente.

Quem ganha agora são labs com computação sobrando e times que sabem operar Lean. Quem perde são grupos que dependem só de API pública para acompanhar a fronteira. Mistral com o Large 4, apelidado de Le Chonk, e a Reflection AI com o Beam tentam responder por fora, com pesos abertos e discurso de alternativa ocidental aos modelos chineses. São movimentos importantes, mas nenhum dos dois joga ainda no tabuleiro de provar teorema novo em escala. O jogo da matemática pesada continua fechado.

A tensão real: ciência aberta com modelo fechado não fecha

Aqui está o ponto que me incomoda. A diretoria do grupo consultivo disse que a publicação é o começo, não a conclusão, do processo de incorporação ao conhecimento matemático. Concordo. Só que como a comunidade valida, refuta ou estende um resultado se não pode interrogar o autor original, que nesse caso é um modelo? Revisar PDF é diferente de revisar processo. Sem prompts, sem sementes, sem histórico de tentativas falhas, a gente recebe o teorema limpo e perde o rastro de como ele foi encontrado.

E tem o custo. Falar em ChatGPT Pro como unidade de medida é esperto para comunicação, mas péssimo para operação. Quantos dólares de H100 por prova? Qual taxa de sucesso por família? Quantos problemas foram tentados e descartados? Sem esses números, ninguém consegue dizer se isso escala ou se foi uma queima de computação pontual para gerar manchete. Resolve ou só move o gargalo da intuição humana para a conta de inferência?

Conclusão

A OpenAI mostrou que um modelo interno já opera em outro nível de matemática formal, com volume e rigor que nenhum modelo público reproduz hoje. Só que sem acesso ao modelo, o avanço vira vitrine, não ferramenta. Vale acompanhar o repositório, testar os limites em Lean e medir o custo real por prova antes de assumir que a matemática foi automatizada. Será que estamos vendo o início de provadores confiáveis ou apenas o lab mais rico testando em segredo o que o resto só vai usar daqui a dois anos?