A OpenAI colocou no GitHub o repositório público ten-proofs, com certificações em Lean 4 para dez resultados em matemática e teoria da computação que a empresa associa ao seu trabalho recente com modelos de IA.
Adicione ao Google NotíciasNeste artigo
Na prática, o openai/ten-proofs é um pacote de provas formalizadas em Lean 4 para dez avanços listados pela OpenAI no texto "Ten advances in mathematics and theoretical computer science". Cada resultado aparece em um módulo separado, com um arquivo .lean correspondente, e pode ser checado de forma automática por terceiros, sem depender de confiar na OpenAI ou no modelo que gerou os argumentos informais.
O que é o repositório ten-proofs no GitHub?
O repositório ten-proofs é descrito pela OpenAI como um conjunto de formalizações em Lean 4.32.0 dos resultados do artigo "Ten advances in mathematics and theoretical computer science". O código usa mathlib e o gerenciador de projetos Lake, com manifestos (lakefile.toml, lake-manifest.json) e um arquivo lean-toolchain que fixa a versão da toolchain usada para verificar tudo.
O README lista dez problemas / resultados, cada um ligado a um arquivo Lean específico:
SpherePacking.lean: limites assintóticos melhores para empacotamento de esferas em alta dimensão, atingindo o limiar de Cohn–Elkies.
MetricCodes.lean: limites exponencialmente mais fortes para códigos binários em qualquer distância mínima, com análogos para códigos esféricos.
NonSoficGroup.lean: construção de um grupo não-sofic, respondendo à questão sobre aproximações por permutações finitas.
ConnesRigidity.lean: contraexemplo à conjectura de rigidez de Connes em álgebras de von Neumann de grupos.
Permanent.lean: novas cotas inferiores para o permanente em circuitos/formulas aritméticas, incluindo um limite de
n^4 / log npara fórmulas.QuantumParallelRepetition.lean: repetição paralela exponencial para jogos quânticos finitos de dois jogadores.
GapCVP.lean: dureza de aproximação, por fator polinomial, para o problema do vetor mais próximo (Closest Vector Problem).
EhrhartVolumeInequality.lean: versão afiada da conjectura de volume de Ehrhart, sobre corpos convexos com único ponto de rede interior.
MulticolorTriangleRamsey.lean: limite inferior superexponencial para números de Ramsey de triângulos multicoloridos, resolvendo o problema 183 de Erdős.
CompactnessAndDegeneracy.lean: contraexemplos às conjecturas de compacidade e degenerescência em teoria extremal de grafos, ligados aos problemas 146 e 180 de Erdős.
Cada um desses arquivos funciona como um certificado verificável de que a prova formal segue das axiomatizações adotadas por Lean/mathlib. O público-alvo não é o estudante de cálculo que abre o repositório por curiosidade, e sim quem trabalha com verificação formal, criptografia, teoria da complexidade e áreas que dependem desse tipo de checagem mecânica.
Como usar as provas Lean publicadas pela OpenAI?
O README descreve um fluxo de uso direto: com elan instalado na máquina, basta baixar o cache do mathlib e compilar tudo com dois comandos. A OpenAI indica:
lake exe cache get
lake build All
Quem quiser inspecionar apenas um dos resultados compila módulos individuais, por exemplo:
lake build SpherePacking
O repositório inclui ainda um arquivo All.lean, que agrega as dez formalizações, e referências a um projeto separado, ComparatorChallenges, com instruções para checagem independente via Comparator. A OpenAI explicita que espera que outras pessoas rodem os checadores por conta própria, sem depender do ambiente interno da empresa.
Um detalhe que salta aos olhos é o tamanho de alguns arquivos. Permanent.lean, por exemplo, tem mais de 27 mil linhas, com cerca de 1,08 MB, o que dá uma ideia do nível de granularidade que a linguagem de provas exige para chegar na cota inferior de n^4 / log n para o permanente. Essa escala afasta a hipótese de um pull request casual de fim de semana, mas vira um benchmark concreto para quem está construindo agentes que escrevem provas em Lean e precisa medir esforço computacional e humano.
Qual é o contexto de IA por trás do ten-proofs?
O repositório não menciona nenhum modelo específico, mas um texto do serviço AI Weekly atribui esses resultados a uma versão interna de um modelo chamado Astra. Segundo o AI Weekly, a OpenAI publicou dez provas de problemas previamente abertos em matemática e teoria da computação, todas acompanhadas de formalização em Lean e de um walkthrough do raciocínio do modelo.
O AI Weekly relata ainda que a OpenAI estima em cerca de US$ 2 mil o custo dos tokens usados para gerar as dez soluções, tomando como base a tabela de preços da API Sol. A publicação ressalta que as provas Lean reduzem o risco clássico de anúncio de prova via IA — a corrente de texto plausível que esconde um salto ilegítimo — mas lembra que checagem em Lean não substitui revisão por pares: a comunidade ainda precisa validar se o enunciado formalizado coincide com o problema de interesse, sem mudanças sutis.
O trecho final do relato aponta o ponto mais incômodo: se a maior parte desses resultados sobreviver ao escrutínio, o custo de atacar um problema em aberto de uma década passa a se comportar mais como uma fatura de nuvem do que como anos de pós-doc. O ten-proofs coloca esse debate em código aberto, com os nomes de arquivos, linhas de código e custos expostos para matemáticos, teóricos de computação e grupos que tentarem reproduzir a façanha fora da OpenAI.
