今天（7 月 21 日），以太坊共同創辦人 Vitalik Buterin 提出建立一種全新的高階程式語言的想法，該語言有可能編譯到像 Lean 和 HOL 這類形式證明系統上，以便優化定義與定理的可讀性，而不是著重在證明流程本身。據 PANews 報導，Buterin 表示，這種語言被設計用來幫助人們清楚理解大型規模的形式證明由 AI 產出時在數學與邏輯層面所呈現的內容，進而讓讀者更容易檢查並驗證 AI 所提出的特定主張。