Erdős problem 353 · problems.science

Let $A\subseteq \mathbb{R}^2$ be a measurable set with infinite measure. Must $A$ contain the vertices of an isosceles trapezoid of area $1$ ? What about an isosceles triangle, or a right-angled triangle, or a cyclic quadrilateral, or a convex polygon with congruent sides?

Sources

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

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

353.lean

Retained formal statement5 of 5

Every measurable $A\subseteq \mathbb{R}^2$ with infinite measure contains the vertices of a right-angled triangle of area $1$ .

Koizumi [Ko25] has resolved this question, proving that any set with infinite measure must contain the vertices of an isosceles trapezoid, an isosceles triangle, and a right-angled triangle, all of area $1$ .

Note the area condition forces a, b, c to be affinely independent, so no separate non-degeneracy hypothesis is needed.

FormalConjectures/ErdosProblems/353.leanErdos353.erdos_353.variants.right_angled_triangle5 linesExact file

1∀ (A : Set (EuclideanSpace ℝ (Fin 2))),2  MeasurableSet A →3    MeasureTheory.volume A = ⊤ →4      ∃ a ∈ A,5        ∃ b ∈ A, ∃ c ∈ A, EuclideanGeometry.IsRightAngled a b c ∧ MeasureTheory.volume ((convexHull ℝ) {a, b, c}) = 1

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