rwst/Even-Integral
A Lean 4 / Mathlib development of a paper, which improves on 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 5 asks whether 𝒮 has an element greater than 2. This formalization decides 𝒮 versus 𝒵 for every quadratic Pisot number: the golden mean is the only one in 𝒮, so none greater than 2 lies there and Problem 5 loses its whole natural class of candidates, though the problem itself…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-20-000006
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-20-000006/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-20-000006/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'