Skip to content

Erdős problem 353

Let AR2A\subseteq \mathbb{R}^2 be a measurable set with infinite measure. Must AA contain the vertices of an isosceles trapezoid of area 11? 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 statement1 of 5

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

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 11.

This statement formalizes the leading question, for isosceles trapezoids; the remaining configurations are given as variants below. The area of a polygon is taken to be the Lebesgue measure of the convex hull of its vertices.

FormalConjectures/ErdosProblems/353.leanErdos353.erdos_3539 linesExact file
True  ∀ (A : Set (EuclideanSpace ℝ (Fin 2))),    MeasurableSet A      MeasureTheory.volume A = ⊤ →aA,bA,cA,dA,                EuclideanGeometry.IsIsoscelesTrapezoid a b c dMeasureTheory.volume ((convexHull ℝ) {a, b, c, d}) = 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.

Search problems.science

Find a Problem, Result, source, or page