OpenAI Dakwa Swarm AI Menemui Penyelesaian Masalah Navier–Stokes

OpenAI Dakwa Swarm AI Menemui Penyelesaian Masalah Navier–Stokes

OpenAI baru sahaja meletakkan satu dakwaan besar di atas meja matematik.

Pada 8 September 2026, syarikat itu menerbitkan hasil daripada model AI dalaman yang, menurut OpenAI, menghasilkan penyelesaian untuk masalah Navier–Stokes — salah satu daripada tujuh Millennium Prize Problems yang ditetapkan oleh Clay Mathematics Institute.

Syarikat itu tidak sekadar menerbitkan penerangan biasa. OpenAI turut membuka formal proof dalam Lean, supaya keputusan itu boleh diperiksa menggunakan theorem prover.

Dalam eksperimen itu, OpenAI mengatakan sehingga kira-kira 10,000 AI agents berjalan serentak. Kes Navier–Stokes mengambil masa sekitar 88 jam, sebelum hasilnya diformalkan dan diperiksa dalam Lean.

Tetapi ada satu perkataan yang penting di sini: dakwaan.

Ini belum bermaksud Clay Mathematics Institute sudah mengiktiraf masalah itu sebagai selesai. Malah, OpenAI sendiri menamakan penerbitannya sebagai cadangan penyelesaian, bukan pengumuman bahawa Clay telah menerima bukti itu.

Dan di situlah cerita ini menjadi jauh lebih menarik.

Apa sebenarnya masalah Navier–Stokes?

Navier–Stokes ialah persamaan asas dalam fluid dynamics. Ia digunakan untuk menerangkan pergerakan bendalir seperti air dan udara.

Masalah matematiknya bukan sekadar mencari jawapan kepada satu simulasi.

Persoalannya lebih asas: kalau kita bermula dengan keadaan yang cukup baik dan licin, adakah penyelesaian persamaan Navier–Stokes akan kekal licin untuk selama-lamanya?

Atau adakah ia boleh sampai ke satu titik di mana sesuatu menjadi tidak terhingga dalam masa terhingga?

Clay Mathematics Institute menyenaraikan soalan tentang kewujudan dan kelicinan penyelesaian ini sebagai salah satu masalah besar yang masih belum mempunyai penyelesaian lengkap.

Secara kasar, keadaan kedua itulah yang dipanggil finite-time blowup atau pembentukan singularity.

Bayangkan velocity field yang pada mulanya semuanya terkawal. Kemudian, apabila masa bergerak ke hadapan, struktur kecil dalam aliran menjadi semakin ekstrem sehingga sesetengah kuantiti tempatan tidak lagi boleh dikekalkan dalam keadaan terhingga.

Persoalannya ialah sama ada fenomena sebegitu memang boleh berlaku dalam persamaan Navier–Stokes tiga dimensi.

Selama puluhan tahun, jawapannya tidak diketahui.

OpenAI kata jawapannya ialah "ya"

Menurut hasil yang diterbitkan OpenAI, mereka menghasilkan contoh yang menunjukkan bahawa penyelesaian Navier–Stokes boleh mengalami breakdown dalam masa terhingga.

Yang menarik, hasil itu bukan sekadar claim bahawa model "nampak" singularity dalam simulasi.

Repository rasmi OpenAI mengandungi formalization Lean untuk dua keputusan Navier–Stokes:

• di ruang Euclidean R³, terdapat initial data dan forcing yang licin sehingga tiada global smooth solution dengan kinetic energy yang kekal bounded;
• pada periodic torus R³/Z³, terdapat initial data dan forcing yang licin sehingga tiada global smooth solution.

OpenAI memetakan kedua-duanya kepada alternatif (C) dan (D) dalam formulasi rasmi Clay Mathematics Institute.

Ini penting kerana tajuk "AI menyelesaikan Navier–Stokes" mudah membuat orang membayangkan sesuatu yang lebih besar daripada apa yang sebenarnya dibuktikan.

Hasil OpenAI berkait secara khusus dengan versi breakdown yang dibenarkan dalam formulasi masalah Clay, termasuk penggunaan smooth forcing. Itu bukan perkara yang sama dengan mengatakan semua versi persoalan Navier–Stokes sudah difahami.

10,000 agents bukan sekadar satu model yang berfikir lama

Bahagian yang paling luar biasa mungkin bukan matematiknya.

Ia ialah cara OpenAI menjalankan carian itu.

