Vitalik：应开发面向人类可读定义与定理的高级语言，支持 AI 生成形式化证明

前沿科技 1 源 1 条原始记录重要度 6/10

主要报道

吴说获悉，Vitalik Buterin 提议开发一种可编译至 Lean、HOL 等系统的高级语言，重点提升定义和定理的可读性，而非证明过程本身。其设想的应用场景是由 AI 生成大规模证明，再通过这种...