Vitalik：应尝试创建新型“可读性证明语言”以提升人类理解 AI 生成证明

Ethereum 联合创始人 Vitalik Buterin 提出，应探索一种可编译为 Lean、HOL 等定理证明系统的新型高级编程语言，重点优化“定义与定理”的可读性，而非证明过程本身。Vitalik 称，该语言的目标场景是 AI 输出大规模形式化证明后，帮助人类清晰理解这些证明究竟“形式化地证明了什么”，即让读者更容易审视与核查 AI 所给出的具体数学与逻辑主张。