SAIR 与 Lean FRO 正式启动 Lean Kernel Challenge，公开竞争优化 Lean 4 内核中的可验证计算性能

SAIR Foundation 与 Lean FRO 在 9 月 15 日正式启动 Lean Kernel Challenge Stage 1，由 Joachim Breitner、Leonardo de Moura、Kim Morrison 与 Terence Tao 共同组织。比赛围绕 Lean 4 kernel 中 verified computation 的性能优化设置八个初始问题，参赛者提交优化实现及机器检查的正确性证明；赛后结果和 benchmark 数据计划以开源方式公开。