Sol 6.1 autoformalized rough-random-design minimax variance theory，并以 Mathlib-only statement 进入 Palomar

P. M. Aronow 与 Patrick Lopatto 将 rough random design 下 constant conditional variance estimation 的主要 minimax 结果完整打包进 Lean：包括 s>1、d>4s 时的 refined minimax bracket、exponent limit、eventual polynomial bounds，以及低 smoothness 与 parametric regimes。仓库披露原始 development 由 Sol 6.1 autoformalize，后续 Codex 负责 Palomar 准备、compiler compatibility 与 automated review。PALOMAR-2026-10-10-000002 于 10 月 10 日注册，Challenge 仅依赖 Mathlib / Lean core；五个 paper-level statements 由 Lean kernel、NanoDa 与 con-ron 接受，并附 automated statement review。作者明确说明这些机器检查不推导出 human mathematical review。