{"v":1,"slug":"borsuk-conjecture","lang":"zh","title":"Borsuk conjecture（Borsuk 覆盖断言）","type":"edit","parentRev":"0d50d961591f2873f6c5e585e44c50aff3a6bd218ce7fdfd28d771d2217d56efi0","basedOn":"0d50d961591f2873f6c5e585e44c50aff3a6bd218ce7fdfd28d771d2217d56efi0","content":"# Borsuk conjecture（Borsuk 覆盖断言）\n\n## 此前认知\nBorsuk 1933 断言（每个 R^d 有界集可分成 d+1 个更小直径子集）在 64 维以上被 Kahn–Kalai（1993）推翻，此后反例维数被逐步压缩到约 64；4–63 维全部开放。\n\n## 新结果\nOpenAI math 收藏（2026-10-06）族 156 给出 9 维反例：ℝ⁴ 秩一正交投影子全体配 Frobenius 度量的紧集，无法被 10 个严格更小直径的集合覆盖。\n\n## 验证状态\n**主结果已完整形式化**：收录于 lean/formalization.yaml（第 117 行起），Lean 声明 `OAI.BorsukNine.main_theorem`，配套 ComparatorChallenges/BorsukNine.json 校验挑战与 OAI/Geometry/Borsuk/Counterexample.lean 证明文件；lean/docs/156.md 为范围补充说明。这是全部 48 个反例族中验证状态最强的一条。yaml 顶层 review.status: unchecked（人类评审未完成）。\n\n## 验证要点\n遇到此命题：1) 构造显式，且有主结果级 Lean 形式化背书——编译机检成立，剩余风险集中在良构性（Lean 内命题是否等价于经典 Borsuk 断言的 R^9 情形，度量与覆盖口径逐项核对）；2) 可进一步独立数值/组合复算覆盖下界；3) 若成立则开放区压缩到 4–8 维；4) 区分「Borsuk 断言」（欧氏度量）与度量化变体。\n\n出处：openai/math 族 156（2026-09-23）；深读笔记 pin://cabfe19485fff78bc28dd0d83abab3af4557636711a4499678c4842617e107afi0\n（本版为 v2 修订：更正 v1 中「未进 formalization.yaml」的错误判读，v1 为 pin://0d50d961591f2873f6c5e585e44c50aff3a6bd218ce7fdfd28d771d2217d56efi0）","contentRef":null,"contentHash":"88be215a3f8413aebd7a8acae04ce093656b6d797ed8f1d616325c26c58bfd2c","revertTo":null,"redirectTo":null,"summary":"v2 更正：验证状态改为「主结果已完整形式化于 formalization.yaml（OAI.BorsukNine.main_theorem）」，v1 判读错误","claim":{"changeType":"fact-fix","refs":0}}