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

> No regular icosahedron in 3D space has a rational point on every face, proved via exact arithmetic and fully verified in Lean 4.

- **Source:** [arXiv](https://arxiv.org/abs/2611.11577)
- **Published:** 2026-11-14
- **Permalink:** https://picx.dev/p/ZW8H4W
- **Whiteboard:** https://picx.dev/p/ZW8H4W/image

## Summary

## Summary (Overview)

- **Main theorem**: No regular icosahedron in $\mathbb{R}^3$ has a rational point on each of its twenty closed triangular faces, in any position, size, orientation, or reflection. This answers a question posed by I. Bogdanov on MathOverflow.
- **Proof strategy**: The problem is reduced via a field automorphism of $\mathbb{C}$ sending $\sqrt{5}$ to $-\sqrt{5}$ to a statement about complex orthogonal matrices: for every $T \in SO(3, \mathbb{C})$, some real linear combination of $\text{Re}\,T$ and $\text{Im}\,T$ separates ten intervals determined by the faces.
- **Computer-assisted verification**: The separation theorem is proven by a case analysis over rational parametrizations of rotation frames, where every inequality is an exact polynomial bound over $\mathbb{Z}[\varphi]$ with $\varphi = (1+\sqrt{5})/2$ — no floating-point arithmetic or Lipschitz estimates are used.
- **Formal verification in Lean**: The entire argument, including 48 certificates, is formalized in the Lean 4 proof assistant with Mathlib and checked by the Lean kernel. The main theorem depends only on standard axioms.
- **AI-assisted development**: The mathematical argument was developed by OpenAI Codex, and the Lean formalization by Anthropic Claude, both under the direction of the author.

## Introduction and Theoretical Foundation

The question of whether a regular icosahedron can contain a rational point on each of its faces was posed by Ilya Bogdanov on MathOverflow in August 2023. For other Platonic solids, the answer is positive and easy: regular tetrahedra, cubes, and octahedra may have all vertices rational, and eight vertices of a regular dodecahedron form a cube. A regular icosahedron cannot have all vertices rational since there is no regular pentagon in an integer lattice of any dimension, but this alone says nothing about one rational point per face.

**Theorem 1.1.** Let $I \subset \mathbb{R}^3$ be a regular icosahedron. Then at least one of the twenty closed triangular faces of $I$ contains no point of $\mathbb{Q}^3$.

Key background facts:
- Points on edges and vertices are allowed; a face is the closed triangle.
- J. Rouse gave a regular icosahedron and six rational points that together lie on all twenty face planes, so the analogue for planes has a positive answer.
- The planar analogue is known: there is no regular pentagon with a rational point on each edge. This proof is algebraic and works even for rational points on the lines through the edges.

The proof has two parts:
1. **Algebraic part (Section 2)**: The face planes are defined over $K = \mathbb{Q}(\sqrt{5})$; applying an automorphism $\tau$ of $\mathbb{C}$ with $\tau(\sqrt{5}) = -\sqrt{5}$ reduces a hypothetical solution to a complex orthogonal matrix $T \in SO(3, \mathbb{C})$ such that ten real intervals have a common point.
2. **Analytic/combinatorial part (Sections 3–4)**: Shows this never happens via a compact parameter space checked on finitely many cells by exact arithmetic.

## Methodology

### 2. Reduction to Complex Orthogonal Matrices

Let $\varphi = (1+\sqrt{5})/2$, $\varphi' = 1-\varphi = (1-\sqrt{5})/2$, $K = \mathbb{Q}(\sqrt{5})$, and let $x \mapsto x'$ denote the nontrivial automorphism of $K$. The canonical icosahedron $I_0$ has twelve vertices obtained from $(0, \pm 1, \pm \varphi)$ by cyclic permutations, with edge length 2. Every regular icosahedron is the image of $I_0$ under $x \mapsto t + sRx$ with $t \in \mathbb{R}^3$, $s > 0$ and $R$ orthogonal.

**Lemma 2.1 (centering)**. Suppose both $t + sRF_i$ and the opposite face $t + sR(-F_i)$ contain rational points. Then there is $m \in F_i$ with $sRm \in \mathbb{Q}^3$.

**Lemma 2.2.** There is a field automorphism $\tau$ of $\mathbb{C}$ with $\tau(\sqrt{5}) = -\sqrt{5}$, i.e., $\tau(\varphi) = \varphi'$.

For a real matrix $A$ and $0 \leq i \leq 9$, $0 \leq k \leq 2$, define:

$$f_{ik}(A) = n_i^{\prime\top} A v_{ik}, \qquad J_i(A) = \left[\min_k f_{ik}(A), \max_k f_{ik}(A)\right]$$

where $n_i'$ are conjugate normals and $v_{ik}$ are vertices of face $F_i$. We say $A$ **separates** if $J_0(A), \ldots, J_9(A)$ have no common point.

**Proposition 2.3.** If every face of $t + sRI_0$ contains a rational point, then the matrix $T = (R^\tau)^\top R$ (where $\tau$ is applied entrywise) satisfies $T^\top T = I$ and $\det T = 1$, and no matrix $\alpha\,\text{Re}\,T + \beta\,\text{Im}\,T$ with $\alpha, \beta \in \mathbb{R}$ separates.

**Theorem 2.4 (separation)**. For every $T \in M_3(\mathbb{C})$ with $T^\top T = I$ and $\det T = 1$, there are $\alpha, \beta \in \mathbb{R}$ such that $\alpha\,\text{Re}\,T + \beta\,\text{Im}\,T$ separates.

### 3. Proof of the Separation Theorem

**Chart frames**: For $u, v \in \mathbb{R}$, let $Q(u,v)$ be the unnormalized rotation matrix of the quaternion $1 + u\mathbf{i} + v\mathbf{j}$:

$$Q(u,v) = \begin{pmatrix} 1+u^2-v^2 & 2uv & 2v \\ 2uv & 1-u^2+v^2 & -2u \\ -2v & 2u & 1-u^2-v^2 \end{pmatrix}, \qquad \mu(u,v) = 1+u^2+v^2$$

Then $Q^\top Q = QQ^\top = \mu^2 I$ and $\det Q = \mu^3$, so $Q/\mu \in SO(3)$. Let $P_0, \ldots, P_5$ be signed permutation matrices with columns $e_i, \sigma e_j, \sigma e_k$ where $(i,j,k)$ is a cyclic shift of $(1,2,3)$ and $\sigma = \pm 1$. The chart frame is $\mathrm{Fr}_c(u,v) = P_c Q(u,v)$.

**Lemma 3.1 (six charts)**. For every unit vector $d \in \mathbb{R}^3$ there are $c \in \{0, \ldots, 5\}$ and $u, v$ with $|u|, |v| \leq 1/2$ and $\mathrm{Fr}_c(u,v)e_3 = \mu(u,v)d$.

**Theorem 3.2 (certificates)**:
- **(R)** For every chart $c$, every sign $\sigma = \pm 1$ and all $|u|, |v| \leq 1/2$, $|t| \leq 1$, the matrix $\mathrm{Fr}_c(u,v)M_r(\sigma, t)$ separates.
- **(C)** For every pair of charts $c_1, c_2$ and all $u, v, u', v' \in [-1/2, 1/2]$, there is a triple $(X, Y, D)$ from Table 1 such that for all $z \in [-1, 1]$ the matrix $\mathrm{Fr}_{c_1}(u,v)M_c(X, Y, Dz)\mathrm{Fr}_{c_2}(u',v')^\top$ separates.

where:

$$M_r(\sigma, t) = \operatorname{diag}\left(\sigma((1-t^2)I_2 + 2tJ), 1+t^2\right), \quad M_c(x,y,z) = \operatorname{diag}(xI_2 + yJ, z)$$

with $J = \begin{pmatrix} 0 & -1 \\ 1 & 0 \end{pmatrix}$.

**Table 1: The sixteen phases $(\pm X, Y, D)$, $X^2 + Y^2 = D^2$**

| X | 1 | 99 | 12 | 91 | 119 | 161 | 5 | 20 | 0 |
|---|---|---|---|---|---|---|---|---|---|
| Y | 0 | 20 | 5 | 60 | 120 | 240 | 12 | 99 | 1 |
| D | 1 | 101 | 13 | 109 | 169 | 289 | 13 | 101 | 1 |

These are the nine listed triples plus the seven triples $(-X, Y, D)$ with $X \neq 0, 1$; they represent directions in the upper half plane.

**Key lemmas**:

**Lemma 3.3 (frame decomposition)**. Let $T^\top T = I$, $\det T = 1$, let $b \in \mathbb{R}^3$ satisfy $Yb = 0$; and let chart frames $F_1 = \mathrm{Fr}_{c_1}(u,v)$, $F_2 = \mathrm{Fr}_{c_2}(u',v')$ satisfy $F_1 e_3 = \mu Xb$ and $F_2 e_3 = \mu' b$. Then there are $p, r \in \mathbb{C}$ with $p^2 + r^2 = 1$ and:

$$F_1^\top T F_2 = \mu\mu' \operatorname{diag}(pI_2 + rJ, 1)$$

**Lemma 3.4**. If $\text{Im}\,T = 0$, then $\text{Re}\,T = \gamma\,\mathrm{Fr}_c(u,v)M_r(\sigma, t)$ for some $\gamma > 0$, chart $c$, sign $\sigma$ and $|u|, |v| \leq 1/2$, $|t| \leq 1$.

**Lemma 3.5**. There is a unit vector $b \in \mathbb{R}^3$ with $Yb = 0$; for it $\|Xb\| = 1$.

**Proposition 3.6**. Let $\text{Im}\,T \neq 0$. There are charts $c_1, c_2$ and $u, v, u', v' \in [-1/2, 1/2]$ such that for every $(X_0, Y_0, D)$ with $D > 0$ and $X_0^2 + Y_0^2 = D^2$ there are $\alpha, \beta \in \mathbb{R}$, $\gamma > 0$ and $z \in [-1, 1]$ with:

$$\alpha\,\text{Re}\,T + \beta\,\text{Im}\,T = \gamma\,\mathrm{Fr}_{c_1}(u,v)M_c(X_0, Y_0, Dz)\mathrm{Fr}_{c_2}(u',v')^\top$$

### 4. The Certificates

**Exact arithmetic**: All checks use natural numbers evaluated directly by the Lean kernel (arbitrary precision via GMP). An element $a + b\varphi$ of $\mathbb{Z}[\varphi]$ is stored as four naturals $(a^+, a^-, b^+, b^-)$. Its sign is decided exactly: with $w = 2a + b$, $a + b\varphi \geq 0$ iff $w + b\sqrt{5} \geq 0$, decided by comparing $w^2$ with $5b^2$ when $w$ and $b$ have opposite signs.

**Cells and polynomial bounds**: A cell of a chart square at level $m$ and index $j$ is $u = (2j + 1 - 2^m + s)/2^{m+1}$, $s \in [-1, 1]$. With $N = 2^{m+1}$, the entries of $N^2 Q(u,v)$ are quadratic polynomials in the cell coordinates with integer coefficients. For $A = \mathrm{Fr}_{c_1}M\mathrm{Fr}_{c_2}^\top$:

$$f_{ik}(A) = (\mathrm{Fr}_{c_1}^\top n_i') \cdot (M\mathrm{Fr}_{c_2}^\top v_{ik}) = (\text{positive constant}) \cdot a_i \cdot w_{ik}$$

where $a_i$ and $w_{ik}$ are vectors of polynomials of degree at most 2 over $\mathbb{Z}[\varphi]$. On $[-1,1]^2$, the polynomial $c_1s + c_2t + c_3s^2 + c_4st + c_5t^2$ is at least $\min(c_3, 0) + \min(c_5, 0) - |c_1| - |c_2| - |c_4|$, giving exact lower bounds.

**Real case (R)**: No certificate data needed. A search function `rsearch` takes a cell, chooses at its center $i_1$ maximizing $\min_k f_{ik}$ and $i_2$ minimizing $\max_k f_{ik}$, and checks whether $(i_1, i_2)$ separates the cell; if not, it splits and recurses with a bound of 40.

**Complex case (C)**: The search is guided by a tree stored as one natural number with hexadecimal digits: 0 = split into four, `1 n i₁ i₂` = leaf with phase $n$ and pair $(i_1, i_2)$ separating at $z = -1$ and $z = 1$, `2 n i₁ i₂ j₁ j₂` = leaf with two pairs separating adjacent z-intervals.

**Table 2: The certificate trees of the complex case**

| pairs of charts | 36 |
|---|---|
| leaves with one pair | 14,472 |
| leaves with two pairs | 4,896 |
| splits | 6,444 |
| maximal total level $m_1 + m_2$ | 6 |
| hexadecimal digits in all trees | 93,708 |

## Empirical Validation / Results

The proof was fully formalized in Lean 4 and checked by the Lean kernel. Key facts about the formalization:

**Main theorem statement in Lean**:
```txt
theorem no_rational_point_on_every_face (t : Fin 3 → R) (s : R) (hs : 0 < s)
(R : Matrix (Fin 3) (Fin 3) R) (hR : R ∈ Matrix.orthogonalGroup (Fin 3) R) :
¬ ∀ j : Fin 20, HasRatPoint t s R j
```

**Axioms used**: `#print axioms` gives `[propext, Classical.choice, Quot.sound]` — the standard axiom set.

**Table 3: Files of the Lean library Icosahedron**

| file | lines | content |
|---|---|---|
| Defs | 58 | the statement: icosahedron, faces, rational points |
| Geometry | 132 | face planes, opposite faces, conjugate normals |
| Embedding | 88 | Lemma 2.2 |
| Reduction | 165 | Lemma 2.1, Proposition 2.3 |
| KCheck | 487 | the checker: Z[φ], polynomials, searches, phases |
| KSound | 349 | soundness of the arithmetic and of the cell bound |
| KGeom | 535 | chart frames; soundness of both searches |
| Frames | 646 | Lemmas 3.1–3.5, Proposition 3.6 |
| CertR/*, CertC/* | | 48 certificates (decide + kernel), 110 KB |
| CertAll | 131 | collects the certificates |
| Separation | 38 | Theorem 2.4 |
| Main | 21 | Theorem 1.1 |

**Computational resources**: On an Intel Core i5-12500 with 32 GB memory, the kernel checks one real certificate in 0.5–2 minutes using up to 7 GB, and one complex certificate in 1.5–3 minutes using 8–13 GB. All 48 certificates take about 1.5 hours when checked sequentially.

## Theoretical and Practical Implications

- **Mathematical significance**: The theorem resolves a notable open question about Platonic solids. It shows that the icosahedron is unique among the five Platonic solids in this respect, highlighting the deep connection between the golden ratio $\varphi = (1+\sqrt{5})/2$ and rationality constraints.
- **Methodological innovation**: The proof demonstrates that the "no floating-point, no Lipschitz estimates" approach can handle genuinely three-dimensional geometric problems. The use of exact polynomial bounds over $\mathbb{Z}[\varphi]$ provides a template for rigorous computer-assisted proofs.
- **Formal verification milestone**: The proof is one of the first major mathematical theorems to be fully formalized in Lean 4 with all computational certificates checked by the kernel itself (via `decide + kernel`), rather than trusting external verified or unverified code. This sets a high standard for formalized computer-assisted proofs.
- **AI collaboration**: The paper documents an unusual workflow where AI systems (OpenAI Codex and Anthropic Claude) developed both the mathematical argument and the formalization under human direction. This demonstrates the potential of AI-assisted mathematical research, while the Lean kernel provides an independent check of correctness.

## Conclusion

The paper proves that no regular icosahedron in $\mathbb{R}^3$ has a rational point on each of its twenty closed faces, answering a question from MathOverflow. The proof combines:

1. An algebraic reduction using the field automorphism $\tau$ with $\tau(\sqrt{5}) = -\sqrt{5}$ to transform the problem into a statement about complex orthogonal matrices and interval separation.
2. A geometric decomposition showing that any such matrix can be represented using chart frames and either a real or complex canonical form.
3. A computer-assisted case analysis using exact polynomial bounds over $\mathbb{Z}[\varphi]$, with 48 certificates verified by the Lean proof assistant kernel.

Key future directions suggested by this work include:
- Extending the approach to other geometric problems involving rational points on polytopes.
- Further developing the methodology of kernel-checked certificates as a standard for formalized proofs.
- Exploring the potential of AI systems in producing both mathematical arguments and their formalizations, with human oversight and machine verification ensuring correctness.

---

_Markdown view of https://picx.dev/p/ZW8H4W, served by PicX — AI-generated visual whiteboard summaries of research papers._