Vitalik Buterin will KI-Beweise mit neuer Sprache lesbarer machen

Buterin setzt auf formale Verifikation: eine Sprache, die von KI erzeugte Beweise für Lean und HOL besser lesbar macht. Das passt zur Lean-Roadmap von Ethereum und zur Entwicklung einer formal verifizierten ZK-EVM.

Wichtigste Erkenntnisse

• Vitalik Buterin schlägt eine Programmiersprache vor, die sich direkt nach Lean oder HOL kompilieren lässt.
• Das Ziel ist nicht, KI beim Schreiben von Beweisen zu beschleunigen, sondern die Ergebnisse für Menschen verständlicher und überprüfbarer zu machen.
• Einen Prototyp hat Buterin bisher nicht vorgestellt, und auch die genaue Syntax der Sprache bleibt offen.

Ethereum-Mitgründer Vitalik Buterin hat eine neue Programmiersprache ins Spiel gebracht, die sich direkt nach Lean oder HOL kompilieren lässt. Der Ansatz zielt nicht darauf ab, KI schneller Beweise schreiben zu lassen. Stattdessen sollen die daraus entstehenden Aussagen für Menschen leichter lesbar und besser überprüfbar werden.

Warum Lean hier wichtig ist

Lean ist ein Proof Assistant, mit dem Mathematiker und Entwickler Beweise Schritt für Schritt von einem Computer prüfen lassen können. Das System existiert seit Jahrzehnten, blieb aber lange ein Nischenthema. Inzwischen hat die Lean-Community in mathlib mehr als 210.000 Theoreme und 100.000 Definitionen dokumentiert. Damit hat sich das Tool zu einer breiten Grundlage für formale Mathematik entwickelt.

Buterin verweist dabei auf ein praktisches Problem: KI kann heute bereits große Teile automatisierter Beweise erzeugen, oft schneller, als ein menschliches Team das manuell leisten könnte. Für Leser ist es jedoch häufig schwer nachzuvollziehen, was ein solcher Beweis im Kern eigentlich zeigt. Aus seiner Sicht muss die innere Logik eines Beweises vor allem mathematisch korrekt sein, während Definitionen und Theoreme gerade dafür gedacht sind, von Menschen gelesen zu werden.

Der Zeitpunkt passt auch zu Ethereums eigenem Umbaupfad, der unter dem Namen Lean Ethereum roadmap bekannt ist. Parallel dazu wird an einer formal verifizierten ZK-EVM gearbeitet, also an einer Zero-Knowledge-Version der Ethereum Virtual Machine, die auf ähnlichen Methoden basiert.

KI schreibt, Menschen prüfen

Buterin nennt unter anderem Claude, DeepSeek 4 Pro und Leanstral als Modelle, die bereits Lean-Beweise erzeugen können. Das fügt sich in einen breiteren Trend ein, bei dem KI zunehmend für formale Verifikation eingesetzt wird. 2025 würdigte ACM SIGPLAN den Einfluss von Lean auf Mathematik, Hardware- und Softwareverifikation sowie KI mit einem Software Award für mehrere zentrale Entwickler des Projekts.

Die Bedeutung reicht allerdings über Ethereum hinaus. Formale Verifikation wird auch genutzt, um die Korrektheit kritischer Systeme abzusichern, etwa bei kryptografischen Protokollen oder medizinischen Geräten. Für Krypto-Entwickler könnte eine besser lesbare Sprache helfen, Aussagen zu prüfen, ohne sich durch die gesamte Beweislogik arbeiten zu müssen.

Bedeutung für Ethereum-Entwickler

Für europäische Krypto-Leser ist das vor allem deshalb relevant, weil formale Verifikation in Infrastrukturen an Bedeutung gewinnt, in denen Fehler direkt Geld oder Sicherheit betreffen können. Ethereum, ZK-Systeme und kryptografischer Code gehören genau zu den Bereichen, in denen schon kleine Fehler große Folgen haben können. Eine Sprache, die KI-Ausgaben besser lesbar macht, dürfte deshalb eher als Baustein für robustere Software interessant sein und nicht als Endprodukt für sich allein.

Buterin hat bislang keinen Prototyp gezeigt und die genaue Syntax offengelassen. Deshalb ist weiterhin unklar, ob sich am Ende ein Standard durchsetzt oder ob mehrere Varianten nebeneinander bestehen bleiben.