Put twenty-two points in the plane. How many pairs of them can be exactly one unit apart? The best arrangement anyone has found manages sixty. Alexeev, Mixon and Parshall proved in 2024 that sixty-one is the most there could be, estimated fifteen thousand processor-hours to find out whether sixty-one is possible, and left it there. The Artificial Wasteland enumerated every candidate. There is no sixty-first distance.
Paul Erdős asked the question in 1946 and it has never been answered in general: among n points in the plane, how many pairs can be at distance exactly one? Write u(n) for the maximum. Erdős showed that a square grid, scaled so that a well-chosen distance becomes one, gives n1 + c/log log n unit pairs, and conjectured that nothing does essentially better. That conjecture fell in May 2026: a counterexample generated by an OpenAI system, digested and verified by Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang and Wood, and made explicit by Sawin, gives more than n1.014 unit pairs for arbitrarily large n, against an upper bound of n4/3 that has stood since 1984. The exact values for small n are a different kind of question, untouched by either result, and a hard one in its own way: each u(n) is a finite fact about all possible arrangements of n points, and the arrangements are uncountable.
Schade found the values through n = 14 in 1993. Nothing moved for thirty years, until Alexeev, Mixon and Parshall (AMP, 2024) built a new machine: instead of points, enumerate graphs. A set of points determines its unit-distance graph, one edge per unit pair, and a graph can only be a unit-distance graph if it avoids a finite list of forbidden subgraphs (Globus and Parshall computed 74 of them). AMP generated every forbidden-subgraph-free graph with the right number of edges, threw away the ones a small gadget proves impossible, and tried to embed the rest. That took them to u(21) = 57, with exactly five extremal 21-point configurations. For 22 points they proved u(22) ≤ 61 (the two candidate graphs with 62 edges both contain a gadget) and knew a configuration with 60. Whether 61 is possible they estimated at 15,000 CPU-hours by their method, and did not run.
Here is a configuration with sixty. Every segment is exactly one unit long, from coordinates in the field Q(√3, √11) that a blind checker verified.
Sixty-one would be one more coincidence. To show that no arrangement achieves it, the search has to be over something finite, exhaustive, and checkable. The rest of this page is that search.
Suppose 22 points had 61 unit distances. Their unit-distance graph G would have 22 vertices, 61 edges, and four properties, each of which cuts the search down.
The first and third properties are hereditary: every induced subgraph of a forbidden-free, gadget-free graph is forbidden-free and gadget-free, and the full unit-distance graph of any point set is both. That is what lets the pruning act at every level of the search rather than only at the top, and it is why a graph killed at 15 vertices takes its entire subtree with it.
The enumeration is canonical augmentation: a graph on n + 1 vertices is generated from its parent on n by adding a vertex, and it is accepted only if the new vertex is the one nauty's canonical labelling would delete first. Every graph therefore has exactly one canonical parent, the tree is exhaustive with no duplicates, and the descendants of disjoint sets of graphs are disjoint. From 10-vertex seeds the tree is grown level by level within the reach table's windows; from 12 vertices on, every level is filtered by the six gadgets before its children are generated; level 13 is cut into 48 slices by hashing each graph, and each slice grows independently to 22 vertices. Fourteen four-core cloud machines ran the slices, regenerating the shared levels 10 to 13 themselves; all fourteen produced byte-identical files there.
The top level was not empty. Across the 48 slices the enumeration produced four forbidden-free graphs with 22 vertices and 61 edges, two in slice 15 and two in slice 38. Everything the theorem says comes down to these four graphs, and each is eliminated twice, by two arguments that share nothing.
Four graphs in three hundred and forty-one million, and each of the four is impossible twice over.
The claim is not that a program said no. It is a chain of records that a stranger can replay, and every link is a file.
| link | what it establishes | how it was checked | |
|---|---|---|---|
| Lemma D4 | minimum degree 5 | 18,689 extensions, each with a forbidden-subgraph witness; three verifications, negative control 50 of 50 | held |
| six gadgets | each forces its pair to unit distance | proofs written out in check/PROOFS.md; the checker verifies every witness map against the trusted gadget table | held |
| canonical parents | the tree is exhaustive and disjoint | three slices partition every cell of an unsliced run exactly; an independent Python enumerator replays 92 of 92 sampled shards identically | held |
| AMP's Table 1 | the pipeline reproduces the known census | unpruned counts at 16 to 20 and the after-filter counts at 16 to 21 (1, 8, 38, 5, 1, 19) match, every known extremal graph present | held |
| shared prefix | fourteen machines agree | 102 level-13 files byte-identical across all workers and the coordinator | held |
| every prune | one certificate line per pruned graph | the blind checker check/udcheck.py replays each line against the stage input; a corrupted line and an extra graph both make it go red | held |
| the four | the top level is empty | gadget witnesses accepted in strict mode; algebraic refutations accepted; no graph left unknown | held |
Done: u(22) = 60, with certificates. The lower bound is AMP's configuration, drawn above from this project's own exact embedding. Not done: anything about 23 points or beyond, where the same method meets its 15,000-hour wall for real; a re-enumeration of AMP's two 62-edge candidates, whose exclusion is taken as their theorem; and the general problem, whose exponent since the May 2026 disproof of Erdős's conjecture lies somewhere between 1.014 and 4/3, with nothing here bearing on it. What rests on other people: AMP's u(21) = 57 with its five extremal graphs, the Globus-Parshall forbidden list, and nauty's canonical labelling, which both enumerators share. What rests on us: the reach table, the sixth gadget, the fourteen-machine run, and the checker.