Armstrong 等用 AI agents 完成约 10 万行 Lean，形式化最优范围的退化椭圆 De Giorgi–Nash–Moser 理论

Scott Armstrong、Benny Avelin、Tuomo Kuusi 与 Aatu Turpeinen 将 De Giorgi–Nash–Moser 理论推广到可能退化且无界、但满足 coarse ellipticity 条件的对称系数椭圆方程，并证明系数范围、局部界中的粗椭圆比幂次及 weak Harnack 指数范围的 sharpness。配套 CoarseDeGiorgi Lean 4 development 约 10 万行、约 1,000 个 modules；仓库明确披露 Lean 代码由 AI agents 在作者监督下完成：Claude Opus 5.5 负责协调和审计，GPT-6 Luna / Sol / 6.1 Sol 与 Claude Sonnet 5 编写 Lean。项目报告无 `sorry`、无自定义公理，并以 Mathlib-only restatements 和 leanprover/comparator 独立检查主陈述。