[Vitalik: A New Advanced Programming Language Worth Trying Should Make Definitions and Theorems Easier to Read] Odaily Planet Daily News: Vitalik posted on the X platform, stating that a new "advanced programming language" worth trying would be one that compiles into Lean (or HOL, etc.), with a focus on making it as easy as possible for humans to read definitions and theorems. The emphasis is not on proofs, as proofs only need to be correct; the key lies in the definitions and theorems themselves. The envisioned use case is for AI to output a large segment of proofs, while readers need to understand as effortlessly as possible which precise claims are actually being proven in those outputs.