Vitalik: Seharusnya mencoba membuat bahasa bukti baru yang “dapat dibaca” untuk meningkatkan pemahaman manusia terhadap bukti yang dihasilkan AI

PANews 21 Juli, Vitalik Buterin, salah satu pendiri Ethereum, mengusulkan untuk mengeksplorasi bahasa pemrograman tingkat lanjut baru yang dapat dikompilasi menjadi sistem pembuktian teorema seperti Lean, HOL, dan lainnya, dengan fokus mengoptimalkan keterbacaan “definisi dan teorema”, bukan proses pembuktiannya sendiri. Vitalik menyebut bahwa skenario target bahasa ini adalah setelah AI menghasilkan bukti formal berskala besar, bahasa tersebut membantu manusia memahami dengan jelas apa sebenarnya yang “dibuktikan secara formal” oleh bukti-bukti tersebut, sehingga pembaca bisa lebih mudah meninjau dan memverifikasi klaim matematika dan logika spesifik yang diberikan AI.