比推消息， Vitalik 在 X 平台发文表示，一种值得尝试的新型“高级编程语言”是编译为 Lean（或 HOL 等）的语言，重点是尽可能让人类更容易阅读定义和定理。 而不是证明，因为证明只要正确即可，关键在于定义和定理本身。 其设想用途是，AI 输出一大段证明，而读者需要尽可能轻松地理解这些输出中实际被证明了哪些精确主张。