Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 353

claims/: The 2 claim pages of Problem 353, one per claimant's result; the problem's standing derives from them.

Statement. 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?

Status. PROVED (LEAN): the site labels the problem proved with a Lean qualification, crediting Koizumi with the trapezoid question and the two triangle variants, recorded on the Koizumi claim page; the cyclic quadrilateral (yes) and the polygon with congruent sides (no) are on the Kovač–Predojević claim page. The statement asks five questions, listed as the problem's parts; four are answered yes and the convex polygon with congruent sides no. Because the parts differ in polarity, the standing derived from the two partial claims records an answer rather than the proof the label names. The Lean proof the label refers to is a third-party development, linked from both pages and under Formalization, which this corpus has not built.

Source. erdosproblems.com/353, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #353, https://www.erdosproblems.com/353.

References.

[Ko23] Kovač, V., Coloring and density theorems for configurations of a given volume. arXiv:2309.09973 (2023).
[Ko25] J. Koizumi, Isosceles trapezoids of unit area with vertices in sets of infinite planar measure. arXiv:2501.01914 (2025).
[KoPr24] Kovač, V. and B. Predojević, Polygons of unit area with vertices in sets of infinite planar measure. arXiv:2412.11725 (2024).

Formalization. Statement in formal-conjectures (read at that commit), where the question and its four variants are five theorems marked solved, each with a sorry in place of the proof, the congruent-sides one stated as the existence of a set that gives the negative answer, all pointing to one Lean 4 file in Jayyhk/erdos-lean that declares itself a formalization of Koizumi's theorems and of Kovač and Predojević's; this corpus has not built or audited either file, so the formalization is a link, not acceptance evidence.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (12)

problems/discrete_geometry/E0353/claims Discrete and Convex Geometry discrete_geometry/erdos_1978_set_theoretic Triangles in sets of infinite measure (p. 122): every prescribed area occurs, also for isosceles or right triangles discrete_geometry/koizumi_2025_isosceles_trapezoids_unit_area_vertices_sets Theorem 1 (p. 1): an unbounded planar set of positive measure contains an isosceles triangle and a right triangle of area 1 Theorem 2 (p. 2): a planar set of infinite measure contains an isosceles trapezoid of area 1 discrete_geometry/kovac_2023_coloring_density_theorems_configurations_given_volume Theorem 7: a set of infinite volume whose parallelotopes are all small discrete_geometry/kovac_2024_polygons_unit_area_vertices_sets_infinite Theorem 1 (p. 1): every measurable planar set of infinite measure contains the vertices of a cyclic quadrilateral of area 1 Theorem 2 (p. 2): a planar set of infinite measure in which every convex polygon with congruent sides has area less than 1

Graph