Mahler's -number problem in its generalized form
Let be coprime integers and let be the set of whose fractional parts all lie in . The question for which parameters is empty remains open.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Computation
- Field
- Distribution mod one; Mahler's Z-numbers
- Posed by
- Mahler
- Year posed
- 1968
- Years open
- 58y
- Solved
- 2026-09-12
- Model
- Fable 5, Opus 5
- Vendor
- Anthropic
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 30 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem E gives : a window of length at base , beating the of [Dub19, Thm. 1.2], and with no assumption on the arithmetic nature of , where that result needs algebraicity. Mahler's problem itself is untouched: for which parameters is empty remains open, and this is a record window rather than a classification.
What the AI did
AI discovered theorems, formalized them and wrote a draft of the paper from the Lean.
Verification
Filed at Lean-checked, as submitted. Challenge2.lean is a trusted statement of record that imports nothing but Mathlib, redeclares verbatim every definition occurring in the certified theorems, and states the paper's lettered results with sorry proofs; comparator2.json names fourteen of them and, as configured, checks constant identity across the challenge and solution environments, restricts axioms to propext, Quot.sound and Classical.choice, and requires the Lean kernel to re-accept the solution from a fresh export with no olean loaded. That configuration reads correctly. It is not lifted to Lean-verified because no CI run was found on the repository and the comparator run was not reproduced here, so the machine check rests on the author's report - which is what Lean-checked means. PRIOR_ART.md is unusually candid and worth reading: it records that the search was targeted rather than exhaustive, that the whole of Section 3 was found in print with Theorems 3.5 and 3.6 a machine-checked fragment of [Bug04, Thm. 1], and concludes "Novelty is therefore recorded as unknown". Not peer reviewed and no independent expert endorsement.
Sources
Submitted by LucidKestrel185 on