Erdős problem 531: exact values through \(k=3\) and a \(k=4\) construction

Audit date: 2026-07-26 UTC.

Live status: OPEN; no claimed proof and no current worker.

Main finite result of this run:

The first equality is elementary. The next two are exact finite

computations; the \(F(3)\) upper bound has a generated LRAT refutation checked

by an independent, from-scratch Python LRAT checker. The \(F(4)\) bound is an

explicit 200-bit colouring checked directly against all \(2{,}535{,}064\)

eligible four-sets. These finite results do not estimate the asymptotic

growth of \(F(k)\), so problem 531 remains open.

Rigor key

• (a) elementary-rigorous: proved here directly from the definitions;
• (b) rigorous-modulo-named-theorem: quoted from the named and linked

source;

• (c) plausible/structural-unverified: interpretation or heuristic, not a

theorem;

• (d) computational-only: an exact finite result, with reproducible code,

but not an asymptotic theorem.

The exact \(F(2)\), exact \(F(3)\), and the \(F(4)\) lower bound below are

(d). I found no primary source recording these small values, but I do not

claim that they are new to the literature.

0. Mandatory live-page gate

I fetched the live problem page through

the configured Bright Data Chromium path before doing any mathematics. The

page displayed the following current statement (verbatim; only line wrapping

has been normalized):

> Let \(F(k)\) be the minimal \(N\) such that if we two-colour

> \(\{1,\ldots,N\}\) there is a set \(A\) of size \(k\) such that all subset

> sums \(\sum_{a\in S}a\) (for \(\emptyset\neq S\subseteq A\)) are

> monochromatic. Estimate \(F(k)\).

The live gate was clear:

• status: OPEN;
• 0 comments on this problem;
• 0 claimed proofs for this problem;
• Interested in collaborating: None;
• Currently working on this problem: None;
• Likes this problem: None;
• This problem looks difficult: None;
• This problem looks tractable: None;
• The results on this problem could be formalisable: None;
• I am working on formalising the results on this problem: None;
• Formalised statement? No;
• Related OEIS sequences: Possible.

The page lists these known results:

1. Sanders and Folkman established existence; it also follows from Rado's

theorem and is commonly called Folkman's theorem.

2. Erdős and Spencer proved

\[ F(k)\geq 2^{c k^2/\log k} \]

for an absolute \(c>0\).

3. Balogh, Eberhard, Narayanan, Treglown, and Wagner improved this to

\[ F(k)\geq 2^{\,2^{k-1}/k}. \]

There was therefore no proof claim or worker collision, so I proceeded.

(d: live-page observation)

Convention forced by the colouring domain

The live sentence leaves “\(A\subseteq[N]\)” and “all sums lie in \([N]\)”

implicit. Both cited quantitative papers make the convention explicit:

\(A\subseteq[N]\) and its finite-sums set must be contained in \([N]\).

Since all elements are positive, this is equivalent to

\(\sum_{a\in A}a\leq N\). Every calculation below uses precisely that

convention. (b)

1. Primary-source literature audit

I checked the actual papers or scans, rather than relying only on search

snippets.

1. Erdős (1973). In

[“Problems and Results on Combinatorial Number

Theory”](https://www.renyi.hu/~p_erdos/1973-21.pdf),

A Survey of Combinatorial Theory, pp. 117–138, PDF page 6 / printed

page 122, Erdős states the Sanders–Folkman finite-sums result and says

that, as far as he knew, there were no good upper or lower bounds for its

function \(g(n)\). This is the source denoted [Er73] on the live page.

(b)

2. Erdős–Spencer (1989). Their two-page paper

“Monochromatic Sumsets”,

J. Combin. Theory Ser. A 50 (1989), 162–163,

DOI 10.1016/0097-3165(89)90011-390011-3),

defines exactly the same \(F(k)\), including \(P(S)\subseteq[n]\), and

proves

\[ F(k)>2^{c k^2/\lg k}. \]

Its closing note attributes to A. D. Taylor an upper bound which is a

tower of threes of height \(4k-3\). (b)

3. Taylor (1981). A. D. Taylor,

