Pada 8 September, OpenAI mempublikasikan bukti untuk masalah eksistensi dan kehalusan Navier-Stokes, sekaligus merilis makalah dan file formalisasi Lean. Ini adalah satu dari tujuh Millennium Prize Problems yang ditetapkan Clay Mathematics Institute pada tahun 2000, dengan hadiah 1 juta dolar AS per soal. Dalam pengumumannya, OpenAI menyatakan tidak berniat mengklaim hadiah tersebut.
Bukti ini dihasilkan oleh sekelompok agent yang menjalankan model yang belum dirilis ke publik, yang menurut keterangan resmi kemampuannya jelas melampaui GPT-6 Astra. Kesimpulannya: fluida yang berawal dari kondisi awal yang mulus tetap bisa menghasilkan singularitas dalam waktu terbatas.
88 Jam, Sepuluh Ribu Agent
Yang lebih jarang dipublikasikan dibanding kesimpulannya adalah angka-angka prosesnya. Agent mulai bekerja pada 1 September dan mendapatkan hasil pada 5 September — sekitar 88 jam — dengan sekitar 10.000 agent berjalan bersamaan pada puncaknya. Soal ini saja menghabiskan 2,7 juta pesan dan sekitar 130 miliar token output; jika seluruh soal yang dicoba dalam putaran ini dijumlahkan, totalnya mencapai 4,9 juta pesan dan sekitar 300 miliar token output. Jika dikonversi dengan harga API publik, taksiran pihak luar berada di kisaran 15 juta dolar AS.
Setelah mendapatkan bukti dalam bentuk analitis, GPT-6 Astra menghabiskan 17 jam lagi untuk menuliskannya ke dalam Lean dan menjalankan pemeriksaannya. File formalisasi ini sudah dipublikasikan, dan lapisan ini lebih kokoh dibanding makalah itu sendiri: bukti panjang di bidang analisis selama ini memang sulit diperiksa, sehingga berhasil dikompilasi di Lean setidaknya menyingkirkan persoalan konsistensi logis dari proses tinjauan manusia.
Tapi tahap yang tersisa tidak bisa disingkirkan dengan cara yang sama. Millennium Problem punya pernyataan soal resmi, dan apakah sebuah bukti benar-benar menyelesaikannya bergantung pada syarat mana yang dipenuhi konstruksi tersebut. Sampai ada matematikawan yang membaca seluruh makalah ini, kata 'selesai' masih harus digantung dulu. Keterangan publik yang beredar saat ini belum menjelaskan secara jelas apakah konstruksi ini mengandung suku gaya paksa (forcing term) atau tidak — padahal ada-tidaknya suku itu adalah titik pemisah paling menentukan untuk soal ini selama dua dekade terakhir.
Pengumuman Resmi, dan Satu Pernyataan Lagi
Di hari yang sama, ada babak lain dari cerita ini. Tristan Buckmaster dari Courant Institute, New York University, dan Levent Alpöge dari Anthropic mempublikasikan hasil blow-up dalam waktu terbatas untuk tiga persamaan, termasuk persamaan Euler paksa (forced Euler equation). Buckmaster juga merilis pernyataan terpisah yang menjelaskan komunikasinya dengan OpenAI.
Menurut pengumuman OpenAI, pada awalnya mereka mengira pihak lain juga telah menyelesaikan Navier-Stokes dan mengusulkan publikasi bersama, sebelum akhirnya menyadari bahwa pihak lain sebenarnya mengerjakan persamaan Euler paksa, dan mengakui prioritas pihak tersebut pada soal itu. Soal data, pengumuman itu menyatakan bahwa peneliti maupun agent mereka tidak pernah melihat pekerjaan pihak lain lewat cara apa pun sebelum dipublikasikan — lalu menambahkan bahwa mereka tidak bisa menampik kemungkinan data yang telah dianonimkan dari perilaku penggunaan pihak lain ikut berperan, sembari menegaskan bahwa kedua bukti tersebut berbeda secara signifikan.
Dalam laporan TechCrunch pada 8 September, versi cerita Buckmaster lebih keras. Ia mengatakan kemajuan risetnya sampai ke OpenAI, bahwa pihak tersebut lalu mengambil jalur yang sama dengannya, dan bahwa "hampir tidak ada orang lain yang mengerjakan soal ini." Ia juga mengutip Sébastien Bubeck yang disebutnya berkata dalam panggilan telepon, "kenapa kamu mau menghancurkan kariermu sendiri," dan "kalau kamu tidak mau aku bersikap baik, aku bisa saja tidak bersikap baik." Bubeck sebelumnya telah membantah lewat X, menyebut tuduhan yang beredar itu palsu dan provokatif. Sampai saat ini, cerita kedua pihak soal panggilan telepon yang sama itu tidak sinkron.
Bedanya dengan Kasus-Kasus Sebelumnya
Titik-titik penting di jalur ini sepanjang setahun terakhir cukup mudah ditelusuri: dimulai dari bukti mesin lengkap untuk Fermat's Last Theorem yang berhasil dikompilasi pada mesin 96-core, lalu serangkaian hasil terkait konjektur Erdős, setelah itu formalisasi Lean menjadi standar dalam setiap rilis. Kesamaannya, yang diperdebatkan selalu matematikanya sendiri, dilengkapi rantai bukti yang bisa direproduksi.
Yang baru kali ini adalah prosesnya sendiri yang jadi bahan perdebatan. Siapa yang memulai lebih dulu, draf siapa yang pernah melewati sistem siapa, apa yang dikatakan lewat telepon — sengketa semacam ini juga pernah terjadi di lingkaran matematika yang murni melibatkan manusia, tapi dulu setidaknya urutan kejadian bisa diperjelas lewat cap waktu preprint dan catatan konferensi. Ketika toolchain satu pihak justru adalah produk pihak lain, cap waktu itu tidak lagi netral. Simon Willison mengatakannya lebih terus terang pada 8 September: jika ia memakai ChatGPT untuk menyelesaikan sebagian dari Millennium Problem, seberapa besar kemungkinan hasil kerjanya ikut memengaruhi proses training, sehingga model berikutnya justru membantu orang lain menyelesaikannya lebih dulu?
Pertanyaan ini tidak dijawab oleh pengumuman OpenAI, dan saat ini belum ada satu pun ketentuan data dari laboratorium mana pun yang bisa menjawabnya.
Sumber: pengumuman Millennium Problem dari OpenAI, TechCrunch, CocoLoop, blog pribadi Simon Willison, pernyataan publik Tristan Buckmaster; angka skala agent, pesan, dan token mengikuti pengumuman resmi dan pemberitaannya, sementara konversi biaya merupakan estimasi eksternal berdasarkan harga API publik.