今天（7 月 21 日），以太坊联合创始人维塔利克·布特林提出创建一种新的高层编程语言。该语言可编译到诸如 Lean 和 HOL 之类的形式化证明系统，从而优化定义与定理的可读性，而非证明过程本身。根据 PANews，布特林表示，该语言旨在帮助人类清楚理解 AI 生成的大规模形式化证明在数学与逻辑层面所展示的内容，使读者能够更容易地审计并核实 AI 所提出的具体主张。
免责声明：本页面信息可能来自第三方，仅供参考，不代表 Gate 的观点或意见，亦不构成任何财务、投资或法律建议。数字资产交易风险较高，请勿仅依赖本页面信息作出决策。具体内容详见
声明。
