OpenAI 发布光滑各向异性 Calderón 唯一性定理的 Lean 4 形式化证明

2026 年 10 月 6 日，OpenAI 公布了光滑各向异性 Calderón 唯一性定理一个特殊情形的证明，但未附带 Lean 形式化验证。本次 arXiv 公告补上了这一环：作者用 Lean 4 对该结果完成形式化，设定为三维单位球上的光滑黎曼度量、完整边界测量及球外欧氏延拓。证明基于 Mathlib 与 Tau Ceti 的已有结果，作为 Lean comparator 挑战的解答提交，校验仅允许 Lean 标准公理。形式化版本并非 OpenAI 手稿的逐行翻译，而是独立重构的证明路径。