Lean 4 形式化证明：正二十面体的 20 个面上不存在全有理点

一篇 arXiv 论文（编号 2611.11577）证明了：任意位置、大小和朝向的正二十面体，其 20 个闭面上不可能同时存在有理坐标点，回答了 MathOverflow 上 I. Bogdanov 提出的问题。 证明方法是利用把 √5 映射为 -√5 的复数域自同构，将问题化归为对每个复正交 3×3 矩阵 T 证明其 Re T 与 Im T 的某个实线性组合能分离由面确定的十个区间。随后通过旋转标架的有理参数化做计算机辅助的分支分析，所有不等式均为 Z[φ] 上的精确多项式界（φ=(1+√5)/2），全程未用浮点运算和 Lipschitz 估计。 整个论证连同 48 个证书都在 Lean 4 证明助手和 Mathlib 中完成形式化，由 Lean 内核检验，主定理只依赖标准公理。论文末尾声明，数学论证与形式化均由 OpenAI Codex 和 Anthropic Claude 在作者指导下完成。