Erdős problem 958 · problems.science

Let $A\subset \mathbb{R}^2$ be a finite set of size $n$ , and let $\{d_1,\ldots,d_k\}$ be the set of distances determined by $A$ . Let $f(d)$ be the multiplicity of $d$ , that is, the number of unordered pairs from $A$ of distance $d$ apart.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/958.lean

Formal Conjectures

FormalConjectures/ErdosProblems/958.leanErdos958.erdos_9587 linesExact file

1False ↔2  ∀ (n : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))),3    A.card = n →4      (EuclideanGeometry.distanceSet A).card = n - 1 ∧5          Finset.image (EuclideanGeometry.distanceMultiplicity A) (EuclideanGeometry.distanceSet A) =6            Finset.Icc 1 (n - 1) →7        Erdos958.IsEquidistantOnLine A ∨ Erdos958.IsEquidistantOnCircle A

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:958
PLBY Lean proofsErdosProblems.Erdos958

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

AI building on literature
Erdős AI contributions wiki · 27 Dec, 2025
Machine
Aristotle
Open the source record
Formalization
Erdős AI contributions wiki · 19 Dec, 2025
Machine
Seed Prover 1.5
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science