Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 215
claims/: The 1 claim page of Problem 215, one per claimant's result; the problem's standing derives from them.
Statement. Does there exist such that every set congruent to (that is, after some translation and rotation) contains exactly one point from ?
Status. PROVED (LEAN).
Source. erdosproblems.com/215, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #215, https://www.erdosproblems.com/215.
References.
- [JaMa02] Jackson, Steve and Mauldin, R. Daniel, [[../library/discrete_geometry/jackson_2002_sets_meeting_isometric_copies_lattice_exactly_one_point/_index|Sets meeting isometric copies of the lattice in exactly one point]]. Proc. Natl. Acad. Sci. USA (2002), 15883-15887.
Formalization. Statement in formal-conjectures.
Current assessment
The question, asked by Steinhaus in the 1950s and apparently first printed by Sierpiński in 1958, is whether some set meets every translated and rotated copy of in exactly one point. Erdős expected that no such set exists.
The answer is yes, by one accepted full claim: Jackson and Mauldin (2002) construct such a set in ZFC, using the axiom of choice, with the extra property that no two of its points are at a distance whose square is an integer. The detailed proof is in the Journal of the American Mathematical Society and the announcement cited by the site in the Proceedings of the National Academy of Sciences; both are refereed and the site's curator credits the result. The frontmatter standing derives from this claim. The site's Lean qualification refers to a third-party Lean development that declares itself a formalization of the Jackson-Mauldin solution, linked from the formal-conjectures entry; this corpus has not built it, and the formal-conjectures file itself states the problem without a proof.
Whether a Lebesgue measurable such set exists is left open by the authors and is a variant, not the problem; no claim page records it.
Status search: the site's page and its formal-conjectures entry, the publishers' records of the two papers, and the Jackson-Mauldin source card, which digests the authors' preprint of the announcement. No proof was checked here.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.
- jackson_2002_sets_meeting_isometric_copies_lattice_exactly_one_point
- jackson_2002_sets_meeting_isometric_copies_lattice_exactly_one_point / theorem_1_1
- jackson_2002_sets_meeting_isometric_copies_lattice_exactly_one_point / theorem_1_2
- erdos_1983_combinatorial_problems_geometry
- erdos_1983_combinatorial_problems_geometry / problem_p47