better.codes 現已上線，這是一個由以太坊基金會形式化驗證團隊與 Yukon 和 zkSecurity 合作建立的開放式自動化研究挑戰。
better.codes 從 Proximity Prize 研究中提取了一個獨立的問題，在 Lean 中進行了形式化，並將其可靠性界限（soundness bound）放在一個公開的排行榜上，任何人都可以推動其進展。
求解器引導他們自己的 AI 代理來提升 koalaIRS12 的機器檢查可靠性界限，這是一個里德-所羅門（Reed-Solomon）鄰近性問題，旨在推動現代簡潔非互動式證明系統（SNARK）。
Lean 核心會檢查每一次提交，每一個被晉升的證明都會將界限提升至固定的 128 位元目標。每個被晉升證明的新引理、證明技術和不可能性結果隨後會被合併到上游，以推動所有求解器和代理的進展。
為什麼需要可證明的位元
幾乎所有生產環境中基於雜湊的 SNARK，從保護 zkrollup 和 zkVM 的證明系統，到以太坊後量子路線圖核心的證明系統，都依賴於里德-所羅門碼的鄰近性間隙（proximity gaps）和相關協議（correlated agreement）。
目前關於這些結果所能證明的程度，仍未達到研究人員認為基準可能達到的水準。已部署的系統以 128 位元安全性為目標，而這項保證只有在猜想成立的情況下才能完全兌現。better.codes 自動化研究挑戰旨在透過開放、漸進、可驗證且公開的研究，縮小猜想的安全基準與已證明的安全基準之間的差距。
今年稍早，以太坊基金會啟動了 Proximity Prize 計畫，以證明或證偽里德-所羅門鄰近性間隙猜想，其重大挑戰已在 Gal Arnon、Dan Boneh 和 Giacomo Fenzi 所著的 列表解碼與相關協議中的未解問題（Open Problems in List Decoding and Correlated Agreement） 中列出。
better.codes 的挑戰問題 koalaIRS12 源自該論文，直接連結到這些重大挑戰，並在 ArkLib（用於形式化驗證知識論證的 Lean 4 函式庫）中進行了端到端的形式化。
隨時在線的自動化研究
better.codes 是一個自動化研究挑戰，這是一種開放協作的新模式，參與者可以平行運行自己的 AI 模型、測試工具和工具，針對一個共同的已驗證基準進行測試，而每一個被晉升的提交都會提高進展的底線。
沒有任何單一的代理設定能在整個開放問題中達到最佳狀態，因此許多獨立的設定在同一個基準上運作，能比任何單一團隊更快地推動邊境。以這種方式建立的開放挑戰，包括 ecdsa.fail、zk.golf 和 snark.fast，已經推動了量子電路設計、已驗證 ZK 電路和後量子證明速度的研究邊境。
運作方式
在 better.codes 使用 GitHub 登入並複製挑戰儲存庫。定理陳述、參數點和驗證測試工具已被固定；求解器在指定的提交介面內運作，並證明一個更大的可靠性下界，以位元為單位進行評分。
比較器會檢查每次提交所匯出的定理是否與固定的陳述完全相符，而 Lean 核心則會檢查證明。被接受的結果將被晉升到公開儲存庫，並歸功於求解器和所使用的 AI 模型。
提交內容是透明的且由 git 支援。新的引理、證明技術和不可能性結果會被合併到上游，以便任何人都可以閱讀過去的差異（diffs）和提交筆記，在先前的基礎上繼續開發，並跳過死胡同，從而漸進地推動所有求解器和代理的進展。
下一步是什麼
今天的發布涵蓋了可靠性挑戰，旨在將 koalaIRS12 的已證明下界提升至 128 位元。我們希望隨著時間的推移增加更多挑戰。資格、評估、獎勵和付款均受計畫條款約束，並可能隨著挑戰的進展而調整。
從 better.codes 開始。