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

证明方法是利用把 √5 映射为 -√5 的复数域自同构，将问题化归为对每个复正交 3×3 矩阵 T 证明其 Re T 与 Im T 的某个实线性组合能分离由面确定的十个区间。随后通过旋转标架的有理参数化做计算机辅助的分支分析，所有不等式均为 Z[φ] 上的精确多项式界（φ=(1+√5)/2），全程未用浮点运算和 Lipschitz 估计。

整个论证连同 48 个证书都在 Lean 4 证明助手和 Mathlib 中完成形式化，由 Lean 内核检验，主定理只依赖标准公理。论文末尾声明，数学论证与形式化均由 OpenAI Codex 和 Anthropic Claude 在作者指导下完成。

No regular icosahedron has a rational point on every face: a proof checked in Lean

We prove that no regular icosahedron in $\mathbb{R}^3$ has a point with rational coordinates on each of its twenty closed faces, in every position, size and orientation, reflections included. This answers a question of I. Bogdanov on MathOverflow. A field automorphism of $\mathbb{C}$ that sends $\sqrt5$ to $-\sqrt5$ reduces the problem to the following statement: for every complex orthogonal $3\times3$ matrix $T$ some real linear combination of $\mathrm{Re}\,T$ and $\mathrm{Im}\,T$ separates ten intervals determined by the faces. We prove this statement by a computer-assisted case analysis over rational parametrizations of rotation frames, in which every inequality is an exact polynomial bound over $\mathbb{Z}[\varphi]$, $\varphi=(1+\sqrt5)/2$; no floating-point arithmetic and no Lipschitz estimates are used. The whole argument, including the $48$ certificates, is formalized in the Lean 4 proof assistant with Mathlib and checked by the Lean kernel; the main theorem depends only on the standard axioms. The mathematical argument and the formalization were produced by AI systems (OpenAI Codex and Anthropic Claude) under the direction of the author; see the statement at the end of the paper.

This report is categorized under AITOP's "Papers" desk. Within our cross-regional analytical framework, it directly maps to AI developer toolchains, coding agents, and engineering workflows. Key entities and technical topics under continuous tracking include Lean 4, Mathlib, OpenAI Codex, Claude.

Primary source verification: published directly by arXiv: Anthropic with first-party authority.