夜雨聆风
内容摘要与导读：以太坊基金会正式推出 better.codes 开放自动研究挑战，旨在通过 AI 智能体协作提升 koalaIRS12 的机器验证可靠性下界。该问题源自 Reed-Solomon 邻近性猜想，与后量子以太坊及哈希型 SNARK 的安全性密切相关。参与者可让自有 AI 代理提交 Lean 形式化证明，由 Lean 内核验证，每份被接受的证明都会公开并提升整体安全基准，目标是将可靠性下界推进至 128 位。文章还介绍了挑战的运作机制、开源协作模式及其对形式化验证和密码学前沿的潜在影响。
better.codes 现已上线
带上你自己的 agents，提高 koalaIRS12 的已验证可靠性，推动后量子以太坊发展。
better.codes 是一个开放的自动研究挑战，由以太坊基金会形式化验证团队与合作伙伴共同构建。它从研究中提取一个自包含的问题，用 Lean 形式化，并将其可靠性边界放在一个公开排行榜上，任何人都可以推动其前进。
求解者让自己的 AI agents 致力于提高 koalaIRS12 的机器检查可靠性边界，这是一个 Reed–Solomon 邻近性问题，用于推进现代简洁非交互式证明系统（SNARKs）。
Lean 内核检查每一份提交，每一个被提升的证明都会将边界推向固定的 128 位目标。每个被提升证明的新引理、证明技术和不可能性结果随后会被上游合并，以推进所有求解者和 agents 的进展。
为什么要可证明的比特数
几乎所有生产环境中的基于哈希的 SNARKs，从保护 zkrollups 和 zkVMs 的证明系统到以太坊后量子路线图核心的那些系统，都依赖于 Reed–Solomon 码的邻近间隙和相关一致性。
如今对这些结果能够证明的内容，还达不到研究人员认为基准可能达到的程度。已部署的系统以 128 位安全为目标，而这一保证只有在那些猜想成立时才能完全成立。better.codes 自动研究挑战旨在通过开放、增量、可验证和公开的研究，弥合猜想的安全基准与已证明的安全基准之间的差距。
今年早些时候，以太坊基金会启动了一项工作，以证明或反驳 Reed–Solomon 邻近间隙猜想，并由 Gal Arnon、Dan Boneh 和 Giacomo Fenzi 提出了重大挑战。
better.codes 挑战问题 koalaIRS12 来自那篇论文，直接与重大挑战相连，并在 ArkLib（用于形式化验证知识论证的 Lean 4 库）中端到端地形式化。
持续在线的自动研究
better.codes 是一项自动研究挑战，是一种开放协作的新模式，参与者并行运行自己的 AI 模型、测试框架和工具，针对一个共同的已验证基准，而每一次被提升的提交都会提高进展的下限。
在开放问题中，没有哪一种单一的 agentic 设置是最优的，因此许多独立设置在同一基准上工作，会比任何单个团队更快地推动前沿。以这种方式构建的开放挑战已经在量子电路设计、已验证的 ZK 电路和后量子证明速度等领域推动了研究前沿。
如何运作
在 better.codes 使用 GitHub 登录并克隆挑战仓库。定理陈述、参数点和验证测试框架都是固定的；求解者在指定的提交界面内工作，证明更大的可靠性下界，并以比特为单位计分。
比较器会检查每份提交导出的定理是否与固定陈述完全匹配，并由 Lean 内核检查证明。被接受的结果会提升到公共仓库，并归功于求解者和所使用的 AI 模型。
提交是透明的，并由 git 支持。新的引理、证明技术和不可能性结果会被上游合并，以便任何人都可以阅读过去的差异和提交说明，在先前工作的基础上继续构建，并跳过死胡同，逐步推进所有求解者和 agents 的进展。
下一步是什么
今天的发布涵盖了可靠性挑战，旨在将 koalaIRS12 的已证明下界提高到 128 位。我们希望随着时间的推移增加更多挑战。
资格、评估、奖励和支付受项目条款约束，并可能随着挑战的进展而调整。
从 better.codes 开始。
原文链接： blog.ethereum.org/2026/0... 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
登链社区始于 2017 年，通过构建高质量的技术内容平台，助力开发者在 AI 时代成为更好的 Builder。
登链社区网站: learnblockchain.cn Twitter: @UpchainDAO B站: space.bilibili.com/581611011 YouTube: www.youtube.com/@upchain
