Svmuu訊 Vitalik 在 X 平台發文表示，一種值得嘗試的新型“高級編程語言”是編譯為 Lean（或 HOL 等）的語言，重點是儘可能讓人類更容易閲讀定義和定理。 而不是證明，因為證明只要正確即可，關鍵在於定義和定理本身。 其設想用途是，AI 輸出一大段證明，而讀者需要儘可能輕鬆地理解這些輸出中實際被證明了哪些精確主張。