OpenAI AI Membuktikan Teorema Matematika Utama, Verifikasi Lean Memicu Perdebatan

Model inferensi terbaru dari OpenAI, merilis sepuluh kemajuan matematis yang menakjubkan sekaligus.

Termasuk:

• Pertama kali membuktikan keberadaan grup non-sofic;
• Memberikan batas bawah sirkuit baru;
• Mengatasi batas kesulitan Masalah Vektor Terdekat (Closest Vector Problem, CVP) terbaru;
• Dan teorema peluruhan eksponensial paralel berulang untuk permainan kuantum dua pemain (Quantum parallel repetition).

Yang paling dihiraukan oleh Asisten Profesor Universitas Columbia, Henry Yuen, adalah yang terakhir—

Pada tahun 2016, Yuen mencapai kemajuan signifikan pada masalah ini, tetapi belum menyelesaikannya sepenuhnya. Selama 10 tahun, ia terus gagal, bahkan sebulan yang lalu ia masih menggunakan ChatGPT 5.5 untuk sekali lagi menyerang bukti utama, namun hasilnya sedikit.

Sementara AI, di atas bahunya, menendang ringan bola ke gawang.

Beberapa hari yang lalu, Lijie Chen mengirimkan draf makalah kepada Henry Yuen dan beberapa orang lainnya.

Pada waktu itu hidupnya sibuk, sehingga ia tidak punya waktu untuk mempelajari secara mendalam. Sekarang, makalahnya telah dipublikasikan. Ia merasa harus mengungkapkan pendapatnya.

Teorema pengulangan paralel kuantum (Quantum parallel repetition theorem) adalah bidang yang telah diteliti Henry Yuen selama bertahun-tahun selama masa studi pascasarjananya, sekaligus pencapaian yang paling ia banggakan.

Henry Yuen, saat ini merupakan Associate Professor of Computer Science di Columbia University, Keluarga Srivani

Dia mengingat sore-sore yang dihabiskan di kafe, malam-malam yang dilewati di kantor, dan berbagai akhir pekan yang seharusnya digunakan untuk istirahat, sambil terus-menerus menguraikan dan mempelajari teorema pengulangan paralel klasik Ran Raz.

Dia ingin menyelesaikan versi kuantum dari teorema ini, hingga tak bisa tidur dan terus berguling-guling di tempat tidur. Dia menelan banyak alat matematika, dan akhirnya berhasil membuktikan peluruhan polinomial.

https://arxiv.org/pdf/1604.04340

Lebih penting lagi, ia membangun kepercayaan diri darinya, akhirnya menyadari kekuatannya sendiri, dan membuktikan bahwa ia memang mampu menyelesaikan masalah-masalah itu (setidaknya sebagian) yang juga diperhatikan orang lain.

Dia percaya sertifikasi dari OpenAI seharusnya benar, mengingat sudah ada bukti formalisasi Lean. Namun, Henry Yuen masih memerlukan waktu untuk memahami bukti baru ini.

Meskipun bukti baru memang melanjutkan dari titik di mana bukti sebelumnya berakhir, AI melampaui batasan strategi bukti sebelumnya dengan menggunakan beberapa teknik dan metode yang mungkin sudah dikuasai oleh peneliti di bidang teori operator dan analisis fungsional.

Selain kegembiraan,感 pertama Yuen adalah kekecewaan terhadap gaya penulisan makalahnya.

Dia mengatakan bukti ini terdengar sangat AI: pembukaan yang panjang dan bertele-tele, tetapi bagian pentingnya tiba-tiba seperti sulap, membuat orang bingung.

Bukti dari OpenAI, meskipun menarik untuk dibaca, juga agak membingungkan.

Ia terlebih dahulu meletakkan masalahnya dengan rapi di atas meja, lalu tiba-tiba melompat ke arah "mencari purification yang benar dengan pre-solving", hampir tanpa langkah logis apa pun di antaranya.

Selanjutnya, dilakukan serangkaian perhitungan entropi matriks yang cukup tidak biasa, dihitung dengan rumit, dan pada akhirnya memberitahu Anda: jalan ini bisa ditempuh.

Namun, langkah paling krusial itu, intuisi itu sebenarnya berasal dari mana, tidak dijelaskan.

Dan langkah paling cemerlang dan paling menguji kreativitas—teknik memperluas ruang operator menggunakan transformasi Uhlmann—seharusnya menjadi klimaks paling menggetarkan dari seluruh bukti, tetapi justru ditinggalkan oleh AI seperti pasir dan kerikil, dibuang tanpa peringatan maupun penjelasan di bagian keempat.

Bukti yang benar, tetapi menyembunyikan ide paling penting.

Dia berharap OpenAI bisa menghabiskan beberapa petunjuk lebih banyak untuk menyusun naskah ini dengan baik.

Yang lebih menyakitkan adalah lapisan kedua: Verifikasi Lean berhasil tidak sama dengan pemahaman.

