Vitalik：值得嘗試的新型高級程式語言應讓人更容易閱讀定義和定理

Odaily 報導，Vitalik 在 X 平台發文表示，一種值得嘗試的新型「高級程式語言」是編譯為 Lean（或 HOL 等）的語言，重點是盡可能讓人類更容易閱讀定義和定理。重點不是在於證明本身，因為只要證明是正確的即可，關鍵在於定義和定理本身。他設想的用途是，AI 輸出大量的證明，而讀者需要能夠盡可能輕鬆地理解這些輸出實際證明了哪些精確的主張。