Erdős problem #107 — wave 8l

Date: 2026-07-28 UTC

Re-verifier: runs/erdos107_wave8l_reverify.py

0. Mandatory live-page gate

I accessed the live page through the Bright Data browser path, not datacenter curl. The page title was 107 | Erdős Problems, and the page said it was last edited on 11 April 2026.

Verbatim current statement

Let $f(n)$ be minimal such that any $f(n)$ points in $\mathbb{R}^2$, no three on a line, contain $n$ points which form the vertices of a convex $n$-gon. Prove that $f(n)=2^{n-2}+1$.

This is copied verbatim from the live page's “View the LaTeX source” view.

Status, claims, comments, and activity markers

• Displayed status: FALSIFIABLE - $500. This says falsifiable, not

falsified. The surrounding page explicitly calls the problem open.

• Claimed proofs: 0 claimed proofs for this problem.
• Currently working: None.
• Interested in collaborating: Sam_Petkov.
• Likes: JineonBaek, old-bielefelder, jnie, Dogmachine, Sam_Petkov.
• “Looks difficult”: JineonBaek; “looks tractable”: None.
• Formalisation-interest markers: both None.
• The header lists the original-source keys

`[Er61,p.245] [Er75f,p.106] [Er81] [Er82e] [Er83c] [Er95,p.184] [Er97c] [Er97e] [Va99,4.66]`.

• The discussion view contains a deleted parent post and two visible

nondeleted contributions. BorisAlexeev's reply says that the deleted topic appears to be problem #216, involving the empty-polygon numbers \(M_6=30\) and nonexistence for \(n\geq7\); that is not a result about the present \(f(n)\). Alfaiz notes that the stronger Szekeres--Peters ordered hypergraph conjecture was disproved by Balko--Valtr. That latter assertion is verified below from the 2017 paper.

Thus none of the requested stop conditions applied.

Known results stated on the live page

The page records:

1. Klein observed \(f(4)=5\), and Turán--Makai showed \(f(5)=9\).
2. Erdős--Szekeres proved

\[ 2^{n-2}+1\leq f(n)\leq \binom{2n-4}{n-2}+1. \]

1. Suk proved \(f(n)\leq2^{(1+o(1))n}\).
2. Holmsen--Mojarrad--Pach--Tardos proved the currently stated best

asymptotic bound \[ f(n)\leq2^{\,n+O(\sqrt{n\log n})}. \]

1. The page says Erdős offered $500 for a proof and $100 for a disproof, and

that Graham offered $1000 for a proof.

There is a bibliographic anomaly worth recording: in /latex/107, the key [Gr04] attached to the sentence about Graham is rendered as Ben Green's unrelated paper The Cameron--Erdős conjecture. I did not rely on that entry.

1. Primary-source literature audit

The following sources were opened and checked, rather than inferred from secondary summaries.

• Erdős--Szekeres lower construction. The 1960/61 paper is

On some extremum problems in elementary geometry, Ann. Univ. Sci. Budapest, 3--4, 53--62. Its bibliographic review explicitly says it constructs \(2^{n-2}\) points with no convex \(n\)-gon. This is also the source cited by the live page. Classification: (b) rigorous-modulo-named-theorem. A from-scratch exact-coordinate version is given in Section 2 below.

• The last exact unrestricted case. Szekeres and Peters,

Computer solution to the 17-point Erdős--Szekeres problem, DOI 10.1017/S144618110000300X, prove that every 17-point configuration has a convex hexagon, hence \(f(6)=17\). They in fact search a larger class of abstract signature functions satisfying the four-point conditions. Classification: (b).

• The stronger conjecture really was refuted. Balko and Valtr,

A SAT attack on the Erdős--Szekeres conjecture, DOI 10.1016/j.ejc.2017.06.010, explicitly refute the unrestricted ordered 3-uniform-hypergraph strengthening of Szekeres--Peters. They do not refute the geometric Erdős--Szekeres conjecture. Classification: (b) for the paper's stated result.

• Asymptotic bounds. Suk's paper exists as

