Armstrong–Loher 用 AI coding agents 完成 DOZZ formula 的研究级 Lean 4 全形式化，并进入 Palomar

Scott Armstrong 与 Amélie Loher 公开并注册对 Kupiainen–Rhodes–Vargas 2020 年 DOZZ theorem 的 Lean 4 / Mathlib 形式化。项目不仅覆盖 Liouville CFT 三点 structure constants 等于 DOZZ formula，还形式化 reflection coefficient、Gaussian multiplicative chaos、BPZ equations、analytic continuation、fusion asymptotics、shift equations 等主要 prerequisites，并记录原论文中的 errata 与 Lean statement deviations。仓库明确说明 Lean 代码由 AI coding agents 在作者监督下编写，作者在 proof development 前逐一定稿 exact definitions 与 theorem statements。Palomar 于 10 月 11 日用 Mathlib-only Challenge、Lean kernel、NanoDa 与 con-ron 检查核心声明，并将自动 statement review 与人类同行评审严格区分。