OpenAI 发布光滑各向异性 Calderón 唯一性定理的 Lean 4 形式化证明
Formal Proof of an Anisotropic Calderón Uniqueness Theorem
OpenAI 那份 Calderón 唯一性定理证明当时没带 Lean 验证，现在有人用 Mathlib 和 Tau Ceti 补上了，还过了只许标准公理的 comparator 挑战。做形式化数学的朋友可以直接看这份独立重构，和原手稿对着读会很有收获。
2026 年 10 月 6 日，OpenAI 公布了光滑各向异性 Calderón 唯一性定理一个特殊情形的证明，但未附带 Lean 形式化验证。
本次 arXiv 公告补上了这一环：作者用 Lean 4 对该结果完成形式化，设定为三维单位球上的光滑黎曼度量、完整边界测量及球外欧氏延拓。证明基于 Mathlib 与 Tau Ceti 的已有结果，作为 Lean comparator 挑战的解答提交，校验仅允许 Lean 标准公理。
形式化版本并非 OpenAI 手稿的逐行翻译，而是独立重构的证明路径。
Formal Proof of an Anisotropic Calderón Uniqueness Theorem
We announce a Lean~4 formal proof of a special case of the smooth anisotropic Calderón uniqueness theorem released by OpenAI on October 6, 2026. We consider smooth Riemannian metrics on the three-dimensional unit ball, with full boundary measurements and Euclidean extensions outside the ball. OpenAI's release did not include a Lean proof of their uniqueness result. Our formalization uses results from Mathlib and Tau Ceti, and it is given as a solution to a Lean comparator challenge whose check permits only the standard axioms of Lean. The Lean proof is not a line-by-line translation of the OpenAI manuscript.
本条情报归属 AITOP「论文」核心栏目，重点聚焦北美前沿实验室与硅谷科技巨头。在跨区域产业观察坐标中，该动态直接关联「AI 开发者工具链、Coding Agent 与工程化实践」「中美大模型技术代差与商业化对照」研究主线，反映出当前技术演进与商业落地的最新风向。涉及核心实体与技术议题包括：OpenAI、Lean 4、Mathlib、形式化证明，读者可通过下方标签进入对应专题页查阅历史脉络与关联对比。
信源核验说明：本文原始信息发布自一手权威信源「arXiv: OpenAI」（Tier-1 一手发布），具备高确定性参考价值。
