Model penalaran terbaru internal OpenAI merilis sepuluh kemajuan matematika yang menakjubkan sekaligus.
Di antaranya termasuk:
- Pembuktian pertama kali keberadaan grup Non-sofic (Non-sofic groups);
- Memberikan batas bawah rangkaian (Circuit lower bounds) yang benar-benar baru;
- Menaklukkan batas kesulitan masalah vektor terdekat (Closest Vector Problem, CVP);
- Serta teorema peluruhan eksponensial pengulangan paralel permainan kuantum dua pemain (Quantum parallel repetition).
Yang paling diperhatikan oleh Associate Professor Universitas Columbia, Henry Yuen, adalah yang terakhir—
Tahun 2016, Yuen mencapai kemajuan signifikan pada masalah ini, tetapi belum menyelesaikannya secara tuntas. Selama 10 tahun, ia terus mencoba dan gagal, bahkan sebulan yang lalu ia menggunakan ChatGPT 5.5 sekali lagi untuk menyerang pembuktian akhir, tetapi hasilnya sangat sedikit.
Sementara AI, di atas pundaknya, dengan ringan mengentakkan kaki, memasukkan bola ke gawang.
Buktinya Benar, Tapi Manusia Tidak Memahami
Beberapa hari yang lalu, Lijie Chen mengirimkan draf makalah kepada Henry Yuen dan beberapa orang lainnya.
Saat itu hidupnya sibuk, ia tidak sempat mempelajarinya secara mendalam. Sekarang, makalah tersebut telah dipublikasikan. Ia tidak tahan lagi, ada yang ingin dikatakan.
Teorema pengulangan paralel kuantum (Quantum parallel repetition theorem), adalah bidang yang dihabiskan Henry Yuen selama bertahun-tahun dengan susah payah di masa studi pascasarjana, dan juga merupakan hasil yang paling ia banggakan.
Henry Yuen, saat ini Associate Professor Ilmu Komputer Keluarga Srivani di Universitas Columbia
Ia ingat sore-sore yang dihabiskan di kafe, larut malam di kantor, dan akhir pekan yang seharusnya istirahat, berulang kali membongkar dan mempelajari teorema pengulangan paralel klasik Ran Raz.
Ia ingin menyelesaikan versi kuantum dari teorema ini, hingga tidak bisa tidur, gelisah. Ia menelan berton-ton alat matematika, dan akhirnya berhasil membuktikan peluruhan polinomial.
https://arxiv.org/pdf/1604.04340
Yang lebih penting, ia membangun kepercayaan diri dari sana, akhirnya menyadari kemampuannya sendiri, membuktikan bahwa ia memang bisa menyelesaikan masalah-masalah (setidaknya sebagian) yang juga dipedulikan orang lain.
Ia percaya pembuktian OpenAI ini seharusnya benar, mengingat sudah ada bukti formalisasi Lean. Tapi untuk mencerna bukti baru ini, Henry Yuen masih butuh waktu.
Meskipun bukti baru ini memang melanjutkan dari tempat ia berhenti sebelumnya, AI berhasil menembus batasan strategi pembuktian aslinya, menggunakan beberapa trik dan metode. Metode-metode ini mungkin sudah dikuasai oleh peneliti di bidang teori operator (operator theory) dan analisis fungsional (functional analysis).
Selain kegembiraan, perasaan pertama Yuen adalah kekecewaan, kekecewaan pada gaya penulisan makalah.
Ia mengatakan pembuktian ini terasa penuh aroma AI: pengantar yang panjang berbelit-belit, tetapi pada bagian kunci tiba-tiba seperti sulap, membuat orang bingung.
Bukti OpenAI ini, dibaca cukup menarik, tapi juga agak membuat pusing.
Pertama-tama masalah diletakkan dengan rapi di atas meja, lalu tiba-tiba melompat ke arah "menggunakan resolvent untuk mencari purifikasi yang tepat", hampir tidak menyisakan tangga logika di antaranya.
Selanjutnya, serangkaian perhitungan entropi matriks yang agak tidak biasa, berbelit-belit terus dihitung, akhirnya memberi tahu: jalan ini bisa dilalui.
Tapi langkah yang paling krusial, dari mana intuisi itu berasal, tidak dijelaskan.
Dan sentuhan paling jenius, paling menguji kreativitas itu—teknik memperluas ruang operator menggunakan transformasi Uhlmann (Uhlmann transformation), seharusnya menjadi klimaks yang paling mendebarkan dari seluruh pembuktian, malah dibuang oleh AI seperti sampah, tanpa peringatan, tanpa penjelasan, diletakkan di bagian keempat.
Bukti yang benar, tetapi menyembunyikan ide terpenting.
Ia berharap OpenAI bisa menghabiskan beberapa prompt lagi, untuk menyusun naskah ini dengan baik.
Yang lebih menyakitkan adalah lapisan kedua: Verifikasi Lean lolos, tidak sama dengan memahami.
Mesin bisa menjamin setiap langkah deduksi tak terbantahkan, tetapi "mengapa trik ini efektif", "apa artinya dalam peta teori yang lebih besar", "bisa digunakan di mana lagi" — pertanyaan-pertanyaan ini, Lean tidak bisa menjawab satu pun.
Yuen mengakui, sampai sekarang ia masih mencerna bukti ini.
Jawaban sudah ada di depan mata, tetapi ia harus seperti membaca makalah orang awam, baris demi baris merekonstruksi intuisi yang tidak diucapkan oleh AI.
Benar, ada bukti Lean di sana. Tapi itu hanya formalisasi, tidak berarti saya paham. Untuk benar-benar mencernanya, mungkin hanya bisa mengandalkan waktu yang perlahan-lahan mengikis.
Memang, AI memperluas wilayah pemahaman manusia, tetapi lalu apa? Kesenangan dan makna penelitian tinggal apa? Jika AI menyelesaikan semua masalah yang selalu ia pikirkan, apa lagi yang tersisa baginya?
Pertanyaan datang bertubi-tubi. Tetapi ada satu hal yang semakin ia yakini: hari-hari berikutnya para matematikawan tidak akan menganggur, harus menjinakkan makhluk pemikiran raksasa ini, sekaligus menerjemahkan bahasa gaul mereka ke bahasa manusia.
AI "Membantah" Dugaan Matematika Berusia Ratusan Tahun Ternyata Palsu! Lean Bukan Kotak Penyimpanan Aman
Minggu lalu, Ramana Kumar menggunakan 300 baris Lean untuk membantah dugaan matematika paling terkenal yang belum terpecahkan "Dugaan Collatz" (Collatz conjecture).
Pertanyaannya sangat sederhana: diberikan sebuah bilangan bulat positif, ikuti dua aturan berulang kali—jika genap bagi dengan 2, jika ganjil kalikan dengan 3 lalu tambah 1—apakah pada akhirnya, tidak pedulidari bilangan berapa pun memulai, akan selalu jatuh ke 1?
Anda bisa menghitungnya:
Dugaan ini mengatakan bahwa: tidak peduli bilangan bulat positif mana yang Anda ambil sebagai awal, akhirnya akan jatuh ke lingkaran 4→2→1 ini.
Masalah ini sejak diajukan oleh matematikawan Lothar Collatz pada tahun 1937, tidak ada yang bisa membuktikannya benar, dan tidak ditemukan contoh penyangkal.
Hal ini disebut oleh matematikawan Paul Erdős sebagai: "Matematika belum siap menghadapi masalah seperti ini", sedangkan anggota Akademi Ilmu Pengetahuan Nasional AS, matematikawan Jeffrey Lagarias, berpendapat "ini adalah masalah yang sangat sulit, sepenuhnya di luar jangkauan matematika saat ini".
Jika dibantah, tentu saja akan menjadi berita yang menggemparkan dunia matematika.
Sayangnya, 3 hari kemudian, bukti formal Lean ini dinyatakan tidak valid, karena sebenarnya hanya memanfaatkan celah lapisan dasar kernel Lean.
Daniel Selsam dari OpenAI, bersama sebuah AI yang khusus mengarahkan keamanan siber, membantu Lean FRO melakukan audit kernel.
Hasilnya, mereka menemukan tidak hanya satu, tetapi beberapa celah di kernel Lean!
Hampir bersamaan, profesor matematika Universitas Rutgers, penasihat organisasi penelitian khusus Lean, Alex Kontorovich, memposting peringatan: jangan anggap Lean sebagai verifikator serba bisa.
Ia menunjuk langsung ke titik mati—penyelarasan semantik (Semantic Alignment).
Bahkan jika kernel Lean sempurna, Lean hanya mengurusi kompilasi kode. Siapa yang memastikan "definisi" yang Anda tulis dalam kode itu sama dengan "intuisi maksud" manusia dalam bahasa alami?
Lean hanya bisa memastikan satu hal: kode berhasil dikompilasi, logika formalnya tidak salah. Tetapi sama sekali tidak memverifikasi masalah yang lebih krusial: Pernyataan formal ini, apakah benar-benar sesuai dengan teorema yang ingin Anda buktikan?
Teoremanya terbukti benar, soalnya salah salin, Lean tetap akan memberi lampu hijau.
Dan masalah penyelarasan ini, tidak bisa diselesaikan murni oleh komputer.
Dalam pidatonya di ICM 2026, Kontorovich pernah menekankan: titik buta terbesar matematika formalisasi, bukan pada "menurunkan dengan benar", tetapi pada "mengatakan dengan benar". Yang terakhir memeriksa, tetap harus pakar manusia.
Eksperimen Liquid Tensor yang dulu dianggap luar biasa, justru mengandalkan pemeriksaan manual yang hampir obsesif oleh peneliti terhadap setiap definisi matematika.
Menyatukan pernyataan dua profesor ini, menunjuk pada fakta yang sama: AI bisa membuktikan, mesin bisa memverifikasi, tetapi memahami dan mengawasi, tetap tugas manusia.
Terakhir, ada juga gosip tentang model penalaran 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 "新智元", penulis: ASI启示录; editor: 大卫
