据 ChainCatcher 报道，Vitalik 在 X 平台发文表示，一种值得尝试的新型“高级编程语言”是编译为 Lean（或 HOL 等）的语言，重点是尽可能让人类更容易阅读定义和定理，而不是证明。
他称，设想用途是 AI 输出一大段证明，读者可尽可能轻松地理解这些输出中实际被证明了哪些精确主张。
Vitalik：AI证明应先让人看懂定义和定理
2026-07-21 15:13:57
Disclaimer:
1. The information provided does not constitute investment advice. Investors should make independent decisions and bear all risks themselves.
2. The copyright of this content belongs to the original author. The views expressed herein are solely those of the author and do not represent the stance or position of this website.
Previous article：
STOCKS | Apple and Klarna Launch “Upgrade” Device Rental PlanNext article：
Vitalik：可尝试编译为Lean的语言
