AI OpenAI Salah Menerjemahkan Bukti Matematika Navier-Stokes-nya Sendiri ke dalam Kode

Apa yang diumumkan OpenAI

OpenAI mengatakan pada 8 September 2026, bahwa sistem multi-agent internal telah menghasilkan bukti yang mengatasi masalah keberadaan dan smoothness Navier-Stokes, salah satu dari tujuh Millennium Prize Problems yang membawa hadiah $1 juta dari Clay Mathematics Institute, menurut situs pelacak AI implicator.ai. Perusahaan melaporkan bahwa sekitar 10.000 agen bekerja selama 88 jam mulai dari 28 Agustus, menghasilkan 2,7 juta pesan agen dan sekitar 130 miliar token output, sebelum model terpisah, dijelaskan sebagai GPT-6 Astra, menghabiskan 17 jam lebih lanjut untuk secara formal memverifikasi argumen dalam bahasa bukti Lean.

Hasilnya adalah manuskrip bahasa alami berjudul "Finite time blowup for Navier–Stokes," disertai proyek Lean yang dimaksudkan untuk memungkinkan komputer memeriksa setiap langkah logis, menurut implicator.ai dan paper arXiv yang kemudian menganalisis pekerjaan tersebut.

Temuan kesalahan-penerjemahan

Sebuah paper yang diposting di server preprint arXiv, berjudul "Navier-Stokes Lost in Translation" dan ditulis oleh ahli matematika Alexander Bastounis, Fabian Circelli dan Anders C. Hansen, memeriksa apakah kode Lean OpenAI benar-benar cocok dengan argumen matematis dalam paper bahasa alami. Para penulis membedakan antara bukti Lean yang hanya dikompilasi dan bukti yang setia secara semantik terhadap penalaran asli, dengan alasan bahwa jenis yang kedua jauh lebih sulit untuk dijamin daripada yang pertama.

Paper tersebut mencantumkan ketidaksesuaian konkret. Dalam satu kasus, Lemma 8.6 paper bahasa alami memerlukan pengebatan turunan menggunakan empat orde input tambahan, ditulis m+4, tetapi teorema Lean yang sesuai malah memerlukan lima orde tambahan, m+5 — kondisi yang lebih kuat daripada yang dinyatakan dalam paper. Dalam yang lain, persamaan 10.19 manuskrip mengebat istilah flux-tekanan menggunakan hanya satu variabel, disebut B_R, sementara versi Lean dari batas yang sama juga bergantung pada variabel kedua, A_R, yang berasal dari teknik matematis yang berbeda.

Para penulis menyimpulkan bahwa file Lean yang berhasil dikompilasi hanya menunjukkan bahwa bukti yang benar ada untuk teorema yang dinyatakan, bukan bahwa itu adalah bukti yang sama yang dijelaskan dengan kata-kata. Mereka menulis bahwa kode Lean OpenAI sering menerapkan kondisi yang lebih kuat pada batas-batas berbagai fungsi daripada hasil yang sesuai dalam paper bahasa alami, dan mereka merekomendasikan bahwa formalisasi Navier-Stokes dan Euler-equation terkait OpenAI menjalani peer review yang sama seperti bukti tradisional sebelum dipercaya.

Sengketa terpisah: masalah mana yang dipecahkan?

Terlepas dari pertanyaan penerjemahan, beberapa ahli matematika memperdebatkan apakah OpenAI menyelesaikan versi Navier-Stokes yang paling diperhatikan oleh peneliti. Pernyataan masalah resmi Lembaga Clay tahun 2000, ditulis oleh Charles Fefferman, mencakup opsi berlabel C yang memungkinkan istilah forcing eksternal yang halus, sementara kebanyakan ahli matematika telah fokus pada kasus tanpa forcing, Scientific American melaporkan.

Bukti OpenAI menargetkan opsi C. Luis Silvestre dari University of Chicago dan rekan-rekan memposting paper yang berpendapat bahwa mekanisme blow-up OpenAI tidak dapat bekerja setelah gaya eksternal dihilangkan, Scientific American melaporkan.

Bagian dari pola scrutiny yang lebih luas

Scrutiny terhadap klaim matematis OpenAI bukanlah hal baru. Pada Oktober 2025, mantan wakil presiden OpenAI Kevin Weil mengatakan GPT-5 telah menyelesaikan sepuluh masalah Erdős yang sebelumnya belum terpecahkan dan membuat kemajuan pada sebelas masalah lainnya; ahli matematika termasuk Thomas Bloom mengatakan hasil sudah ada dalam literatur yang dipublikasikan, dan Weil menarik kembali post tersebut, TechCrunch melaporkan. Ketika OpenAI mengumumkan pada Mei 2026 bahwa model penalaran telah membantah konjektur geometri Erdős dari tahun 1946, itu menerbitkan pernyataan pendukung dari ahli matematika Noga Alon, Melanie Wood dan Thomas Bloom — Bloom yang sama yang telah menandai kesalahan sebelumnya — bersama dengan klaim tersebut, TechCrunch melaporkan.

Pada 7 Oktober 2026, OpenAI menerbitkan 372 hasil matematika yang dihasilkan AI di GitHub, masing-masing dimaksudkan untuk menyelesaikan masalah terbuka atau membuat kemajuan substansial terhadapnya, sebagian besar dihasilkan dari prompt tunggal ke model internal dengan biaya sekitar tiga jam waktu komputasi ChatGPT Pro masing-masing, the-decoder melaporkan. Dua puluh lima pemenang Fields Medal menandatangani surat terbuka yang memperingatkan bahwa memproduksi secara massal pernyataan matematis yang benar berisiko merusak bidang daripada memajukannya, menurut laporan yang sama, yang mencatat bahwa sebagian besar hasil tidak telah melalui peer review standar.

Di mana klaim berdiri sekarang

Clay Mathematics Institute masih mencantumkan Navier-Stokes di antara Millennium Prize Problems yang belum terpecahkan, implicator.ai melaporkan. Presiden Institut Martin Bridson mengatakan pengumuman itu menarik tetapi bahwa evaluasi formal apa pun akan dilakukan dengan tidak terburu-buru dan ketat.