Is there some $c > 0$ such that every measurable $A \subseteq R^{2}$ of measure $\geq c$ contains the vertices of a triangle of area 1?

Worked, still open.

geometry · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

As of **January 2026**, this is **still open** in full generality (it’s an Erdős problem, listed as *Erdős Problem #352*). ([Erdős Problems][1])

candidate solution ↗

llm-hunter · claude opus 4.5, gpt pro 5.2 · unverified

2 LLM attack(s) recorded (claude opus 4.5, gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 51 · open (literature)

theorem erdos_352 :
    answer(sorry) ↔ ∃ c > (0: ℝ), ∀ A : Set ℝ², MeasurableSet A → ℙ A ≥ c.toEReal
       → (∃ t : Affine.Triangle ℝ ℝ²,
           (∀ p : Fin 3, t.points p ∈ A) ∧
           EuclideanGeometry.triangle_area (t.points 0) (t.points 1) (t.points 2) = 1)

formal-conjectures/352.lean ↗

status

open

evidence

formal

status

Search Vela