Erdős problem #1183 — wave 6w
Date: 2026-08-12 UTC (initial report 2026-07-27)
2026-08-12 update: the exact seventh values
The finite table now extends by one case:
This is a [d] finite computer-assisted result. It does not settle either asymptotic question in Problem 1183 and makes no novelty or priority claim.
For the lower bound on \(F(7)\), a definition-level CNF fixes the empty set blue up to swapping the two colours and forbids every monochromatic seven-member union-closed family. Its 42,035 clauses have all been checked directly from the set masks. CaDiCaL proves the CNF unsatisfiable, and the included 5.6 MB DRAT proof independently replays to s VERIFIED with no RAT lemmas. For the upper bound, colour ranks \(3,4,6\) red and the other ranks blue; an exact closure search gives colour maxima \(6\) and \(7\), and the short case analysis in the verification report proves the same bounds.
For \(f(7)\), an eight-member maximal chain supplies the elementary lower bound \(4\). Colouring ranks \(0,2,3,5\) red and the other ranks blue gives exact lattice-closed maxima \(4,4\). Independently, a direct C++ audit checked all 21,111,090 red and 2,118,760 blue five-seed choices and found no five-member monochromatic sublattice.
The live page and all ten comments were rechecked through Bright Data on 2026-08-12: the problem remained OPEN, with zero claimed proofs and no current worker, collaborator, or formalisation worker. The complete certificate is frozen at verification/1183/f7-exact, with an independent cold audit at verification/1183/f7-hostile-audit.
0. Mandatory live-page gate
I fetched https://www.erdosproblems.com/1183 and its linked discussion thread through the Bright Data browser, not through datacenter curl. The live page showed:
- status: OPEN;
0 claimed proofs for this problem;Currently working on this problem: None;Interested in collaborating: None;- likes:
ebarschkis, Dogmachine; - all of “looks difficult”, “looks tractable”, “results could be
formalisable”, and “working on formalising” were None.
Thus the stop condition did not fire.
Verbatim live statement
Let \(f(n)\) be maximal such that in any \(2\)-colouring of the subsets of \(\{1,\ldots,n\}\) there is always a monochromatic family of at least \(f(n)\) sets which is closed under taking unions and intersections. Estimate \(f(n)\).
Let \(F(n)\) be defined similarly, except that we only require the family be closed under taking unions. Estimate \(F(n)\). In particular, is it true that \(F(n)\geq n^{\omega(n)}\) for some \(\omega(n)\to\infty\) as \(n\to\infty\), and \(F(n)<(1+o(1))^n\)?
The page attributes the problem to Erdős and Ulam. Its listed remarks say that the nested chain gives
that Erdős had no plausible conjecture for the order of \(f\), and that he also had no good guess for \(F\). It also records, without a reference, his statement that Howorka proved the superpolynomial lower bound when every rank receives a single colour.
All ten current comments
The discussion thread is https://www.erdosproblems.com/forum/thread/1183. These comments are explicitly marked by the site as unverified user content.
- Przemek Chojecki, 12:06 on 18 Mar 2026: links
https://www.ulam.ai/research/erdos1183.pdf and claims the subexponential upper half, using free rank/VC dimension for \(F\) and distributive lattices/bounded-width posets for \(f\).
- Quanyu Tang, 12:40: says Tang, He, and Li independently obtained nearly
the same partial result with GPT and links a PDF in https://github.com/QuanyuTang/erdos-problem-1183.
- Chojecki, 13:03: asks for an English version.
- Tang, 13:29: links the English translation.
- Chojecki, 13:44: thanks Tang.
- Tang, 13:58: reports an AI comparison saying the \(F\)-proofs are
essentially the same and Chojecki's bound is more precise.
old-bielefelder, 13:22: reports another AI comparison and identifies
the remaining questions as the scale of \(f\) and polynomial versus quasipolynomial growth of \(F\).
- Chojecki, 13:43: thanks the commenter.
- Nat Sothanaphan, 14:45: says a “standard check” found the manuscript
plausible but incomplete.
- Nat Sothanaphan, 14:47: says another standard check found four likely
minor required issues.
No comment is registered as a claimed proof, and there is no current worker.
1. Claim labels
Every mathematical claim below is marked as one of:
- [a] elementary-rigorous;
- [b] rigorous modulo a named theorem;
- [c] plausible/structural-unverified;
- [d] computational-only.
Page-status and bibliographic observations are factual audit notes rather than mathematical claims.
2. Primary-source literature audit
The actual 1978 source
The correct primary source is:
P. Erdős, Problems and Results in Combinatorial Analysis and Combinatorial Number Theory, Proceedings of the Ninth Southeastern Conference on Combinatorics, Graph Theory, and Computing (1978), 29–40, especially p. 39:
https://combinatorica.hu/~p_erdos/1978-36.pdf.
The source states the problem essentially as on the live page. It also contains a relevant result that the page remarks do not spell out: Erdős proves probabilistically that there is a two-colouring with no monochromatic free \(k\)-tuple once
where “free” means that all \(2^k-1\) nonempty unions are distinct and monochromatic. [a]
The self-hosted Chojecki manuscript has a bibliographic mismatch: its reference [7] names Some more problems on elementary geometry, Austral. Math. Soc. Gazette 5 (1978), 52–54. That is not the p. 39 source for this problem. This mismatch does not by itself affect its arguments, but the 1978-36 PDF above is the source that actually contains #1183.
The March 2026 documents
Chojecki's nine-page, self-hosted manuscript (dated 18 March 2026) claims
and
The Tang repository contains an exploratory GPT chat record claiming the same quasipolynomial type of upper bound for \(F\) and the weaker \((4+o(1))n\log n\) upper bound for \(f\). Because these are a self-hosted manuscript and a chat transcript, and the live comments themselves flag incomplete checking, I record their full \(f\)-bounds as [c] and do not use them in the small-case theorem below.
I did independently check the short \(F\)-argument. If a union-closed family \(\mathcal U\subseteq 2^{[n]}\) has
then Sauer–Shelah says that \(\mathcal U\) shatters a \(d\)-set \(X\). Choosing \(A_i\in\mathcal U\) whose trace on \(X\) is the \(i\)-th singleton makes all nonempty unions of the \(A_i\) distinct. [b]
There are at most \(2^{nd}\) ordered \(d\)-tuples, and a fixed free tuple has \(2^d-1\) distinct unions, monochromatic with probability \(2^{2-2^d}\). Thus the expected number is at most
Taking \(d=\lceil\log_2 n+\log_2\log_2 n+5\rceil\) makes this less than one for large \(n\), and hence
This is [b], modulo Sauer–Shelah. It verifies the subexponential upper half claimed in the comments, but it does not prove the requested superpolynomial lower bound.
Exact-title, exact-statement, author, and arXiv searches found no arXiv or journal version of the Chojecki manuscript and no other primary paper specifically treating these two parameters. This is a search miss, not a proof that none exists. I verified the existence and contents of every document named above; I do not rely on unrelated union-closed-set papers.
3. Exact small cases
The new finite result is:
The \(f\)-row and the entries \(F(1),\ldots,F(4)\) have elementary proofs [a]. The exact lower bounds for \(F(5)\) and \(F(6)\) use exhausted finite certificates and are therefore labelled [d], even though the certificates and checker are explicit.
3.1 Universal chain lower bound [a]
The chain
has \(n+1\) elements. At least \(\lceil(n+1)/2\rceil\) have one colour, and every subfamily of a chain is closed under both union and intersection. Hence
This already supplies all the displayed \(f\)-lower bounds and all \(F\)-lower bounds through \(n=4\).
3.2 Finite certificate for \(F(5)\geq4\) [d]
Inside \(2^{[5]}\), take the following ten sets:
Among their \(\binom{10}{4}\) quadruples, exactly 84 are union-closed. The checker exhausts all \(2^9=512\) two-colourings up to swapping the colours and verifies that every one contains a monochromatic one of these 84 quadruples. Restricting an arbitrary colouring of \(2^{[5]}\) to \(\mathcal V_5\) therefore proves \(F(5)\geq4\).
3.3 Finite certificate for \(F(6)\geq5\) [d]
Inside \(2^{[6]}\), take:
Exactly 824 of its \(\binom{17}{5}\) quintuples are union-closed. The checker exhausts \(2^{16}=65\,536\) colourings up to colour swap and finds a monochromatic one in every colouring. Hence \(F(6)\geq5\).
These certificates are substantially smaller than exhaustively enumerating the \(2^{32}\) and \(2^{64}\) colourings of the full Boolean lattices.
4. Explicit upper-bound colourings
In this section red receives the displayed ranks and blue receives all other ranks.
For \(n\leq4\), the \(F\)-colourings and \(f(n)\leq F(n)\) complete the table. Direct pair checks give the displayed maxima. [a]
4.1 \(F(5)\leq4\) [a]
Colour odd ranks red and even ranks blue.
In a red union-closed family there is at most one singleton. Two distinct 3-sets can coexist only when their union is \([5]\), equivalently when their 2-element complements are disjoint; hence there are at most two 3-sets. Adding the possible singleton and \([5]\) gives at most four sets.
In a blue union-closed family, distinct selected 2-sets must be disjoint (otherwise their union has rank 3), so there are at most two. There is at most one 4-set because two distinct 4-sets have union \([5]\). Including \(\varnothing\) gives at most four. Thus \(F(5)\leq4\).
4.2 \(F(6)\leq5\) [a]
Colour ranks \(0,1,4,6\) red and ranks \(2,3,5\) blue.
For red, at most one singleton is selected. Distinct selected 4-sets must have union \([6]\); their 2-element complements are therefore pairwise disjoint, so there are at most three. If a singleton \(\{i\}\) is selected, every selected 4-set contains \(i\), so their complements are pairwise disjoint pairs in the other five points and there are at most two. With the optional bottom and top, both cases have size at most five.
For blue, there is at most one 5-set. Distinct selected 3-sets must intersect in one point and have a common selected 5-set as their union. Taking complements inside that 5-set shows there are at most two such 3-sets.
The selected 2-sets form a pairwise-intersecting graph, since disjoint pairs have a red 4-set as union. Such a graph is a star or a triangle. A star with three leaves forces two selected 3-sets whose union is a red 4-set, so a star contributes at most two edges. A triangle contributes three 2-sets and forces its 3-set. In the triangle case, no second 3-set can coexist: it would meet the triangle in one point, and its union with either triangle edge through that point would be a red 4-set. Therefore:
- with at most two 2-sets, there are at most \(2+2+1=5\) sets;
- with three 2-sets, there are at most \(3+1+1=5\) sets.
Thus \(F(6)\leq5\).
4.3 \(f(5)\leq3\) [a]
Colour ranks \(0,1,3\) red and ranks \(2,4,5\) blue.
Red contains at most one singleton (two have a blue union) and at most one 3-set (two have a blue union), plus \(\varnothing\). Blue contains at most one 2-set (two have a red intersection), at most one 4-set (two have a red intersection), plus \([5]\). Hence every monochromatic sublattice has at most three members.
4.4 \(f(6)\leq4\) [a]
Colour ranks \(0,1,3,6\) red and ranks \(2,4,5\) blue.
Red contains at most one singleton. Two distinct selected 3-sets must be disjoint complements; all other intersection sizes make either their union or their intersection blue. Thus there are at most two 3-sets. If a singleton is selected, it must lie in every selected 3-set, so it cannot coexist with two complementary 3-sets. Including bottom and top gives at most four.
Within blue, no two distinct 2-sets, no two distinct 4-sets, and no two distinct 5-sets can coexist: in each case either their union or intersection is red. Thus blue has at most one member of each available rank, hence at most three. This proves \(f(6)\leq4\).
Combining Sections 3 and 4 proves the exact table with the labels stated there.
5. Independent standard-library verifier
The standalone verifier is runs/erdos1183_wave6w_verify.py (SHA-256 2179c5bbb3ac567dace8dc33d052e7f3353f5c1e0525f6c9efa878cc570d396f). It has no third-party dependencies.
For upper bounds it does not assume that a large lattice contains a closed subfamily of every smaller cardinality. Instead, if a closed family \(L\) has at least \(k\) members, it chooses any \(k\) seeds; the union/intersection closure generated by those seeds remains inside \(L\). The script enumerates every \(k\)-seed set and checks whether its generated closure stays monochromatic. This is an exhaustive from-scratch test.
Command and observed output:
$ python runs/erdos1183_wave6w_verify.py
certificate F(5)>=4: 84 edges; 512 colourings up to swap
certificate F(6)>=5: 824 edges; 65536 colourings up to swap
example F(5) upper-colouring witness: {{1}, {1,2,3}, {1,4,5}, {1,2,3,4,5}}
example F(6) upper-colouring witness: {{}, {1}, {1,2,3,4}, {1,2,5,6}, {1,2,3,4,5,6}}
example f(5) upper-colouring witness: {{}, {1}, {1,2,3}}
example f(6) upper-colouring witness: {{}, {1}, {1,2,3}, {1,2,3,4,5,6}}
n: 1 2 3 4 5 6
f(n): 1 2 2 3 3 4
F(n): 1 2 2 3 4 5
ALL CHECKS PASSED in 11.336s
Complete source:
#!/usr/bin/env python3
"""Standard-library re-verifier for the small cases in Erdős problem 1183.
Subsets of [n] are represented by n-bit integers. The script verifies:
n 1 2 3 4 5 6
f(n) 1 2 2 3 3 4
F(n) 1 2 2 3 4 5
It does not use the SAT solver that was used to discover the two finite
Ramsey certificates. It checks those certificates by exhaustive
two-colouring, and checks every upper-bound colouring by generating the
closure of every potentially offending seed set.
"""
from itertools import combinations
from math import ceil
from time import perf_counter
def union_closed(family):
"""Return whether an iterable of bitsets is closed under union."""
family = frozenset(family)
return all((a | b) in family for a in family for b in family)
def lattice_closed(family):
"""Return whether an iterable of bitsets is closed under union and meet."""
family = frozenset(family)
return union_closed(family) and all(
(a & b) in family for a in family for b in family
)
def generated_closure_stays_inside(seeds, colour, require_intersections):
"""Generate the closure of seeds, stopping if it leaves colour.
If a monochromatic closed family L has at least k members, any k of
its members generate a closed family contained in L. Consequently,
checking every k-subset of a colour class with this routine is an
exhaustive test for the existence of a closed family of size >= k.
"""
colour = frozenset(colour)
closure = set(seeds)
while True:
old_size = len(closure)
members = tuple(closure)
for i, a in enumerate(members):
for b in members[i:]:
results = (a | b, a & b) if require_intersections else (a | b,)
for result in results:
if result not in colour:
return None
closure.add(result)
if len(closure) == old_size:
predicate = lattice_closed if require_intersections else union_closed
assert predicate(closure)
return frozenset(closure)
def find_closed_family_at_least(colour, k, require_intersections):
"""Find a closed family of size >= k in colour, or return None."""
colour = tuple(sorted(colour))
if len(colour) < k:
return None
for seeds in combinations(colour, k):
closure = generated_closure_stays_inside(
seeds, colour, require_intersections
)
if closure is not None:
assert len(closure) >= k
return closure
return None
def rank_colouring(n, red_ranks):
universe = frozenset(range(1 << n))
red = frozenset(a for a in universe if a.bit_count() in red_ranks)
blue = universe - red
assert red.isdisjoint(blue) and red | blue == universe
return red, blue
def check_upper_colouring(n, red_ranks, bound, require_intersections):
"""Exhaustively verify that a displayed colouring has maximum <= bound."""
red, blue = rank_colouring(n, red_ranks)
for name, colour in (("red", red), ("blue", blue)):
offender = find_closed_family_at_least(
colour, bound + 1, require_intersections
)
assert offender is None, (n, name, bound, sorted(offender))
# Also ensure that the claimed bound occurs in this colouring.
witnesses = [
find_closed_family_at_least(colour, bound, require_intersections)
for colour in (red, blue)
]
assert any(witness is not None for witness in witnesses)
return red, blue, next(w for w in witnesses if w is not None)
def check_chain_lower_bound(n):
"""Check the elementary ceil((n+1)/2) chain argument for this n."""
chain = tuple((1 << j) - 1 for j in range(n + 1))
assert lattice_closed(chain)
target = ceil((n + 1) / 2)
for colouring in range(1 << (n + 1)):
red = tuple(chain[j] for j in range(n + 1) if colouring >> j & 1)
blue = tuple(chain[j] for j in range(n + 1) if not (colouring >> j & 1))
assert max(len(red), len(blue)) >= target
assert lattice_closed(red) and lattice_closed(blue)
return target
def verify_union_ramsey_certificate(n, target, vertices, expected_edges):
"""Exhaust a finite non-2-colourable hypergraph certificate.
Hyperedges are the target-element union-closed subfamilies induced by
``vertices``. Colour swapping lets us fix the first vertex blue, so
only 2^(|vertices|-1) colourings need be checked.
"""
vertices = tuple(vertices)
assert len(vertices) == len(set(vertices))
assert all(0 <= a < (1 << n) for a in vertices)
position = {a: i for i, a in enumerate(vertices)}
edge_masks = []
for edge in combinations(vertices, target):
if union_closed(edge):
mask = sum(1 << position[a] for a in edge)
edge_masks.append(mask)
assert len(edge_masks) == expected_edges
full = (1 << len(vertices)) - 1
checked = 0
for tail in range(1 << (len(vertices) - 1)):
# Bit 0 (the first certificate vertex) is fixed blue.
red = tail << 1
blue = full ^ red
assert any(
(edge & red) == edge or (edge & blue) == edge
for edge in edge_masks
), (n, target, red)
checked += 1
return len(edge_masks), checked
def fmt_family(n, family):
def fmt_set(bits):
entries = [str(i + 1) for i in range(n) if bits >> i & 1]
return "{" + ",".join(entries) + "}"
return "{" + ", ".join(fmt_set(a) for a in sorted(family)) + "}"
def main():
started = perf_counter()
# Explicit rank colourings proving the F upper bounds for n=1,...,6.
# The other colour always receives all ranks not displayed.
union_upper_colourings = {
1: ({0}, 1),
2: ({0, 2}, 2),
3: ({0, 2}, 2),
4: ({0, 1, 3}, 3),
5: ({1, 3, 5}, 4),
6: ({0, 1, 4, 6}, 5),
}
# For n <= 4, f(n) <= F(n) and the chain lower bound is sharp.
# These two additional colourings prove the f upper bounds at n=5,6.
lattice_upper_colourings = {
5: ({0, 1, 3}, 3),
6: ({0, 1, 3, 6}, 4),
}
chain_bounds = {n: check_chain_lower_bound(n) for n in range(1, 7)}
union_witnesses = {}
for n, (red_ranks, bound) in union_upper_colourings.items():
_, _, witness = check_upper_colouring(
n, red_ranks, bound, require_intersections=False
)
union_witnesses[n] = witness
lattice_witnesses = {}
for n, (red_ranks, bound) in lattice_upper_colourings.items():
_, _, witness = check_upper_colouring(
n, red_ranks, bound, require_intersections=True
)
lattice_witnesses[n] = witness
# Small non-2-colourable union-closed hypergraph for F(5) >= 4.
cert5 = (0, 1, 5, 13, 17, 19, 21, 27, 29, 31)
cert5_stats = verify_union_ramsey_certificate(
n=5, target=4, vertices=cert5, expected_edges=84
)
# Small non-2-colourable union-closed hypergraph for F(6) >= 5.
cert6 = (
0,
1,
3,
15,
32,
33,
35,
47,
48,
50,
51,
52,
54,
55,
60,
62,
63,
)
cert6_stats = verify_union_ramsey_certificate(
n=6, target=5, vertices=cert6, expected_edges=824
)
f_values = [chain_bounds[n] for n in range(1, 7)]
F_values = [
chain_bounds[1],
chain_bounds[2],
chain_bounds[3],
chain_bounds[4],
4,
5,
]
assert f_values == [1, 2, 2, 3, 3, 4]
assert F_values == [1, 2, 2, 3, 4, 5]
assert f_values[4] == lattice_upper_colourings[5][1]
assert f_values[5] == lattice_upper_colourings[6][1]
assert all(f <= F for f, F in zip(f_values, F_values))
print("certificate F(5)>=4:", cert5_stats[0], "edges;",
cert5_stats[1], "colourings up to swap")
print("certificate F(6)>=5:", cert6_stats[0], "edges;",
cert6_stats[1], "colourings up to swap")
print("example F(5) upper-colouring witness:",
fmt_family(5, union_witnesses[5]))
print("example F(6) upper-colouring witness:",
fmt_family(6, union_witnesses[6]))
print("example f(5) upper-colouring witness:",
fmt_family(5, lattice_witnesses[5]))
print("example f(6) upper-colouring witness:",
fmt_family(6, lattice_witnesses[6]))
print("n: ", " ".join(map(str, range(1, 7))))
print("f(n):", " ".join(map(str, f_values)))
print("F(n):", " ".join(map(str, F_values)))
print(f"ALL CHECKS PASSED in {perf_counter() - started:.3f}s")
if __name__ == "__main__":
main()
6. What remains and the precise wall
The finite table does not settle either asymptotic order.
For the superpolynomial lower bound on \(F\), a sufficient missing lemma would be a quantitative Ramsey statement forcing a monochromatic free rank \(k=\omega(\log n)\) in every colouring, because its \(2^k-1\) unions form a monochromatic union-closed family. Erdős records only a fixed-\(k\) result with an exorbitantly growing threshold; the random colouring argument shows that free rank above about \(\log_2 n\) can be avoided. Thus this particular route would have to beat an actual probabilistic obstruction, or use large bounded-free-rank families in a new way. This is the exact structural bottleneck, not merely a lack of search effort. [c]
For \(f\), the chain remains the only uniform lower mechanism used here. The small rank colourings show that the chain bound is sharp through \(n=7\), but they do not form a verified uniform construction. Determining whether every colouring forces a superlinear distributive sublattice is the missing uniform step. [c]
The initial report estimated that a naïve six-set-family computation for \(F(7)\) would be expensive. The 2026-08-12 update avoids that route: it enumerates the actual seven-member union-closed constraints, certifies their SAT core, and independently checks the upper colourings. This closes the next finite case but supplies no uniform mechanism in \(n\).
PARTIAL: Exact exhaustive certificates now give f(1..7)=1,2,2,3,3,4,4 and F(1..7)=1,2,2,3,4,5,7; both asymptotic Erdős-Ulam questions remain open.