VibeMathedMath problems solved with AI
Sign in

Problem 3 of Dubickas (2006): Is 3∈Z\sqrt{3} \in \mathcal{Z}?

Dubickas splits (1,+∞)(1,+\infty) into the set Z\mathcal{Z} of those α\alpha for which some nonzero real ξ\xi makes every integral part ⌊ξαn⌋\lfloor \xi\alpha^n \rfloor even, and its complement S\mathcal{S}; at α=3/2\alpha = 3/2 the question of which side one lies on is Mahler's. His Problem 3 asks which side 3\sqrt{3} is on. Answered: 3∈Z\sqrt{3} \in \mathcal{Z}, with the explicit witness ξ=1.34160899796112665163…\xi = 1.34160899796112665163\ldots, and more generally m∈S\sqrt{m} \in \mathcal{S} if and only if m=2m = 2. The mechanism is Cantor-set arithmetic rather than Diophantine approximation: since m 2\sqrt{m}^{\,2} is an integer, the two-scale problem collapses to a base-mm covering induction on restricted-digit expansions.

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Construction
Field
Distribution mod 1; Mahler Z-numbers
Posed by
Artūras Dubickas
Year posed
2006
Years open
20y
Solved
2026-08-21
Model
Fable 5, Opus 5
Vendor
Anthropic
Collaborators
Ralf Stephan
Verification
Lean-checked, statement unaudited
Publication
Preprint
Significance
20 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Answers Problem 3 and generalizes it: the classification m∈S  ⟺  m=2\sqrt{m} \in \mathcal{S} \iff m = 2 covers every square root, and a further theorem replaces parity by divisibility by any p≥2p \ge 2. Note the scope of the machine-checking, which is narrower than the paper: the author states that the case m=3m = 3 is what is verified in Lean, and the repository flags the thickness computation of section 4.1 and all of section 8 as not formalized.

What the AI did

The author's account: "The mathematical discovery is the Fable-5 agent's; the formalization is the Fable-5 and Opus-5 agents'; the agents also drafted the prose of the companion paper, which the author revised; the direction and the review are the author's, who is responsible for the mathematical content." The Lean development carries the same framing in its copyright line, "in collaboration with Claude Code".

Verification

The Lean was read here on 22 August 2026, at github.com/rwst/Square-Roots: eleven modules totalling 4415 lines with zero sorry, zero declared axioms and no native_decide, comparator.json permitting only propext, Quot.sound and Classical.choice, and the MahlerZ and S definitions faithful to the statement above. Challenge.lean's ten sorries are the placeholders a comparator challenge is meant to carry, and it imports nothing from the development. Recorded lean-checked rather than lean-verified, which the submission claimed, because that rung wants kernel-checking AND an independent anchor and this has neither: the repository has no CI workflow and no runs, so nothing has compiled it, and the challenge file is written by the author of the proof. The README also flags that the thickness computation of section 4.1 and all of section 8 are not formalized, and the paper's abstract says it is the case m = 3 that is verified in Lean.

Sources

Submitted by LucidKestrel185 on

Changelog2 changes

Discussion