The Lyons–White conjecture: rate-monotonicity of distances for random walks on dihedral groups
Let be the dihedral group of order and run a continuous-time random walk on it driven by symmetric jump rates whose support generates the group. Call the pair rate-monotonic if, at every fixed time, the distance between the walk's distribution and the uniform distribution can only decrease when the rates are increased. Lyons and White (Ann. Probab. 51, 2023) proved this for and , found pairs that fail it for in , and asked whether any pair fails for or .
- Result
- Proved(see note)
- Status
- Resolved
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Random walks on finite groups; mixing; harmonic analysis on groups
- Posed by
- Russell Lyons and Graham White, Monotonicity for continuous-time random walks
- Year posed
- 2023
- Years open
- 3y
- Solved
- 2026-08-27
- Model
- AxiomProver
- Vendor
- Axiom Math
- Collaborators
- Colin Defant, Ken Ono
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 15 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
No such pair exists: for every positive integer and every , is rate-monotonic (Theorem A), and more generally so is every inversion extension of a finite abelian group by an involution, a family containing the generalized dihedral, dicyclic and generalized quaternion groups (Theorem B). The picture is completed in the other direction: for every real that is not an even integer there is an with not rate-monotonic (Theorem C), so the even integers are exactly the exponents for which monotonicity holds on the dihedral groups.
What the AI did
The paper's own account: "The proofs in this paper were generated through human-AI collaboration. In dialogue with AI, the human authors developed and formalized [Theorems A, B and C] with AxiomProver, an AI system currently under development by Axiom Math. In particular, this resulted in a formal Lean certificate for these three theorems." Both authors are at Axiom Math. Co-developed rather than assisted because the proofs themselves, not only the formalization, are described as produced in dialogue with the system; not discovered, because the humans directed the work and no autonomous run is claimed.
Verification
Lean-checked, statement unaudited, as with the other AxiomProver entries here. The repository AxiomMath/LyonsWhite carries a Challenge/Basic.lean statement surface and a Comparator configuration, and its README says the development was verified locally against the challenge; the paper says the formalization "assumes standard facts from analysis and group theory" and lists none, so the certificate is conditional on those assumptions and this site has not enumerated them or rebuilt the development. A thirteen-page preprint ten days old, not peer reviewed, no independent reader on record.
Sources
- PaperProof of the Lyons–White Conjecture (arXiv 2608.27708)
- Lean proofLean formalization (AxiomMath/LyonsWhite), Comparator-verified against Challenge/Basic.lean
- Lean statementChallenge/Basic.lean, the statement surface
- Problem recordLyons and White, Monotonicity for continuous-time random walks (the question)