Finst

Vitalik Buterin Wants to Make AI Proofs Easier to Read With a New Language

Buterin is focusing on formal verification, with a language designed to make AI-generated proofs easier for Lean and HOL to read. That fits with Ethereum’s Lean roadmap and the work on a formally verified ZK-EVM.

By Zenz van der Wielen
• 2 min read
Vitalik Buterin Wants to Make AI Proofs Easier to Read With a New Language

Key Takeaways

  • Vitalik Buterin is proposing a programming language that can compile directly to Lean or HOL.
  • The goal is to make AI proofs easier for people to read and check, not to help AI write faster.
  • Buterin has not shown a prototype yet and left the language’s exact syntax open.

Ethereum cofounder Vitalik Buterin has floated a new programming language that would compile straight into Lean or HOL. The point is not to speed up AI-generated proofs, but to make the logic inside them easier for people to inspect and verify.

Why Lean Matters Here

Lean is a proof assistant that lets mathematicians and engineers have a computer check proofs one step at a time. It has been around for decades, but for a long time it stayed relatively niche. That has changed in a big way: the Lean community now lists more than 210,000 theorems and 100,000 definitions in mathlib, turning it into a major base layer for formal mathematics.

Buterin is pointing to a real usability issue. AI can now generate large sections of proofs automatically, often faster than a human team could write them from scratch. The problem is that readers still have a hard time quickly understanding what those proofs are actually proving. In his view, the core logic only needs to be mathematically sound, while the definitions and theorems should be written in a way humans can easily follow.

The timing also fits with Ethereum’s own rebuild effort, known as the Lean Ethereum roadmap. That work also includes a formally verified ZK-EVM, a zero-knowledge version of the Ethereum Virtual Machine built with similar techniques.

AI Writes, Humans Check

Buterin says models like Claude, DeepSeek 4 Pro, and Leanstral are already able to produce Lean proofs. That reflects a broader shift toward using AI in formal verification. In 2025, ACM SIGPLAN highlighted Lean’s influence on math, hardware and software verification, and AI by giving a software award to several of the project’s core developers.

The use case is bigger than Ethereum. Formal verification is also used to help prove the correctness of important systems, including cryptographic protocols and medical devices. For crypto developers, a more readable language could make it easier to audit claims without having to work through the full proof stack.

What This Means for Ethereum Developers

For European crypto readers, the takeaway is that formal verification is becoming more important in infrastructure where mistakes can directly affect money or security. Ethereum, ZK systems, and cryptographic code are exactly the kinds of places where even a small bug can have serious consequences. A language that makes AI output easier to read could become a useful building block for more reliable software, even if it is not meant to stand on its own.

Buterin has not released a prototype yet, and he has left the language’s exact syntax open. That means it is still unclear whether developers will eventually settle on one standard version or end up using several variants side by side.

Disclaimer: This content is for informational purposes only and does not constitute financial, investment, legal, or tax advice. The information provided may be incomplete, inaccurate, or outdated and should not be relied upon as such. Nothing on this website should be considered a recommendation to buy, sell, or hold any cryptocurrency. Investing in crypto-assets involves risk of loss.