今天（7 月 21 日），以太坊聯合創始人 V 神提出建立一種新的高階程式語言，將其編譯至像 Lean 與 HOL 這樣的形式化證明系統，重點在於最佳化定義與定理的可讀性，而非證明流程本身。根據 PANews 的說法，V 神表示，該語言旨在協助人類清楚理解 AI 生成的大規模形式化證明在數學與邏輯上所呈現的內容，讓讀者能更容易稽核並驗證 AI 所提出的特定主張。
免責聲明：本頁面資訊可能來自第三方來源，僅供參考，不代表 Gate 的立場或觀點，亦不構成任何財務、投資或法律建議。虛擬資產交易具有高風險，請勿僅依賴本頁資訊作出決策。詳情請參閱
免責聲明。
