Vitalik: Bahasa pemrograman tingkat lanjut yang baru patut dicoba harus membuat definisi dan teorema lebih mudah dibaca oleh orang.

Odaily melaporkan bahwa Vitalik memposting di platform X mengatakan bahwa salah satu jenis "bahasa pemrograman tingkat lanjut" baru yang layak dicoba adalah bahasa yang dikompilasi ke dalam Lean (atau HOL dan sejenisnya), dengan fokus agar manusia dapat membaca definisi dan teorema semudah mungkin. Bukan pembuktiannya, karena yang penting dari pembuktian adalah kebenarannya; kunci utama terletak pada definisi dan teorema itu sendiri. Vitalik membayangkan penggunaannya adalah ketika AI menghasilkan pembuktian yang sangat panjang, pembaca harus dapat dengan mudah memahami klaim spesifik apa yang benar-benar dibuktikan dari output tersebut.