OpenAI menggunakan sistem yang terdiri daripada agents yang bekerja secara selari. Pada kemuncaknya, kira-kira 10,000 agents terlibat dalam usaha menyelesaikan masalah Navier–Stokes. Keseluruhan carian itu mengambil sekitar 88 jam.

Ini lebih dekat kepada distributed research system daripada penggunaan chatbot biasa.

Satu agent boleh mencadangkan idea.

Agent lain boleh cuba membuktikannya.

Agent lain mencari counterexample.

Sebahagian lagi mengubah construction atau lemma.

Kemudian hasil yang nampak menjanjikan boleh dihantar ke formalization pipeline.

Dalam model seperti ini, masalahnya bukan lagi:

"Bolehkah satu model AI menyelesaikan masalah matematik?"

Soalan yang lebih menarik ialah:

"Bolehkah ribuan proses AI mencari ruang kemungkinan secara selari sehingga sesuatu yang betul akhirnya muncul?"

Itu perubahan seni bina yang jauh lebih besar.

Lean mengubah standard pembuktian

Di sinilah eksperimen OpenAI menjadi sangat relevan kepada developer.

OpenAI menerbitkan repository NavierStokesAndEuler yang mengandungi formalization dalam Lean 4. Repository itu juga menyatakan bahawa formalization itu boleh dibina dan diperiksa secara bebas menggunakan Lean dan Comparator.

Repository itu menggunakan Lean 4.34.0-rc2, Mathlib dan Lake. Konfigurasi projek juga menyatakan sorry_count: 0 untuk keputusan utama yang diformalisasikan.

Ini bahagian yang membezakan cerita ini daripada "AI menghasilkan proof dalam bentuk teks".

LLM boleh menghasilkan hujah yang kelihatan sangat meyakinkan tetapi sebenarnya mempunyai satu langkah yang salah.

Lean tidak peduli sama ada hujah itu nampak cantik.

Jika term terakhir tidak memenuhi theorem yang diperlukan, kernel tidak menerimanya.

Jadi pembahagian kerjanya menjadi lebih jelas:

AI mencari idea. Lean memeriksa formalization. Manusia menilai matematiknya.

Itu bukan pengganti matematik manusia. Tetapi ia boleh menjadi cara baru untuk melakukan matematik.

Ada satu masalah besar dengan dakwaan ini

Walaupun proof sudah diformalisasikan, itu tidak bermaksud semua ahli matematik perlu terus menganggap masalah ini selesai.

Formal verification hanya menjawab sebahagian daripada persoalan.

Kita masih perlu memahami:

• apakah sebenarnya theorem yang telah dibuktikan;
• sama ada theorem itu benar-benar sepadan dengan persoalan Clay;
• sama ada semua andaian digunakan dengan tepat;
• sama ada construction itu mempunyai tafsiran yang dimaksudkan;
• dan sejauh mana hasil itu menyelesaikan persoalan asal, bukan hanya versi tertentu daripadanya.

Repository OpenAI sendiri menerangkan keputusan Navier–Stokes mereka sebagai breakdown untuk kes dengan smooth forcing dan memadankannya kepada alternatif (C) dan (D) dalam dokumen Clay.

Itulah sebabnya perkataan "selesai" perlu digunakan dengan berhati-hati.

Proof checker boleh memberitahu kita bahawa formalization itu konsisten dengan theorem yang diberikan kepadanya.

Ia tidak secara automatik memberitahu kita bahawa tajuk berita yang kita tulis adalah tepat.

Kemudian muncul pertikaian Buckmaster dan Alpöge

Beberapa jam selepas pengumuman OpenAI, cerita ini berubah daripada kisah matematik kepada pertikaian mengenai kredit dan data.

Ahli matematik NYU Tristan Buckmaster dan penyelidik Anthropic Levent Alpöge sedang mengusahakan penyelidikan berkaitan finite-time blowup dalam fluid equations.

Buckmaster kemudian mempersoalkan sama ada kerja mereka mungkin mempunyai hubungan dengan usaha OpenAI selepas beliau memberitahu penyelidik OpenAI mengenai kerja itu. Sebahagian daripada kerja mereka juga pernah dilakukan menggunakan tools daripada OpenAI.

Ini menimbulkan persoalan yang lebih besar daripada siapa mendapat kredit.

