Vitalik: It’s worth trying to create a new kind of “proof language for readability” to improve human understanding of AI-generated proofs

PANews, July 21: Ethereum co-founder Vitalik Buterin proposed exploring a new kind of high-level programming language that can be compiled into theorem-proving systems such as Lean and HOL. The focus is on optimizing the readability of “definitions and theorems,” rather than the proof process itself. Vitalik said the target scenario for this language is to help humans clearly understand what these proofs are “formally proving” after AI outputs large-scale formal proofs—making it easier for readers to review and verify the specific mathematical and logical claims provided by the AI.