Ethereum co-founder Vitalik Buterin has proposed a new programming language that compiles directly into Lean or HOL, designed to make AI-generated formal proofs more readable for humans. The language focuses on the clarity of definitions and theorems, not the proof steps themselves — those only need to be mathematically correct. The proposal aligns with Ethereum's 'Lean Ethereum roadmap' and ongoing work to build a formally verified ZK-EVM.
Why readability matters for AI proofs
Large language models like Claude, Deepseek 4 Pro, and Leanstral can already write usable Lean proofs. But the output is often dense and hard for humans to follow. Buterin's language aims to fix that by prioritizing human-readable definitions and theorems, while leaving the proof steps to the machine. Security researchers have tracked a jump in AI-assisted exploit attempts this year, and formally verified code offers a defense — but only if developers can actually understand what the code is doing.
The Lean connection
Ethereum researchers already use Lean to verify cryptographic code and consensus logic. One example is evm-asm, an EVM implementation verified against a readable reference. Buterin's proposal would make it easier to write such verified implementations by letting developers work in a language that's more natural to read, then compile it into Lean or HOL for formal verification. He recently demoed an anonymous billboard built with zero-knowledge proofs, showing his continued interest in practical applications of advanced cryptography.
No prototype of the new language exists yet, and the exact syntax is left open. Developers may converge on one standard or end up with multiple dialects. The proposal is still early-stage, but it's a concrete step toward making formal verification more accessible — especially as AI-generated code becomes more common and the need for verifiable correctness grows.
