Erdős Problem #959

Erdős Problem

www.erdosproblems.com/959

The problem

Let $A\subset \mathbb{R}^2$ be a set of size $n$ and let $\{d_1,\ldots,d_k\}$ be the set of distinct distances determined by $A$ . Let $f(d)$ be the number of times the distance $d$ is determined, and suppose the $d_i$ are ordered such that $f(d_1)\geq f(d_2)\geq \cdots \geq f(d_k).$ Estimate $\max (f(d_1)-f(d_2)),$ where the maximum is taken over all $A$ of size $n$ .

(Erdős Problem #959 — geometry, distances — https://www.erdosproblems.com/959)

Result

M(n) ≥ n^(1 + 1/(50000·log log n)) for all large n — superlinear lower bound on the top-two distance-multiplicity gap (previous best Ω(n log n))

Report

Erdős Problem #959 — superlinear lower bound (accepted 2026-07-14)

Proved a fully formal explicit superlinear lower estimate for the faithful maximum-gap reformulation of Erdos Problem 959: with c=1/50000, for every sufficiently large n, (n : R)^(1 + c/log(log n)) <= M(n)=extremalGap(n). This resolves the explicit modern question whether M(n) >= n^(1+c/log log n); it does not claim a matching upper bound or exact asymptotic order. The proof constructs normalized replicated lattice disks indexed by subsets of primes 1 mod 4, suppresses every competitor by reduced-denominator support, places blocks and padding points generically, chooses replication adaptively for every n, and uses a formal PNT in arithmetic progressions for the asymptotics.

Exact local verifier command: check_answer/verify.sh Exact final output: PASS: faithful formal quantity and all current Lean proofs compile without placeholders The verifier also prints: 'chebyshev_asymptotic_pnt' depends on axioms: [propext, Classical.choice, Quot.sound], and rejects sorryAx. Final theorem: Erdos959.erdos959_superlinear_lower_bound in Research/FinalLowerBound.lean and verified_math/F-044_erdos959-superlinear-lower-bound/FinalLowerBound.lean.

Post-referee hardening

Two trivial native_decide certificates (both Nat.totient 4 = 2) were replaced with kernel decide after referee approval; the full pinned verifier re-ran PASS.

Referee

The agent claims a fully formal Lean proof that Erdős #959's extremal top-two distance-multiplicity gap satisfies M(n) ≥ n^(1+1/(50000·log log n)) for all sufficiently large n — a superlinear lower bound resolving the modern lower-bound question (previous best was Ω(n log n)); it explicitly does not claim a matching upper bound or exact order. I audited the formal definitions line-by-line against problem.md (faithful: exact real squared distances, unordered pairs, correct gap semantics including ties, true maximum over all n-point sets), rebuilt the entire 8624-job Lean project from a cleared build cache and reproduced the verifier's PASS (exit 0), and ran my own #print axioms on the final theorem: clean except two native_decide certificates that reduce to Nat.totient 4 = 2, which I re-proved by kernel decide. The result is machine-verified, honestly scoped, and answers the explicit superlinear-gap question; note when reviewing that the exact asymptotic order of M(n) (versus the O(n^(4/3)) unit-distance ceiling) remains open and is not claimed.

Independent verification (separate hardware)

Fresh GCP box, correct snapshot layout (project + pinned PNT fork): full lake build PASS; #print axioms Erdos959.erdos959_superlinear_lower_bound → [propext, Classical.choice, Quot.sound]; word-boundary escape-hatch grep clean.

Public bundles

https://pub-23f3a588e04a481196ed22d7e3a6f48d.r2.dev/verify/erdos-959/erdos-959-solution.zip (+ verify-cursor / verify-claude-code / verify-codex)

Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly downloading Mathlib.

Download & Verify w/ Cursor Download & Verify w/ Claude Code Download & Verify w/ Codex

↓ Download full solution raw