Um modelo experimental de inteligência artificial produziu centenas de manuscritos de pesquisa em matemática, agora acessíveis a especialistas de todo o mundo.
Em 6 de outubro de 2026, a OpenAI tornou público um catálogo de trabalhos obtidos com um modelo interno ainda experimental. O repositório, hospedado no GitHub, reúne 719 manuscritos distribuídos em 372 famílias de resultados. Uma família pode reunir várias demonstrações, métodos alternativos ou consequências de uma mesma descoberta proposta.
Um quadro transparente coberto de símbolos e equações matemáticas. Os trabalhos matemáticos propostos por uma IA precisam ser verificados antes de poderem ser considerados demonstrados.
Foto: Preply.com Images, licença Creative Commons Attribution, via Wikimedia Commons.
Imagem Wikimedia
Esses documentos abrangem ramos muito diferentes da matemática: teoria dos números, geometria, álgebra e também física matemática. Portanto, não se parecem com uma série de exercícios escolares resolvidos automaticamente. Alguns abordam problemas de pesquisa estudados há muitos anos.
Como foi produzida uma quantidade tão grande de textos? A OpenAI explica que submeteu cerca de 4.000 problemas ao modelo durante sua avaliação. Em média, cada resultado selecionado teria exigido o equivalente a aproximadamente três horas de cálculo intensivo no ChatGPT Pro. Os pesquisadores então organizaram os trabalhos e sua documentação para torná-los consultáveis.
Mas um manuscrito não é uma descoberta confirmada. Uma demonstração pode conter um erro discreto, usar uma hipótese forte demais ou estabelecer um resultado já conhecido. Portanto, especialistas precisam verificar tanto o raciocínio quanto o interesse científico e a novidade de cada proposta.
O repositório já apresenta um exemplo concreto disso. Em 7 de outubro, a OpenAI removeu três manuscritos após a identificação de um erro de sinal em uma demonstração. Outros quatorze textos foram revisados para corrigir argumentos, esclarecer condições ou reparar provas. O catálogo é, assim, apresentado como um conjunto de trabalhos em evolução.
Para facilitar as verificações, algumas demonstrações foram transcritas em Lean, uma linguagem que permite a um computador verificar as etapas de uma prova formal. Atualmente, cerca de 42% dos principais resultados dispõem de uma formalização. Isso ajuda a verificar sua coerência lógica, mas não basta para estabelecer sua novidade nem a importância das questões resolvidas.
O grande desafio é saber se as IAs podem agora contribuir para avanços matemáticos reais e, em seguida, produzir argumentos suficientemente precisos para serem examinados por pesquisadores. A publicação aberta permite justamente confrontar essas propostas com a comunidade científica.
A OpenAI planeja acrescentar outras provas formais e organizar encontros dedicados à avaliação desses trabalhos. O repositório também mantém o histórico das correções e remoções. As próximas verificações independentes determinarão quais propostas resistem ao exame e quais ainda precisarão ser modificadas.