arXiv:1604.08657 and states \(f(n)=2^{n+o(n)}\) at exponential scale. The Holmsen--Mojarrad--Pach--Tardos paper exists as arXiv:1710.11415 and proves the \(2^{n+O(\sqrt{n\log n})}\) bound, also for pseudo-configurations. Classification: (b).

• A sharp constrained regime. Baek,

On the Erdős--Tuza--Valtr Conjecture, arXiv:2206.04260, proves the case with a forbidden 4-cap (or, symmetrically, 4-cup). The published paper is European J. Combin. 124 (2025), 104085, and reports a Lean 4 formalisation. Classification: (b).

• Current structured progress. Baek and Balko,

The Erdős--Szekeres Conjecture Revisited, DOI 10.4230/LIPIcs.SoCG.2025.13, prove the conjectured threshold for split polygons and for decomposable point sets, and give new extremal \(2^{k-2}\)-point constructions. They still call \(k=7\) the first open unrestricted case. Classification: (b).

• Most directly relevant recent computation. Dumitru,

Notes on the 33-point Erdős--Szekeres problem, arXiv:2512.24061, reports UNSAT results only for selected convex-layer-anchored subfamilies, not for an exhaustive partition of all 33-point configurations. The paper reports a base encoding with 578,336 variables and 16,670,808 clauses, and explicitly suggests replacing its 14 four-type selectors by a coarse convex/nonconvex indicator. I verified that the preprint exists and says this; I did not independently validate its archived certificates. Classification: (d) computational-only for the reported runs.

The literature search therefore agrees with the live page: the unrestricted problem is open, \(f(7)=33\) is the first unknown equality, and neither the 2017 disproof nor the recent anchored SAT calculations settle it.

2. Explicit exact-coordinate lower construction

This section gives an elementary construction, not just a citation. It recovers the known lower bound, but it produces a compact real witness and a standalone checker.

2.1 Deep-below composition

For finite point sets \(A,B\), say \(A\) is deep below \(B\) when \(x(A)<x(B)\), \(y(A)<y(B)\), every point of \(B\) is above every line through two points of \(A\), and every point of \(A\) is below every line through two points of \(B\).

Given integer-coordinate \(A,B\), first translate \(B\) far enough right that \(x(A)<x(B)\). There are then finitely many strict rational lower bounds on a vertical translation \(Y\): one for each A-line/B-point and each B-line/A-point. Taking one plus the floor of their maximum gives an integer \(Y\) satisfying all inequalities. This is exactly what deep_below_union() computes with fractions.Fraction. No floating-point test is used.

If points are ordered by increasing \(x\), this composition has two elementary orientation rules:

• two points in \(A\) followed by one in \(B\) have positive orientation;
• one point in \(A\) followed by two in \(B\) have negative orientation.

Strictness preserves general position.

2.2 Cap/cup blocks

Define \(P(a,u)\) recursively by

Pascal's identity gives

Inductively, \(P(a,u)\) has no \(a\)-cap and no \(u\)-cup. For example, a cap meeting both blocks cannot contain two points of the left block and one of the right block, because that triple has positive orientation. It therefore has at most one left-block point, and its right-block part would contain a forbidden \((a-1)\)-cap. The cup argument is symmetric. This proof is (a) elementary-rigorous.

2.3 The \(2^{k-2}\)-point set

For \(i=2,\ldots,k\), let

and place the blocks successively deep below one another. Then

Here is a direct proof that this union has no convex \(k\)-subset. Any convex subset, ordered by \(x\), is the union of a cup and a cap with their leftmost and rightmost points in common.

Suppose those endpoints lie in \(Q_i,Q_j\).

• If \(i=j\), the no-\(i\)-cup and no-\((k-i+2)\)-cap properties bound the

union by \(k-2\) points.

• If \(i<j\), the left endpoint's block contributes at most \(i-1\) points,

all on the cup; the right endpoint's block contributes at most \(k-j+1\), all on the cap.

• An intermediate block contributes at most one point. Indeed, if it