[“Bounds for the Disjoint Unions

Theorem”](https://doi.org/10.1016/0097-3165(81)90031-5),

J. Combin. Theory Ser. A 30 (1981), 339–344, gives the quantitative

disjoint-unions/non-repeating-sums argument underlying that tower upper

bound. (b)

4. Balogh–Eberhard–Narayanan–Treglown–Wagner (2017).

[“An improved lower bound for Folkman's

theorem”](https://arxiv.org/abs/1703.02473),

Bull. London Math. Soc. 49 (2017), 745–747,

DOI 10.1112/blms.12058, is genuinely

arXiv:1703.02473 and proves, in the nontrivial range \(k\geq2\),

\[ F(k)\geq 2^{\,2^{k-1}/k}. \]

Its construction colours odd integers randomly and imposes

\(\chi(2x)\neq\chi(x)\). A repeated subset sum then puts both \(y\) and

\(2y\) in the finite-sums set and prevents monochromaticity; if all

\(2^k-1\) sums are distinct, the set meets at least \(2^{k-1}\) independent

odd-part chains. (b)

5. Later state check. Balogh–Lavrov–Shakan–Wagner,

[“Monochromatic Hilbert cubes and arithmetic

progressions”](https://www.combinatorics.org/ojs/index.php/eljc/article/download/v26i2p22/pdf/),

Electronic J. Combin. 26 (2019), P2.22, explicitly records the

BENTW lower bound and Taylor tower bound as the state of the art for

\(F(k,2)\). The 2020 survey of Raigorodskii–Cherkashin,

[“Extremal problems in hypergraph

colourings”](https://doi.org/10.1070/RM9905), §9.3, repeats the same

quantitative result. (b)

Exact-title, exact-formula, forward-citation, and “small Folkman number”

searches found no later primary paper improving these quantitative bounds

and no source giving \(F(3)\) or \(F(4)\). This is an honest search miss,

not evidence that no such item exists.

Thus the literature gap I could verify is still

for \(k\geq2\). (b)

2. Exact finite reduction to hypergraph 2-colourability

For a finite set \(A\) of positive integers, write

Define the hypergraph

Then \(F(k)\) is exactly the first \(N\) for which \(H(N,k)\) has no proper

2-colouring. This is merely the definition rewritten as Property B for a

hypergraph. (a)

Introduce a Boolean variable \(x_i\) for the colour of \(i\). Each edge

\(E\) contributes the two clauses

They exclude the all-zero and all-one colourings of \(E\), respectively.

Global colour exchange is a symmetry, so adding the unit clause

\(\neg x_1\) loses no solution. Hence the \(H(N,k)\) colouring problem is

equivalent to the CNF consisting of (3) and \(\neg x_1\). (a)

The \(k=3\) edges

Let \(A=\{a \[ a,\ b,\ c,\ a+b,\ a+c,\ b+c,\ a+b+c. \tag{4} \]

All seven are distinct except possibly \(c=a+b\); the strict inequalities

between the remaining terms rule out every other collision. Thus every

edge of \(H(N,3)\) has size six or seven. (a)

Direct generation from (2) gives

The verifier recomputes both rows independently. (d)

In general, different generator sets can have the same finite-sums set

(collisions can make two such sets into the same interval). Repeating a

constraint is harmless. For \(k=3\) and \(N=53,54\), the verifier also

checks that the edges counted in (5) are pairwise distinct. The larger

\(k=4\) counts below deliberately count eligible generator sets \(A\), not

deduplicated hyperedges.

3. Exact first values

3.1 \(F(1)=1\)

The only colouring of a nonempty one-point interval contains a

one-generator finite-sums set, so \(F(1)=1\). (a)

3.2 \(F(2)=9\)

Read each bit below as the colour of \(1,2,\ldots\). The colouring

of \([8]\) contains no monochromatic

\(\operatorname{FS}(\{a,b\})=\{a,b,a+b\}\) with \(a

For \(N=9\), fixing the colour of 1 leaves only \(2^8=256\) colourings.

Exhausting them against all 16 eligible pairs leaves none. Therefore

(d)

This is the two-colour weak Schur threshold: \(a\) and \(b\) must be

distinct because \(A\) is a set.

3.3 A lower certificate for \(F(3)\)

A SAT search produced the following 53-bit colouring; its validity is then

checked without trusting the search. It is proper for \(H(53,3)\):

00101110000000000110110111111111101101111000000001110

Equivalently, its colour-1 class is

The checker regenerates all 3572 triples \(a

\(a+b+c\leq53\), forms the set of nonempty subset sums from scratch, and

checks that each edge sees both bits. Hence

(d)

3.4 A proof certificate for the upper bound \(F(3)\leq54\)

For \(H(54,3)\), (3) produces

The one extra clause is \(\neg x_1\). CaDiCaL 2.1.2, with preprocessing

disabled, generated a plain-text LRAT refutation. On the final run it had:

• 265,304 clause additions;
• 263,102 individual clause deletions;
• 34,905,742 bytes;
• SHA256

0b653ddc976b7e3505295c8128108353e89f68cc7cc851e27fc9d1f54fdf795c.

The supplied Python does not accept CaDiCaL's UNSAT answer on trust. It

parses the LRAT proof independently. For every learned clause \(C\), it:

1. falsifies all literals of \(C\);

2. reads the positive LRAT hints in order;

3. requires each hinted clause to be unit under the current partial

assignment;

4. propagates that unit;

5. requires the last hinted clause to be false; and

6. finally requires the proof to derive the empty clause.

It also honours every clause deletion, rejects absent clause identifiers,

rejects variables outside \([54]\), and rejects negative/RAT hints. The

--plain proof contained only RUP additions, so this small checker covers

the entire certificate. CaDiCaL's own proof checking was enabled as an

additional check, but the reported result rests on the independent LRAT

pass. The logical fact used here is just that adding a RUP clause preserves

satisfiability; deriving the empty clause proves unsatisfiability. (d)

Combining the explicit colouring (8) and the checked refutation (9) gives

4. A concrete four-generator construction

A bounded CaDiCaL search produced this witness. Concatenate the following

four 50-bit lines. The resulting bit string colours \(1,\ldots,200\):

01110111101101100001110011000000100100000100011100
10011010001011110101000110010100000101111101101010
10011110001111110100100110111010101011111110101001
10100010100100101111110000100011100011001010000011

The checker streams over every \(a

\(a+b+c+d\leq200\), without retaining the whole hypergraph, and constructs

all distinct nonempty subset sums. It verifies all \(2{,}535{,}064\)

eligible four-sets. Their edge-size histogram is

No row is monochromatic, so

This is an explicit construction with a from-scratch checker, but only a

finite lower bound. (d)

5. Reproduction

The standalone verifier is

runs/erdos531_wave5x_verify.py. It uses only

the Python standard library for constraint generation, witness checking,

DIMACS generation, and LRAT checking. To generate the LRAT proof it calls

the CaDiCaL already installed in this VM; an alternative path can be passed

with --cadical.

Run:

/usr/bin/python3 runs/erdos531_wave5x_verify.py

The salient output from a complete run was (the machine-dependent timing

line is omitted):

PASS explicit k=2 lower witness on [8]: 00101110
PASS exhaustive k=2 upper check on [9]: 256 colourings
PASS explicit k=3 lower witness on [53]: 00101110000000000110110111111111101101111000000001110
PASS generated k=3 distinct-edge counts: H(53,3)=3572 {6:156,7:3416}; H(54,3)=3789 {6:169,7:3620}
PASS explicit k=4 lower witness on [200]: 01110111101101100001110011000000100100000100011100100110100010111101010001100101000001011111011010101001111000111111010010011011101010101111111010100110100010100100101111110000100011100011001010000011
PASS streamed k=4 constraints on [200]: 2535064 eligible A, sizes {10:20,11:1569,12:2952,13:148837,14:61964,15:2319722}
PASS independent DP eligible-set counts: N=250 -> 6304811, N=500 -> 104646514
PASS CaDiCaL UNSAT generation: /home/exedev/.elan/toolchains/leanprover--lean4---v4.32.1/bin/cadical (2.1.2)
PASS independent LRAT check: 265304 additions, 263102 clause deletions, 34905742 bytes
PASS LRAT SHA256: 0b653ddc976b7e3505295c8128108353e89f68cc7cc851e27fc9d1f54fdf795c
VERIFIED exact table: F(1)=1, F(2)=9, F(3)=54; explicit construction proves F(4)>=201

The 200-bit witness pass took about 11 seconds. LRAT generation and

independent validation took about 21 seconds on this VM. The LRAT file is

generated in a temporary directory, checked, hashed, and removed; no large

opaque certificate needs to be trusted or committed.

For a quick construction-only check, omitting the UNSAT certificate, run:

/usr/bin/python3 runs/erdos531_wave5x_verify.py --elementary-only

6. What remains and why the standard approaches stall

6.1 The first-moment lower-bound ceiling

In a uniform independent two-colouring, a fixed edge \(E\) is monochromatic

with probability

A dissociated \(k\)-set has the maximum

\(|\operatorname{FS}(A)|=2^k-1\), so even in the most favourable case its

probability is \(2^{2-2^k}\). Meanwhile,

The leading term follows by taking the volume of the positive \(k\)-simplex

and dividing by \(k!\) for order; coincidences and the lattice boundary

contribute only \(O_k(N^{k-1})\). (a)

Consequently, even pretending that every set is dissociated, a direct union

bound only reaches

Thus the naive random-colouring/first-moment framework is intrinsically

limited to a doubly exponential lower bound. The BENTW exponent

\(2^{k-1}/k\) is already within a factor two of this idealized ceiling in

\(\log_2N\). Its essential advance is handling the non-dissociated sets,

for which uniform random colouring is much worse. **(a) for (13)–(15);

(b) for the BENTW theorem**

A lower bound of qualitatively greater than doubly exponential size would

therefore require a genuinely different ingredient: a highly correlated

colouring or structural mechanism that simultaneously rules out enormous

families of dissociated \(A\), not merely a sharper count of small sumsets.

That is the exact missing lower-bound mechanism identified by this audit.

(c)

6.2 The upper-bound gap

Taylor's quantitative finite-unions argument iterates Ramsey steps and pays

one exponentiation at each stage, producing height \(4k-3\). Closing the

gap in (1) from above needs a substantially stronger quantitative

finite-unions/non-repeating-sums lemma which avoids that stage-by-stage

tower growth. Neither the hypergraph encoding nor the exact \(k=3\)

certificate supplies such a uniform lemma. **(b) for Taylor's bound;

(c) for the diagnosis**

6.3 Why brute force will not address the asymptotic question

The number of eligible \(k=4\) generator sets already grows as

\(N^4/576\). An independent dynamic program gives

The direct, non-deduplicating encoding used by the verifier would give the

latter instance over 209 million clauses and as many as 3.14 billion

literal occurrences: 12.6 GB even for raw 32-bit literals, before clause

indices, watch lists, learned clauses, and proof logging. Deduplicating

coincident finite-sums edges could only reduce this, but almost all

fixed-\(k\) generator sets are dissociated, so it does not change the

\(N^4\) leading order: a subset-sum collision is one of only \(3^k-1\)

nonzero signed linear relations, and each relation has

\(O_k(N^{k-1})\) solutions, while a positive dissociated set can be

recovered greedily from its subset-sum set (take the smallest positive

sum and remove translated pairs, then repeat). A realistic direct

\(N=500\) run would therefore

need roughly 50–100 GB of RAM and at least tens of core-hours; proof

generation could cost more. This is an engineering estimate, not a

benchmark. The instance was not run. The \(N=200\) construction was the

last bounded probe; all heavier figures in (16) come from the

\(O(kN^2)\) counting DP in the verifier, not from constructing or solving

those CNFs. **(d) for the exact counts; (a) for the leading-order count;

(c) for the resource estimate**

The exact small table is consequently real, certificate-backed progress,

but it does not supply the uniformity step needed to improve either side of

(1).

PARTIAL: Verified \(F(1)=1\), \(F(2)=9\), and certificate-backed \(F(3)=54\); an explicit checked colouring proves \(F(4)\geq201\), while the asymptotic tower-versus-double-exponential gap remains open.