Solving Erdős Problem #662

Why this problem was unusually difficult

Erdős Problem #662 asks whether the triangular lattice is extremal for the number of short distances in a large one-separated planar set. The natural comparison function counts triangular-lattice neighbours up to a threshold, and Erdős also proposed a stronger version at the lattice’s distance shells.

The main obstacle was not initially the geometry. The surviving statement is corrupt. Its sample values disagree with the natural cumulative lattice count, its final “less than 1” clause is impossible as printed, and the total/local normalization is unclear. This created two incompatible historical narratives:

• a threshold or shell extremal conjecture, which might be false;
• Vesztergombi’s theorem on the multiplicities of the two smallest distances, which is true and was published in 1987.

The maintained problem page consequently remained open and explicitly said that Erdős’s intent was unknown. A proof about any self-selected repair could be mathematically correct yet fail to answer the historical problem.

There was a second trap. The triangular lattice is the densest planar lattice packing, so it is tempting to expect it to maximize every fixed-radius neighbour count. Density is an asymptotic invariant; finite-shell coordination is not. A slightly less dense oblique lattice can place more lattice points inside one particular ball.

Where the earlier routes stalled

Several natural attacks clarified the ambiguity but did not resolve it.

• Square-grid blocks immediately defeat continuous-threshold average-degree readings between the first triangular shells. This is elementary, however, and does not address a conjecture restricted to genuine triangular-lattice shell radii.
• A 38-point packing gives one point 37 neighbours below radius 3, beating the corrected triangular local count 36. That disproves a local interpretation, but not the global average-degree version suggested by the “sufficiently large” qualifier.
• Formalizing Vesztergombi’s bound proved a beautiful theorem, but primary literature showed that it was already known and concerned the first two distinct distance values—not an absolute threshold.
• Even exact counterexamples to closed shell readings were not enough while the 1997 source remained unauthenticated. The possible interpretations gave opposite answers.

The recurring mistake was to treat statement repair and mathematical proof as one task. They had to be separated: first identify the historical subject externally, then cover the remaining damaged formula conventions rather than silently choosing one.

Breakthrough 1: recovering the primary passage

The missing source was found in the National Diet Library of Japan:

• NDL PID 10996926;
• DOI 10.11501/10996926;
• Mathematica Japonica 46(3), November 1997;
• P. Erdős, “Some of my favourite unsolved problems,” pp. 527–537.

The scan images require authorized library or personal transmission, but the NDL explicitly permits anonymous full-text snippets. Twenty-eight exact-phrase responses from the target content were captured. Their OCR windows overlap to reconstruct 943 consecutive characters with no gap and no conflicting character.

The primary text itself contains, in order:

• the triangular lattice and the function f(t);
• an arbitrary separated point sequence;
• the comparison between its number of short distances and f(t);
• the possible triangular-lattice equality case;
• the particular sub-√3 question; and
• Erdős’s stronger conjecture over the distance shells of the triangular lattice.

This settled the historical fork. The 1997 problem really is about absolute thresholds and triangular shells. It is not Vesztergombi’s separate 1987 multiplicity theorem. The OCR is poor on displayed formulas, so it does not justify inventing one missing factor; instead, all natural local/global and printed/corrected conventions were treated separately.

Breakthrough 2: finite-shell coordination beats density

For the corrected closed global reading, consider the rational oblique lattice with basis

u = (1,0),   v = (136/305, 273/305).

It is one-separated because every integer offset satisfies

305m² + 305n² + 272mn
  = 136(m+n)² + 169m² + 169n² ≥ 305

when (m,n) ≠ (0,0).

At ordinary radius 6, exact enumeration gives:

triangular lattice: 126 nonzero offsets
oblique lattice:    128 nonzero offsets.

A finite patch needs boundary correction; an infinite-lattice count alone is not a counterexample to an eventual finite statement. For a 365 × 365 patch, exact incidence counting gives

n = 133,225
directed short pairs = 16,786,618
126n                 = 16,786,350
excess               = 268.

Equivalently, there are 8,393,309 unordered short pairs, 134 more than 63n. Far-separated translated copies preserve the excess and produce counterexamples above every requested cardinality. Thus “sufficiently large” cannot rescue the conjecture.

Breakthrough 3: the strict shell version also fails

The quoted stronger conjecture uses strict inequalities at shell thresholds. A second rational lattice handles that version:

u = (1,0),   v = (276/565, 493/565).

Its separation follows from

565m² + 565n² + 552mn
  = 276(m+n)² + 289m² + 289n² ≥ 565.

Squared radius 300 is a genuine triangular shell, since 300 = 10² + 10² + 10·10. Exact counts are

oblique offsets strictly below 300: 1078
triangular offsets through 300:     1074
triangular offsets strictly below:  1068.

For a 4535 × 4535 patch:

n = 20,566,225
directed strict pairs = 22,088,128,946
1074n                 = 22,088,125,650
excess                = 3,296
unordered excess      = 1,648.

Again, separated replicas remove every cutoff. Under the printed comparison f(3)=18, the exact 38-point block already has 710 directed and 355 unordered pairs strictly below 3, exceeding 18·38=684 and 9·38=342; its central degree 37 also defeats both the printed local bound 18 and corrected local bound 36.

The answer to the shell-extremality question is therefore no, under closed or strict thresholds and under the printed or corrected comparison conventions. The natural repaired particular statement below √3 is nevertheless true: angular separation gives fewer than 12 neighbours at every point and fewer than 6n unordered pairs.

Verification

Every geometric and counting claim was formalized in Lean 4 with Mathlib.

• One-separation is derived symbolically from the displayed positive quadratic decompositions.
• Offset windows are proved complete, not sampled.
• Small finite censuses use kernel decide, never floating point or native_decide.
• Huge patch counts are proved through dependent incidence types and injective endpoint maps; Lean does not enumerate billions of pairs.
• Replication theorems quantify over every requested cutoff.
• Independent Python scripts recompute all integer counts and boundary sums.
• The source gate hash-checks the NDL captures and semantically verifies all 28 OCR overlaps offline.

Running check_answer/verify.sh checks provenance hashes, reconstructs the primary OCR, runs both independent arithmetic audits, clean-builds 8570 Lean jobs, rejects sorry, admit, and native_decide, and prints an axiom audit. The only reported axioms are the standard Mathlib axioms propext, Classical.choice, and Quot.sound.

Prior work

Przemek Chojecki's April 2026 note, "Reconstructing a corrupted Erdos problem on small distances" (posted on the problem's erdosproblems thread), diagnosed the corrupted printed text first and worked out two repaired variants: a threshold-count repair with true breakpoint sqrt(2), and the historically intended shell-multiplicity reading via Vesztergombi's 1987 theorem. Full credit to him for the first public diagnosis and those repairs. Our submission treats different readings of the extremality question (closed and strict thresholds, both comparison conventions, at general radius), proved in Lean.