Berita viral dari dunia sains: konjektur KLS yang terbuka sejak 1995 akhirnya terbukti. Dua peneliti menyelesaikan teka-teki geometri dimensi tinggi itu lewat proses riset yang diarahkan manusia, dengan agen AI menjelajahi lebih dari 100 pendekatan kandidat. Bukti lengkapnya dipublikasikan di arXiv pada awal Oktober 2026.
Berita Viral: Apa Itu Konjektur KLS
Konjektur Kannan, Lovasz, dan Simonovits diajukan pada 1995. Pertanyaannya sederhana untuk diucapkan, tetapi sangat sulit dibuktikan. Apakah potongan datar terbaik pada sebuah bangun cembung selalu hampir sebaik potongan berbentuk apa pun, dengan selisih yang dibatasi konstanta universal tanpa bergantung jumlah dimensi.
Jika jawabannya ya, maka ada prinsip geometri yang berlaku di semua dimensi. Prinsip itu penting karena memengaruhi cara algoritma acak menjelajahi ruang berdimendi tinggi. Selama tiga dekade, para matematikawan mengumpulkan bukti bahwa konjektur ini benar, tetapi pembuktian penuh belum ada. Penjelasan rinci ada di blog Microsoft Research.
Sebelum hasil ini, batas terbaik yang diketahui masih membesar perlahan seiring naiknya jumlah dimensi. Hasil Juli 2026 memperbolehkan batas itu tumbuh lambat, tetapi belum konstan. Pembuktian baru menghapus ketergantungan pada dimensi sepenuhnya.
Makalahnya berjudul An O(1) Bound for the KLS Constant, ditulis Zhao Song dan Xinzhi Zhang. Versi pertama masuk arXiv pada 1 Oktober 2026, versi kedua pada 4 Oktober 2026, dengan total 140 halaman. Abstrak makalah tersedia di arXiv.
Iklan
Paviliun Akademika: punya kost tanpa repot kelola
Paviliun Akademika menghadirkan pilihan investasi kost terkelola di Akademika Townhouse, Gowa. Unit disiapkan untuk disewakan, dengan pengelolaan kawasan yang ditangani pemilik proyek.
Siapa Penelitinya
Xinzhi Zhang adalah peneliti di kelompok Machine Learning and Optimization, Microsoft Research. Ia bekerja bersama Zhao Song sebagai kolaborator di luar Microsoft. Blog resmi Microsoft menyebut hasil ini sebagai terobosan ilmiah mendasar, bukan sekadar kemajuan teknis.
Keduanya memulai dengan memperbaiki hasil Juli 2026 agar batas matematisnya lebih presisi. Mereka lalu bekerja dengan agen AI dalam proses terstruktur. Agen menjelajahi lebih dari 100 pendekatan kandidat, banyak di antaranya melibatkan perhitungan tensor tingkat tinggi yang panjang.
Dari penjelajahan itu muncul kriteria matematis baru yang menjadi fondasi pembuktian akhir. Para peneliti lalu menemukan bahwa kriteria tersebut bisa diterapkan secara rekursif. Setiap batas yang membaik bisa dimasukkan kembali ke argumen yang sama untuk menghasilkan batas lebih ketat.
Peran Agen AI dalam Pembuktian
Pada versi 1 Oktober 2026, ketergantungan pada dimensi turun menjadi iterated logarithm. Fungsi itu tumbuh sangat lambat, tetapi tetap tumbuh. Karena itu, pembuktian belum sepenuhnya menyelesaikan konjektur.
Versi 4 Oktober 2026 menghapus ketergantungan itu dan menuntaskan pembuktian. Menurut blog Microsoft, agen AI membantu menjelajahi pendekatan, menjalankan derivasi rinci, menyiapkan manuskrip, dan melakukan pemeriksaan internal. Namun arah matematisnya ditentukan manusia.
Para peneliti memilih ide yang menjanjikan, menyusunnya menjadi argumen akhir, dan memverifikasi hasilnya. Tanpa arahan manusia, menurut blog itu, beberapa model terkemuka gagal dengan anggaran token serupa. Ini pembeda penting antara alat bantu dan penemu.
Kombinasi itu menunjukkan pola kerja yang mulai muncul di riset matematika. Manusia memegang kendali arah, mesin mempercepat pencarian. Hasilnya bukan AI yang menggantikan matematikawan, melainkan proses riset yang lebih cepat. Rubrik ini pernah membahas agen AI yang membantu riset ilmiah.
Konfirmasi Independen dan Verifikasi Mesin
Pada hari yang sama ketika makalah lengkap diposting, kelompok ahli lain memposting pembuktian penuh yang dikembangkan secara paralel. Kelompok itu menyebut versi pertama makalah Microsoft sebagai langkah krusial dalam pembuktian. Makalah pembuktian independen ada di arXiv.
Pembuktian ketiga juga muncul pada hari yang sama dengan ide yang berhubungan erat. Selain itu, formalisasi Lean 4 dirilis untuk memeriksa sebagian argumen secara mekanis. Formalisasi itu menggabungkan kriteria kunci dari makalah pertama dengan riset tambahan. Repositori formalisasi tersedia di GitHub.
Konfirmasi independen penting karena pembuktian matematika tidak cukup dengan satu makalah. Ketika beberapa kelompok sampai pada hasil yang sama dengan jalur berbeda, keyakinan komunitas meningkat. Formalisasi mesin menambah lapisan pemeriksaan yang tidak bergantung pada penilaian manusia.
