AI Proof WatchKeep up with AI contributions

Even integral parts of powers of quadratic Pisot numbers

Ralf Stephan

Among real quadratic Pisot numbers α, the golden ratio is the only one in Dubickas’s set S: every other α admits a nonzero ξ for which all floors ⌊ξαⁿ⌋ are even for n≥1. For α=1+√2, ξ=(2−√2)/4 gives the exact Pell identity ⌊ξ(1+√2)⁽ⁿ⁺¹⁾⌋=Pₙ−[n odd].

Sources for this record

What was already known

Dubickas introduced S and supplied four of the five cases needed for this classification. The 1+√2 case and full quadratic-Pisot classification remained; his broader question for α>2 remains open.

AI involvement AI-led

Stephan chose the problem and revised the paper. He credits Claude Opus 5 with the multiplier, trace-parity method, five-cell classification and Lean proof.

Claude originated the multiplier, trace-parity mechanism and five-cell classification under Stephan's direction.

Importance Notable

Settles the missing quadratic case and classifies a natural family in Dubickas’s problem.

Limitations

The conclusion concerns quadratic Pisot numbers, not every α>2. The separate designed-divisibility theorem is outside this assessment, and historical priority beyond the cited comparison is uncertain.

Technical verification Formal (Lean 4/Mathlib kernel and Comparator)

The source reports a successful Lean/Mathlib proof and Comparator check of every clause of Theorems A–D, including the classification, Pell identity and silver-number membership, under the three standard axioms. Stephan's statement comparison is not a completed human proof check, and the separate exact-arithmetic sweep is finite testing. The review did not reproduce the build.

Formal checking

challenge/solution comparison, axiom audit and kernel replay via lake test

Checker
Repository Comparator and Lean kernel
Scope
SZ.quadPisot_mem_S_iff, SZ.quadPisot_notMem_S_of_two_lt, SZ.floor_silver_pell, SZ.even_floor_silver and SZ.silver_mem_MahlerZ at the pinned revision
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

Stephan revised the agent-drafted paper and checked statements, but the sources do not document a human explanation of the new multiplier and trace-parity mechanism. Few is a missing-evidence default, not a finding that Stephan cannot understand them.

Correction and publication history

2026-10-18 · publication

Settles the missing quadratic case and classifies a natural family in Dubickas’s problem.

Read this published revision