Reading source record 2062b0e6c9770c81e397bfe41148e90b92ca0567. View default cited record →
The pinned submission proves a positive exponent gain for arbitrarily large finite Euclidean planar point sets.
Public formal source; execution and statement correspondence are separate checks.
1 cited passage ↓1 problem ↓Record 2062b0e6c9770c81e397bfe41148e90b92ca0567 ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
The pinned submission proves a positive exponent gain for arbitrarily large finite Euclidean planar point sets.
Replaces an earlier passage. View versioned records →
Passage ID: erdos-unit-distances:entry:lean:v2
Source item: lean
Source record: erdos-unit-distances:source:lean:v2
Replaces passage: erdos-unit-distances:entry:lean:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v6
Source assessment
Proved
Formal exponent-gain endpoint reported complete
Exact Euclidean norm and unordered counting; external proof execution.
Source date Jun 27, 2026 · Observed Oct 13, 2026
Formal declaration
Lean: positive exponent in the Euclidean plane
History
A pinned Euclidean Lean submission
Question
Erdős unit-distance problem
Further reading
Inspect the formal statement, assumptions and reported checks.
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Exact proof source inspected. This digest identifies this file only, not a project build, theorem correspondence or independent reproduction.
Resource revision: 2062b0e6c9770c81e397bfe41148e90b92ca0567
SHA-256 for this linked file. A matching checksum identifies the same bytes; it does not assess the mathematics.
51e80f264d618539a8ce31fae79ad95814678d081cc7fc952d74e7904b243ab8Complete formal proof reported externally
The finite-set definition counts ordered off-diagonal distance-one pairs and divides by two. The formal theorem uses EuclideanSpace ℝ (Fin 2), not the product sup norm, and proves arbitrarily large sizes. It does not specify δ = 0.014.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Submission.erdos_unit_distance_conjecture_falseCommit 2062b0e6c9770c81e397bfe41148e90b92ca0567
Recorded authorship
plby/Erdos90 project
No specific AI contribution is attributed by this source record.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
Unit-distance counterexample in Lean
Unit-distance counterexample in Lean
OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Source terms ↗