Armstrong–Bou-Rabee–Kuusi 公开 159 万行 AI-assisted Lean，完整形式化 log-correlated potential 中的反常扩散极限

Scott Armstrong、Ahmed Bou-Rabee 与 Tuomo Kuusi 研究 log-correlated random potential 中 Brownian particle 的弱无序极限，证明其缩放极限相对 Brownian motion 奇异、可逆测度由 Gaussian multiplicative chaos 给出，并建立 quantitative homogenization、anomalous exit-time scaling 与 large-scale Hölder / Liouville 结果。配套 Lean 4 library 含 5,884 个文件、1,592,483 行，覆盖论文主要定理；公开仓库披露 Claude、OpenAI GPT 以及部分 DeepSeek、Mistral、GLM 模型参与 Lean 编写。项目报告无 `sorry`、无 `native_decide`、无新增公理，并用 Mathlib-only restatements、axiom audit 与 Lean/NanoDa/con-ron Comparator 检查主陈述。