Vitalik Proposes Lean-Compiled Languages for Easier Reading of Definitions and Theorems

Vitalik said on X that a new type of "advanced programming language" worth trying is one that compiles to Lean or similar systems, with a focus on making definitions and theorems as easy for humans to read as possible. According to ChainCatcher, he said the goal is not to make proofs easier to read, since proofs only need to be correct, but to clarify the definitions and theorems themselves. He described a possible use case in which AI outputs a long proof, and readers need to understand as easily as possible which exact claims were actually proven.