Michael Schroeder · Preprint · Version 1 · 19 September 2026 · ORCID 0009-0004-3249-0195
Erdős–Szekeres: Upper Bounds for Convex Heptagons and Octagons
Abstract
The Erdős–Szekeres number ES(n) is the least N such that every set of N points in the plane, with no three collinear, contains n points in convex position. We prove ES(7) ≤ 81 and ES(8) ≤ 319. Both bounds follow from a common geometric partition and exact finite certificates for the resulting cup–cap configurations. The heptagon proof combines a five-point transversal with exclusions that preserve shared geometric witnesses. The octagon proof counts missing Ferrers states using hereditary convexity and four-cap compression. We also establish the (7,5,6) case of the Erdős–Tuza–Valtr conjecture: the largest planar set in general position with distinct abscissae avoiding a convex heptagon, a five-cap, and a six-cup has 25 points. All three upper bounds are formalized in Lean, including the geometric reductions and the validity of the finite encodings. The accompanying archive provides sources, exact certificates, and independent checkers. Finite Lean checks use native evaluation with an explicitly documented trust boundary.
Explore the problem with draggable points ↓
Read the Paper
Proof Package
The complete archive includes the PDF and LaTeX manuscript, 208 Lean modules, exact certificates, independently implemented checkers, pinned dependencies, reproduction instructions and verification records.
Start with README.md in the archive. The upper-bound proofs include the geometric reductions, encoding semantics, complete finite coverage and certificate soundness. Finite checks use Lean’s native evaluation; the release documents 19 native-evaluation dependencies for the heptagon endpoint and eight for the octagon endpoint. This is not kernel-only evaluation of every finite computation. No external peer review is claimed.
Citation and verification
Schroeder, Michael. Erdős–Szekeres: Upper Bounds for Convex Heptagons and Octagons. Version 1, Zenodo, 2026. DOI: 10.5281/zenodo.22842891.
The final Lean declarations are ES7FinalVerified.es7_le_81 and ES8Final.es8_le_319. The archive supplies its own SHA-256 manifest and instructions for a fresh rebuild and axiom audit.
The PDF on this site is byte-identical to the published Zenodo file. Download the SHA-256 checksums for the PDF and full archive.
The problem
How many points in the plane force the vertices of a convex polygon? The Erdős–Szekeres problem asks this when no three points lie on a line. A polygon is convex if each of its vertices lies on the boundary of its convex hull. Other points of the set may lie inside it: the polygon need not be empty.
The paper gives the intervals 33 ≤ ES(7) ≤ 81 and 65 ≤ ES(8) ≤ 319. The conjectured exact values remain 33 and 65. The accompanying proofs establish the upper bounds; they do not settle those conjectures.
Explore the Erdős–Szekeres problem
Drag the points, then look for seven or eight that form a convex polygon. The remaining points can be anywhere—even inside it.
You can also select a point and use the arrow buttons, or Tab to a point and use your keyboard’s arrow keys. Hold Shift for a smaller step.
This illustration checks every seven- or eight-point subset of just 12 points. It explains the problem; the accompanying proofs establish the bounds 81 and 319. Those bounds concern every admissible arrangement, however the points are placed.
Licence
The manuscript, original explanatory text and original accompanying certificate data are licensed under CC BY 4.0. Original code, including the Lean formalization and verification scripts, is licensed under MIT. The attributed compatibility port of Jineon Baek’s ErdosTuzaValtr is licensed under Apache 2.0. Third-party dependencies retain their own licences; the archive includes the applicable notices.