JAKARTA — Platform Palomar, sebuah registry untuk memverifikasi bukti matematika formal dalam bahasa pemrograman Lean, resmi dibuka untuk penerimaan kiriman. Inisiatif yang diinkubasi oleh Lean FRO dan ICARM ini hadir sebagai solusi untuk mengatasi meluasnya bukti yang dihasilkan AI dalam beberapa bulan terakhir.
Tantangan yang dihadapi komunitas matematika saat ini cukup kompleks. Dengan semakin banyaknya bukti berbasis AI yang diformalkan dalam Lean, memverifikasi apakah repository Lean benar-benar membuktikan pernyataan yang diklaim menjadi tugas tidak trivial.
Apalagi bagi audiens yang tidak ahli dalam penggunaan Lean, mereka harus memastikan bahwa pernyataan formal Lean memiliki bukti yang lolos typechecking, tanpa “kecurangan” seperti menambahkan aksioma tambahan, dan deskripsi informal cocok dengan hasil formal.
Palomar dirancang sebagai analog dari server preprint untuk bukti Lean. Registry ini mencatat repository eksternal di Github yang berisi kode Lean mengikuti praktik terbaik, dilengkapi tiga komponen utama: “challenge file” (deskripsi singkat hasil yang diklaim), “solution module” (bukti arbitrer panjang), dan “formalization.yaml” (penjelasan informal dengan metadata relevan).
Sistem Verifikasi Dua Lapisan
Ketika repository disubmisikan ke Palomar, sistem melakukan dua pemeriksaan berbeda. Pertama, verifikasi mekanis menggunakan tool Lean Comparator untuk memastikan solution module berhasil typechecking dan membuktikan hasil persis seperti diklaim.
Kedua, model bahasa besar melakukan pemeriksaan non-deterministik untuk memastikan deskripsi informal di formalization.yaml cocok dengan pernyataan challenge file dan repository memenuhi standar minimal registry.
Penting dicatat bahwa kedua pemeriksaan ini masih jauh dari peer review manusia yang mendalam mengenai novelty, ketertarikan, dan akurasi. Palomar bukan jurnal peer-reviewed, melainkan platform registrasi untuk menjamin transparansi dan konsistensi formal.
Terence Tao, matematikawan terkemuka yang menjabat di scientific advisory board bersama Jeremy Avigad, Matthew Ballard, dan ilmuwan lainnya, telah berhasil menguji proses submisi. Dia berhasil mensubmisikan formalisasi bukti Sendov’s conjecture miliknya sendiri ke Palomar dan merencanakan mengajukan formalisasi lama lainnya segera.
Terbuka untuk Semua Jenis Formalisasi
Registry kini menerima formalisasi hasil baik baru maupun lama. Submisi—baik yang dihasilkan manusia, AI, atau campuran keduanya—disambut. Proses submisi dianggap menyeluruh namun dapat dicapai. Tim mencatat bahwa agen AI modern sangat membantu dalam menangani detail mekanis submisi, meskipun review manusia tetap sangat direkomendasikan sebelum pengajuan final.
Tao menekankan bahwa Palomar hadir untuk membawa kejelasan dalam situasi proliferasi bukti AI. Dengan standar verifikasi yang jelas dan transparan, komunitas matematika dapat lebih percaya diri dalam mengadopsi dan membangun atas hasil-hasil baru yang diformalkan, seiring transformasi matematika menuju era formal verification yang lebih kuat.
📝 Tinggalkan Komentar
Komentar sebagai . Ditinjau admin sebelum tampil.