Svmuu News: Vitalik posted on X, stating that a new type of “high-level programming language” worth exploring is one that compiles to Lean (or HOL, etc.), with a focus on making definitions and theorems as easy as possible for humans to read. The emphasis is on definitions and theorems themselves, rather than proofs, because proofs only need to be correct—the key lies in the definitions and theorems themselves. The envisioned use case is that an AI outputs a large block of proof, and the reader needs to be able to understand as easily as possible exactly which precise claims are actually proven in that output.