Pada 26 Oktober, OpenAI sekaligus mengumumkan tiga hasil riset yang dihasilkan model AI-nya, mencakup ilmu komputer teoretis, analisis harmonik, dan fisika matematika. Yang paling berbobot adalah bukti bahwa Hipotesis Waktu Eksponensial (ETH) tidak benar. Perusahaan tidak menyebutkan model mana yang dipakai, hanya menulis "model AI OpenAI", dan menyatakan ketiga hasil itu masih memerlukan konfirmasi independen lebih lanjut dari kalangan akademis.
ETH: fondasi bagi ratusan makalah
Hipotesis Waktu Eksponensial berkaitan dengan tingkat kesulitan komputasi masalah keterpenuhan rumus Boolean (3-SAT). Secara kasar, hipotesis ini menyatakan bahwa masalah semacam itu tidak dapat diselesaikan dalam waktu subeksponensial. Hipotesis ini lebih kuat daripada "P tidak sama dengan NP" dan juga lebih mudah dipakai, sehingga selama puluhan tahun diperlakukan sebagai asumsi bawaan: ratusan makalah di bidang teori graf, biologi komputasi, basis data, dan geometri komputasi menyandarkan kesimpulan batas bawahnya pada hipotesis ini.
Menurut lini masa yang dipublikasikan OpenAI, model menghasilkan bukti dalam bahasa alami pada 16 Oktober, dan formalisasi Lean selesai keesokan harinya. Kolaboratornya adalah Russell Impagliazzo dan Ramamohan Paturi dari University of California, San Diego, serta Ryan Williams dari Massachusetts Institute of Technology. Dua nama pertama adalah salah satu pengusul ETH.
Menurut keterangan yang dibuka, para akademisi mengajukan dua syarat kepada OpenAI: membuka seluruh data mentah, dan mendanai sebuah konferensi akademik khusus untuk membahas dampak hasil ini bagi ilmu komputer. OpenAI menyetujui keduanya. Jika buktinya tahan uji, makalah-makalah yang berpremis ETH harus dinilai ulang satu per satu, untuk melihat kesimpulan mana yang hanya kehilangan syaratnya dan mana yang bisa diselamatkan dengan asumsi lain. Itu pekerjaan yang tidak kecil.
Konjektur Kakeya: lini yang akrab bagi matematikawan Tiongkok
Hasil kedua adalah pembuktian konjektur local smoothing di semua dimensi, dan dari situ diturunkan konjektur Kakeya serta konjektur restriksi Stein di semua dimensi. Yang berperan di sini adalah sebuah persamaan diferensial parsial bantu yang dikonstruksi oleh model. OpenAI menyatakan memperoleh bukti pada 18 Oktober dan menyelesaikan formalisasi Lean pada hari berikutnya; versi bahasa alami dan berkas Lean sudah diunggah ke GitHub.
Lini ini tidak asing bagi pembaca berbahasa Mandarin. Konjektur local smoothing diajukan oleh Christopher Sogge pada 1991. Pada 2019, Larry Guth, Hong Wang, dan Ruixiang Zhang membuktikan kasus dua dimensi; pada 2025, Hong Wang dan Joshua Zahl membuktikan konjektur Kakeya tiga dimensi, yang kala itu dipandang sebagai salah satu kemajuan terpenting dalam analisis harmonik selama bertahun-tahun. Lompatan dari tiga dimensi ke semua dimensi sangat besar, dan bagaimana penilaian matematikawan luar, saat ini belum terlihat dalam pernyataan publik.
Yang–Mills: hanya ditelaah para pakar
Hasil ketiga berada di bidang fisika matematika. Riset ini membuktikan, dalam pengertian matematika yang ketat, bahwa teori medan kuantum berinteraksi tertentu di ruang empat dimensi yang memuat medan gauge sekaligus fermion memang ada, termasuk kromodinamika kuantum, dan sekaligus menangani satu submasalah tentang keberadaan teori Yang–Mills murni. Keberadaan dan celah massa teori Yang–Mills murni adalah salah satu Masalah Hadiah Milenium Clay Mathematics Institute.
Metodenya mengikuti jalur teori medan kuantum konstruktif Tadeusz Balaban. Karena Model Standar tidak dapat diekstrapolasi langsung ke skala jarak yang sangat pendek secara sembarang, bukti ini menyasar teori penyatuan besar paling sederhana yang memuat medan gauge dan fermion Model Standar. Telaah dipimpin peraih Nobel David Gross, dengan keterlibatan Michael Douglas, Arthur Jaffe, Igor Klebanov, dan Nikita Nekrasov. Hasil yang satu ini tidak diverifikasi secara formal.
Dari Mei hingga Oktober
Jika rangkaian pengumuman matematika OpenAI tahun ini dirunut, temponya makin cepat dan sasarannya berubah. Mei adalah sebuah masalah Erdős berusia delapan puluh tahun; September adalah masalah kehalusan persamaan Navier–Stokes, yang juga disertai berkas Lean, tetapi saat itu belum ada matematikawan yang menuntaskan verifikasi independen; kali ini sasarannya adalah hipotesis kompleksitas komputasi yang menjadi sandaran banyak pekerjaan hilir, dan untuk pertama kalinya pengusul hipotesis itu sendiri dimasukkan ke daftar kolaborator.
Cara verifikasinya pun terbelah: dua hasil matematika disertai bukti Lean yang dapat diperiksa mesin, sedangkan hasil fisika hanya bisa bergantung pada telaah manusia. Lean dapat menjamin bahwa penurunan tidak memiliki celah, dengan syarat rumusan pernyataan itu sendiri tidak bergeser saat diformalisasi. Hal ini baru bisa dipastikan setelah tim independen membaca berkasnya baris demi baris.
Sumber: pengumuman riset OpenAI, CocoLoop, ITHome; berkas formalisasi Lean yang dipublikasikan di GitHub digunakan untuk memeriksa objek pembuktian dan cara verifikasinya.