Vitalik提议开发面向人类阅读的Lean编译语言

BiRun 消息，以太坊创始人 Vitalik Buterin 在 X 平台表示，值得尝试开发一种新的高级编程语言，该语言可编译为 Lean 或 HOL 等形式化验证系统。其核心目标是让人类更轻松地阅读定义和定理，而非证明过程，因为证明的正确性由机器保证。该语言的预期应用场景是辅助人类审查 AI 生成的证明代码块，降低阅读门槛。