Tantangan AI dalam Membuktikan Matematika: Bukti yang Meyakinkan tapi Sulit Dipahami

Beberapa matematikawan terkemuka mengadakan pertemuan rahasia pada tahun 2025 untuk menguji kemampuan model bahasa besar AI terbaru, o4-mini, dalam memberi bukti matematis. Mereka terkagum-kagum dengan bagaimana jawaban AI terasa seperti diberikan oleh matematikawan sejati yang menguraikan bukti rumit. Namun, ada keraguan apakah AI tersebut benar-benar layak mendapat pujian atau hanya sekadar meyakinkan dalam penyampaian. Ken Ono dan Terry Tao mengingatkan bahwa AI mampu menyampaikan argumen dengan sangat percaya diri meskipun bisa jadi tidak benar. Hal ini memperbesar risiko menerima bukti yang salah karena tampaknya sangat meyakinkan. Sebelumnya, kepiawaian seorang matematikawan dalam menyusun argumen menjadi tanda kebenaran, namun AI telah menghilangkan sinyal tersebut. Sejarah pembuktian matematis pun tidak luput dari kesalahan seperti yang dialami Andrew Wiles dengan bukti Teorema Terakhir Fermat yang awalnya terdapat kekeliruan. Untuk menghindari kesalahan yang tidak terdeteksi akibat ambiguitas bahasa, saat ini berkembang metode formal verification yaitu penerjemahan bukti ke format yang sangat rinci dan logis, yang dapat diuji oleh komputer secara ketat. Matematikawan seperti Kevin Buzzard mendorong penggunaan AI bersama sistem seperti Lean, sehingga AI dapat menghasilkan bukti dalam bahasa formal, diverifikasi secara otomatis, dan diperbaiki bila ditemukan kesalahan. Meski demikian, ada kemungkinan di masa depan AI akan menghasilkan bukti yang terlalu kompleks hingga tidak lagi bisa dipahami manusia, menimbulkan dilema filosofis tentang tujuan matematika. Selain itu, penggunaan komputer dan AI dalam pembuktian sudah berlangsung lama, seperti pada teorema empat warna, namun peran AI yang kini mampu mengusulkan dan memverifikasi bukti secara menyeluruh merupakan paradigma baru. Dunia matematika harus mulai mempersiapkan diri menghadapi era di mana bukti bermutu tinggi bisa dihasilkan tanpa pemahaman manusia penuh.