AI 生成的超矩阵计数乘积公式解决 Koprowski–Lewis 问题，并附 Lean 核验

YURAN XIU 在 Hexagon 发布对有限域上 2×(k+1)×k、带分区形状零元约束的非退化超矩阵计数公式，报告证明 Koprowski–Lewis 的乘积猜想。方法把第一切片固定后的非退化性还原为偏线性映射的 simple-extension 条件，再逐层使用已有定理；作者报告完整计数结论及语义等价关系已在 Lean 中形式化，另有 HAL 登记。页面标为主要 AI 生成且人类尚不理解，不可升级为人类独立审稿。