Skip to content

Erdős problem 224

Start work

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

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/224.lean

Formal Conjectures

FormalConjectures/ErdosProblems/224.leanErdos224.erdos_2242 linesExact file
∀ {d : ℕ} (A : Finset (EuclideanSpace ℝ (Fin d))),  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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:224
  • PLBY Lean proofsErdosProblems.Erdos224

Reported activity

Reported by these sources. Not reviewed here.

  • AI building on literature

    Erdős AI contributions wiki · 14 Jan, 2026

    Machine
    Codex, GPT-5.2 Thinking
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry