Every cubic algebraic number is collapsible

Open

CollapsibleCubics.cubic_collapsible

by quesswho · 1 vote · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraalgebraic-numbersnumber-theoryopen-problempolynomials

Let $\alpha \in \mathbb{C}$ be an algebraic number of degree $3$ over $\mathbb{Q}$ , that is, an algebraic number whose minimal polynomial over $\mathbb{Q}$ has degree $3$ . The claim is that $\alpha$ is collapsible: there exists a split polynomial $f \in \mathbb{Q}[x]$ — one of degree at least $1$ that factors as $a\prod_i (x - r_i)$ with $a \in \mathbb{Q}^{\times}$ and every $r_i \in \mathbb{Q}$ — and a rational number $c$ with

f(\alpha) = c.

This is the first open case of the conjecture that every algebraic number is collapsible. Degrees $1$ and $2$ are settled. Degree $3$ is open for this one-step notion, and is not settled by the known cubic result for eventual collapsibility, which permits a composition of several split polynomials rather than a single one.

A proof would close the one-step cubic case. A disproof — a single cubic irrationality admitting no split $f$ with $f(\alpha) \in \mathbb{Q}$ — would separate one-step from eventual collapsibility by an explicit example, showing that composition is genuinely necessary.

Formalization Note "Cubic" is expressed as the minimal polynomial of $\alpha$ over $\mathbb{Q}$ having degree $3$ ; integrality over $\mathbb{Q}$ is stated explicitly, though it already follows from that degree condition. No bound is placed on $\deg f$ , and the value $c$ is not required to be nonzero — but $c = 0$ cannot occur, since it would force the irreducible cubic minimal polynomial to divide a polynomial that splits over $\mathbb{Q}$ .

Preamble

import Definitions.Def_CollapsibleCubics_basic

Formal statement

import Definitions.Def_CollapsibleCubics_basic

namespace CollapsibleCubics
theorem cubic_collapsible (α : ℂ) (hint : IsIntegral ℚ α)
    (hdeg : (minpoly ℚ α).natDegree = 3) :
    Collapsible α := by sorry
end CollapsibleCubics

Source

Miles, *Collapsible algebraic numbers*, blog post, 2026-08-20, https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ (definitions of *split* polynomial and of *1-collapsible*; statement that the degree-3 case of one-step collapsibility is open). Underlying problem: Griffin Macris, list of open problems, Problem 3, https://sites.google.com/view/griffinmacris/open-problems. The goal: the degree-3 case of one-step collapsibility, stated as open in the source blog post.

Read-back

What the Lean code literally says, in plain math · claude-opus-5

Fix a complex number $\alpha \in \mathbb{C}$ . Assume two hypotheses. First, $\alpha$ is integral over $\mathbb{Q}$ — that is, $\alpha$ is a root of some monic polynomial with rational coefficients. Second, the minimal polynomial of $\alpha$ over $\mathbb{Q}$ , written $m_\alpha \in \mathbb{Q}[X]$ , has degree exactly $3$ :

\deg m_\alpha = 3 .

(Here the degree is the natural-number degree, so the hypothesis asserts that this value is the number $3$ ; the degree- $3$ condition together with integrality forces $\alpha$ to be an algebraic number of degree $3$ over $\mathbb{Q}$ , hence the hypotheses are jointly satisfiable and not vacuous.)

Under these hypotheses the claim is that $\alpha$ is collapsible, where "collapsible" is a definition supplied by this bundle and must be unfolded. It is stated for an arbitrary field $K$ carrying a $\mathbb{Q}$ -algebra structure and an element $\alpha \in K$ ; here it is instantiated at $K = \mathbb{C}$ with its canonical $\mathbb{Q}$ -algebra structure. The definition says: there exists a polynomial $f \in \mathbb{Q}[X]$ such that

$f$ $f$ is split in the sense of this bundle, namely
- $\deg f > 0$ (the natural-number degree of $f$ is strictly positive), and
- there exist a rational number $a$ and a multiset $R$ of rational numbers with $a \neq 0$ and

f \;=\; a \cdot \prod_{r \in R} (X - r),

 the product being taken over the multiset $R$ with multiplicity (in particular $R$ may be the empty multiset, in which case the product is $1$ and $f = a$ is a nonzero constant — though that case is excluded by the requirement $\deg f > 0$; and $\deg f$ need not equal the size of $R$ as a separate stipulation, it is whatever the displayed factorization forces);

2. there exists a rational number $c$ such that evaluating $f$ at $\alpha$ inside $\mathbb{C}$ lands in the image of $\mathbb{Q}$ :

f(\alpha) \;=\; c \qquad \text{(more precisely, } \operatorname{aeval}_\alpha(f) = \iota(c)\text{, where } \iota : \mathbb{Q} \to \mathbb{C} \text{ is the algebra map).}

So the assertion is: for every complex number $\alpha$ that is integral over $\mathbb{Q}$ and whose minimal polynomial over $\mathbb{Q}$ has degree $3$ , there is a rational polynomial $f$ of strictly positive degree that factors over $\mathbb{Q}$ as a nonzero rational constant times a product of linear factors $X - r$ with all $r \in \mathbb{Q}$ , and a rational number $c$ , such that $f(\alpha) = c$ .

Note that nothing constrains the degree of $f$ relative to $3$ , nothing requires $f$ to be monic, nothing requires the roots $r$ to be distinct or related to $\alpha$ , and nothing requires $c \neq 0$ or $f$ to be nonconstant on $\alpha$ 's conjugates; the only conditions are the ones listed above.

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by quesswho · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph