Erdoes #107 - working report - Erdős Problem a Day

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. \]

3. Suk proved $f(n)\leq2^{(1+o(1))n}$.

4. Holmsen--Mojarrad--Pach--Tardos proved the currently stated best

asymptotic bound

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

5. 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](https://www.cambridge.org/core/services/aop-cambridge-core/content/view/0EC7876789232266D60439A4C00D86D9/S144618110000300Xa.pdf/computer_solution_to_the_17point_erdosszekeres_problem.pdf),

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](https://cris.bgu.ac.il/en/publications/a-sat-attack-on-the-erd%C5%91sszekeres-conjecture-2/),

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](https://arxiv.org/abs/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](https://drops.dagstuhl.de/entities/document/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](https://arxiv.org/abs/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)

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)

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

\[ P(2,u)=P(a,2)=\{\text{one point}\}, \qquad P(a,u)=P(a,u-1)\ \mathbin{\text{deep-below}}\ P(a-1,u). \]

Pascal's identity gives

\[ |P(a,u)|=\binom{a+u-4}{a-2}. \]

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

\[ Q_i=P(k-i+2,i), \]

and place the blocks successively deep below one another. Then

\[ \left|\bigcup_{i=2}^kQ_i\right| =\sum_{i=2}^k\binom{k-2}{i-2}=2^{k-2}. \]

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

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

endpoints and $p,q$ have x-ordered orientation pattern

$-,+,+,+$, so that four-set is nonconvex.

Consequently every convex subset has at most

\[ (i-1)+(j-i-1)+(k-j+1)=k-1 \]

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 \[ D^\epsilon_a(i,j)=1+ \max_{\substack{a\leq hwith 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

\[ \max |C|=\max_{aFor 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):

|---:|---:|---:|---:|

| 4 | 4 | 7 | 3 |

| 5 | 8 | 47 | 4 |

| 6 | 16 | 1000 | 5 |

| 7 | 32 | 280909 | 6 |

| 8 | 64 | 281032556 | 7 |

| 9 | 128 | 924554810015 | 8 |

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

\[ N(n,4,n)=\sum_{r=0}^{2}\binom{n-2}{r}. \]

Therefore

\[ N(7,4,7)=1+5+10=16. \]

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 \[ x_{abc},x_{abd},x_{acd},x_{bcd} \]

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

\[ x_{abc}=x_{abd}\quad\text{and}\quad x_{acd}=x_{bcd}. \]

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:

|---:|---:|---:|---:|---:|

| 16 | 2380 | 53820 | SAT, 0.188 s | SAT, 0.092 s |

| 17 | 3060 | 79356 | UNSAT, 44.334 s | UNSAT, 30.514 s |

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

\[ \binom{33}{3}+\binom{33}{4}=46,376 \]

variables and

\[ 16\binom{33}{4}+\binom{33}{7}+1 =654,720+4,272,048+1 =4,926,769 \]

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.

3. 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.

This is the AI working report, labelled by outcome — not an independently verified claim unless marked PROVED. ← ledger