contributed \(p<q\), the four points consisting of the two global endpoints and \(p,q\) have x-ordered orientation pattern \(-,+,+,+\), so that four-set is nonconvex.

Consequently every convex subset has at most

points. This is (a) elementary-rigorous and proves the lower bound \(f(k)\geq2^{k-2}+1\).

2.4 Explicit 32-point \(k=7\) witness

The deterministic “smallest safe integer translation” rule gives:

(0,0)       (1,5)       (2,9)       (3,12)
(4,14)      (5,15)      (6,193)     (7,196)
(8,198)     (9,199)     (10,221)    (11,223)
(12,224)    (13,229)    (14,230)    (15,232)
(16,3537)   (17,3539)   (18,3540)   (19,3545)
(20,3546)   (21,3548)   (22,3570)   (23,3571)
(24,3573)   (25,3576)   (26,49798)  (27,49799)
(28,49801)  (29,49804)  (30,49808)  (31,280909)

The checker recomputes every triple determinant, so general position is not assumed. It verifies the maximum convex-subset size by the following independent dynamic programme. For a fixed left endpoint \(a\), sign \(\epsilon\), and ending pair \(i<j\),

with the two-point chains \(D^\epsilon_a(a,j)=2\). If \(L^\pm(a,b)\) are the longest cup/cap chains with common endpoints \(a,b\), then

For actual points, consecutive positive (respectively negative) turns imply all triples on that chain are positive (respectively negative), by monotonicity of consecutive slopes. The two interiors are therefore automatically disjoint: a shared interior point would make the same triple with the common endpoints both positive and negative. Thus the DP identity is (a); the computed table is (d):

As a second algorithm, the checker enumerates all \(\binom{32}{7}=3,365,856\) seven-subsets. A geometric set is convex iff all its four-subsets are convex, so the scan tests the exact four-point orientation criterion and rejects every seven-subset. The coordinate tuple's SHA-256 is bb1b9f7d85ebc30f7551036717ceb6c016a397f4a68705216d9a3884a0e90d25.

3. A sharp concrete regime: no 4-cap and no 7-cup

Let \(N(n,a,b)\) be the maximum size of a general-position point set having no convex \(n\)-set, no \(a\)-cap, and no \(b\)-cup. Baek's verified theorem gives

Therefore

This exact geometric result is (b). The checker independently constructs the following 16-point lower witness:

(0,0) (1,2) (2,3) (3,8) (4,9) (5,11) (6,33) (7,34)
(8,36) (9,39) (10,200) (11,201) (12,203) (13,206)
(14,210) (15,1006)

It checks from determinants that there is no 4-cap, no 7-cup, and that the largest convex subset has size 6. Correctness of the determinant criteria is (a); the reported finite-search outcome is (d).

I also tested a stronger abstract statement. Label points by increasing \(x\), let \(x_{ijk}\) be the sign of every increasing triple, and impose on each \(a<b<c<d\) that

has at most one sign change. This is the rank-3 signotope four-point condition, necessary for every real configuration but admitting nonrealizable assignments. A four-set is marked convex exactly when

The generated CNF additionally says every 7-set has a nonconvex four-subset, every 4-set has a positive triple (no 4-cap), and every 7-set has a negative triple (no 7-cup). Results:

Both SAT models are rechecked by a semantic validator independent of the CNF clauses. The two UNSAT answers are agreement of unrelated solver engines, but no DRAT/LRAT certificate is included, so the abstract strengthening is deliberately classified only as (d) computational-only. It is not needed to justify Baek's already rigorous geometric theorem.

As local sanity checks, the script truth-table checks all \(2^5\) assignments to four orientation bits plus the convexity bit. It also enumerates every signotope on at most six ordered elements: 8, 62, and 908 for sizes 4, 5, and 6, checking 19,976 cup/cap subsets at size 6. Finally, both solvers reproduce the sharp signotope transitions \(4\to5\) for a convex quadrilateral and \(8\to9\) for a convex pentagon.

4. A smaller one-sided reduction of the open 33-point case

