Formally verified AI-assisted

Proof of the Lyons–White conjecture on rate-monotonic random walks

For continuous-time random walks on dihedral groups, raising the jump rates never increases the $\ell^p$ distance from the uniform distribution when $p$ is an even integer, and for every other $p \ge 1$ some dihedral group breaks this, which answers a question Lyons and White left open; all three theorems come with a Lean formalization produced by AxiomProver.

Lab: Axiom Math
Model: AxiomProver
Field: Mathematics
Date: 2026-08-27
Human collaborators: Colin Defant, Ken Ono
Problem posed: 2021 · open 5 yrs

Sources

Original work

arXivProof of the Lyons–White Conjecture↗GitHubAxiomMath/LyonsWhite, the Lean formalization and challenge file↗arXivLyons and White, Monotonicity for continuous-time random walks↗

Announcement

axiommath.aiAxiom Math: Faster Is Not Nearer↗

What was found

Lyons and White proved that for every finite group the $\ell^2$ and $\ell^\infty$ distances to stationarity are monotone in the rates, and found dihedral groups where monotonicity fails for exponents in $[1, 1.997]$ , $[2.001, 3.999]$ and $[4.001, 5.995]$ , but none at $p = 4$ or $p = 6$ , and asked why. Defant and Ono prove that $(D_n, 2m)$ is rate-monotonic for all positive integers $m$ and $n$ , extend this to every inversion extension of a finite abelian group by an involution (a family containing the generalized dihedral, dicyclic and generalized quaternion groups), and prove the converse: for every real $p \ge 1$ that is not an even integer, some $D_n$ fails. The paper's appendix says the proofs were generated through human-AI collaboration, with the authors developing and formalizing the three main theorems in dialogue with AxiomProver. The repository's challenge file, which it describes as written by humans, states those three theorems against Mathlib alone, and its Comparator configuration permits only propext, Quot.sound and Classical.choice, with the independent nanoda kernel enabled.

Novelty check

Lyons and White posed the question in 'Monotonicity for continuous-time random walks', arXiv:2109.10386 (September 2021), published in the Annals of Probability in 2023; the paper cites it and thanks Lyons for introducing the authors to the topic. No earlier answer for $p = 4$ or $p = 6$ was found, and on 2026-10-08 none of vibemathed, Palomar, ProofAtlas or MathDB carried a record of the result.

Caveats and known objections

Graded formal on the repository: a human-written challenge file with the three theorems, a Comparator configuration restricted to the three standard axioms, and a public CI build of commit 0cd9e3b1c5335869b304924d51bbba39327a17e9 that passed on 2026-08-27. That CI step is a plain build; the Comparator replay itself was not rerun for this entry and no third-party registration exists yet. The paper's abstract says the formal verification assumes 'standard literature'; the repository's Imported files re-export Mathlib lemmas as named theorems rather than declaring axioms, which is consistent with the axiom allowlist. Autonomy is graded ai-assisted on the strictest reading: Axiom Math's announcement, written by Defant, credits the mathematics to the two authors and describes AxiomProver as generating the Lean formalization, while the appendix says the theorems were developed in dialogue with the system without saying what the system contributed to the mathematics. If that contribution is documented as substantive the grade should move to collaborative. Both authors work at Axiom Math, which builds the prover, so nothing here is independent of the lab. Unrefereed at entry.

Nobody outside the lab has checked this yet.

Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.

Submit a check Challenge the grade

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

Entry history (1 event)

2026-10-12AddedEntered the registry graded Formally verified and AI-assisted.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Graded formally verified for verification and ai-assisted for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Proof of the Lyons–White conjecture on rate-monotonic random walks. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-27-lyons-white-conjecture

BibTeX

@misc{whataifound-axiommath-2026-conjecture,
  title        = {Proof of the Lyons–White conjecture on rate-monotonic random walks},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Axiom Math. Verification: Formally verified. Autonomy: AI-assisted.},
  url          = {https://whataifound.org/finding/2026-08-27-lyons-white-conjecture}
}

Related findings

ClaimedBrowning-Sawin conjecture on random sign-coefficient hypersurfaces proved, with a Lean formalization assuming existing literatureAxiom Math · 2026-09-16 ClaimedLean proof that the percolation probability vanishes at the critical point in every dimensionAnthropic · 2026-08-28 Formally verifiedErdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateralPlasma AI · 2026-10-19

probability random-walks group-theory lean formalization argument

← All mathematics findings in the registry