Skip to content

Erdős problem 353

Let A⊆R2A\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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/353.lean

Formal Conjectures

FormalConjectures/ErdosProblems/353.leanErdos353.erdos_3539 linesExact file
True ↔  ∀ (A : Set (EuclideanSpace ℝ (Fin 2))),    MeasurableSet A →      MeasureTheory.volume A = ⊤ →        ∃ a ∈ A,          ∃ b ∈ A,            ∃ c ∈ A,              ∃ d ∈ A,                EuclideanGeometry.IsIsoscelesTrapezoid a b c d ∧ MeasureTheory.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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:353

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page