Faster random clocks, farther away? The Lyons–White conjecture

The claim, in plain words

This is AX05. Take a regular pentagon with labelled corners. Its rotations and reflections form the dihedral group D_5, so the pentagon can sit in ten states. Give each move a random clock, running at the same rate as its inverse’s; when a clock rings, the machine makes that move. Over time, every state becomes equally likely. To measure how far the walk is from that balance, take each state’s gap from 1/10, raise it to a power p, add them up, and take the p-th root. Now speed up some clocks. Can the walk end up farther from balance?

The paper is Proof of the Lyons–White Conjecture, by Colin Defant and Ken Ono, both of Axiom Math: thirteen pages on the arXiv, version one of August 27, 2026. A group and a power p are called rate-monotonic if raising symmetric clock rates never increases the distance, at any fixed time. Theorem A: D_n with p = 2m is rate-monotonic, for all positive integers m and n. Theorem B extends this to inversion extensions of finite abelian groups, including dicyclic and generalized quaternion groups. Theorem C: for every real p greater than one that is not an even integer, some dihedral group is not rate-monotonic. The appendix says the proofs were generated through human-AI collaboration, with AxiomProver.

What it doesn’t claim

What is not claimed. Not that every walk misbehaves at 4.001: only some dihedral group, some rates and some time. Not p = 1 in Theorem C; for that case the paper cites Lyons and White’s own example on D_5. Not every finite group: Lyons and White found examples at exactly four on the symmetric group S_5. And not the paper’s broader conjecture, for groups with an abelian subgroup of index two, which is left open. The word conjecture is the paper’s; Lyons and White reported what their searches found.

Where it stands

Preprint on arXiv

Version 1, August 27, 2026 (the only version), 13 pages. Both authors give Axiom Math as their address.

Independent expert review

None named in our sources.

Peer reviewed

No journal publication found.

Lean proof, by Axiom

AxiomMath/LyonsWhite, published August 27, 2026 in one commit (an earlier repository, August 17, covers Theorem A alone). Axiom’s blog: “AxiomProver generated Lean/Mathlib formalizations of the central results.” The challenge file, “written by humans”, states Theorems A, B and C (C for p > 1); the comparator allows only Lean’s three standard axioms; README “locally verified with the comparator”; GitHub build check passed (a build, not a comparator run). The paper says the formalization “assumes standard facts from analysis and group theory”; our keyword scan finds no added axioms. Not built or run by us.

Last checked November 4, 2026. Where it stands. The arXiv has one version; we found no journal publication and no independent expert review. Both authors work at Axiom Math, which published the blog post. That post says AxiomProver generated the Lean, which appeared the same day as the paper, in one commit; an earlier repository, from August 17, covers Theorem A alone. The challenge file, described as written by humans, states Theorems A, B and C, with C for p greater than one, and the comparator allows only Lean’s three standard axioms. The README says it was locally verified with the comparator, and GitHub’s build check passed. Our keyword scan of its 81 Lean files finds sorry only in the three challenge statements. We did not build or run it.

This result is outside OpenAI’s math catalogue. If it holds, faster symmetric clocks never leave a dihedral walk farther from balance when distance uses an even power, and every other real power above one fails on some dihedral group: the puzzle Lyons and White found at four and six, answered by Defant and Ono with AxiomProver, with a Lean proof we did not run.

How the proof goes

1. History. Russell Lyons and Graham White studied this in a paper first posted in 2021. They proved that faster clocks never hurt when p is two or infinity, on every finite group. On dihedral groups, their computer searches found walks where faster is farther, for p from one to just below two, between two and four, and from 4.001 to 5.995; but none at exactly four, in groups up to D_131, and none at six. They wrote that they had no explanation for four or six. Our own example, from a computer search: on the pentagon, raise one reflection’s clock from two to twelve. With p = 1, the faster walk is up to about seven percent farther from balance, around time one; with p = 4, it is nearer at every time we computed.
2. Even powers. How the proof goes, in the authors’ account. For even powers, the rotations supply frequencies, and Fourier analysis reduces the key calculations to two by two matrices, whose positivity bounds one set of Fourier coefficients by another. Then the even power does the work: a sum of 2m-th powers is a sum of squares of m-th powers, so Parseval’s identity applies, and the products can be bounded term by term. For a reflection’s clock, differentiating the distance with Duhamel’s formula shows it never grows; rotations are handled more directly. The paper points to a close analogue in the Hardy–Littlewood majorant problem.
3. Other powers. For a p that is not even, the paper builds the bad walk from a negative Fourier coefficient. With p between 2m and 2m + 2, and K equal to 2m + 3, a cosine integral obeys a recurrence with factors (p − 2l)/(p + 2l), and only the last factor is negative. At 4.001, the factors are positive, tiny, then negative; at exactly four, in our arithmetic, one factor is zero. A small two-frequency perturbation, adjusted and scaled into a genuine walk, then drifts farther when a reflection’s clock speeds up.

The numbers in the video

• Ours: on the pentagon (D_5, 10 states), slower rates 2, 2, 1 on the reflections r³b, r²b, rb and 1.4 on the rotations r², r³; the faster walk raises r³b to 12. With p = 1 the faster walk is up to 6.9% farther from uniform (near t = 1; farther for t from 0.83 to 2.2); with p = 2 and p = 4 it is nearer at every time we computed (t from 0.05 to 3). Found by a computer search and rounded.
• Ours (a sample, not a proof): 238 random walks on D_3 to D_9 with one inverse pair sped up; for p = 2, 4, 6 the largest relative increase was at rounding level (below 10⁻¹⁰).
• Ours: the Lemma 3.1 cosine sum for p = 3 (K = 5) at n = 11 is -0.135; the recurrence factors are 1/5 and −1/7. At p = 4.001 (K = 7) they are 0.333, 0.000125 and -0.200; at p = 4 the same three factors are 1/3, 0 and −1/5.
• Ours (keyword scan, not an audit): Axiom’s repository has 81 Lean files (16,030 lines); sorry appears only in the 3 challenge statements.

Read the source

• “Proof of the Lyons–White Conjecture”, Colin Defant and Ken Ono, arXiv 2608.27708 (version 1, August 27, 2026, 13 pages).
• “Faster Is Not Nearer”, Axiom Math blog post by Colin Defant, October 5, 2026.
• The Lean repository (file headers say Apache 2.0; the repository has no license file; not run by us), and the earlier EvenExponentDihedralMonotonicity (Theorem A).
• Russell Lyons and Graham White, “Monotonicity for continuous-time random walks”, arXiv 2109.10386 (first posted September 21, 2021); Annals of Probability 51 (2023).

AI Proved What? is independent and not affiliated with Axiom Math, OpenAI, Russell Lyons or Graham White.

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.