AI membantu membuat “proof” Collatz tanpa sorry. Masalahnya, proof itu ternyata bisa lolos karena bug di kernel Lean. Bukan karena matematika Collatz tiba-tiba runtuh, dan bukan juga bukti bahwa formal verification tidak berguna. Ini cerita tentang sesuatu yang lebih penting buat developer: tool yang memeriksa kebenaran tetaplah software, jadi implementasinya tetap harus diuji, dipatch, dan diaudit.

Kalau lu memakai AI untuk menulis kode, proof, query, atau konfigurasi yang terlihat formal, pelajarannya sederhana: output yang lolos checker belum otomatis berarti benar. Lu perlu tahu apa yang dipercaya oleh sistem, bagian mana yang masuk trusted computing base, dan bagaimana hasil itu diverifikasi secara independen.

Apa yang sebenarnya terjadi di Lean?

Lean adalah proof assistant: software yang membantu menulis pembuktian formal lalu memeriksa apakah setiap langkahnya mengikuti aturan logika yang sudah ditentukan. Kernel Lean adalah bagian paling dipercaya dalam proses itu. Kalau kernel menolak proof yang valid, itu masalah usability. Kalau kernel menerima proof yang tidak valid, itu masalah soundness.

Pada 25 Juli 2026, Ramana Kumar mempublikasikan repository berisi “disproof” terhadap Collatz conjecture yang dibuat dengan bantuan AI. Proof tersebut tidak memakai sorry. Namun pada 28 Juli, Kiran Gopinathan mereduksinya menjadi proof kecil dari False dan melaporkan issue #14576 di repository Lean.

Intinya, proof itu memanfaatkan bug pada cara kernel menangani nested inductive types dan projection. Ada argumen yang seharusnya diperiksa, tetapi bisa lolos dalam jalur tertentu. Hasil akhirnya absurd: Lean menerima deklarasi yang memungkinkan pembuktian False tanpa aksioma tambahan.

Detail ini penting karena headline “AI membuktikan Collatz salah” sangat menyesatkan. Yang terjadi bukan penemuan matematika baru. Yang terjadi adalah AI-assisted exploration menemukan input yang memicu bug implementasi pada proof checker.

Formal verification bukan jaminan magis

Formal verification sering terdengar seperti lapisan terakhir yang tidak mungkin salah. Secara ideal, sistem formal memang memberi jaminan jauh lebih kuat daripada test biasa. Tetapi jaminan itu bergantung pada beberapa komponen: teori yang dipakai, kernel yang mengimplementasikannya, parser atau elaborator di depannya, format artifact, dan proses verifikasi yang dijalankan.

Leonardo de Moura, chief architect Lean, menyebut kasus ini sebagai implementation bug, bukan lubang pada meta-theory Lean. Pembedaan ini bukan basa-basi teknis. Teori logikanya tidak otomatis menjadi salah hanya karena implementasi kernel-nya punya missing check.

Analogi sederhananya: aturan permainan bisa benar, tetapi referee yang menjalankan aturan tetap bisa salah membaca situasi. Karena itu, “sudah dicek secara formal” harus dibaca sebagai pernyataan dengan scope yang jelas: dicek oleh checker versi apa, terhadap artifact apa, dengan asumsi apa?

Kenapa independent checker juga bisa gagal?

Kasus ini makin menarik karena repository tersebut juga lolos versi lama nanoda, sebuah independent kernel atau proof/type checker untuk Lean yang ditulis dalam Rust. Seharusnya checker independen menambah kepercayaan karena implementasinya berbeda dari kernel utama.

Ternyata ada dua bug yang tidak berhubungan. Kernel resmi punya bug pada nested inductive type. Versi lama nanoda punya bug lain: tidak memeriksa type name pada projection node. Proof tersebut dirancang sedemikian rupa sehingga dua bug itu bisa saling menutupi.

Ini bukan alasan untuk menyerah pada independent verification. Justru sebaliknya: ini menunjukkan kenapa versi checker dan proses update sangat penting. Leonardo menulis bahwa independent checking tetap berguna, tetapi pengguna harus memakai versi terbaru dari kedua implementasi.

Dengan kata lain, menambah checker bukan berarti “satu kali pasang lalu selesai”. Checker juga punya lifecycle. Ada release, regression test, advisory, dan patch yang harus diikuti.

AI membantu menemukan edge case, bukan memegang kebenaran

