Vitalik提议开发支持AI生成证明的高级语言

BiRun 消息，以太坊联合创始人 Vitalik Buterin 提议开发一种可编译至 Lean、HOL 等形式化验证系统的高级语言。该语言旨在提升定义和定理的人类可读性，而非专注于证明过程本身。Vitalik 设想的应用场景是由 AI 生成大规模形式化证明，再通过这种高级语言进行表达与验证，从而降低形式化数学的门槛，促进 AI 在严谨逻辑推理领域的应用。这一提议结合了加密货币社区对形式化验证的重视与 AI 技术的发展趋势，有望推动智能合约安全性及数学证明自动化的进步。