353.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 353

References:

erdosproblems.com/353
[Er83d] Erdős, Paul, Some combinatorial, geometric and set theoretic problems in measure theory. Measure Theory, Oberwolfach 1983 (1984), 321-327.
[Ko23] Kovač, V., Coloring and density theorems for configurations of a given volume. arXiv:2309.09973 (2023).
[KoPr24] Kovač, V. and B. Predojević, Polygons of unit area with vertices in sets of infinite planar measure. arXiv:2412.11725 (2024).
[Ko25] J. Koizumi, Isosceles trapezoids of unit area with vertices in sets of infinite planar measure. arXiv:2501.01914 (2025).

Imports (1)

FormalConjecturesUtil

theorem Erdos353.erdos_353 Let $A\subseteq \mathbb{R}^2$ be a measurable set with infinite measure sorry line 57 source
Source documentation
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?
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$.
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.

depends on sorry what this means
Statement uses: Iff, True, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, MeasurableSet, ENNReal, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Top.top, Exists, And, Membership.mem, EuclideanGeometry.IsIsoscelesTrapezoid, ClosureOperator, convexHull and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
140 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_353 : answer(True) ↔
    ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
      ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, ∃ d ∈ A,
        IsIsoscelesTrapezoid a b c d ∧
        volume (convexHull ℝ {a, b, c, d}) = 1 := by
…
```
Mentions: c
theorem Erdos353.erdos_353.variants.isosceles_triangle Every measurable $A\subseteq \mathbb{R}^2$ with infinite measure contains the vertices of an isosceles triangle of area $1$ sorry line 76 source
Source documentation
Every measurable $A\subseteq \mathbb{R}^2$ with infinite measure contains the vertices of an isosceles 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.

depends on sorry what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, MeasurableSet, ENNReal, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Top.top, Exists, And, Membership.mem, IsIsosceles, ClosureOperator, convexHull, Insert.insert, Singleton.singleton
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
146 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_353.variants.isosceles_triangle :
    ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
      ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A,
        IsIsosceles a b c ∧
        volume (convexHull ℝ {a, b, c}) = 1 := by
…
```
Mentions: c, IsIsosceles
theorem Erdos353.erdos_353.variants.right_angled_triangle Every measurable $A\subseteq \mathbb{R}^2$ with infinite measure contains the vertices of a right-angled triangle of area $1$ sorry line 95 source
Source documentation
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.

depends on sorry what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, MeasurableSet, ENNReal, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Top.top, Exists, And, Membership.mem, EuclideanGeometry.IsRightAngled, ClosureOperator, convexHull, Insert.insert, Singleton.singleton
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
158 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_353.variants.right_angled_triangle :
    ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
      ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A,
        IsRightAngled a b c ∧
        volume (convexHull ℝ {a, b, c}) = 1 := by
…
```
Mentions: c
theorem Erdos353.erdos_353.variants.cyclic_quadrilateral Every measurable $A\subseteq \mathbb{R}^2$ with infinite measure contains the vertices of a cyclic quadrilateral of area $1$ sorry line 112 source
Source documentation
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.

depends on sorry what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, MeasurableSet, ENNReal, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Top.top, Exists, And, LE.le, Set.ncard, EuclideanGeometry.Cospherical, ClosureOperator, convexHull
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
140 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_353.variants.cyclic_quadrilateral :
    ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
      ∃ Q : Set ℝ², Q ⊆ A ∧ Q.ncard = 4 ∧ Cospherical Q ∧
        volume (convexHull ℝ Q) = 1 := by
…
```
theorem Erdos353.erdos_353.variants.congruent_sides Documented declaration: congruent_sides sorry line 124 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Exists, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, MeasurableSet, ENNReal, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Top.top, HAdd.hAdd, EuclideanGeometry.IsCcwConvexPolygon, Membership.mem, Dist.dist, LT.lt, ClosureOperator and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
180 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_353.variants.congruent_sides :
    ∃ A : Set ℝ², MeasurableSet A ∧ volume A = ⊤ ∧
      ∀ (n : ℕ) (v : Fin (n + 3) → ℝ²),
        IsCcwConvexPolygon v → (∀ i, v i ∈ A) →
        (∀ i, dist (v i) (v (i + 1)) = dist (v 0) (v 1)) →
        volume (convexHull ℝ (Set.range v)) < 1 := by
…
```