rwst/Square-Roots
A Lean 4 / Mathlib development of a paper, which answers a problem by Dubickas. Dubickas (Glasgow Math. J. 48 (2006), 331–336) splits the reals α > 1 in two: α lies in 𝒵 when some real ξ ≠ 0 makes every integral part ⌊ξαⁿ⌋, n ≥ 1, even, and in 𝒮 otherwise. At α = 3/2 this is Mahler's question, and open; his Problem 3 asks whether √3 lies in 𝒮 or in 𝒵. This formalization settles that question and the whole square-root slice: √3 ∈ 𝒵 by an explicit ξ = 1.34160899796…, and for an integer m ≥ 2 one has √m ∈ 𝒮 exactly when m = 2. The cells √5, √6, √7, √8 put four explicit points of 𝒵 in the…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-23-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-23-000002/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-23-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'