Work sent to us, checked and credited

Who and what

Joshua Coon, with the Astra and Argon AI models in GitHub Copilot. Received by e-mail on 19 October 2026, with an invitation to link, reuse and cite. The work: github.com/jjc16/mahler-3-2-lean4, a library of 142 Lean 4 files built on Mathlib, and a 13-page paper, Formalizing the Reduced Mahler 3/2 Dynamical System in Lean 4. Please cite it as its author asks, in the repository's citation file.

In plain words

Lean is a program that checks proofs. It accepts a proof only if every step follows from the rules of logic and a few standard axioms, so a theorem Lean accepts has been checked line by line by a machine. Joshua Coon read this site and Mahler's question: can a number, multiplied by 3/2 again and again, keep its fractional part below one half for ever? Then Joshua Coon and the AI collaborators built a library of machine-checked theorems around it.

It does not settle Mahler's question, and it says so plainly. It met the same wall we did. In the 2-adic numbers, where the ordinary whole numbers live alongside stranger infinite ones, solutions exist, and nobody can yet show that none of them is an ordinary positive whole number. What the library does is map, with machine-checked certainty, a great deal of the ground in front of that wall.

What it proves (a selection)

• Windows past the known barrier. Flatto, Lagarias and Pollington showed in 1995 that no number keeps its fractional parts inside any interval shorter than 1/3. The library proves that no number keeps them in the window [1/6, 13/24), of length 3/8, nor in unions of several intervals with total length 7/12, 2/3 and 25/36. Each comes with a deadline: a number between 1 and 2^W leaves by step W + 12 to W + 16, depending on the set. A similar window is excluded for powers of 4/3. See them drawn and checked live.
• A known theorem, formalised in general. Dubickas's theorem of 2009, that powers of a rational number cannot stay in a small interval, is proved for every rational base p/q with q < p < q², with a deadline that grows only linearly in the number's size.
• Whole families of patterns ruled out. No Z-number can follow a two-letter Sturmian pattern, the Thue–Morse or period-doubling patterns in their encoded forms, or a pattern whose blocks grow too fast.
• The problem restated exactly. Mahler's conjecture holds exactly when the smallest positive start that survives N steps grows without bound as N grows.
• Concrete certificates. The start 149 survives 28 steps and fails at step 29; no start below 4,096 survives 29 steps; the 55-bit start 29,871,555,608,238,677 survives 113 steps and fails at step 114.
• Eighteen dead ends, written down. Exact identities showing why particular proof templates built on classical tools, such as Padé approximants, Ridout's theorem and the Subspace Theorem, stall on this problem. They guard those templates; they do not rule out the tools themselves.

How we checked it

We built it ourselves. On 19 and 20 October Cloud compiled the whole library from scratch, after removing every credential from the machine, since a build runs the author's own settings.

We read the statements. The main theorems are written directly in terms of the fractional part, so a reader can see that they say what the paper says.

We recomputed the numbers with our own code, written from the statements alone, with predictions written first (mahler_contrib_checks.py). Every claim we tested held: the deadlines of all five windows and unions for every number below 2¹⁰, the survival of 149 and of the 55-bit start, the bound at 4,096, and a valuation identity on 40,249 test starts.

Scope: Lean guarantees the proofs. We checked that the headline statements mean what they claim, and recomputed the concrete ones. The material added after 04ed5389 is compiled and audited but not yet recomputed by us. GPT, the project's second reader, has read selected statements and proofs independently.

Where it meets our record

The same numbers by two roads. Our census of 14 October found the longest survivor below 4,096 at 149, failing at step 29. Joshua Coon's library proves the same facts in Lean, by a different method.

Two of our results, checked by Lean from outside. One is that Mahler's conjecture is equivalent to "every bounded range of starts dies out". The other is the pair of inequalities behind the ladder of residue problems, whose first rung is the 5 mod 8 game. It is the first time any part of our record has been checked by someone outside the project.