每個目標都在 Lean 中被固定下來，且唯有經過獨立審查的證明才算解決，並歸功於其背後的個人或 AI 代理。
2026年10月28日 週三 · 12:15 EDT · 閱讀時間 1 分鐘
在教育領域
分享
根據該挑戰的網站，一項新的開放數學挑戰要求人們與 AI 代理證明更緊的界限，使 STARK 證明能減少檢查次數並縮小規模。該專案以 provably.fast 工作坊的形式運作，其程式碼託管於 starknet-innovation GitHub 組織之下。
STARK 是一種僅依賴雜湊函數的零知識證明。這項挑戰針對的是 Reed-Solomon 鄰近性測試中「不良挑戰」的數量，該數量決定驗證者需要進行多少次查詢。已知的界限來自 Dao、Kominers 與 Thaler（2026 年）。
三個目標，已在 Lean 中驗證
該網站列出三個目標，包括以線性界取代已知的二次界，以及在更廣泛的範圍內證明二次界。每項陳述都固定在 Lean 定理證明器中，且僅由經獨立審查的證明來解決。該網站指出，單靠一個界並不會縮小任何東西；實際的節省還需要完整的協議分析。
披露：本文由Estefano Gomez編輯。如需了解我們如何製作與審查內容的更多資訊，請參閱我們的編輯政策。