拉姆齐数上界改进至 3.49135655^k 并获 Lean 验证

开发者 ctjlewis 宣布将拉姆齐数对角上界的指数基改进到 3.49135655，即对充分大的 k 有 R(k,k) ≤ 3.49135655^k，把此前最优基降低约 0.2%，并使用 Lean 对结果完成形式化验证。他同时分享了提升机器证明可读性的工程实践：按论文「证明顺序」呈现 Lean 验证，使代码与论文章节对应，并将模块数量精简到 400 以内。

2026-10-18 ~ 2026-10-18 · 2 条相关

• 拉姆齐数上界再逼近:R(k,k) ≤ 3.49135655ᵏ 获 Lean 形式化验证 — ctjlewis · 2026-10-18
• 让 Lean 机器证明更可读:按论文顺序呈现验证,模块砍到 400 以内 — ctjlewis · 2026-10-18