Edisi Markdown

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

# Repositori matematika OpenAI: naskah, versi, dan bukti Lean

> Koleksi OpenAI memuat 722 naskah dalam 372 keluarga. Tinjauan mendalam terhadap satu konfigurasi bukti Lean menunjukkan cara memeriksa versi, cakupan, dan persyaratan pemeriksaannya.

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.

Rilis matematika OpenAI pada 6 Oktober menyediakan koleksi publik berisi 722 naskah yang dikelompokkan ke dalam 372 keluarga hasil. Satu keluarga dapat memuat beberapa makalah, sementara bukti formal mungkin mencakup pernyataan yang lebih sempit daripada naskah pendampingnya. Menelusuri sebuah makalah di repositori hingga konfigurasi buktinya menunjukkan klaim mana yang dipilih untuk diperiksa.

Pada 7 Oktober, BIG CHANGE memeriksa inventaris lengkap berkas repositori, katalog, dan sejumlah artefak bukti. Ini merupakan analisis dokumentasi dan artefak statis; kami tidak mengompilasi pustaka Lean, menjalankan pemeriksa bukti, ataupun menelaah matematikanya. [pengumuman OpenAI](https://openai.com/index/sharing-ai-progress-in-mathematics/) menjelaskan rilis yang terus berkembang dan menyebutkan bahwa formalisasi tambahan akan menyusul.

## Perubahan besar

- **Apa yang berubah:** Peneliti kini dapat menelusuri ratusan naskah yang dihasilkan AI dari katalog publik bersama ke berkas pendukung dan, untuk beberapa hasil, ke pernyataan formal serta implementasi bukti yang diusulkan.
- **Mengapa penting:** Matematikawan yang mempertimbangkan penggunaan suatu hasil dapat memeriksa pernyataan yang benar-benar dipilih untuk diuji, asumsi-asumsinya, dan hubungannya dengan makalah. Susunan repositori membantu menunjukkan batas hasil formal yang lebih sempit dan awal dari penelaahan matematika lebih lanjut.
- **Hal yang perlu dipantau:** OpenAI berencana menambahkan formalisasi dan menyimpan revisi. Pembaruan itu penting bagi siapa pun yang mengutip atau mengembangkan karya ini: suatu tinjauan perlu menyebutkan versi dan teorema yang diperiksanya.

## Hitung naskah dan keluarga secara terpisah

Inventaris kami menemukan 722 direktori naskah langsung di bawah `preprints/`, masing-masing berisi satu PDF, serta 10 PDF di bawah `reasoning_traces/`. Peta [naskah](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/CONTENTS.md) memuat 372 entri keluarga yang berbeda dan 722 tautan ke naskah.

Angka-angka itu merujuk pada objek yang berbeda:

| Artefak | Hal yang dapat diperiksa pembaca |
| --- | --- |
| Keluarga hasil | Kelompok makalah terkait, termasuk argumen pendamping, konsekuensi, atau bukti alternatif. |
| Naskah | Dokumen matematika tersendiri dengan berkas sumber dan informasi sitasinya sendiri. |
| Ringkasan penalaran | Uraian ringkas tentang penalaran model untuk hasil yang dipilih. |
| Artefak Lean | Definisi, pernyataan, dan bukti usulan dalam bentuk formal, disertai tautan dan konfigurasi yang menunjukkan apa yang perlu diperiksa. |

README [repositori](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md) menjelaskan kategori-kategori ini dan memperingatkan bahwa tingkat verifikasinya tidak merata. Sejumlah hasil belum memiliki formalisasi Lean, dan OpenAI menyebut pekerjaan yang belum diformalkan mungkin mengandung masalah. [katalog formalisasi](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/formalization.yaml) itu mencatat cakupan sebagai “Partial progress” dan status tinjauan sebagai `unchecked`. Kedua kolom itu adalah metadata publikasi, bukan hasil pemeriksaan yang dijalankan BIG CHANGE.

Berkas publik dapat dibaca tanpa akun OpenAI. Pengumuman menyebut model pembuatnya sebagai model internal dan mengatakan OpenAI sedang berupaya merilisnya. Jadi, akses ke dokumen ini tidak membuktikan akses ke model tersebut.

## Tetapkan versinya sebelum menelusuri bukti

Snapshot repositori yang digunakan di sini berada pada commit [`adc7f1241b42e322a6451854ab7e4b4c146bf78a`](https://github.com/openai/math/commit/adc7f1241b42e322a6451854ab7e4b4c146bf78a), bertanggal 6 Oktober 2026 pukul 21.58.50 UTC. Tautan yang memuat pengenal itu mempertahankan snapshot yang diperiksa; tautan yang memuat `main` mengikuti cabang default yang terus berubah. README OpenAI berjanji menyimpan rilis terdahulu saat koreksi atau revisi muncul.

Mulailah dari [ikhtisar](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/overview.pdf), yang mengelompokkan keluarga menurut bidang matematika. Lalu gunakan peta naskah untuk menemukan makalah tertentu. Catat nama direktorinya, commit repositori, dan sitasi yang disediakan makalah. Tanggal naskah dapat berbeda dari tanggal rilis koleksi publik.

Keluarga 003 mencakup makalah yang mengklaim adanya wilayah bebas nol di sebelah kanan 7/8, bukti alternatif untuk wilayah di sebelah kanan 11/12, serta makalah terpisah tentang nol Landau-Siegel. [Direktori makalah pertama](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/README.md) bertanggal 30 September dan menyediakan sitasi BibTeX. Mencatat makalah yang tepat menjaga perbedaan di antara klaim-klaim tersebut.

Halaman [cakupan Lean](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/003.md) menjelaskan pernyataan yang dicakup formalisasi, mencatat pengecualian, dan menyebut bahwa penerapan lebih lanjut dalam makalah tidak disertakan. Halaman itu menautkan pernyataan pemeriksaan terpisah untuk hasil zeta, fungsi-L Dirichlet dan Hecke, serta celah seragam bagi nol real. Pemeriksaan satu pernyataan pilihan tidak otomatis mewakili semua butir pada halaman itu.

## Telusuri pernyataan yang dipilih hingga ke konfigurasinya

Petunjuk OpenAI untuk [Comparator](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/README.md) menggunakan keluarga 003 sebagai contoh. Comparator adalah alat untuk membandingkan bukti Lean yang diusulkan dengan tantangan yang ditentukan. Contoh [konfigurasi JSON](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.json) memilih satu teorema: fungsi zeta Riemann tidak bernilai nol ketika bagian real argumennya lebih besar dari 7/8.

Konfigurasi itu menunjuk ke modul tantangan dan modul solusi yang terpisah. Konfigurasi mengizinkan aksioma standar `propext`, `Quot.sound` dan `Classical.choice`, serta menetapkan `enable_nanoda` menjadi `false`. Nanoda adalah pemeriksa independen yang dapat digunakan Comparator; contoh konfigurasi ini tidak mengaktifkannya.

Berkas [tantangan](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.lean) memuat `sorry`, placeholder Lean untuk bukti yang belum selesai. Di sini, placeholder itu berfungsi sebagai pernyataan yang harus dicocokkan. Dokumentasi Comparator mengizinkan placeholder dalam tantangan dan mewajibkan bukti yang benar dalam solusi. Menemukan `sorry` di berkas tantangan ini saja tidak menunjukkan apakah solusi terpisahnya lolos pemeriksaan. [Dokumentasi Comparator](https://github.com/leanprover/comparator#readme).

Untuk pemeriksaan lokal yang terdokumentasi, siapkan konfigurasi tersebut, modul tantangan dan solusi, serta dependensinya. Repositori ini menetapkan [Lean 4.34.1](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lean-toolchain). [Manifest Lake](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lake-manifest.json) mencatat revisi dependensi, termasuk Mathlib pada `d13f23b723b8a846827a245b89c10fc7d3f11612`.

OpenAI mewajibkan `comparator`, `landrun` dan `lean4export` tersedia di jalur pencarian executable, lalu mendokumentasikan perintah berikut dari direktori `lean/`:

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

Ini adalah petunjuk penerbit, bukan perintah yang kami jalankan. Versi ketiga alat eksternal tersebut tidak ditetapkan di sana. Dokumentasi Comparator saat ini mensyaratkan lingkungan `lean4export` yang kompatibel, menjelaskan prasyarat sandbox, dan menetapkan kondisi ketika keberhasilan membuktikan kecocokan dengan tantangan, penggunaan aksioma yang diizinkan, serta penerimaan kernel. Laporan yang dapat direproduksi perlu mencatat versi alat yang terpasang dan keluaran sebenarnya, bersama commit repositori.

Dokumen [README pustaka Lean](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/README.md) menyarankan kompilasi bagian-bagian kecil dari pustaka besar ini. README itu juga menjelaskan batas pemetaan memori Linux yang dapat menghalangi build lengkap. Kami tidak mengukur waktu jalan lokal atau biaya perangkat keras untuk contoh ini.

## Pahami hasil pemeriksaan sesuai cakupan yang dinyatakan

Dokumen [referensi validasi Lean](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/), versi 4.35.0-rc3 saat dibaca, membedakan penerimaan bukti formal dari penafsiran makna teorema. Versi dokumentasi itu berbeda dari toolchain yang ditetapkan di repositori ini.

Pemeriksaan dasar yang berhasil berarti kernel menerima pernyataan formal berdasarkan definisi, impor, dan aksiomanya. Dependensi masih dapat memuat bukti yang belum selesai. Lean mendokumentasikan `#print axioms` untuk menampilkan aksioma yang digunakan, termasuk `sorryAx` jika ada bukti yang belum selesai dalam rantai dependensi.

Pemeriksaan yang lebih kuat memutar ulang bukti tersimpan atau membandingkan solusi dengan pernyataan yang ditentukan secara terpisah. Pemeriksaan itu tetap bergantung pada lingkungan pemeriksaan dan ketepatan perumusan makna yang dimaksud. Karena itu, laporan verifikasi perlu mencantumkan tantangan yang tepat, aksioma yang diizinkan, dan pengaturan pemeriksa eksternal. Penerimaan kernel maupun kecocokan dengan tantangan tidak membuktikan penerimaan jurnal atau bahwa setiap klaim dalam naskah telah diformalkan.

## Angka komputasi menjelaskan proses pembuatan

OpenAI melaporkan bahwa rata-rata setiap hasil menggunakan komputasi setara kira-kira tiga jam berpikir ChatGPT Pro. README-nya menyebut evaluasi mencakup sekitar 4.000 masalah; keluarannya kemudian dikelompokkan dan dipilih berdasarkan signifikansi. README itu juga menyebut pengecualian dari prosedur umum. Ini adalah angka pembuatan dari perusahaan; angka tersebut tidak menetapkan biaya pemeriksaan Lean bagi pembaca atau total tagihan dalam dolar. [Pengumuman rilis](https://openai.com/index/sharing-ai-progress-in-mathematics/), [keterangan proses pembuatan](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md#how-the-results-were-produced).

Untuk keluarga 003, pemeriksaan ini mengidentifikasi pernyataan zeta tertentu, solusi yang diusulkan, dan aksioma yang diizinkan pemeriksa. Pemeriksaan ini juga memastikan bahwa contoh yang disediakan menonaktifkan Nanoda. Apakah pemeriksaan yang dikonfigurasi itu berhasil hanya dapat dipastikan melalui proses yang dijalankan dan dicatat.

## Sumber dan bacaan lanjutan

- [Pengumuman OpenAI pada 6 Oktober](https://openai.com/index/sharing-ai-progress-in-mathematics/) menetapkan tanggal rilis, status model internal, penambahan yang direncanakan, dan perkiraan komputasi perusahaan. Ini adalah keterangan pengembang tentang karyanya sendiri.
- [Repositori pada commit yang dipatok](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a) menyediakan katalog, berkas naskah, dan konfigurasi bukti yang diperiksa di sini. Jumlahnya berasal dari inventaris lengkap dan peta naskah; berkas formal terpilih dibaca tanpa dijalankan. Kami juga memeriksa sumber LaTeX ikhtisar untuk memahami susunannya.
- [Referensi validasi Lean](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/) menjelaskan arti dan batas pemeriksaan bukti. Kami menggunakan referensi versi 4.35.0-rc3; proyek OpenAI menetapkan Lean 4.34.1.
- [Dokumentasi Comparator](https://github.com/leanprover/comparator#readme) menjelaskan berkas tantangan dan solusi, persyaratan lingkungan, serta jaminan bersyarat. Dokumentasi itu tidak melaporkan hasil verifikasi untuk koleksi ini.
- [Ulasan Curtis Pyke di Kingy.ai](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/) menyajikan pemeriksaan statis independen atas rilis tersebut. Ulasan itu secara eksplisit menyatakan tidak ada eksekusi Lean independen; kami tidak menganggapnya sebagai pengulangan pemeriksaan bukti.
- [Laporan AI dan matematika BIG CHANGE sebelumnya](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes) mencakup rangkaian perkembangan dari Mei hingga September. Artikel ini menelaah struktur artefak koleksi baru dan cara memeriksanya.

## Sources

- [Pengumuman OpenAI pada 6 Oktober](https://openai.com/index/sharing-ai-progress-in-mathematics/) — Menetapkan tanggal rilis, status model internal, penambahan yang direncanakan, dan perkiraan komputasi perusahaan. Ini adalah keterangan pengembang tentang karyanya sendiri.
- [Repositori matematika OpenAI yang dipatok](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a) — Menyediakan katalog, berkas naskah, dan konfigurasi bukti yang diperiksa di sini. Jumlahnya berasal dari inventaris lengkap dan peta naskah; berkas formal terpilih dibaca tanpa dijalankan. Kami juga memeriksa sumber LaTeX ikhtisar untuk memahami susunannya.
- [Referensi validasi Lean](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/) — Menjelaskan arti dan batas pemeriksaan bukti. Kami menggunakan referensi versi 4.35.0-rc3; proyek OpenAI menetapkan Lean 4.34.1.
- [Dokumentasi Comparator](https://github.com/leanprover/comparator#readme) — Menjelaskan berkas tantangan dan solusi, persyaratan lingkungan, serta jaminan bersyarat. Dokumentasi itu tidak melaporkan hasil verifikasi untuk koleksi ini.
- [Ulasan Curtis Pyke di Kingy.ai](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/) — Menyajikan pemeriksaan statis independen atas rilis tersebut. Ulasan itu secara eksplisit menyatakan tidak ada eksekusi Lean independen; kami tidak menganggapnya sebagai pengulangan pemeriksaan bukti.
- [Laporan AI dan matematika BIG CHANGE sebelumnya](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes) — Mencakup rangkaian perkembangan dari Mei hingga September. Artikel ini menelaah struktur artefak koleksi baru dan cara memeriksanya.