Vitalik Buterin vuole rendere più leggibili i proof generati dall’AI con un nuovo linguaggio

Buterin punta sulla verifica formale: un linguaggio che rende i proof generati dall’AI più leggibili per Lean e HOL. Il tutto si inserisce nella roadmap Lean di Ethereum e nello sviluppo di una ZK-EVM formalmente verificata.

In breve

• Vitalik Buterin propone un linguaggio di programmazione che può compilare direttamente in Lean o HOL.
• L’obiettivo è rendere i proof generati dall’AI più leggibili e controllabili per le persone, non far scrivere proof più in fretta all’AI.
• Buterin non ha ancora mostrato un prototipo e ha lasciato aperta la sintassi esatta del linguaggio.

Il cofondatore di Ethereum Vitalik Buterin ha messo sul tavolo una proposta per un nuovo linguaggio di programmazione capace di compilare direttamente in Lean o HOL. Il punto, però, non è accelerare la scrittura dei proof da parte dell’AI, ma rendere più semplice per le persone capire e verificare ciò che viene prodotto.

Perché Lean conta qui

Lean è un proof assistant che consente a matematici e ingegneri di far controllare i proof passo dopo passo da un computer. Esiste da anni, ma per molto tempo è rimasto uno strumento di nicchia. Oggi, però, la community di Lean ha superato quota 210.000 teoremi e 100.000 definizioni in mathlib, trasformandolo in una base molto ampia per la matematica formale.

Buterin evidenzia un problema concreto: l’AI è ormai in grado di generare grandi blocchi di proof automatizzati, spesso più rapidamente di quanto riuscirebbe a fare un team umano. Il punto critico, però, è un altro: per chi legge, non è sempre immediato capire cosa dimostri davvero quel proof. Secondo lui, la correttezza matematica della logica interna è fondamentale, ma definizioni e teoremi devono restare leggibili per chi li deve controllare.

Il tempismo si inserisce anche nel percorso di ricostruzione di Ethereum, noto anche come Lean Ethereum roadmap. All’interno di questo lavoro si sta sviluppando anche una ZK-EVM formalmente verificata, cioè una versione zero-knowledge della Ethereum Virtual Machine costruita con approcci simili.

L’AI scrive, le persone controllano

Buterin cita tra i modelli già in grado di generare proof in Lean anche Claude, DeepSeek 4 Pro e Leanstral. Il tutto si inserisce in una tendenza più ampia, in cui l’AI viene usata sempre più spesso per la verifica formale. Nel 2025 ACM SIGPLAN ha riconosciuto l’impatto di Lean su matematica, verifica hardware e software e AI con un software award assegnato a diversi sviluppatori chiave del progetto.

La portata del tema va oltre Ethereum. La verifica formale viene infatti impiegata anche per dimostrare la correttezza di sistemi critici, dai protocolli crittografici ai dispositivi medici. Per chi sviluppa nel settore crypto, un linguaggio più leggibile può rendere più semplice auditare le affermazioni senza dover entrare in ogni dettaglio della macchina dei proof.

Cosa significa per gli sviluppatori Ethereum

Per chi segue il settore crypto in Europa, il tema è interessante soprattutto perché la verifica formale sta diventando sempre più centrale nelle infrastrutture in cui un errore può avere un impatto diretto su denaro o sicurezza. Ethereum, i sistemi ZK e il codice crittografico sono proprio gli ambiti in cui anche un piccolo bug può avere conseguenze pesanti. Un linguaggio che renda più chiaro l’output dell’AI può quindi essere utile soprattutto come base per software più affidabile, non come prodotto finale.

Buterin, per ora, non ha mostrato alcun prototipo e non ha definito la sintassi esatta. Resta quindi da capire se gli sviluppatori convergeranno su uno standard unico oppure se finiranno per usare più varianti in parallelo.