Claims

../

2026_07_15_snyder: A Lean 4 theorem credited to Colin Snyder of Star Fleet Math gives an infinite plane set in general position whose integer-distance graph has no finite proper coloring; linked by the formal-conjectures catalog, not audited in the corpus.

2026_07_17_lloyd_h: A countably infinite planar set with no three points collinear and no four concyclic whose integer-distance graph is triangle-free with infinite chromatic number; a forum proof claim with a Lean development, claimed.

---