今天（7 月 21 日），以太坊联合创始人 Vitalik Buterin 提议创建一种新的高级编程语言，该语言有可能编译到 Lean 和 HOL 等形式化证明系统之上，以便优化对定义和定理的可读性，而不是对证明过程本身进行优化。据 PANews 报道，Buterin 表示，该语言旨在帮助人类清晰理解由 AI 生成的大规模形式化证明在数学和逻辑层面所表达的内容，从而让读者更容易检验和验证 AI 提出的具体断言。