Erdős Problem 655: General Position
Let be such that no circle whose centre is one of the contains three other points. Are there at least distinct distances determined between the , for some constant and all sufficientl...
Mathematical statement
Let be such that no circle whose centre is one of the contains three other points. Are there at least distinct distances determined between the , for some constant and all 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
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