Edição Markdown

AI-translated from English; not yet reviewed by a fluent editor.

# Repositório matemático da OpenAI: manuscritos, versões e provas em Lean

> A coleção da OpenAI contém 722 manuscritos em 372 famílias. Um olhar atento sobre uma configuração de prova em Lean mostra como verificar versões, âmbito e requisitos de validação.

By BIG CHANGE Editorial

Published: 2026-10-07T04:13:00.689Z
Updated: 2026-10-07T04:13:00.689Z
Canonical: https://bigchange.ai/blog/openai-math-repository-manuscripts-formal-proofs

![Charcoal concept illustration of one reader holding loose manuscript folios, seen from behind, beside a second stack with an orange tab.](https://bigchange.ai/api/media/file/openai-math-manuscript-reading-hero-v1.png)
AI-generated conceptual illustration by BIG CHANGE.

O lançamento matemático da OpenAI, a 6 de outubro, disponibiliza ao público uma coleção de 722 manuscritos organizados em 372 famílias de resultados. Uma família pode incluir vários artigos, enquanto uma prova formal pode abranger uma afirmação mais restrita do que o manuscrito associado. Seguir um artigo no repositório até à sua configuração de prova revela que afirmação foi escolhida para validação.

A BIG CHANGE analisou a 7 de outubro o inventário completo de ficheiros do repositório, o catálogo e alguns artefactos de prova. Trata-se de uma análise documental e estática dos artefactos; não compilámos a biblioteca Lean, não executámos um verificador de provas nem avaliámos a matemática. [Anúncio da OpenAI](https://openai.com/index/sharing-ai-progress-in-mathematics/) Descreve um lançamento em evolução e afirma que se seguirão mais formalizações.

## A grande mudança

- **O que mudou:**Os investigadores podem agora acompanhar centenas de manuscritos produzidos por IA através de um catálogo público comum até aos ficheiros de apoio e, para alguns resultados, às afirmações formais e implementações de prova propostas.
- **Porque é importante:**Um matemático que pondere utilizar um resultado pode analisar a afirmação efetivamente selecionada para validação, os seus pressupostos e a relação com o artigo. A organização do repositório ajuda a identificar onde termina um resultado formal mais restrito e começa uma análise matemática adicional.
- **O que acompanhar:**A OpenAI planeia acrescentar formalizações e preservar as revisões. Estas atualizações interessam a quem cita ou utiliza este trabalho: a análise deve identificar a versão e o teorema examinados.

## Conte os manuscritos e as famílias separadamente

O nosso inventário encontrou 722 diretórios de manuscritos diretamente em `preprints/`; cada um contém um PDF, e havia 10 PDFs em `reasoning_traces/`. O [mapa de manuscritos](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/CONTENTS.md) contém 372 entradas de famílias distintas e 722 ligações para manuscritos.

Estes números descrevem objetos diferentes:

| Artefacto | O que o leitor pode analisar |
| --- | --- |
| Família de resultados | Conjunto de artigos relacionados, incluindo argumentos complementares, corolários ou provas alternativas. |
| Manuscrito | Documento matemático individual, com os seus próprios ficheiros de origem e informação de citação. |
| Resumo do raciocínio | Relato abreviado do raciocínio do modelo para um resultado selecionado. |
| Artefacto Lean | Definições, afirmações e provas propostas em formato formal, com ligações e configurações que identificam o que deve ser verificado. |

O [README do repositório](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md) explica estas categorias e alerta para a desigualdade dos níveis de verificação. Alguns resultados não têm formalizações em Lean, e a OpenAI afirma que o trabalho não formalizado pode conter problemas. O próprio [catálogo de formalizações](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/formalization.yaml) regista o âmbito como "Partial progress" e o estado da revisão como `unchecked`. Estes campos são metadados de publicação, não o resultado de uma execução de verificação pela BIG CHANGE.

Os ficheiros públicos podem ser lidos sem uma conta OpenAI. O anúncio descreve o modelo que os gerou como interno e afirma que a OpenAI está a trabalhar para o disponibilizar. O acesso a estes documentos não demonstra, portanto, acesso a esse modelo.

## Fixe a versão antes de seguir uma prova

O snapshot do repositório utilizado aqui corresponde ao commit [`adc7f1241b42e322a6451854ab7e4b4c146bf78a`](https://github.com/openai/math/commit/adc7f1241b42e322a6451854ab7e4b4c146bf78a) , datado de 6 de outubro de 2026, às 21:58:50 UTC. As ligações que incluem esse identificador preservam o snapshot analisado; as que incluem `main` seguem o ramo predefinido, que está sempre a mudar. O README da OpenAI promete manter versões anteriores quando surgirem correções ou revisões.

Comece pela [visão geral](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/overview.pdf), que agrupa as famílias por área matemática, e depois use o mapa de manuscritos para chegar a um artigo específico. Guarde o nome do diretório, o commit do repositório e a citação fornecida pelo artigo. A data do manuscrito pode diferir da data de lançamento da coleção pública.

A família 003 contém um artigo que reivindica uma região sem zeros à direita de 7/8, uma prova alternativa para uma região à direita de 11/12 e um artigo separado sobre zeros de Landau–Siegel. O [diretório do primeiro artigo](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/README.md) tem a data de 30 de setembro e fornece uma citação BibTeX. Identificar o artigo específico preserva a distinção entre estas afirmações.

A [página de âmbito do Lean](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/003.md) descreve as afirmações abrangidas pela formalização, identifica exclusões e indica que aplicações posteriores no artigo foram omitidas. Liga a afirmações de verificação distintas para o resultado da função zeta, funções L de Dirichlet e Hecke e uma lacuna uniforme de zeros reais. A verificação de uma afirmação selecionada não representa automaticamente todos os elementos dessa página.

## Siga a afirmação selecionada até à configuração

As [instruções do Comparator](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/README.md) da OpenAI usam a família 003 como exemplo. O Comparator é uma ferramenta que compara uma prova Lean proposta com um desafio especificado. A [configuração JSON](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.json) do exemplo seleciona um teorema: a ausência de zeros da função zeta de Riemann quando a parte real do argumento excede 7/8.

A configuração aponta para um módulo de desafio e outro de solução. Permite os axiomas padrão `propext` , `Quot.sound` e `Classical.choice` , e define `enable_nanoda` como `false` . O Nanoda é um verificador independente que o Comparator pode utilizar; a configuração fornecida não o ativa.

O [ficheiro de desafio](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.lean) contém `sorry` , o marcador do Lean para uma prova inacabada. Aqui tem uma função específica: fornecer a afirmação a comparar. A documentação do Comparator permite um marcador no desafio e exige uma prova adequada na solução. Encontrar `sorry` apenas neste desafio não diz se a solução separada passa. [Documentação do Comparator](https://github.com/leanprover/comparator#readme).

Para uma verificação local documentada, os dados de entrada são essa configuração, os módulos de desafio e solução e as respetivas dependências. O repositório fixa [Lean 4.34.1](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lean-toolchain). O [manifesto Lake](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lake-manifest.json) regista as revisões das dependências, incluindo a do Mathlib: `d13f23b723b8a846827a245b89c10fc7d3f11612`.

A OpenAI exige que `comparator` , `landrun` e `lean4export` estejam no caminho de pesquisa dos executáveis e documenta depois estes comandos a partir do diretório `lean/` :

```sh
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json
```

Estas são instruções do publicador, não comandos que executámos. Não fixam as versões das três ferramentas externas. A documentação atual do Comparator exige uma versão compatível de `lean4export` e descreve os requisitos da sandbox e as condições em que o sucesso demonstra correspondência com o desafio, uso dos axiomas permitidos e aceitação pelo kernel. Um relatório reproduzível deve registar as versões instaladas e a saída real, além do commit do repositório.

O [README da biblioteca Lean](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/README.md) recomenda compilar pequenas partes desta grande biblioteca. Também documenta limites de mapeamento de memória no Linux que podem impedir uma compilação completa. Não medimos o tempo de execução local nem o custo de hardware deste exemplo.

## Leia uma verificação bem-sucedida dentro do âmbito declarado

A [referência de validação do Lean](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/), consultada na versão 4.35.0-rc3, distingue a aceitação de uma prova formal da interpretação do significado do teorema. Essa versão da documentação é diferente da cadeia de ferramentas fixada neste repositório.

Uma verificação básica bem-sucedida significa que o kernel aceitou a afirmação formal segundo as suas definições, imports e axiomas. As dependências ainda podem conter provas inacabadas. O Lean documenta `#print axioms` para mostrar os axiomas utilizados, incluindo `sorryAx` para uma prova inacabada na cadeia de dependências.

Verificações mais fortes repetem provas guardadas ou comparam uma solução com uma afirmação definida separadamente. Continuam dependentes do ambiente de verificação e da expressão correta do significado pretendido. Por isso, o relatório deve registar o desafio exato, os axiomas permitidos e as definições do verificador externo. Nem a aceitação pelo kernel nem a correspondência com um desafio demonstram aceitação por uma revista ou que todas as afirmações de um manuscrito foram formalizadas.

## O valor de computação descreve a geração

A OpenAI afirma que cada resultado utilizou, em média, um esforço computacional equivalente a cerca de três horas de raciocínio no ChatGPT Pro. O README diz que a avaliação apresentou aproximadamente 4 000 problemas, agrupou as saídas e selecionou as consideradas significativas. Também identifica exceções ao procedimento habitual. Estes são valores da empresa relativos à geração; não indicam o preço de uma verificação Lean do leitor nem uma fatura total em dólares. [Anúncio do lançamento](https://openai.com/index/sharing-ai-progress-in-mathematics/), [relato da geração](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md#how-the-results-were-produced).

Para a família 003, esta análise identifica uma afirmação específica sobre a função zeta, a solução proposta e os axiomas permitidos pelo verificador. Também confirma que o exemplo fornecido deixa o Nanoda desativado. Só uma execução registada pode determinar se esta configuração passa na verificação.

## Fontes e leituras adicionais

- [Anúncio da OpenAI de 6 de outubro](https://openai.com/index/sharing-ai-progress-in-mathematics/)Confirma a data de lançamento, o estado interno do modelo, os acréscimos previstos e a estimativa de computação da empresa. É o relato do próprio programador sobre o seu trabalho.
- [Repositório fixado](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a)Disponibiliza o catálogo, os ficheiros dos manuscritos e as configurações de prova analisadas aqui. Os números provêm do inventário completo e do mapa de manuscritos; os ficheiros formais selecionados foram lidos sem execução. Consultámos o código LaTeX da visão geral para compreender a organização.
- [Referência de validação do Lean](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/)Explica o significado e os limites da verificação de provas. Usámos a referência 4.35.0-rc3; o projeto da OpenAI fixa o Lean 4.34.1.
- [Documentação do Comparator](https://github.com/leanprover/comparator#readme)Explica os ficheiros de desafio e solução, os requisitos do ambiente e as garantias condicionais. Não apresenta um resultado de verificação para esta coleção.
- [Análise de Curtis Pyke na Kingy.ai](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/)Apresenta uma análise estática independente do lançamento. Declara explicitamente que não houve execução independente do Lean; não a consideramos uma reprodução de uma verificação de prova.
- [Artigo anterior da BIG CHANGE sobre matemática e IA](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes)Abrange a sequência de maio a setembro. Este artigo analisa a estrutura dos artefactos da nova coleção e o processo de inspeção.

## Sources

- [Anúncio da OpenAI de 6 de outubro](https://openai.com/index/sharing-ai-progress-in-mathematics/) — Confirma a data de lançamento, o estado interno do modelo, os acréscimos previstos e a estimativa de computação da empresa. É o relato do próprio programador.
- [Repositório matemático fixado da OpenAI](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a) — Disponibiliza o catálogo, os ficheiros dos manuscritos e as configurações de prova analisadas. Os números provêm do inventário completo e do mapa de manuscritos; os ficheiros formais selecionados foram lidos sem execução. Consultámos o código LaTeX da visão geral para compreender a organização.
- [Referência de validação do Lean](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/) — Explica o significado e os limites da verificação de provas. Usámos a referência 4.35.0-rc3; o projeto da OpenAI fixa o Lean 4.34.1.
- [Documentação do Comparator](https://github.com/leanprover/comparator#readme) — Explica os ficheiros de desafio e solução, os requisitos do ambiente e as garantias condicionais. Não apresenta um resultado de verificação para esta coleção.
- [Análise de Curtis Pyke na Kingy.ai](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/) — Análise estática independente do lançamento. Declara que não houve execução independente do Lean; não a consideramos uma reprodução de uma verificação de prova.
- [Artigo anterior da BIG CHANGE sobre matemática e IA](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes) — Abrange a sequência de maio a setembro. Este artigo analisa a estrutura dos artefactos da nova coleção e o processo de inspeção.