Lean 定理证明器内核基准上线：16 款验证器同台竞技
burny_tech · x · 2026-08-14
Lean 官方推出了名为 Lean Kernel Arena 的公开基准测试平台，用于评估和对比各类 Lean 定理证明器的内核（proof checkers）。
- 测试机制：平台对所有提交的内核运行统一的测试套件，包含 121 个有效证明（必须接受）和 62 个无效证明（必须拒绝），并记录它们在 Mathlib 和标准库上的运行时间与内存消耗。
- 核心目的：通过鼓励独立开发多样化的内核来提升系统的可靠性。如果一个漏洞要让所有独立开发的内核同时接受一个无效证明才不会被察觉，这种概率极低。
- 当前榜单：截至 2026 年 8 月，已列出 16 款验证器。其中 5 款通过了全部测试，包括官方内核。运行时间从最快的 3.2 分钟到超过 1 小时不等。
「研究」频道最新
- 残差强化学习结合动捕数据训练物理角色控制器 — Rudy_AA · 2026-08-14
- Eratos Therapeutics 探讨生物学领域的「世界模型」 — staraman_r · 2026-08-14
- Grok 4.6 生物学评测：准确率比肩 Opus 5 且成本更低 — kenbwork · 2026-08-14
- Cooperative AI 研讨会：用安全帕累托改进解决AI博弈困境 — xuanalogue · 2026-08-14
- AI 脑电波诊断创企 Hemispheric 获 5200 万美元融资 — rjhaier · 2026-08-14
- 音频生成模型 RVQ 编码器缺失：研究脉络与解法汇总 — andrew_n_carr · 2026-08-14