Erdős problem 224 · problems.science

If $A\subseteq \mathbb{R}^d$ is any set of $2^d+1$ points then some three points in $A$ determine an obtuse angle.

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

224.lean

Retained formal statement1 of 1

If $A\subseteq \mathbb{R}^d$ is any set of $2^d+1$ points then some three points in $A$ determine an obtuse angle.

The general case was proved by Danzer and Grünbaum [DaGr62].

FormalConjectures/ErdosProblems/224.leanErdos224.erdos_2242 linesExact file

1∀ {d : ℕ} (A : Finset (EuclideanSpace ℝ (Fin d))),2  A.card = 2 ^ d + 1 → ∃ x y z, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ Erdos224.ObtuseAt x y z

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.

Sources

Search problems.science