Discrete geometry: Erdős–Szekeres-type conjectures on unavoidable structures in point sets (k-holes and big- line-big-clique)

Title: Discrete geometry: Erdős–Szekeres-type conjectures on unavoidable structures in point sets (k-holes and big-line-big-clique)

### What is the conjecture

This issue collects several famous conjectures in discrete geometry, from various publications and in part covered by the standard textbook of Brass, Moser and Pach. They are Erdős–Szekeres-type questions about *unavoidable* structures in point sets: patterns that every sufficiently large point set must contain. They concern k-holes and related problems.

A k-hole of a finite planar point set in general position (no three collinear) is a set of k points in convex position whose convex hull contains no other point of the set. It is the empty variant of the classical Erdős–Szekeres k-gon problem (the Happy Ending problem, already in the repository as `ErdosProblems/107`), proposed by Erdős in the 1970s and studied by many researchers worldwide since then.

Let `h_k(n)` be the minimum number of k-holes over all n-point sets in general position. The asymptotic growth is `h_k(n) ~ c_k · n²`, and the following **three conjectures** about the leading constant `c_k` are open:

- **3-holes** (Bárány–Károlyi): `c_3 > 1`.
- **4-holes** (Brass–Moser–Pach): `c_4 > 1/2`.
- **5-holes**: `c_5 > 0`, i.e. `h_5(n) = Ω(n²)`.

The three conjectures are not independent. Pinchasi, Radoičić and Sharir proved the relations `c_4 ≥ c_3 − 1/2` and `c_5 ≥ c_3 − 1`, so a positive answer for 3-holes would settle all three. For `k = 3` and `k = 4` quadratic growth is known and only the leading constant is open; for `k = 5` even quadratic growth is open. The first super-linear lower bound, `Ω(n · log^{4/5} n)`, is due to Aichholzer, Balko, Hackl, Kynčl, Parada, Scheucher, Valtr and Vogtenhuber (2020), and the current record, very recently, is `Ω(n^{20/11})` (Astudillo-Marbán and Solé-Pi, 2026).

The number `h_6(n)` also lies between `Ω(n)` and `O(n²)` and its growth is open as well. This was never stated as an explicit problem, because the existence of 6-holes itself was open for decades, until Gerken and Nicolás independently proved it in 2006 (the empty hexagon theorem). For `k ≥ 7` there is nothing to state, since `h_k(n) = 0` by Horton's construction (1983) of arbitrarily large sets with no 7-hole.

The exact counts `h_3`, `h_4`, `h_5` were first studied by Dehnhardt (1987), who determined them by hand up to `n = 12`; further terms were determined with exhaustive search and SAT encodings. The values are recorded in OEIS ([A063541](https://oeis.org/A063541), [A063542](https://oeis.org/A063542), [A276096](https://oeis.org/A276096)).

**Two related conjectures** are included as well:

- **Big-line-big-clique** (Kára, Pór and Wood): for all `k` and `ℓ` there is an `n` such that every n-point planar set has `ℓ` collinear points or `k` mutually visible points (a clique in the visibility graph). The case `ℓ ≤ 3` is known.
- **Higher-dimensional holes** (Valtr): in the plane the largest guaranteed hole size is `H(2) = 6`. In 3-space, whether 8-holes always appear (`H(3) ≥ 8`) is open. The known bounds `7 ≤ H(3) ≤ 22` are due to Scheucher: every 14 points in general position contain a 7-hole, while arbitrarily large sets without a 23-hole exist.

References:
- I. Bárány and G. Károlyi, [*Problems and results around the Erdős–Szekeres convex polygon theorem*](https://doi.org/10.1007/3-540-47738-1_7), Japanese Conference on Discrete and Computational Geometry (2000), 91–105.
- P. Brass, W. Moser and J. Pach, [*Research Problems in Discrete Geometry*](https://doi.org/10.1007/0-387-29929-7), Springer (2005), Chapter 8.4.
- R. Pinchasi, R. Radoičić and M. Sharir, [*On empty convex polygons in a planar point set*](https://doi.org/10.1016/j.jcta.2005.03.007), Journal of Combinatorial Theory Series A 113(3) (2006), 385–419.
- O. Aichholzer, M. Balko, T. Hackl, J. Kynčl, I. Parada, M. Scheucher, P. Valtr and B. Vogtenhuber, [*A superlinear lower bound on the number of 5-holes*](https://doi.org/10.1016/j.jcta.2020.105236), Journal of Combinatorial Theory Series A 173 (2020), 105236.
- O. Astudillo-Marbán and O. Solé-Pi, [*There are many 5-holes*](https://arxiv.org/abs/2603.18484), arXiv:2603.18484 (2026).
- J. Kára, A. Pór and D. R. Wood, [*On the chromatic number of the visibility graph of a set of points in the plane*](https://doi.org/10.1007/s00454-005-1177-z), Discrete & Computational Geometry 34 (2005), 497–506.
- M. Scheucher, [*A SAT attack on Erdős–Szekeres numbers in ℝ^d and the empty hexagon theorem*](https://doi.org/10.57717/cgt.v2i1.12), Computing in Geometry and Topology 2(1) (2023).
- K. Dehnhardt, *Leere konvexe Vielecke in ebenen Punktmengen*, PhD thesis, TU Braunschweig, 1987 (in German). First study of the counts `h_3`, `h_4`, `h_5`.
- M. Scheucher, [*Two disjoint 5-holes in point sets*](https://arxiv.org/abs/1807.10848), arXiv:1807.10848 (2018). SAT encoding for hole-counting searches.
- OEIS: [A063541](https://oeis.org/A063541) (3-holes), [A063542](https://oeis.org/A063542) (4-holes), [A276096](https://oeis.org/A276096) (5-holes).
- [Big-line-big-clique conjecture (Wikipedia)](https://en.wikipedia.org/wiki/Big-line-big-clique_conjecture)

### Prerequisites needed

A dimension-generic hole layer: convex position, empty hulls, k-holes, and general position over `EuclideanSpace ℝ (Fin d)`. These build directly on Mathlib's `convexHull`, `Collinear` and `AffineIndependent`, and the PR adds them to `FormalConjecturesForMathlib` (so the plane and 3-space share one basis). No open Mathlib dependency.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-52 Convex and discrete geometry

### Choose either option
- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by reading the dimension-generic hole layer in FormalConjecturesForMathlib, especially convexHull, Collinear, and AffineIndependent over EuclideanSpace ℝ (Fin d). Determine which of the listed k-hole, big-line-big-clique, or higher-dimensional statements belongs in the shared basis; done means the selected conjecture is stated in Lean with the cited prerequisites.

Written by the indexing model from the issue text.