All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsCombinatorics

Erdős Problem 655: General Position

Let x1,,xnR2x_1,\ldots,x_n\in \mathbb{R}^2 be such that no circle whose centre is one of the xix_i contains three other points. Are there at least(1+c)n2(1+c)\frac{n}{2} distinct distances determined between the xix_i, for some constant c>0c>0 and all nn sufficientl...

Mathematical statement

Let x1,,xnR2x_1,\ldots,x_n\in \mathbb{R}^2 be such that no circle whose centre is one of the xix_i contains three other points. Are there at least(1+c)n2(1+c)\frac{n}{2} distinct distances determined between the xix_i, for some constant c>0c>0 and all nn sufficiently large?

In the spirit of related conjectures of Erdős and others, presumably some kind of assumption that the points are in general position (e.g. no three on a line and no four on a circle) was intended.

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_655.variants.general_position

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_655.variants.general_position :    answer(sorry)   c > (0 : ), ᶠ n in atTop,  (X : Finset ²), #X = n  IsValid X       InGeneralPosition X  (1 + c) * n / 2  distinctDistances X := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References