What we need from you
Seven ways to move this problem
Each ask below says what it is in plain words, what it is exactly, what we already have, and what you would need to know. None requires permission. Everything we have is in the trove and the repository. The statements in full, with definitions, are on the exact page.
1. The white-band lemma Open
Plain words
Show that the forced left side of a pattern with an alternating centre cannot stay white for ever at any depth. Not "white runs are bounded": they grow with depth. Just finite, at every depth.
Exactly
Beside the wall x₀(t) = t mod 2, the left half-plane is determined by column 1 (left permutivity: x(i−1, t) = x(i, t+1) XOR (x(i, t) OR x(i+1, t))). Call a column-1 sequence real if some configuration beside the wall produces it. For a depth d, let R(d) be the supremum over real sequences of the length of the white run of the left row at time 0 starting at depth d. Prove R(d) < ∞ for every d.
What we have. R(d) exactly to depth 120 and at 125, 132, 139, 142, 143 and 147, with the configurations achieving it; the values grow (21 at 125; 17 at 132, 139, 142 and 143; 18 at 147; at least 23 at 133; at least 38 at depth 1,035 by sampling; drawn depth by depth). Theorem B proves finiteness when column 1 is periodic over the relevant window, and GC1148 and GC1151, proof sketches not yet second-read, bound it for the two pure "rings" column 1 can run in, with gaps 5 and 6. At depths 132 and 139 the exact mechanism that ends the record is known: the white extension would force a certified forbidden word of length 24 into column 1, or is read off the masked samples. What you would need: combinatorics on words, automata, and the certified forbidden-word lists in the trove.
Sources. PERIOD-TWO.md section 2 and row Q6; CHAT-LEDGER.14.md CL355, GC1148, GC1151, GC1153, GC1155 to GC1157, CL356, CL359; L643 (the census).
2. Conjecture LR for the kicked wheel Open
Plain words
Beside an alternating centre the next column is a rotation with kicks. Show that no such column, kicked however it may be, lets the left side become empty.
Exactly
Conjecture LR: no column 1 beside the alternating wall makes the left half eventually white. Proved when column 1 is eventually periodic (Jen) and when it is Sturmian (Theorem E, section 8.57), and for near-squares, block codes of Sturmian words and resets that come further apart than geometrically (Corollary F, Theorems E″, A⁗). Open for the real column, whose kicks after a settled wheel fall in at most four classes with short size ranges, and in three after 140 steps (Propositions 13 and 14).
Sources. RULE30-PRIZE.md sections 8.13, 8.54, 8.57; PERIOD-TWO.md row Q7; PROOFS.md entry 26.
3. The counting form Open
Plain words
Count the starting patterns of a given width whose centre stays alternating for T steps, and show the count shrinks by a fixed fraction with every step.
Exactly
Let N(w, T) be the number of configurations on w cells whose centre reads 0101… for T steps. Prove N(w, T) ≤ 2^(w − αT + c) for some α > 0. Measured: α close to 1 at w = 24. Proved: the part paid by the seed's left part (section 8.51). Open: the right part. The same statement for Collatz, with the free bits in place of the left part, is in COLLATZ-PRIZE.md section 1.
Sources. RULE30-PRIZE.md section 8.51; PERIOD-TWO.md section 7, question 1; COLLATZ-PRIZE.md section 1.
4. Read our proofs
309 statements have a written proof and a second reader inside the project: the 301 second-read proof pages, and eight results of 14 October recorded in MAHLER.md section 2. None has been reviewed outside it. The ones that carry weight are Theorems A, B, E and the channel bound (RULE30-PRIZE.md sections 8.54, 8.57, 8.20 and 8.33). If you find an error, we want to know; if you confirm one, say so and we will record it with your name or handle.
5. Go deeper with a machine
The record census is exact to depth 120 and at six depths beyond, by SAT; machine-checked certificates back it to depth 111, at 113 and 114, and at 125, 132 and 143; 112, 115 to 120, 139 and 142 are solver verdicts (RULE30-PRIZE.md 8.108). Deeper exact values, and the exact values between 126 and 141 where only lower bounds of 18 are known, would tell the lemma hunters what the mechanism looks like at scale. The certified forbidden-word lists in git stop at 44 (one phase reached 48 on 11 October; that list is not yet in git). The code is in the repository under tests/probes; the formats are in the trove.
6. Formalise
Theorems A and B are already machine-checked in Lean (tests/probes/lean), by us. Theorem E and the solid-row proposition are short and elementary and are not. A Lean formalisation of either, or an outside review of our Lean files, would make the first outside-checked piece of this record.
First answered in part, 19 October 2026
The first outside-checked pieces arrived from Joshua Coon, working with the Astra and Argon AI models in GitHub Copilot: a Lean 4 library of 142 files on Mahler's 3/2 problem. It checks two of our Mahler results by machine: that Mahler's conjecture holds exactly when every bounded range of starts dies out, and the inequalities behind the ladder of residue problems. We rebuilt it and recomputed its numbers (the full entry). The Rule 30 asks above, Theorem E and the solid-row proposition, are still open to anyone.
7. Tell us what we missed
PRIOR-ART.md lists what we found: Jen, Condrey, Kopra, Kari and Kopra, Flatto, Lagarias and Pollington, Terras, Lagarias, Dubickas, Tao, Yolcu, Aaronson and Heule, and more. Several of our "new" results turned out to be known (for example, the window principle's complexity bound is Dubickas 2009). If a paper settles or sharpens anything above, send it.
First answered in part, 19 October 2026
The same library extends Dubickas's work of 2008 and 2009. It proves, in Lean and with explicit deadlines, that no number keeps its fractional parts of ξ·(3/2)n inside a window of length 3/8, or inside unions of total length 7/12, 2/3 and 25/36 (drawn and checked live). Joshua Coon, with Astra and Argon via GitHub Copilot; the full entry.
How we check a contribution
- A proof is read in full by one of us and the step it rests on is checked independently, by a second person or a program; a refutation waits for the author's reply before the record changes.
- A computation comes with its predictions written before it ran, its code, its data and a checksum; a certificate (SAT, DRAT) is adopted on sight once replayed.
- Failures are kept. A closed route is recorded with the reason it closes.
Sources. WORKFLOW-SAVED-MEMORY.md (the two-tier review rule, predictions first, failures retained) and WORKING-TOGETHER.md.