Vitalik 提议开发可编译为 Lean 的高级编程语言，以提升 AI 证明的可读性

深潮 TechFlow 消息，7 月 21 日，据 Vitalik Buterin（@VitalikButerin）发文表示，其建议开发一种新型高级编程语言，该语言可编译为 Lean（或 HOL 等形式化验证工具），核心目标是让人类尽可能轻松地阅读定义与定理内容（而非证明本身）。其设想的使用场景为：AI 负责输出证明内容，而该语言则帮助读者快速理解 AI 所证明的具体命题。