The same x-sorted signotope relaxation gives a substantially smaller SAT instance than the recent selector-based preprint.

For \(N\) labels:

• orientation variables: \(\binom N3\);
• one convexity variable per four-set: \(\binom N4\);
• eight forbidden sign-pattern clauses and eight convexity-reification

clauses per four-set;

• one clause of length \(\binom74=35\) per seven-set.

After fixing the harmless global orientation reversal, the \(N=33,k=7\) instance has exactly

variables and

clauses. These counts and all binomial arithmetic are recomputed by the standalone script.

Dumitru's preprint reports 578,336 variables, 16,670,808 clauses, and 280-literal seven-set clauses. Thus this version has 12.471 times fewer variables, 3.384 times fewer clauses, and eight times shorter seven-set clauses. It implements the preprint's suggested coarse convex/nonconvex-indicator direction, with the important change that labels are first sorted by \(x\). The two model spaces are not identical, so this is a size comparison between sound one-sided relaxations, not a claim that one CNF is a drop-in equivalent replacement.

Why the reduction is sound

Rotate any real counterexample so all \(x\)-coordinates differ and relabel in increasing \(x\)-order.

1. Every geometric quadruple obeys the at-most-one-sign-change rule.
2. The displayed equality test is exactly the convex/concave classification

of an x-ordered quadruple.

1. If a seven-set is not convex, it contains a nonconvex four-set: choose a

non-hull point and a hull triangle containing it.

Hence every real 33-point counterexample yields a satisfying assignment. Consequently UNSAT would prove \(f(7)=33\). SAT would not disprove it, because the satisfying signotope might be nonrealizable. The reduction and counts are (a) elementary-rigorous.

Capped computation and exact remaining obstruction

I generated the 4,926,769 clauses incrementally in 38.4 seconds. Immediately before solving, the process reported 889,476 KiB peak resident memory. Kissat then ran for about 142 seconds without returning SAT or UNSAT, at which point I interrupted it to respect the few-CPU-minute limit. This timing observation is (d) and is not evidence either way.

The coarse encoding is already hard on the known \(N=17,k=6\) theorem: CaDiCaL did not finish it in roughly 165 seconds and Kissat did not finish it in 120 seconds, although the 16-point SAT instance takes about 0.2 seconds. That explains why a short failed \(N=33\) run is unsurprising.

The exact missing object for this route is now unambiguous:

• either a satisfying 33-label signotope, followed by enough realizability

constraints to decide whether it corresponds to actual points;

• or a global UNSAT certificate for the 46,376-variable CNF, independently

checked by DRAT/LRAT;

• or an exhaustive, mathematically justified partition into anchored

subinstances, with a checked certificate for every member.

The 2025 preprint reports anchored single-thread runtimes from \(2.5\times10^3\) to \(2.28\times10^6\) seconds, i.e. about 0.7 to 633 core-hours per selected subinstance. It does not give an exhaustive cube count, so assigning a total full-proof cost would be speculation. A sensible next pilot would be 32 independent one-hour solver seeds/cubes: 32 core-hours, roughly $1.30--$3.20 at a realistic $0.04--$0.10 per core-hour, plus certificate storage and checking. A complete campaign could be much larger; the current data do not justify a sharper estimate.

5. Reproduction

From the repository root:

python runs/erdos107_wave8l_reverify.py

This reruns exact geometry, the \(3,365,856\)-subset scan, the dynamic programmes through \(k=9\), local truth tables, all small signotope checks, and both SAT engines. On this VM it completed successfully in about 1.5 minutes. The geometry-only part has no third-party dependency:

python runs/erdos107_wave8l_reverify.py --geometry-only

No claim in this report closes the unrestricted problem.

PARTIAL: Explicitly verified a 32-point integer \(n=7\) lower-bound witness, certified the sharp \((7,4,7)\) constrained regime in a stronger signotope relaxation with two SAT engines, and reduced the open 33-point case to a sound 46,376-variable/4,926,769-clause CNF; its global SAT/UNSAT status remains unresolved.