Wu Shuo learned that Vitalik Buterin proposed developing a high-level language that can be compiled to systems such as Lean and HOL, focusing on improving the readability of definitions and theorems rather than the proof process itself. The envisioned use case is that AI generates large-scale proofs, and then this language helps readers more easily understand exactly which precise definitions and theorems have been proven.