拉姆齐数上界再逼近:R(k,k) ≤ 3.49135655ᵏ 获 Lean 形式化验证
ctjlewis · x · 2026-10-18
开发者 ctjlewis 宣布将拉姆齐数对角上界的指数基改进到 3.49135655,即对充分大的 k 有 R(k,k) ≤ 3.49135655ᵏ,把此前最优基降低约 0.2%。
- 方法上改进了 Zhao、Booth-Clibborn 与 Schwahn 的框架:保留补邻域矩约束,推导标量可行性与包络律,并重新调校 source/root 构造;底层沿用 Lu 与 Wang 的 retained-set 下降法。
- 证明完全经 Lean 形式化验证,论文与代码以 hashes.sh 上的时间戳哈希公开,仓库为 EvolvingPrograms/DiagonalRamsey(MIT 协议),证明按 S1–S8 分节组织,可直接核对各定理声明。
所属事件:拉姆齐数上界改进至 3.49135655^k 并获 Lean 验证(2 条相关)→
「研究」频道最新
- 菲尔兹奖得主 Kontsevich：AI 智能体主动提出更好的数学定义 — luislamb · 2026-10-18
- MIT–OpenAI 研究：长期使用聊天机器人与幸福感下降相关 — patpat_mit · 2026-10-18
- 用 Opus 模拟 Hox 基因网络,生成了蜥蜴与蛇的骨骼图 — repligate · 2026-10-18
- OpenEnv Arena 免 GPU 做 RL 环境：每 24 小时可跑一次训练 — ben_burtenshaw · 2026-10-18
- 法国数学博士生：20 欧的 ChatGPT 就能解掉我做了两年的题 — FlorianGallwitz · 2026-10-18
- 「想法盆地」观察:同一任务多次独立运行得分悬殊,且加算力也追不平 — menhguin · 2026-10-18