Source authenticated

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

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.

Exact FrontierDelta

Prior state unknown→proved

Scope and record

Occurred: Aug 21, 2026

Delta type: SOURCE CLAIM

Assumptions: VibeMathed verification: lean-checked. Publication: preprint. AI contribution: ai-discovered. Editorial metadata: CC BY 4.0; linked content retains its own rights.

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

Confidence: Not scored

Registry verification: lean checked · preprint · candidate

Open the source record ↗

Attribution

VibeMathed
registry · event recorded by

Ralf Stephan
human · human collaborator

Fable 5
model · ai model contributor · Anthropic

Opus 5
model · ai model contributor · Anthropic

Evidence vector

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review

Named evidence

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

specialist registry · passed

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.

Source ↗