Claude 辅助排除维数 35 与 805 的半径 3 Lee 球格铺砌，完整 Lean 证明收束特定有限范围遗留案例

Deep Bhattacharjee 与 Ushashi Bhattacharya 在 Hexagon 报告：维数 35 和 805 的半径 3 Lee 球均不能格铺砌 Z^n，填补 Xiao–Zhou 已覆盖规模范围内的剩余两例。论文披露主要证明、Lean 代码与多语言精确计算由人类在 Claude Code 中协作完成，给出 Mathlib 环境下不依赖 sorry、native_decide 或新增公理的 kernel-checked 结论，并提供 Zenodo 归档。该结果只证明 Golomb–Welch 猜想的 lattice form 中特定两例，不涉及任意非格铺砌，更未整体解决该猜想。