今天（7 月 21 日），以太坊联合创始人维塔利克·布特林提出创建一种新的高层编程语言。该语言可编译到诸如 Lean 和 HOL 之类的形式化证明系统，从而优化定义与定理的可读性，而非证明过程本身。根据 PANews，布特林表示，该语言旨在帮助人类清楚理解 AI 生成的大规模形式化证明在数学与逻辑层面所展示的内容，使读者能够更容易地审计并核实 AI 所提出的具体主张。