The Ethereum co-founder linked the idea to formal verification work around Ethereum and argued that human-readable definitions and theorems matter more than making machine-checked proof output easy to inspect.
Ethereum co-founder Vitalik Buterin outlined a proposed programming language that would compile directly into Lean or HOL, aiming to make AI-generated formal proofs easier for humans to interpret. He argued that the internal steps of a proof only need to satisfy mathematical correctness, while definitions and theorems should be optimized for readability so people can clearly see what a proof actually guarantees. The idea comes as large language models increasingly generate usable Lean proofs and as Ethereum researchers expand formal verification work, including the Lean Ethereum roadmap, a formally verified ZK-EVM and efforts to verify consensus clients in Lean. Buterin has pointed to Claude, Deepseek 4 Pro and Leanstral as tools capable of producing Lean proofs. He also linked the concept to a broader pattern he discussed in May: separating readable specifications from efficient low-level code and then proving the two match, which can let a single audit cover both. No prototype exists yet, and Buterin left the syntax open, with the eventual pace of adoption likely to depend on whether developers converge on a common standard or fragment across incompatible dialects.