SAIR 竞赛——Lean 内核挑战赛
核心概要
这是一则竞赛公告：SAIR 基金会与 Lean FRO 联合发起多阶段的 Lean 内核挑战赛，第一阶段围绕八个固定问题（斐波那契、整数分拆、Mertens 函数、素数计数、矩阵积和式、Rule 110、SHA-256、多项式判别式）征集算法，并要求参赛者在 Lean 中证明其算法对每个输入都符合给定规范，提交截止日期为 2026 年 11 月 20 日 23:59 AoE。
深度剖析
发起一项多阶段竞赛，目标是提升 Lean 4 内核中「已验证计算」（verified computation）的性能，即用 Lean 内核在证明过程中检查计算结果。 与主要评测替代性 Lean 证明检查器的 Lean Kernel Arena 不同，本挑战赛聚焦于已验证计算的算法与表示，且第一阶段采用固定任务、由固定 Lean 内核评测。 公告文本明确说明其灵感来自 Lean Kernel Arena 并致谢其贡献者，同时说明两者定位差异；未给出任何性能数据或评测结果。
第一阶段设定八个具体问题：斐波那契、整数分拆、Mertens 函数、素数计数、矩阵积和式、Rule 110、SHA-256 与多项式判别式。 以一份公开、固定的问题清单作为社区共同攻关的起点，覆盖数论、组合、线性代数、元胞自动机与密码学哈希等不同计算对象。 问题清单在公告中直接列出；公告未说明各问题的规模、评分细则或基线实现。
参赛要求是为每个问题开发算法，并在 Lean 中证明该算法对每一个输入都符合所提供的规范。 把「算法效率」与「形式化正确性证明」绑定为同一提交要求，而非仅比较运行速度。 公告以一句话给出该要求；未描述证明的验收方式、允许的假设或依赖库范围。
赛事由 Lean FRO 与 SAIR 基金会共同组织，组织委员会包括 Joachim Breitner、Leonardo de Moura、Kim Morrison 和 Terence Tao，并提供竞赛网站、SAIR Playground 与官方代码仓库。 以公开基础设施（提交入口、练习场、仓库）支撑社区参与，便于参赛者获取任务与提交作品。 公告列出组织方、委员会成员与三个链接；未说明奖金、评审流程或结果公布方式。
启示与展望
该公告界定的适用范围是 Lean 4 内核中的已验证计算，第一阶段为实验性阶段，从基础问题起步，后续阶段将覆盖更广泛的数学与科学领域以及更复杂的问题。它面向愿意用 Lean 编写算法并完成形式化正确性证明的参赛者，提交截止时间为 2026 年 11 月 20 日 23:59 AoE（UTC−12）。
公告未说明各问题的输入规模与评分标准、评测环境的具体配置、是否允许使用外部库或公理、奖项与评审安排，也未给出任何基线性能或往届结果。此外，本次读取的文本为博客页面内容，未包含竞赛网站、Playground 与代码仓库中的任务细节，因此各问题的具体规范与验收方式仍需以官方渠道为准。