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

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.

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.