Mesin dapat menjamin setiap langkah deduksi tanpa cela, tetapi pertanyaan-pertanyaan seperti "Mengapa trik ini efektif?", "Apa artinya dalam peta teori yang lebih luas?", dan "Di mana lagi ini bisa digunakan?"—tidak satu pun dari pertanyaan ini bisa dijawab oleh Lean.

Yuen mengakui bahwa ia sampai sekarang masih mencerna bukti ini.

Jawabannya ada di depan matanya, tetapi ia harus membacanya seperti membaca makalah orang awam, baris demi baris, untuk merekonstruksi intuisi yang tidak diucapkan oleh AI.

Ya, memang ada bukti Lean di sana. Tapi itu hanya formalitas, tidak berarti saya benar-benar mengerti. Untuk benar-benar memahaminya, mungkin hanya waktu yang bisa mengolahnya perlahan.

Memang, AI memperluas batas pemahaman manusia, tapi lalu apa? Apa yang tersisa dari kesenangan dan makna penelitian? Jika AI menyelesaikan semua masalah yang selalu ia pikirkan, apa yang tersisa baginya?

Pertanyaan datang bertubi-tubi. Tetapi satu hal yang semakin ia yakini: matematikawan tidak akan punya waktu luang dalam hari-hari mendatang—ia harus mengendalikan raksasa-raksasa pemikiran ini sekaligus menerjemahkan istilah teknis mereka menjadi bahasa yang mudah dipahami.

Minggu lalu, Ramana Kumar membantah teka-teki matematika paling terkenal, "Konjektur Collatz", dengan hanya 300 baris Lean.

Pertanyaannya sangat sederhana: Diberikan bilangan bulat positif, lakukan operasi berulang sesuai dua aturan—jika genap, bagi dengan 2; jika ganjil, kalikan dengan 3 lalu tambah 1—apakah akhirnya, tidak peduli dari angka mana pun Anda memulai, Anda akan selalu turun hingga mencapai 1?

Anda bisa menghitungnya:

Teori ini menyatakan bahwa tidak peduli bilangan bulat positif mana yang Anda mulai, Anda akhirnya akan jatuh ke dalam lingkaran 4→2→1.

Masalah ini belum terbukti benar maupun ditemukan contoh penyangkalnya sejak diusulkan oleh matematikawan Lothar Collatz pada tahun 1937.

It was called by mathematician Paul Erdős: "Mathematics is not yet ready for such problems," and by American Academy of Sciences member and mathematician Jeffrey Lagarias: "This is an extraordinarily difficult problem, completely beyond the reach of contemporary mathematics."

Jika dibuktikan salah, ini pasti menjadi berita bombastis di dunia matematika.

Sayangnya, tiga hari kemudian, bukti Lean formal ini dinyatakan tidak sah, karena sebenarnya hanya memanfaatkan celah bawah di inti Lean.

Daniel Selsam dari OpenAI, dengan bantuan AI yang berspesialisasi dalam keamanan siber, membantu Lean FRO melakukan audit kernel.

Hasilnya, mereka menemukan lebih dari satu kerentanan di dalam inti Lean!

Pada waktu yang hampir bersamaan, profesor matematika dari Universitas Rutgers dan penasihat organisasi penelitian Lean, Alex Kontorovich, memposting peringatan: Jangan anggap Lean sebagai validator serba bisa.

Dia langsung menargetkan titik lemahnya—semantic alignment.

Meskipun inti Lean tak terbantahkan, Lean hanya bertanggung jawab atas kompilasi kode. Siapa yang memastikan bahwa "definisi" yang Anda tulis dalam kode sama dengan "niat intuitif" manusia dalam bahasa alami?

Yang dapat dikonfirmasi oleh Lean hanyalah satu hal: kode berhasil dikompilasi dan logika formalnya benar. Namun, Lean sama sekali tidak memverifikasi masalah yang lebih krusial: apakah pernyataan formal ini benar-benar sesuai dengan teorema yang ingin Anda buktikan?

Bukti teorema benar, soalnya salah disalin, Lean tetap memberikan lampu hijau.

Namun, masalah penyelarasan ini tidak bisa diselesaikan semata-mata oleh komputer.

Dalam pidatonya di ICM 2026, Kontorovich menunjukkan: celah terbesar dalam matematika formal terletak bukan pada "menghasilkan turunan yang benar", melainkan pada "mengucapkan hal yang benar". Yang akhirnya menjadi penjaga terakhir tetaplah para ahli manusia.

Liquid Tensor Experiment pada masa itu menjadi legenda justru karena para peneliti melakukan tinjauan manual hampir obsesif terhadap setiap definisi matematis.

Dengan mempertimbangkan pernyataan kedua profesor tersebut bersama-sama, hal ini menunjukkan fakta yang sama: AI dapat membuktikan, mesin dapat memverifikasi, tetapi pemahaman dan pengawasan tetap menjadi tugas manusia.

Terakhir, ada gosip tentang model inferensi AI:

Referensi:

https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/

https://x.com/AlexKontorovich/status/2083919186825236831

https://x.com/henryquantum/status/2083623700608237956

Artikel ini berasal dari akun WeChat "Sinzhiyuan", penulis: ASI Revelation; editor: David