Vitalik: Le nuove lingue di programmazione avanzate che vale la pena provare dovrebbero rendere più facile leggere definizioni e teoremi.

Secondo quanto riportato da Odaily, Vitalik ha pubblicato su X affermando che un nuovo tipo di "linguaggio di programmazione avanzato" che vale la pena provare è un linguaggio che si compila in Lean (o HOL, ecc.), con l'obiettivo di rendere la lettura delle definizioni e dei teoremi il più semplice possibile per le persone. L’attenzione non è sulle dimostrazioni, poiché è sufficiente che queste siano corrette, ma sulle definizioni e sui teoremi stessi. L’idea è che l’IA possa generare una lunga sequenza di dimostrazioni, mentre il lettore dovrebbe essere in grado di comprendere facilmente quali affermazioni specifiche sono effettivamente dimostrate in tali output.