SAIR竞赛——Lean内核挑战赛
内容提要
陶哲轩等人宣布启动Lean内核挑战赛第一阶段，旨在提升Lean 4内核验证计算的性能。比赛设八个问题：斐波那契、整数分拆、梅尔滕斯函数、素数计数、矩阵积和式、Rule 110、SHA-256和多项式判别式。参赛者需用Lean开发算法并证明其符合规范。截止日期为2026年11月20日，由Lean FRO与SAIR基金会合办。
延伸解读
比赛定位：内核验证性能优化
Lean内核挑战赛专注于提升Lean 4内核中验证计算的性能，即用内核检查计算结果作为证明的一部分。与Lean Kernel Arena基准测试不同，本比赛要求参赛者开发算法和表示，并在固定内核下评估。第一阶段为实验性，聚焦基础问题，后续阶段将覆盖更广领域和更复杂问题。
参赛任务与提交要求
第一阶段包含八个问题：斐波那契、整数分拆、梅尔滕斯函数、素数计数、矩阵积和式、Rule 110、SHA-256和多项式判别式。针对每个问题，参赛者需用Lean开发算法，并证明该算法对所有输入都符合提供的规范。提交截止日期为2026年11月20日23:59 AoE（UTC−12）。
组织背景与参与价值
比赛由Lean FRO和SAIR基金会联合组织，组织委员会包括Joachim Breitner、Leonardo de Moura、Kim Morrison和Terence Tao。比赛灵感来自Lean Kernel Arena，旨在通过社区贡献开发更快的算法和更好的表示，支持Lean发展并惠及全球用户。参赛者可通过官方仓库和SAIR Playground获取资源。
Q&A
Lean内核挑战赛是什么？
Lean内核挑战赛是一个多阶段竞赛，旨在提升Lean 4内核中验证计算的性能，由Lean FRO与SAIR基金会合办。
Lean内核挑战赛第一阶段有哪些问题？
第一阶段包含八个问题：斐波那契、整数分拆、梅尔滕斯函数、素数计数、矩阵积和式、Rule 110、SHA-256和多项式判别式。
参赛者需要做什么？
参赛者需针对每个问题开发算法，并在Lean中证明该算法对所有输入都符合提供的规范。
Lean内核挑战赛的截止日期是什么时候？
提交截止日期为2026年11月20日23:59 AoE（UTC−12）。
Lean内核挑战赛与Lean Kernel Arena有何不同？
Lean Kernel Arena对替代的Lean证明检查器进行基准测试，而Lean Kernel Challenge专注于验证计算的算法和表示，第一阶段使用固定的Lean内核评估固定任务。
Lean内核挑战赛由谁组织？
由Lean FRO和SAIR基金会共同组织，组织委员会包括Joachim Breitner、Leonardo de Moura、Kim Morrison和Terence Tao。
