Reading source record 2062b0e6c9770c81e397bfe41148e90b92ca0567. This record is retained from earlier public citations. 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.
Passage ID: erdos-unit-distances:entry:lean:v1
Source item: lean
Source record: erdos-unit-distances:source:lean:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v2
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
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Exact source inspected; OpenMath has not executed this formal proof project.
Resource revision: 2062b0e6c9770c81e397bfe41148e90b92ca0567
SHA-256 for this linked file. A matching checksum identifies the same bytes; it does not assess the mathematics.
db155ffc72c15808cd47302f38fe8d77b94b48287fcdf50c5e09fb695201290dComplete formal proof reported externally
The finite-set definition counts ordered off-diagonal distance-one pairs and divides by two. The endpoint 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 ↗