Bagian paling relevan buat workflow AI adalah peran AI dalam cerita ini. AI tidak duduk sebagai hakim terakhir. AI membantu menghasilkan atau mengeksplorasi kode yang kemudian diperiksa manusia dan tool lain. Ketika output-nya terlihat meyakinkan, manusia tetap perlu bertanya: apakah ini benar-benar proof, atau hanya artifact yang berhasil melewati celah checker?

Pola ini mirip dengan AI coding agent. Agent bisa menghasilkan test yang hijau, tetapi test-nya mungkin tidak menguji behavior penting. Agent bisa membuat migration yang jalan, tetapi constraint datanya salah. Agent bisa memberi query yang valid secara sintaks, tetapi hasil bisnisnya keliru.

“Lolos pemeriksaan” adalah bukti bahwa pemeriksaan tertentu berhasil, bukan bukti universal bahwa semua asumsi sudah benar.

Checklist saat memakai output AI yang terlihat formal

Gua akan memakai checklist ini saat menerima output AI untuk kode, proof, security config, atau data pipeline:

  • Definisikan klaimnya. Apa yang sebenarnya dibuktikan? Jangan puas dengan output yang hanya terlihat rapi.
  • Cek asumsi dan boundary. Versi compiler, kernel, library, model, input, dan environment apa yang dipakai?
  • Uji dengan kasus kecil. Reduksi minimal sering lebih mudah dibaca daripada artifact besar yang dibuat agent.
  • Pakai verifikasi independen bila risikonya tinggi. Beda implementasi bisa menemukan bug yang luput dari tool utama.
  • Update checker dan dependency. Regression fix tidak berguna kalau environment lu masih memakai versi lama.
  • Simpan bukti proses. Commit, command, versi tool, hasil test, dan review lebih berguna daripada chat history panjang.
  • Bedakan hasil dari otoritas. AI boleh membantu menghasilkan kandidat. Keputusan merge, publish, atau klaim tetap ada di manusia.

Pelajaran buat developer yang tidak memakai Lean

Lu tidak harus belajar theorem proving untuk mengambil pelajaran dari bug ini. Setiap stack punya “kernel” atau komponen yang menerima input sebagai benar: compiler, type checker, validator schema, migration runner, policy engine, CI, sampai sistem permission.

Semakin tinggi trust yang lu berikan ke sebuah komponen, semakin penting lu memahami failure mode-nya. Jangan cuma bertanya “tool ini pintar atau tidak?”. Tanya juga:

  • Bagian mana yang benar-benar memutuskan sesuatu?
  • Apa yang tidak diperiksa oleh tool ini?
  • Apakah ada cara menjalankan checker kedua?
  • Bagaimana bug dilaporkan dan dipatch?
  • Apakah artifact bisa direproduksi dari source dan versi tool yang sama?

Ini juga alasan kenapa supply chain dan reproducible build penting. Kode lu mungkin benar, tetapi hasil yang diproduksi environment berbeda belum tentu sama. Trust bukan cuma soal siapa yang menulis kode. Trust juga soal siapa yang memeriksa, dengan versi apa, dan apakah prosesnya bisa diulang.

Kesimpulan singkat

Bug Lean ini bukan argumen melawan AI atau formal verification. Menurut gua, ini justru contoh sehat tentang bagaimana sistem yang serius seharusnya merespons: bug direduksi menjadi kasus kecil, dilaporkan, diperbaiki cepat, regression test ditambahkan, dan proses verifikasi diperkuat.

Pelajaran utamanya: AI bisa membantu menemukan edge case, formal tool bisa mempersempit ruang kesalahan, tetapi kebenaran tetap membutuhkan proses verifikasi yang bisa diaudit. Kalau lu mengirim hasil kerja, lu tetap pemilik keputusan dan tanggung jawabnya—meskipun sebagian besar draft awal datang dari AI.

FAQ

Apakah Lean “rusak total” karena bug ini?

Nggak. Postmortem Lean mengklasifikasikannya sebagai bug implementasi pada kernel, bukan kerusakan meta-theory. Bug sudah direduksi, diperbaiki, dan patch release diterbitkan.

Apakah AI benar-benar menemukan bug tersebut?

Repository awal dibuat dengan bantuan AI, lalu manusia mereduksi dan melaporkan bug-nya. Jadi framing yang aman adalah AI membantu eksplorasi; validasi, diagnosis, dan perbaikannya tetap melibatkan manusia.

Apakah independent checker selalu cukup?

Nggak selalu. Independent checker menambah lapisan verifikasi, tetapi implementasinya juga bisa punya bug. Pakai versi terbaru dan pahami scope jaminannya.

Referensi / Bacaan Lanjut

Tags:
#AI#Software Development#Formal Verification#Developer Education