During Lean 4 formalization of a 2012 paper on Ehrenfest urns, we found that a key theorem’s proof does not work for an infinite family of degrees. The smallest counterexample is $d = 7{,}775$. The theorem itself is true, but the fix requires invoking Mihailescu’s theorem (the former Catalan conjecture). This post tells the story.

The Paper

In 2012, Albenque and Gerin published a beautiful paper in Discrete Mathematics and Theoretical Computer Science asking: what real numbers can you “compute” with a generalized Ehrenfest urn?

The model is simple. You have an urn with $n$ black and white balls. At each step, draw $k$ balls, count how many are black, and recolor all $k$ according to a fixed rule $f$. As $n \to \infty$, the fraction of black balls converges to a root of a certain polynomial $b(y)$ called the drift polynomial.

Their main result (Theorem 5) characterizes the set $\mathcal{L}$ of computable numbers:

1. $\mathcal{L}$ is symmetric about $1/2$.
2. $\mathcal{L}$ is dense in $[0,1]$.
3. $\mathcal{L}$ contains algebraic numbers of every degree $d \ge 1$.
4. $\mathcal{L}$ does not contain every algebraic number.

Parts (i), (ii), and (iv) have clean proofs. Part (iii) is where the trouble hides.

The Two-Sentence “Proof”

Here is the paper’s complete proof of (iii), quoted verbatim from page 11:

Fix $k \ge 1$ and consider the set $E = \{1\}$. The associated polynomial is $k\alpha(1 - \alpha)^{k-1} - \alpha$. Its unique root in $(0,1)$ is $x_0 = 1 - \sqrt[k-1]{1/k}$, which has algebraic degree $k - 1$.

Setting $k = d + 1$ is supposed to give degree $d$. That last clause — “which has algebraic degree $k - 1$” — is where the gap lives.

Why It Breaks

The number $\alpha = 1 - (d+1)^{-1/d}$ has the same algebraic degree as $\beta = (d+1)^{1/d}$, which is a root of $X^d - (d+1)$. By a classical criterion (Lang, Algebra, Theorem VI.9.1), the polynomial $X^n - a$ is irreducible over $\mathbb{Q}$ if and only if $a$ is not a $p$-th power in $\mathbb{Q}$ for any prime $p$ dividing $n$.

So $X^d - (d+1)$ is irreducible if and only if: for every prime $p \mid d$, the integer $d + 1$ is not a perfect $p$-th power.

This can fail.

The Counterexample

Take $d = 7{,}775$. Then:

• $d + 1 = 7{,}776 = 6^5$
• $d = 7{,}775 = 5^2 \times 311$, so $5 \mid d$

The factor $X^{1555} - 6$ is irreducible (since $1555 = 5 \times 311$, and $6$ is neither a 5th nor a 311th power). The root $6^{1/1555}$ has degree 1,555, not 7,775. The paper’s construction fails.

To make matters worse, $7775 \equiv 5 \pmod{6}$, which means the usual fallback — the rule $E = \{0\}$ with its Selmer polynomial $Y^d + Y - 1$ — also fails, because $Y^2 - Y + 1$ divides $Y^d + Y - 1$ whenever $d \equiv 5 \pmod{6}$.

This is not a one-off. The counterexamples form an infinite family. For any prime $q \ge 5$ with $q \equiv 5 \pmod{6}$ and even $m \ge 2$ with $m \equiv 1 \pmod{q}$, the degree $d = m^q - 1$ breaks both constructions.

The Fix

The theorem is still true. The repair uses a second singleton construction $E = \{2\}$ and a Newton polygon argument.

Newton polygon criterion. If $\binom{d+1}{2}$ has some prime $r$ with $r$-adic valuation exactly 1, then the Newton polygon of $P_B$ at $r$ is a single segment from $(0, 1)$ to $(d, 0)$ with slope $-1/d$. Since $\gcd(1, d) = 1$, the Eisenstein–Dumas theorem gives irreducibility.

The disjunction. For $d \equiv 5 \pmod{6}$, at least one of:

• (A) $d + 1$ is not a $p$-th power for any prime $p \mid d$ (Construction $E = \{1\}$ works), or
• (B) $\binom{d+1}{2}$ has a prime of valuation 1 (Construction $E = \{2\}$ works).

If both fail simultaneously, we get a Catalan-type equation: $a^p = u^q + 1$ with $p, q \ge 5$. By Mihailescu’s theorem (2002), the only solution to $x^m - y^n = 1$ with $x, y, m, n \ge 2$ is $3^2 - 2^3 = 1$. Since $p, q \ge 5$, no solution exists.

For the counterexample $d = 7{,}775$: $\binom{7776}{2} = 30{,}229{,}200 = 2^4 \cdot 3^5 \cdot 5^2 \cdot 311$, and the prime 311 has valuation 1. Construction B works.

The Formalization

This gap was found during Lean 4 formalization of Albenque–Gerin as part of the Ripple project — a framework for formalizing chemical reaction network computability. The file EhrenfestUrn.lean stands at 9,799 lines with zero sorry and zero errors. The complete proof of the corrected theorem is machine-checked, conditional on Mihailescu’s theorem (stated as a hypothesis, since it is not yet in Mathlib).

The full reduction chain — from the main theorem through two singleton constructions, Newton polygon irreducibility, Selmer–Ljunggren factorization, and rational non-computability, down to Mihailescu — is entirely formalized.

What This Means

Three observations.

The gap is real. This is not a “the details are routine” situation. The paper’s proof literally does not produce a number of the claimed degree for $d = 7{,}775$, and no obvious fix avoids deep number theory.

The theorem is true. Our fix works, but it draws on Mihailescu’s theorem — a result from a completely different area of mathematics than the combinatorics and probability that form the paper’s natural toolkit. It is unsurprising that this dependency was missed.

Formalization found it. The Lean proof assistant forced us to justify a claim that fourteen years of citing the paper had taken on faith. The irreducibility of a specific polynomial is the kind of assertion that looks obviously true in a handwritten proof but requires real work to verify in general.

This is, in a small way, what formal verification is for.

The corrected proof will appear as a short note. The Lean formalization is part of the Ripple framework for CRN-computable real numbers.

“The art of doing mathematics consists in finding that special case which contains all the germs of generality.”

— David Hilbert