Vitalik：新型高级编程语言应让人更易阅读定义和定理

Vitalik在X平台表示，一种值得尝试的新型高级编程语言是编译为Lean或Hol等的语言，重点是让人类更容易阅读定义和定理，而非证明，因为AI输出证明时，读者需要轻松理解其中被证明的精确主张。