OpenAI Dots 七智能体团队将 C(24,14,4) 覆盖数下界从 19 提升到 20，并公开 Lean 验证

James Chang 公开一份由 OpenAI Dots 数学研究 campaign 产生的 covering-design 结果：证明 C(24,14,4) ≥ 20，并由 Schönheim bound 推出 C(25,15,5) ≥ 34，分别改进此前 19 与 32 的公开下界。项目说明 10 月 1–3 日由 1 个 coordinating dot 与 6 个 Astra research subagents 开展数学探索和 Lean 形式化，Chang 负责选题、研究指导与路线判断；公开仓库随后提供 Challenge / Solution、约 8,800 行 Lean、fresh rebuild 与 Comparator 检查，Palomar 于 10 月 4 日登记固定提交并重放 Lean 及独立 kernel 检查。维护者同时明确说明尚无数学家完成独立人工审查，而且两个 covering number 的精确值仍未确定。