Problem detail · source-aware
VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Dubickas splits $(1,+\infty)$ into the set $\mathcal{Z}$ of those $\alpha$ for which some nonzero real $\xi$ makes every integral part $\lfloor \xi\alpha^n \rfloor$ even, and its complement $\mathcal{S}$; at $\alpha = 3/2$ the question of which side one lies on is Mahler's. His Problem 3 asks which side $\sqrt{3}$ is on. Answered: $\sqrt{3} \in \mathcal{Z}$, with the explicit witness $\xi = 1.34160899796112665163\ldots$, and more generally $\sqrt{m} \in \mathcal{S}$ if and only if $m = 2$. The mechanism is Cantor-set arithmetic rather than Diophantine approximation: since $\sqrt{m}^{\,2}$ is an integer, the two-scale problem collapses to a base-$m$ covering induction on restricted-digit expansions.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.
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".
Provider: Anthropic · Prompt public: unknown · Independence: unknown
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 the cases m = 2 (reproof), m = 3, the cases m > 3, the p-divisibility theorem and the transcendentality theorem are all verified in Lean 4 and depend only on Lean’s three standard axioms.
Correctness: supported · statement fidelity: unaudited · peer review: none
Answers Problem 3 and generalizes it: the classification $\sqrt{m} \in \mathcal{S} \iff m = 2$ covers every square root, and a further theorem replaces parity by divisibility by any $p \ge 2$. Note the scope of the machine-checking, which is narrower than the paper: the author states that the case $m = 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.
Source-reported tools: construction.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.