feat: add Erdős unit-distance problem set#321
Merged
Conversation
Two planar unit-distance problems on a shared prelude:
* unit_distance_upper_bound — Spencer-Szemerédi-Trotter (1984):
ν(n) = O(n^{4/3}). Best known upper bound; exponent unchanged
since 1984 with only constant-factor improvements.
* erdos_unit_distance_conjecture_false — OpenAI (2026, Theorem 1.1
of Planar Point Sets with Many Unit Distances): refutes Erdős's
1946 conjecture ν(n) ≤ n^{1 + C / log log n} via an unramified
pro-3 tower of totally real number fields with prescribed split
primes, projecting CM-lattice norm-one elements to the plane.
The shared module LeanEval.Combinatorics.UnitDistance defines E2
(EuclideanSpace ℝ (Fin 2), so dist is Euclidean, not sup-norm) and
unitDist P = (P.offDiag.filter (dist · = 1)).card / 2; the two
@[eval_problem] theorems live in their own files so each
comparator workspace's deps contain only the definitions, not the
other theorem as a sorry-axiom.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
alreadydone
reviewed
May 26, 2026
Comment on lines
+61
to
+63
| ∃ δ : ℝ, 0 < δ ∧ | ||
| ∀ N : ℕ, ∃ (n : ℕ) (P : Finset E2), | ||
| N ≤ n ∧ P.card = n ∧ (n : ℝ) ^ (1 + δ) ≤ (unitDist P : ℝ) := by |
Contributor
There was a problem hiding this comment.
Why not
Suggested change
| ∃ δ : ℝ, 0 < δ ∧ | |
| ∀ N : ℕ, ∃ (n : ℕ) (P : Finset E2), | |
| N ≤ n ∧ P.card = n ∧ (n : ℝ) ^ (1 + δ) ≤ (unitDist P : ℝ) := by | |
| ∃ δ : ℝ, 0 < δ ∧ | |
| ∀ N : ℕ, ∃ P : Finset E2, | |
| N ≤ P.card ∧ (P.card : ℝ) ^ (1 + δ) ≤ (unitDist P : ℝ) := by |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds two planar unit-distance problems built on a shared prelude.
unit_distance_upper_bound— Spencer–Szemerédi–Trotter (1984): there is an absoluteC > 0such that every finiteP ⊆ ℝ²satisfiesunitDist P ≤ C · |P|^{4/3}. The exponent has stood since 1984 with only constant-factor improvements.erdos_unit_distance_conjecture_false— OpenAI (2026), Theorem 1.1 of Planar Point Sets with Many Unit Distances: there is an absoluteδ > 0and infinitely manynfor which somen-point planar set has at leastn^{1+δ}unit-distance pairs. This refutes Erdős's 1946 conjectureν(n) ≤ n^{1 + C / log log n}. Construction: an unramified pro-3tower of totally real number fields with prescribed completely-split rational primes (Hajir–Maire / Golod–Shafarevich), projecting CM-lattice norm-one elements through a Minkowski window.The shared module
LeanEval.Combinatorics.UnitDistancedefinesE2 := EuclideanSpace ℝ (Fin 2)(sodistis Euclidean, not the sup-norm carried byℝ × ℝ) andunitDist P = (P.offDiag.filter (dist · = 1)).card / 2. The two@[eval_problem]theorems live in their own files so each comparator workspace'sChallengeDeps.leancarries only the definitions, not the other theorem as a sorry-axiom.Local checks green:
check-problem-build,validate-manifest,generateandcheck-generated-buildsfor both problems.🤖 Prepared with Claude Code