Bukti Navier-Stokes OpenAI Dipertanyakan Riset Baru
Judul asli: Navier–Stokes Lost in Translation
Mengapa Ini Penting
Meragukan metode verifikasi formal AI yang kian populer di komunitas matematika.
Makalah arxiv oleh Bastounis dkk (6 Okt 2026) membuktikan verifikasi Lean atas bukti Navier-Stokes OpenAI tidak menjamin kebenaran argumen bahasa alami aslinya.
Tiga peneliti — Alexander Bastounis, Fabian Circelli, dan Anders C. Hansen — menerbitkan makalah 25 halaman yang secara langsung menyasar klaim OpenAI soal bukti blow-up solusi persamaan Navier-Stokes. Inti argumen mereka: proses autoformalisasi AI, yakni menerjemahkan teks matematika dari bahasa alami ke bahasa formal seperti Lean, tidak dapat menjamin kesetiaan semantik terjemahan tersebut.
Para peneliti menunjukkan bahwa masalah resolusi ambiguitas dalam teks matematika bahasa alami berada di tingkat yang arbitrarily tinggi dalam hierarki Solvability Complexity Index (SCI) — tepatnya SCI = ∞. Ini berarti masalah tersebut secara komputasional lebih sulit dari Halting problem (SCI = 1), sehingga tidak ada sistem AI yang dapat menyelesaikannya secara umum.
Sebagai bukti empiris, mereka menampilkan beberapa contoh nyata kesalahan terjemahan AI dari pernyataan dan bukti bahasa alami ke Lean. Salah satunya adalah bukti Navier-Stokes OpenAI sendiri — di mana mereka menyimpulkan bukti Lean yang terverifikasi tidak berkorespondensi dengan argumen blow-up dalam teks bahasa alami yang diklaim.