Erdős Problem a Daythe open tracker

Erdős Problem #353

PROVED LEANdatabase updated 2026-06-21

The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

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.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 4 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/353.
Prizenone
Topicsgeometry
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/353
NOBODY HAS SENT US AN ATTEMPT YET

If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.