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

The answer is negative for convex polygons with congruent sides: Kovač and Predojević [KoPr24] prove that there exists a set of infinite measure such that every convex polygon with congruent sides and all vertices in the set has area $<1$ .

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

1∃ A,2  MeasurableSet A ∧3    MeasureTheory.volume A = ⊤ ∧4      ∀ (n : ℕ) (v : Fin (n + 3) → EuclideanSpace ℝ (Fin 2)),5        EuclideanGeometry.IsCcwConvexPolygon v →6          (∀ (i : Fin (n + 3)), v i ∈ A) →7            (∀ (i : Fin (n + 3)), dist (v i) (v (i + 1)) = dist (v 0) (v 1)) →8              MeasureTheory.volume ((convexHull ℝ) (Set.range v)) < 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