A OpenAI publicou um preprint em que alega resolver uma questão aberta da teoria dos conjuntos há mais de um século: o Princípio da Partição não implica o Axioma da Escolha. O texto, datado de 24 de setembro de 2026 e assinado pela própria empresa, está disponível no repositório openai/math no GitHub (abre em nova aba), cujo commit inicial é de 6 de outubro e cuja atualização mais recente, em 8 de outubro, acrescentou manuscritos e formalizações. Não há revisão por pares, e a reação pública de um especialista da área foi de franca decepção com a qualidade da apresentação. Entre o anúncio e uma demonstração aceita pela comunidade matemática, há hoje uma distância considerável.
O problema, em termos simples
A teoria dos conjuntos estuda coleções de objetos e serve de alicerce para o resto da matemática. Esse alicerce é descrito por axiomas, regras básicas aceitas como ponto de partida. O sistema mais usado é o ZF, batizado pelos matemáticos Ernst Zermelo e Abraham Fraenkel.
Dois conceitos bastam para entender a disputa. Uma função de um conjunto X para um conjunto Y é sobrejetiva quando todo elemento de Y é atingido por ela, nenhum fica de fora. Ela é injetiva quando elementos diferentes recebem resultados diferentes, sem sobreposição. O Princípio da Partição afirma o seguinte: se existe uma sobrejeção de X sobre Y, então existe uma injeção de Y em X. Em português direto, se X consegue "cobrir" todo Y, então Y não é maior do que X. É uma forma de comparar tamanhos de conjuntos, inclusive infinitos.
O Axioma da Escolha, por sua vez, diz que, dada qualquer família de conjuntos não vazios, é possível escolher um elemento de cada conjunto, mesmo sem nenhuma regra explícita de escolha. Ele é famoso entre matemáticos por gerar consequências surpreendentes, e sua aceitação não é automática: pesquisadores estudam o que acontece com e sem ele.
A ligação entre os dois é antiga. Com o Axioma da Escolha, o Princípio da Partição sai de graça: basta escolher, para cada elemento de Y, um dos elementos de X que a sobrejeção mapeia para ele. O preprint da OpenAI atribui a origem do princípio ao matemático italiano Beppo Levi, em 1902. Desde então, a pergunta ficou no ar: será que a recíproca também vale? Se o princípio fosse verdadeiro, o axioma viria junto?
O que a OpenAI alega ter provado
O teorema principal do preprint é uma afirmação de consistência relativa: se o ZF é consistente, ou seja, não leva a contradições, então também é consistente o sistema que junta o ZF, o Princípio da Partição, uma versão restrita do Axioma da Escolha (válida apenas para famílias indexadas por ordinais, que são números generalizados capazes de medir infinitos) e a negação do axioma completo. Em outras palavras, existe um mundo matemático coerente em que o princípio vale e o axioma falha.
Há um segundo resultado, mais forte em aparência: a partir de um modelo que satisfaz o ZF mais o Axioma da Escolha, os autores constroem uma extensão com propriedades adicionais de preservação, que mantém as mesmas sequências contáveis do modelo original. O preprint, cujo PDF está no diretório do repositório (abre em nova aba), registra um contexto curioso: uma versão de agosto de 2026 do levantamento de Arnold Miller ainda listava a questão como aberta, e correções publicadas em setembro de 2026 por um pesquisador retiraram as alegações de construção de modelo de três tentativas anteriores. Ou seja, pouco antes do anúncio da OpenAI, outras abordagens tinham acabado de fracassar.
Como o resultado foi produzido
O catálogo da OpenAI descreve o método com números incomuns para uma publicação matemática. Foram propostos cerca de 4.000 problemas a um modelo interno da empresa, não liberado ao público. Cada resultado consumiu, em média, três horas de computação de raciocínio do ChatGPT Pro com esse modelo. O acervo reúne 719 manuscritos, organizados em 372 famílias de resultados, e cerca de 42% dos resultados principais já foram formalizados em Lean.
O Lean merece explicação: é um verificador de provas, um programa que confere cada passo de uma demonstração mecanicamente. Se uma prova está formalizada em Lean e o programa a aceita, erros de raciocínio estariam, em princípio, descartados. A formalização, porém, nem sempre cobre tudo o que o texto em linguagem humana promete, e é aí que a história fica mais nuançada.
O que está verificado e o que não está
A entrada 244 do catálogo confirma que o resultado sobre o Princípio da Partição possui documentação de formalização em Lean. O escopo descrito é preciso: o que está checado é a implicação de consistência relativa, a construção de um modelo do Princípio da Partição sem Axioma da Escolha a partir de um modelo de base que contém um cardinal fortemente inacessível, um pressuposto de existência de um conjunto muito grande que não decorre dos axiomas usuais. Já as afirmações mais fortes do preprint, sobre preservação de sequências no modelo transitivo, ficam fora da construção selecionada.
| Afirmação do preprint | Status declarado no repositório |
|---|---|
| Se ZF é consistente, então ZF + Princípio da Partição + escolha para famílias indexadas por ordinais + negação do Axioma da Escolha também é | Formalizada em Lean |
| Construção transitiva com preservação de sequências contáveis do modelo original | Fora do escopo da formalização |
| Revisão por pares ou checagem independente por matemáticos externos | Não há registro |
O próprio repositório admite limitações, em um aviso que soa honesto para quem percorre os arquivos: alguns resultados ainda sem formalização podem ter problemas. E a página do preprint não menciona periódico, aceite editorial ou verificação independente. A distinção importa porque a imprensa internacional já tratou o pacote como um conjunto de "soluções", enquanto o comunicado da OpenAI, segundo a leitura de um especialista, sugere apenas "progresso".
O uísque que não foi enviado
Asaf Karagila é um teórico dos conjuntos que mantém uma lista pública de problemas favoritos e havia prometido, nessa lista, uma garrafa de uísque para quem resolvesse a questão. Ele conta, em seu blog pessoal (abre em nova aba), que três pessoas o procuraram antes mesmo de ele sair da cama no dia do anúncio, em 8 de outubro, perguntando se a promessa seria cumprida com Sam Altman, presidente da OpenAI. A resposta foi não.
O uísque continua guardado. Karagila fez uma leitura breve do preprint, sem examinar o código em Lean, que ele diz não dominar na prática e que considera enorme. O veredito sobre o texto foi duro: confuso, embolado, de estrutura estranha, com terminologia destoante e lemas que ele não esperaria encontrar ali, enunciados de forma esquisita. Ele cita ainda o uso de três conjuntos de notas de aula não publicadas e sem revisão, uma delas dele próprio, entre as referências. Segundo Karagila, se o texto fosse submetido a um periódico científico, mereceria rejeição imediata, sem entrar em revisão. E encerra dizendo que não pretende gastar tempo tentando dar sentido ao artigo.
Duas observações deixam a crítica em perspectiva. Primeiro, ela é sobre a forma e a apresentação, não uma refutação matemática: Karagila não apontou um erro específico na demonstração, e disse explicitamente que não a analisou a fundo. Segundo, a existência de uma formalização parcial em Lean significa que o núcleo do resultado pode estar correto mesmo que o texto em prosa seja ruim. São camadas diferentes de confiança, e nenhuma delas foi ainda atestada por um matemático externo à OpenAI.
Onde a alegação está hoje
O quadro factual, na data desta reportagem, é o seguinte: um modelo interno não liberado produziu uma demonstração que a empresa considera válida; parte dela foi checada mecanicamente por um verificador de provas, com pressupostos e recortes documentados; o restante depende da leitura de seres humanos, e o primeiro especialista de renome que olhou o texto o rejeitou pela qualidade, não pelo conteúdo. Nada disso equivale a uma refutação, e nada equivale a um consenso.
Para quem não trabalha com lógica matemática, o impacto prático é, no momento, nenhum: o resultado interessa aos fundamentos da matemática, e o modelo que o produziu não está disponível para uso. O que qualquer pessoa pode fazer é ler o material, já que o repositório é público e gratuito. Se a demonstração sobreviver ao escrutínio da comunidade, uma pergunta com 124 anos se encerra. Até lá, trata-se de uma alegação forte, com checagem parcial e um uísque por pagar.
Perguntas frequentes
O problema do princípio da partição já foi resolvido?
Não há resolução confirmada até 9 de outubro de 2026. A OpenAI publicou um preprint alegando que o princípio não implica o Axioma da Escolha, com parte do resultado formalizada no verificador Lean, mas o texto não passou por revisão por pares e não houve verificação independente anunciada por matemáticos externos.
O que afirma o princípio da partição?
O princípio diz que, se existe uma função sobrejetiva de um conjunto X sobre um conjunto Y, ou seja, que atinge todos os elementos de Y, então existe uma função injetiva de Y em X, que atribui elementos distintos de X a elementos distintos de Y. É uma forma de comparar tamanhos de conjuntos infinitos.
Como a OpenAI produziu o resultado?
Segundo o catálogo da empresa, um modelo interno não liberado ao público resolveu cerca de 4.000 problemas, com média de três horas de computação de raciocínio do ChatGPT Pro por resultado. O acervo tem 719 manuscritos, e cerca de 42% dos resultados principais foram formalizados em Lean.
Isso muda algo para quem não é matemático?
Não diretamente. A alegação é relevante para a pesquisa em fundamentos da matemática, não para aplicações cotidianas, e o modelo usado não está disponível ao público. O repositório com os manuscritos e as formalizações, porém, é público e pode ser consultado gratuitamente no GitHub.