イーサリアムの共同創業者はこの構想をイーサリアムを巡る形式検証の取り組みと結び付け、人間が読める定義や定理は、機械検証済みの証明出力を精査しやすくすることより重要だと主張した。
イーサリアム共同創業者のヴィタリック・ブテリンは、LeanまたはHOLに直接コンパイルするプログラミング言語の構想を示し、AIが生成した形式証明を人間が解釈しやすくすることを目指すとした。証明の内部手順は数学的に正しければ十分である一方、定義や定理は可読性を最優先で設計すべきであり、そうすることで証明が実際に何を保証しているのかを人間が明確に把握できると主張した。 この構想が浮上した背景には、大規模言語モデルが実用的なLeanの証明を生成する力を高めていることに加え、イーサリアム研究者がLean Ethereum roadmap、形式検証済みのZK-EVM、Leanによるコンセンサスクライアントの検証など、形式検証の取り組みを拡大していることがある。ブテリンは、Claude、Deepseek 4 Pro、LeanstralをLeanの証明を生成できるツールとして挙げている。 またブテリンは、この考え方を5月に論じたより広範なパターンとも結び付けた。すなわち、読みやすい仕様と効率的な低水準コードを切り分けたうえで、両者が一致することを証明するという発想であり、これにより1回の監査で双方をカバーできる可能性がある。 提案言語のプロトタイプはまだ存在せず、ブテリンは構文も定めていない。今後の普及速度は、開発者が共通標準に収束するのか、それとも互換性のない方言へ分裂するのかに左右される可能性が高い。