Romik 双手沙发问题最优性被 Lean 4 形式化证明
IgorCarron · x · 2026-10-17
社区仓库 lean4-ambidextrous-sofa 用 Lean 4 完成了 Romik「双手沙发」（ambidextrous sofa）问题最优性与唯一性的形式化证明：在宽 1 的直角走廊里，同一形状既要能绕过右转弯、也要能绕过左转弯时，最大面积是 Romik 2016 年构造的 1.64495…。该仓库含 MovingSofaOptimality 等完整形式化文件与 CI 工作流，回应了 Dan Romik 的猜想。
「研究」频道最新
- NannyML 团队 ML Metrics 新书序言：107项指标写了两年多 — santiviquez · 2026-10-17
- EpochGo 开源：本地 LLM 编排加 Scikit-Learn 离线跑 AutoML — Grouchy-Excitement28 · 2026-10-17
- 生物只需 5% 能量做计算,人脑实际功耗可能仅 1-2 瓦 — JosephJacks_ · 2026-10-17
- 自然视觉刺激下 V1 神经响应会变「脏」，群体效应是主因 — HistedLab · 2026-10-17
- 神经科学家：大脑几乎每个区域都存在强多义性表征 — HistedLab · 2026-10-17
- Google.org 选出 17 家机构，投入 3600 万美元支持 AI for Science — ymatias · 2026-10-17