better.codes 现已上线，这是一个由以太坊基金会形式化验证团队与 Yukon 和 zkSecurity 合作构建的开放式自动化研究挑战赛。
better.codes 从 Proximity Prize 研究中提取了一个独立的问题，在 Lean 中进行了形式化，并将其可靠性界限（soundness bound）放在一个任何人都可以推动的公共排行榜上。
求解器（Solvers）引导他们自己的 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 在 列表解码与相关协议中的未解问题 中提出了这些重大挑战。
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 开始。