这位以太坊联合创始人将这一想法与围绕以太坊开展的形式化验证工作联系起来，并认为，相比让机器检查的证明输出更易于审阅，人类可读的定义和定理更为重要。
以太坊联合创始人维塔利克·布特林概述了一种拟议中的编程语言，该语言将直接编译为 Lean 或 HOL，旨在让 AI 生成的形式化证明更便于人类理解。他认为，证明的内部步骤只需满足数学上的正确性，而定义和定理则应针对可读性进行优化，以便人们能够清楚看到证明究竟保证了什么。在大型语言模型越来越多地生成可用的 Lean 证明之际，以及以太坊研究人员不断推进形式化验证工作之时，这一想法应运而生；相关工作包括 Lean Ethereum 路线图、经过形式化验证的 ZK-EVM，以及以 Lean 验证共识客户端的努力。布特林曾指出，Claude、Deepseek 4 Pro 和 Leanstral 都是能够生成 Lean 证明的工具。他还将这一概念与自己在 5 月讨论的一种更广泛模式联系起来：将可读的规范与高效的底层代码分离，再证明二者一致，从而使一次审计即可覆盖两者。目前尚无原型，布特林也未限定语法；最终采用速度可能取决于开发者是收敛到共同标准，还是分化为彼此不兼容的方言。