OpenAI divulga 722 manuscritos matemáticos criados por IA ainda não lançada

RESUMO ＋

A OpenAI publicou 722 manuscritos matemáticos produzidos por um modelo interno ainda não lançado. Os trabalhos estão organizados em 372 grupos de resultados relacionados e apresentam diferentes estágios de verificação. Parte das demonstrações foi formalizada em Lean, ferramenta que permite conferir provas por computador. A divulgação inclui informações sobre o processo de produção e segue consultas a um grupo independente de matemáticos.

Um modelo de inteligência artificial (IA) ainda não disponível ao público produziu a coleção de 722 manuscritos matemáticos que a OpenAI divulgou nesta terça-feira, 6. Os trabalhos foram publicados no GitHub, acompanhados de materiais para examinar suas demonstrações.

Segundo a empresa, a avaliação envolveu aproximadamente quatro mil problemas. O catálogo reúne 372 grupos de trabalhos relacionados, que podem incluir um resultado principal, consequências ou demonstrações alternativas.

Isso significa que os 722 manuscritos não correspondem necessariamente a 722 problemas distintos resolvidos. A OpenAI informa que os resultados estão em diferentes estágios de verificação e que alguns dos trabalhos ainda não formalizados podem apresentar problemas.

Como conferir uma prova produzida por IA

Parte das demonstrações foi formalizada em Lean, uma linguagem de programação e um assistente de provas que permite verificar argumentos matemáticos por computador.

Nesse processo, a demonstração é expressa em uma linguagem formal, com definições e etapas que o sistema consegue conferir. O objetivo é verificar se a conclusão decorre das premissas e das regras utilizadas.

A OpenAI afirma que acrescentará novas formalizações ao repositório conforme estiverem disponíveis. Também manterá versões anteriores acessíveis e registrará correções e revisões.

A verificação é uma das questões centrais no avanço da IA na matemática. Conferir a validade de uma demonstração e compreender as ideias que a tornam possível são etapas distintas do trabalho científico.

O que a empresa revelou sobre o processo

A divulgação inclui dez resumos do raciocínio do modelo e estimativas do esforço computacional. Segundo a OpenAI, cada resultado consumiu, em média, computação equivalente a aproximadamente três horas de raciocínio do ChatGPT Pro.

A comparação descreve uma equivalência de recursos computacionais. Não significa que usuários do serviço público consigam reproduzir os resultados no mesmo prazo.

https://t.co/edRBkXdUAN

— OpenAI (@OpenAI) October 6, 2026

A empresa afirma que trabalha para disponibilizar o modelo e que financiará workshops, conferências e programas dedicados à compreensão dos resultados.

Publicar não encerra o trabalho dos matemáticos

A OpenAI diz ter consultado o Grupo Consultivo de Matemática e Inteligência Artificial, independente e sediado no Institute for Advanced Study, para orientar a divulgação.

Em recomendações publicadas em 29 de setembro, o grupo defende que laboratórios divulguem resultados relevantes com documentação, referências, informações sobre o processo e provas formalizadas sempre que possível.

O documento também pede financiamento para que pesquisadores compreendam e incorporem os resultados, com iniciativas conduzidas pela comunidade matemática.

A consulta não equivale a um aval às demonstrações. O grupo declara que não endossa a prática de testar problemas matemáticos avançados em modelos proprietários inacessíveis à comunidade científica e pede aos laboratórios que interrompam essa prática.

Para os integrantes, a produção de argumentos por máquinas não elimina a necessidade de compreensão humana, verificação coletiva e responsabilidade pelo conteúdo publicado.

---

Perguntas frequentes

O que a OpenAI publicou?

Uma coleção de 722 manuscritos matemáticos, organizada em 372 grupos de resultados relacionados, com materiais de apoio às demonstrações.

Todos os resultados estão verificados?

Não. A empresa informa que os trabalhos estão em diferentes estágios de verificação e que alguns dos resultados ainda não formalizados podem apresentar problemas.

O que é Lean?

É uma linguagem de programação e um assistente de provas que permite escrever e verificar demonstrações matemáticas formalmente por computador.

O modelo já está disponível?

Não. A OpenAI descreve o sistema como um modelo interno ainda não lançado e afirma que trabalha para disponibilizá-lo.