Em resumo
- A OpenAI publicou 722 manuscritos de matemática em 372 famílias de resultados no GitHub, provenientes de um modelo interno não lançado.
- Apenas 162 dos 722 artigos têm um resultado principal formalizado em Lean, e a OpenAI adverte que alguns resultados não formalizados podem ter problemas.
- Andrew Sutherland, do MIT, diz que a alegação de um único prompt e agente único não é verificada até que o modelo seja lançado, e o lançamento omite os prompts que um grupo consultivo do Institute for Advanced Study recomendou divulgar.
A OpenAI publicou 722 manuscritos de matemática no GitHub na terça-feira, todos produzidos por um modelo interno que a empresa não lançou. Um porta-voz da OpenAI disse que quase tudo veio de um único prompt entregue a um único agente de IA, embora alguns possam ter exigido várias tentativas.
É uma alegação ousada e um avanço potencialmente significativo no campo da matemática. Mas não são todos que são fãs, ou que compram o hype.
“Até e a menos que eles lancem o modelo e as pessoas possam replicar seus resultados, acho que você deve tratar quaisquer alegações sobre resolver problemas de uma só vez com um único agente como não verificadas”, Andrew Sutherland, um matemático do MIT, disse à Scientific American. “Deveríamos pedir recibos”, disse ele.
Os artigos estão agrupados em 372 “famílias” de resultados relacionados, e uma família pode agrupar um teorema principal com argumentos complementares, consequências ou provas alternativas. Isso faz com que 722 seja uma contagem de manuscritos, não de problemas resolvidos. A OpenAI diz que apresentou aproximadamente 4.000 problemas ao modelo e manteve os resultados que julgou suficientemente significativos para publicar.
O resultado médio usou o equivalente a aproximadamente três horas de computação de pensamento do ChatGPT Pro, segundo a OpenAI. A alegação sobre Navier-Stokes no mês passado pareceu muito diferente, com 10.000 agentes coordenadores trabalhando por 88 horas.
A OpenAI divulgou resumos de raciocínio abreviados para 10 dos resultados. Dito isso, apenas 162 dos 722 artigos vêm com um resultado principal verificado por computador, de acordo com um catálogo de formalização no repositório. Isso é cerca de 22% da coleção, traduzida para Lean, um software que verifica cada etapa lógica mecanicamente.
A própria OpenAI diz que nem todos os manuscritos têm formalizações em Lean e que “alguns dos resultados não formalizados podem ter problemas”. Em outras palavras, muito do que eles publicaram pode estar errado.
Uma verificação bem-sucedida no Lean confirma apenas que a prova segue a afirmação como escrita em Lean. Isso não mostra que a afirmação corresponde ao problema original, nem que o resultado é novo ou importante, que é a parte que os matemáticos agora têm que julgar.
E é aqui que os pesquisadores levantam as sobrancelhas.
Eu estava tentando ler a prova da OpenAI de que o número cromático de um plano é >= 6. Mas é uma matemática alienígena totalmente inacreditável?
De alguma forma, o modelo descobriu que qualquer K-coloração <=> K-coloração “fracamente mensurável”, o que parece vir do nada
1/2 pic.twitter.com/W13ScT3nel
— Dmitry Rybin (@DmitryRybin1) 7 de outubro de 2026
O repositório openai/math tem as Issues desativadas e nunca aceitou um pull request. Isso é decepcionante. Se você publica 722 manuscritos e pede formalizações em Lean, você precisa de algum lugar para as pessoas enviarem.
Estou formalizando a prova da Conjectura de Saxl da OpenAI em Lean 4 contra…
— Keith Adler (@keithadler) 7 de outubro de 2026
“Agora é o caso de que a IA pode produzir argumentos matemáticos em situações sem que o humano que a solicitou seja capaz de entender os argumentos, verificá-los ou assumir responsabilidade por eles”, disse o Instituto de Estudos Avançados de Princeton, Nova Jersey, em um comunicado. “Acreditamos que a compreensão humana da matemática continua sendo de suma importância. Como, nesta nova era, podemos trabalhar em direção a um novo paradigma que inclua a compreensão humana da matemática como parte da produção acadêmica responsável?”
Outros, no entanto, como o professor Abhishek Saha, estão bastante entusiasmados. “É um dia muito importante para a matemática”, escreveu ele, mas observou que a maioria dos problemas se encaixa nas categorias de “avanços excepcionais dentro de um programa existente” ou de “descobertas surpreendentes”.
Isso significa que a maioria dos problemas do conjunto é interessante, mas não impossível ou revolucionária como os problemas do milênio. Esse lugar é reservado para exatamente um problema dos 722: a Hipótese Quase-Riemann.
Alguns pensamentos adicionais sobre os 372 resultados divulgados pela OpenAI hoje, em 722 manuscritos.
Se eu fosse classificar os teoremas que os matemáticos provam e publicam de acordo com sua natureza revolucionária, eu os dividiria (muito aproximadamente) em quatro categorias:
A) Não revolucionário… https://t.co/BA10SxBlx7
— Abhishek Saha (@ObhishekSaha) 7 de outubro de 2026
O lançamento também fica aquém do que um grupo consultivo do Institute for Advanced Study recomendou em 29 de setembro: o nome do modelo, os prompts, uma cadeia de pensamento resumida, o tempo gasto e o custo computacional para cada resultado. A OpenAI publicou médias de computação e 10 resumos de raciocínio, mas nenhum prompt, e afirma que ainda está trabalhando para lançar o modelo de forma responsável.
Daniel Litt, um matemático da Universidade de Toronto, adotou a visão oposta, argumentando que não há razão para pedir à empresa que mantenha as respostas a essas questões matemáticas em segredo.
A Anthropic seguiu um caminho diferente com sua prova do Último Teorema de Fermat verificada pelo Lean no mês passado, publicando todas as 13 milhões de linhas publicamente no GitHub. Essa prova formalizou um teorema que Andrew Wiles publicou em 1995, em vez de reivindicar novos resultados.
A OpenAI diz que adicionará formalizações em Lean à medida que as obtiver; por enquanto, 162 dos 722 manuscritos têm uma.
