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 statement3 of 5

Every measurable $A\subseteq \mathbb{R}^2$ with infinite measure contains the vertices of a cyclic quadrilateral of area $1$ .

Kovač and Predojević [KoPr24] have proved that this is true for cyclic quadrilaterals - that is, every set with infinite measure contains four distinct points on a circle such that the quadrilateral determined by these four points has area $1$ . The quadrilateral determined by four distinct concyclic points is their convex hull.

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

1∀ (A : Set (EuclideanSpace ℝ (Fin 2))),2  MeasurableSet A →3    MeasureTheory.volume A = ⊤ →4      ∃ Q ⊆ A, Q.ncard = 4 ∧ EuclideanGeometry.Cospherical Q ∧ MeasureTheory.volume ((convexHull ℝ) Q) = 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