A OpenAI (abre em nova aba) publicou uma extensa coleção de trabalhos dedicados a problemas em aberto na matemática e na ciência da computação teórica, gerados inteiramente por um modelo de fronteira interno ainda não disponibilizado comercialmente. O material, distribuído em repositórios abertos sob a licença Apache-2.0, traz centenas de textos técnicos acompanhados de código de verificação formal em Lean, uma linguagem funcional e provador interativo de teoremas que permite a validação determinística de demonstrações por compilador.
O volume de material divulgado chama a atenção de imediato. No repositório openai/math (abre em nova aba), a empresa reuniu 722 manuscritos agrupados em 372 famílias temáticas, cobrindo 17 disciplinas matemáticas distintas. Uma família reúne o resultado principal, derivações auxiliares, eventuais provas alternativas e consequências teóricas de uma mesma frente de ataque. Ao submeter cerca de 4.000 problemas ao sistema, a equipe computou que cada resultado aceito exigiu, em média, o equivalente a três horas de processamento contínuo de inferência no padrão de raciocínio do ChatGPT Pro.
A escala dessa produção é surpreendente se comparada ao ritmo histórico da pesquisa matemática humana, embora exija uma leitura sóbria sobre o que foi de fato comprovado.
A barreira entre o texto matemático e a verificação formal
Trabalhos teóricos redigidos em prosa técnica, mesmo quando diagramados em LaTeX com notação rigorosa, são notavelmente vulneráveis a lacunas lógicas invisíveis à primeira vista. Redes neurais aplicadas à matemática tradicionalmente sofrem desse mal: produzem argumentos estruturalmente convincentes, repletos de vocabulário correto, mas que contêm saltos inferenciais falsos.
Para contornar essa fragilidade epistemológica, o foco técnico da divulgação reside na formalização em Lean. O Lean opera tratando proposições como tipos e provas como programas (pelo isomorfismo de Curry-Howard, princípio lógico no qual uma prova matemática é computacionalmente análoga a um programa que satisfaz uma especificação de tipos). Se o código compila sem erros no verificador do Lean, a prova é matematicamente válida dentro dos axiomas estabelecidos, eliminando qualquer incerteza sobre alucinação semântica do modelo de linguagem.
O catálogo do repositório revela que, dos 722 artigos publicados, 162 contam com a formalização completa do seu resultado principal em Lean. Uma fração relevante foi formalmente checada pela máquina, enquanto a maior parte dos manuscritos permanece, até o momento, como literatura matemática escrita em linguagem natural que aguarda escrutínio humano e codificação formal complementar.
A formalização total não é trivial. Para os matemáticos, traduzir uma ideia conceitual de dez páginas para o Lean pode exigir meses de trabalho braçal de decomposição em lemas atômicos. O fato de o sistema ter gerado tanto os artigos quanto os arquivos .lean correspondentes indica que o modelo operou em duas frentes: a elaboração conceitual do argumento e a transcrição sintática estrita das etapas lógicas.
Resultados alcançados e problemas de referência
Dentre os resultados cobertos com certificados em Lean 4, disponíveis de forma consolidada no repositório openai/ten-proofs (abre em nova aba), figuram tópicos complexos da análise harmônica, combinatória, teoria dos operadores e física matemática.
Entre as provas destacam-se:
- Empacotamento de esferas em altas dimensões (
SpherePacking.lean): obtenção de limites superiores assintóticos aprimorados para a densidade de empacotamento, alcançando o limiar de Cohn-Elkies. - Códigos métricos binários e esféricos (
MetricCodes.lean): limites superiores exponencialmente mais estritos para códigos binários em qualquer distância mínima arbitrária. - Construção de grupos não-sóficos (
NonSoficGroup.lean): resolução estrutural sobre a capacidade de todo grupo admitir aproximações de permutações finitas. - Rigidez de Connes (
ConnesRigidity.lean): apresentação de um contraexemplo para a conjectura de que certos grupos discretos seriam univocamente determinados por suas álgebras de von Neumann associadas. - Limites inferiores em circuitos aritméticos (
Permanent.lean): novas fronteiras inferiores de complexidade para o cálculo do permanente matricial, incluindo um limite de fórmula da ordem de n elevado a quatro dividido pelo logaritmo de n. - Repetição quântica paralela (
QuantumParallelRepetition.lean): repetição paralela exponencial para jogos quânticos de dois participantes arbitrários e finitos.
Adicionalmente, os registros cobrem investigações sobre o expoente de irracionalidade de pi, formulações da conjectura de Mahler simétrica, a fórmula de Mézard-Parisi para vidros de spin diluídos e contraexemplos para a conjectura de divisores de zero de Kaplansky.
Para facilitar a auditoria humana, a organização incluiu dez resumos analíticos detalhando o fluxo de raciocínio empregado pelo modelo na dedução dos teoremas mais densos. O objetivo declarado desses sumários é permitir que pesquisadores reconstruam o mapa de dependências adotado pelo sistema durante a busca da prova.
A assimetria do custo de inferência
Analisar apenas o sucesso dos 162 teoremas verificados daria uma impressão distorcida do estado da arte. A métrica operacional exposta pela OpenAI é reveladora: foram cerca de 4.000 problemas matemáticos propostos para que 372 famílias de resultados fossem sintetizadas, exigindo em média três horas de computação intensiva de pensamento para cada resultado publicado.
Seria ingênuo supor que o modelo resolveu problemas abertos de forma linear e contínua. Houve milhares de execuções descartadas, becos sem saída conceituais e ramos de dedução abandonados. Essa dinâmica expõe uma antítese conhecida na ciência da computação: encontrar uma prova matemática pode ser exponencialmente árduo, enquanto verificar um certificado sintático fornecido pelo Lean consome frações de segundo no processador.
Essa assimetria entre busca e verificação sustenta o modelo metodológico atual. Ao alocar grandes volumes de computação no momento da inferência (test-time compute, fase em que o modelo explora múltiplos caminhos de resolução antes de responder), o agente de inteligência artificial atua explorando grafos de possibilidades combinatórias até encontrar uma cadeia que satisfaça as regras do compilador Lean.
Com o objetivo de normatizar como esses achados devem circular no meio acadêmico, a empresa estabeleceu diretrizes explícitas para citações, correções de eventuais falhas nos preprints e submissões a periódicos tradicionais. Para balizar esse processo, a organização buscou aconselhamento externo especializado.
Estamos publicando uma ampla gama de novos resultados matemáticos produzidos por um modelo de fronteira interno. Temos consultado o Grupo Consultivo independente sobre Matemática e Inteligência Artificial no Instituto de Estudos Avançados, e nos baseamos em seus conselhos e recomendações públicas para informar como publicamos esses resultados.
Implicações metodológicas para a computação técnica
A transição da matemática recreativa ou de competição escolar para problemas de fronteira em aberto altera a relação dos desenvolvedores com ferramentas formais. O Lean deixa de ser uma curiosidade acadêmica restrita a especialistas em lógica pura para atuar como ambiente de execução (runtime) e barreira de segurança contra alucinações de inteligência artificial.
A dependência de verificação algorítmica expõe uma lição que ultrapassa a matemática pura: a confiança em sistemas cognitivos de inferência complexa depende fundamentalmente de compiladores determinísticos. Enquanto a literatura dos preprints permanecer aberta para escrutínio humano, o subconjunto de 162 repositórios Lean serve como uma fundação cujas propriedades já foram auditadas pelo próprio kernel de prova.
O repositório continuará recebendo commits contendo novas formalizações para os manuscritos restantes conforme forem compiladas. O avanço representa um passo técnico relevante, ainda que circunscrito à proporção observada entre os milhares de nós explorados e as poucas centenas de caminhos lógicos validados pelas regras da máquina.