Ethereum co-founder Vitalik Buterin proposed a new programming language aimed at improving the readability of automated proofs generated by artificial intelligence. The proposed language would compile directly into Lean or HOL, a formal proof assistant.
The initiative addresses a gap in how readers interpret the output of AI systems, which are increasingly capable of producing extensive blocks of proofs faster than human teams can create them. Few individuals can swiftly verify the implications of these proofs.
Lean functions as a proof assistant that mathematicians and engineers use to draft proofs that a computer can check line by line. Ethereum researchers already utilize Lean to verify cryptographic code and consensus logic. While proof assistants have been around for nearly 60 years, their use remains limited to niche applications.
In a post, Buterin highlighted the need for a “high-level programming language” that facilitates easier comprehension of definitions and theorems, rather than focusing solely on the proofs themselves. He stated, “Not the proofs – as all…” in reference to the complexities involved in understanding proof methodologies.
Buterin emphasized that the internal steps of a proof must only meet the requirement of mathematical correctness. In contrast, definitions and theorems serve a different purpose, as readers rely on them to grasp the guarantees a piece of software provides.
In a previous blog post from May, Buterin explored the concept that a mathematical proof can demonstrate that efficient low-level code aligns with a more accessible specification, allowing for a single audit to suffice for both versions.
This proposal coincides with Ethereum’s ongoing rebuild initiative, known as the Lean Ethereum roadmap. Researchers are also developing a formally verified zero-knowledge Ethereum virtual machine (ZK-EVM) using similar methodologies.
Buterin noted that large language models, such as Claude and Deepseek 4 Pro, are capable of generating usable Lean proofs. He identified Leanstral, a model specifically tuned for Lean, as another useful tool. One project demonstrating this capability is evm-asm, which implements EVM verified against a comprehensible reference.
The importance of this development extends beyond mere convenience. Security researchers have reported a rise in AI-assisted exploit attempts this year. Formally verified code presents a defense against these increasing threats. A more user-friendly specification language could play a significant role in enhancing security measures.