Bolehkah penyelidik menggunakan AI lab untuk kerja yang belum diterbitkan tanpa risau bahawa idea itu akhirnya membantu lab yang sama menghasilkan penyelesaian?

OpenAI menafikan bahawa ia mengakses data khusus daripada kerja itu atau menggunakan hasil mereka secara langsung. Pada masa yang sama, syarikat itu mengakui tidak dapat menolak kemungkinan data pengguna yang telah dinyahkenal pasti memberi pengaruh tidak langsung terhadap model mereka.

Jadi buat masa ini, dua perkara perlu dipisahkan.

Pertama, ada dakwaan matematik OpenAI.

Kedua, ada pertikaian tentang bagaimana idea dan data penyelidikan AI sepatutnya dikendalikan.

Kedua-duanya belum mempunyai keputusan akhir.

Jadi, adakah OpenAI benar-benar menyelesaikan masalah Millennium Prize?

Belum boleh kita kata begitu dengan yakin.

Yang boleh dikatakan sekarang ialah OpenAI telah menerbitkan satu hasil yang mendakwa menunjukkan finite-time breakdown untuk formulasi Navier–Stokes tertentu, bersama formalization Lean yang tersedia untuk pemeriksaan.

Itu sudah cukup besar.

Tetapi pengiktirafan matematik tidak berfungsi seperti benchmark AI.

Tidak ada leaderboard yang terus bertukar daripada unsolved kepada solved sebaik sahaja model menerbitkan repository GitHub.

Ahli matematik perlu membaca proof.

Mereka perlu cuba memecahkannya.

Mereka perlu melihat sama ada semua andaian sepadan dengan masalah asal.

Dan akhirnya, komuniti matematik perlu bersetuju bahawa hasil itu memang menyelesaikan persoalan yang dimaksudkan.

OpenAI juga tidak bercadang untuk menuntut hadiah $1 juta yang dikaitkan dengan Millennium Prize Problem itu (TNW).

Perubahan sebenar mungkin bukan pada Navier–Stokes

Kalau proof ini akhirnya bertahan, sejarah mungkin mengingatinya sebagai satu lagi penyelesaian masalah matematik besar.

Tetapi bagi dunia AI, perkara yang lebih menarik ialah cara keputusan itu dicapai.

Selama ini kita banyak bercakap tentang AI sebagai model yang menghasilkan jawapan.

Eksperimen OpenAI menunjukkan bentuk yang berbeza:

model → agents → parallel search → candidate proofs → formal verification → human review

Itu sudah hampir menyerupai research pipeline.

AI tidak perlu memahami matematik seperti seorang profesor untuk menjadi berguna. Ia mungkin cukup jika sistem boleh menghasilkan ribuan hipotesis, membuang sebahagian besar yang salah, memformalkan calon yang menjanjikan dan menyerahkan hasil yang tinggal kepada manusia.

Lean pula memberikan sesuatu yang sangat diperlukan dalam workflow seperti ini: mekanisme untuk menolak bukti yang tidak sah.

Masih terlalu awal untuk mengatakan AI sudah mengambil alih mathematical research.

Tetapi satu perkara memang berubah.

Kita kini mempunyai contoh sebenar di mana ribuan agents digunakan bukan untuk menulis code atau merumuskan dokumen, tetapi untuk mencari jalan keluar daripada masalah matematik yang telah bertahan selama beberapa dekad.

Dan jika pendekatan itu boleh diskalakan kepada masalah lain, persoalan seterusnya bukan lagi sama ada AI boleh membantu matematik.

Persoalannya ialah berapa banyak matematik yang boleh dicari apabila compute, agents dan formal verification semuanya boleh diskalakan serentak.

Sumber

• OpenAI — An OpenAI model proposes a solution to the Navier–Stokes problem
• OpenAI — NavierStokesAndEuler Lean formalizations
• Clay Mathematics Institute — Navier–Stokes Equation
• Clay Mathematics Institute — Millennium Prize Problems
• The Guardian — OpenAI claims to have solved maths problem
• The Verge — Drama swirls around OpenAI's mathematical milestone
• Axios — OpenAI's historic math solution overshadowed by credit controversy

---

Nota editorial

Artikel ini sengaja menggunakan "OpenAI mendakwa", "menurut OpenAI" dan "belum boleh dianggap selesai". Ini penting kerana pengumuman rasmi OpenAI sendiri menyebutnya sebagai proposes a solution, manakala komuniti matematik masih perlu menilai implikasi dan ketepatan hasil itu.