Vitalik Buterin wil AI-proofs leesbaar maken met nieuwe taal

Buterin richt zich op formele verificatie: een taal die AI-gegenereerde proofs beter leesbaar maakt voor Lean en HOL. Dat sluit aan bij Ethereum’s Lean-roadmap en de ontwikkeling van een formeel geverifieerde ZK-EVM.

Korte samenvatting

• Vitalik Buterin stelt een programmeertaal voor die direct kan compileren naar Lean of HOL.
• Het doel is AI-proofs beter leesbaar en controleerbaar te maken voor mensen, niet om AI sneller te laten schrijven.
• Buterin heeft nog geen prototype getoond en liet de exacte syntax van de taal open.

Ethereum medeoprichter Vitalik Buterin heeft een nieuwe programmeertaal voorgesteld die direct kan compileren naar Lean of HOL. Het doel is niet om AI sneller proofs te laten schrijven, maar om de claims daaruit beter leesbaar en controleerbaar te maken voor mensen.

Waarom Lean hier telt

Lean is een proof assistant waarmee wiskundigen en engineers stap voor stap bewijzen laten controleren door een computer. De tool bestaat al decennia, maar bleef lang een niche. De Lean-community heeft inmiddels meer dan 210.000 theorema’s en 100.000 definities vastgelegd in mathlib, wat het systeem tot een brede basis voor formele wiskunde maakt.

Buterin wijst op een praktisch probleem: AI kan inmiddels grote blokken geautomatiseerde proofs produceren, vaak sneller dan een menselijk team dat handmatig kan doen. Voor lezers is het lastig om snel te zien wat zo’n proof nu echt bewijst. Volgens hem hoeft de interne logica van een proof alleen mathematisch correct te zijn, terwijl definities en theorema’s juist bedoeld zijn om door mensen gelezen te worden.

De timing sluit aan bij Ethereum’s eigen herbouwtraject, dat ook bekendstaat als de Lean Ethereum roadmap. Binnen dat werk wordt bovendien gewerkt aan een formeel geverifieerde ZK-EVM, een zero-knowledge versie van de Ethereum Virtual Machine, met vergelijkbare methoden.

AI schrijft, mensen controleren

Buterin noemt onder meer Claude, DeepSeek 4 Pro en Leanstral als modellen die al Lean-proofs kunnen genereren. Dat past in een bredere trend waarin AI steeds vaker wordt ingezet voor formele verificatie. In 2025 erkende ACM SIGPLAN de impact van Lean op wiskunde, hardware- en softwareverificatie en AI met een software award voor meerdere kernontwikkelaars van het project.

De relevantie reikt verder dan Ethereum alleen. Formele verificatie wordt ook gebruikt om de juistheid van kritieke systemen te onderbouwen, van cryptografische protocollen tot medische apparaten. Voor crypto-ontwikkelaars kan een leesbaardere taal helpen om claims te auditen zonder door de volledige proof-machinerie te hoeven ploegen.

Betekenis voor Ethereum-ontwikkelaars

Voor Europese crypto-lezers is dit vooral relevant omdat formele verificatie steeds belangrijker wordt in infrastructuur waar fouten direct geld of veiligheid kunnen raken. Ethereum, ZK-systemen en cryptografische code zijn precies de plekken waar een kleine fout grote gevolgen kan hebben. Een taal die AI-output beter leesbaar maakt, kan daarom vooral waardevol zijn als bouwsteen voor betrouwbaardere software, niet als eindproduct op zichzelf.

Buterin heeft nog geen prototype laten zien en liet de exacte syntax open. Daardoor is het nog onduidelijk of ontwikkelaars uiteindelijk één standaard zullen kiezen of juist meerdere varianten naast elkaar zullen gebruiken.