---

Jackson and Mauldin prove that there is a set $S\subseteq\mathbb R^2$ such that every isometric copy of $\mathbb Z^2$, that is, every translated and rotated copy of the integer lattice, meets $S$ in exactly one point. Equivalently, every set congruent to $S$ contains exactly one point of $\mathbb Z^2$, which answers the question of Problem 215 affirmatively. The theorem is proved in ZFC; the construction is a transfinite one that uses the axiom of choice, and Erdős had expected that no such set exists. The authors prove the stronger statement that $S$ can be chosen so that no two of its points are at a distance whose square is an integer. The source card [[../library/discrete_geometry/jackson_2002_sets_meeting_isometric_copies_lattice_exactly_one_point/_index|records the announcement's Theorems 1.1 and 1.2]] and the question, left open there, of whether a Lebesgue measurable such set exists.

The result is refereed twice. The detailed proof is Steve Jackson and R. Daniel Mauldin, On a lattice problem of H. Steinhaus, J. Amer. Math. Soc. 15 (2002), no. 4, 817-856, published electronically on 2002-06-13; the announcement cited by the site is Steve Jackson and R. Daniel Mauldin, Sets meeting isometric copies of the lattice $\mathbb Z^2$ in exactly one point, Proc. Natl. Acad. Sci. USA 99 (2002), no. 25, 15883-15887. The site's curator, T. F. Bloom, marks the problem proved and credits the result to this work.

The site's label carries a Lean qualification: the formal-conjectures entry for the problem points to a Lean development in the lean-proofs repository that declares itself a formalization of Jackson and Mauldin's solution, with the systems Codex and GPT-5.6 Sol named as its formal authors (the formalization link above, at its pinned commit). This corpus has not built or audited that development, so it is recorded as a link and not as evidence. No proof was checked here.