Vitalik Buterin Proposes Language to Make AI Proofs Readable

Ethereum co-founder Vitalik Buterin proposed a new programming language. It would compile directly into Lean or HOL, another formal proof assistant.

The idea targets a specific gap in how people read AI output. Artificial intelligence increasingly produces large blocks of automated proofs, often faster than any human team could write them by hand. Few readers can quickly confirm what those proofs actually establish.

A Language Built Only for AI Proof Readers

Lean is a proof assistant, a software that mathematicians and engineers use to write proofs a computer can check line by line. Ethereum researchers already use on it to verify cryptographic code and consensus logic. Proof assistants have existed for nearly 60 years, yet the field has stayed a niche pursuit.

A new type of "high-level programming language" that seems really worth trying to make, is a language that gets compiled to Lean (or HOL, or…) that is specifically about making it as friendly as possible for a human to read definitions and theorems.Not the proofs – as all…

— vitalik.eth (@VitalikButerin) July 21, 2026

In his post, Buterin argued that a proof’s internal steps carry only one requirement. That requirement is mathematical correctness, nothing more. Readers never inspect that machinery directly. Definitions and theorems work differently, since humans read those parts to learn what a piece of software actually guarantees.

Buterin explored a related split in a May blog post. There, a mathematical proof shows that efficient low-level code matches a separate, readable specification, so a single audit covers both versions at once.

His timing also lines up with Ethereum’s own rebuild effort, which carries a separate nickname, the Lean Ethereum roadmap. Researchers are meanwhile building a formally verified ZK-EVM, a zero-knowledge-provable version of Ethereum’s virtual machine (EVM), using comparable methods.

AI Writes the Proofs, Humans Check the Claims

Large language models can already write usable Lean proofs. Buterin has named Claude and Deepseek 4 Pro as capable tools, alongside Leanstral, a smaller model tuned specifically for Lean. One example project is evm-asm, an EVM implementation verified against a readable reference. That capability echoes the reasoning skills developers displayed in a recent Buterin AI challenge. Testers solved that challenge within hours.

The stakes extend past convenience, however. Security researchers have tracked a jump in AI-assisted exploit attempts this year. Formally verified code offers one defense against that trend. A friendlier specification language would let developers audit claims without wading through the surrounding proof.

Beyond Ethereum’s Research Circles

Buterin keeps testing these ideas in public as he recently demoed an anonymous billboard built with zero-knowledge proofs. The demo showed how verifiable claims can move from research repositories into working products. Researchers have also begun formally verifying consensus clients in Lean to catch bugs early.

Still, the direction echoes a familiar pattern: separate fast code from readable claims, then prove the two match.

No prototype of the new language exists yet, and Buterin left the exact syntax open. Developers may converge on one shared standard, or settle for several incompatible dialects instead. That choice could determine how quickly AI-verified code reaches production systems.