Stability Radius of the Lamplighter Group
Dogon, Levit and Vigdorovich asked for an explicit upper bound on the stability radius of an infinitely presented group. The lamplighter group provides the first: explicit polynomial bounds on both its Hilbert-Schmidt stability rate and its stability radius, obtained through approximately invariant measures and an effective marker construction.
- Result
- Proved
- Status
- Resolved
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Group theory
- Posed by
- Alon Dogon, Arie Levit, Itamar Vigdorovich
- Year posed
- —
- Years open
- —
- Solved
- 2026-07-22
- Model
- ChatGPT 5.5, Aristotle
- Vendor
- OpenAI / Harmonic
- Collaborators
- Alon Dogon, Thomas Vidick
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 10 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
The disclosure separates the mathematics from the formalization. The authors had an exponential bound with a greedy marker construction; on being given the marker lemma, ChatGPT 5.5 produced the polynomial improvement, which is the paper's headline. The authors then recognized that the polynomial marker lemma follows from known descriptive-combinatorics techniques and holds for general group actions. The model also supplied the statement and proof of the Appendix A lower bound. Separately, after the paper was complete, Aristotle auto-formalized the main theorem in Lean over 64 prompts and roughly 14 partial days.
Verification
An Aristotle-produced Lean formalization of the main statement accompanies the paper, including background material not already in Mathlib, with a comparator file supplied so the formalized statement can be checked against the paper. We have not compiled it. arXiv preprint, not yet peer-reviewed.
Source
arXiv:2607.20135 - Polynomial Hilbert-Schmidt stability of the lamplighter group