Bound $L_4$: $33,070,982 \le R$

This mission formalizes the lower bound $33,070,982 \le R$ on the number of reversible binary cellular automata on the $3 \times 3$ Moore neighborhood. Extending the conserved-landscape marker families to both centered and off-centered rules.

Erdős Problem 68: Irrationality of sum 1/(n! - 1)

Problem Statement & Context

Erdős Problem 68 asks whether the infinite series 184987\sum_{n=2}^{\infty} rac{1}{n! - 1}184987 is irrational.

Paul Erdős proved in 1948 that \sum_{n=1}^{\infty} rac{1}{2^n - 1} is irrational, but the problem for factorial denominators ! - 1$ remains open.

Main Target Theorem

Motivation

Given a real matrix $A=(a_{ij})\in\mathbb R^{m\times n}$, consider maximizing the bilinear form $\sum_{i,j}a_{ij}x_iy_j$ over sign vectors $x\in\{\pm1\}^m$, $y\in\{\pm1\}^n$. This discrete optimum, written $\mathrm{OPT}(A)$, is closely tied to the cut norm of a matrix and is NP-hard to compute. Relaxing each sign to a unit vector and each product to an inner product gives the semidefinite value $\mathrm{SDP}(A)$, computable in polynomial time. Grothendieck's inequality (Grothendieck, 1953) states that the relaxation overshoots by at most a universal factor: there is a finite $K$, independent of $A$, of $m,n$, and of the dimension of the vectors, with $\mathrm{SDP}(A)\le K\cdot\mathrm{OPT}(A)$ for every $A$. The Grothendieck constant $K_G$ is the least such $K$ — equivalently, the worst-case integrality gap of the canonical semidefinite relaxation of this bilinear problem.

The constant is not a curiosity of one optimization problem. It originated in functional analysis, where it is central to the geometry of Banach spaces and to harmonic analysis; it governs the approximation ratio available for cut norms; and, in quantum information, it measures the maximal advantage of quantum over classical correlations in Bell-type experiments. Its exact value has been open since 1953.

A timeline of the bounds:

• 1953, Grothendieck. Existence of a finite $K$, together with the lower bound $K_G\ge\pi/2=1.5707\ldots$
• 1977, Krivine. $K_G\le\pi/\bigl(2\log(1+\sqrt2)\bigr)=1.7822\ldots$, obtained by analyzing hyperplane rounding, and conjectured to be optimal.
• 1984/1991, Davie and Reeds (independently). $K_G\ge1.6769\ldots$, from an explicit high-dimensional Gaussian hard instance.
• 2011, Braverman–Makarychev–Makarychev–Naor. Krivine's conjecture is false: $K_G<\pi/(2\log(1+\sqrt2))$ strictly, with no quantitative gap.
• 2014, Naor–Regev. Mixtures of Krivine schemes are asymptotically optimal: rounding schemes of this one family approach the true value of $K_G$.
• 2026, Heilman; Jones–Malavolta. The first improvements on Davie–Reeds, by $10^{-26}$ and $10^{-12}$ respectively; and the first explicit numerical improvements on Krivine's bound, of order $10^{-5}$ (Heilman; Li–Saha–Xue et al.).
• 2026, Saha–Li–Xue–Chaudhuri–Klivans–Kothari–Meka. The bounds this mission targets:

i.e. $1.7135\ldots\le K_G\le1.7818\ldots$, which fixes the tenths digit of $K_G$ at $7$.

Setting

Fix $m,n\in\mathbb N$ and $A\in\mathbb R^{m\times n}$.

Here $u_1,\dots,u_m$ and $v_1,\dots,v_n$ are unit vectors of a common but arbitrary finite dimension $d$. Since a sign is a unit vector in dimension one, $\mathrm{OPT}(A)\le\mathrm{SDP}(A)$. Call $K$ a Grothendieck bound if $\mathrm{SDP}(A)\le K\cdot\mathrm{OPT}(A)$ for every $m$, $n$ and $A$, and set $K_G:=\inf\{K: K\text{ is a Grothendieck bound}\}$.

Upper bounds on $K_G$ come from rounding algorithms. A Krivine scheme of dimension $k$ is a pair of partitions of $\mathbb R^k$ into a $+1$ region and a $-1$ region, encoded by measurable odd functions $f,g:\mathbb R^k\to\{\pm1\}$: the algorithm maps each SDP vector to a Gaussian point in $\mathbb R^k$, correlated according to the inner products, and reads off the label of the region the point lands in. Taking $f=g=\operatorname{sgn}(z_1)$ recovers random hyperplane rounding. The quality of a scheme is carried by its normalized correlation function

where $X,Y$ are standard Gaussian vectors in $\mathbb R^k$ with $\mathbb E[X_iY_i]=t$ for every coordinate $i$. For the half-space partition $H(t)=\arcsin t$, whose analysis gives Krivine's bound. Writing the odd expansion $H(t)=b_1t+b_3t^3+\cdots$, the hyperplane scheme sits at $(b_1,b_3)=(1,\tfrac16)$.

Formalization targets

Goal

This is the two-sided bound the source paper states as the outcome of its Theorems 2.1 and 2.2. It is the weakest statement that carries both of the paper's contributions at once; each side is also a milestone in its own right, so partial progress is recorded even if only one direction closes.

Milestones

The milestone list runs from the classical background to the two new bounds: $\mathrm{OPT}\le\mathrm{SDP}$; the existence of a finite Grothendieck bound; $K_G\ge\pi/2$; Krivine's $K_G\le\pi/(2\log(1+\sqrt2))$; the affine coefficient constraint $b_3\ge2b_1-\tfrac{11}{6}$ valid for every Krivine scheme (Theorem 2.2, equation (1)); the transfer of a member of the affine family into a lower bound on $K_G$ (Appendix A); the lower bound $K_G\ge6\pi/11$ (Theorem 2.2); and the cubic–quintic upper bound (Theorem 2.1).

Significance

The two target bounds narrow an interval that had been essentially static for four decades: before 2026 the state of the art was $1.6769\ldots\le K_G\le1.7822\ldots$, wide enough that the tenths digit was unknown. The lower bound is also methodologically new. Every previous lower bound was obtained by exhibiting a hard instance; this one instead proves a ceiling on the performance of every rounding scheme in the Krivine family and converts that ceiling, through the Naor–Regev optimality theorem, into a bound on the constant. The affine constraint $b_3\ge2b_1-\tfrac{11}{6}$ is the transportable core of that argument: being affine in the coefficients, it survives mixing schemes and passing to limits, which is exactly what the reduction to $K_G$ requires.

On the formalization side, nothing here is machine-checked today. The upper bound (Theorem 2.1) is certified by interval arithmetic in the companion paper, and the lower bound's central one-dimensional inequality likewise rests on a computer-assisted certificate; reproducing either inside Lean means building a rigorous numeric layer on top of the analytic argument. Ahead of that, the mission needs a formal definition of $K_G$ itself and of the Krivine-scheme apparatus, neither of which exists in Mathlib — these are reusable well beyond this mission, since Grothendieck's inequality feeds cut-norm approximation and Bell-inequality bounds. Contributions of intermediate lemmas about $\mathrm{OPT}$, $\mathrm{SDP}$, Gaussian correlation identities, and Hermite expansions are welcome even when the headline bounds stay open.

Difficulty

The obvious route to a lower bound is to write down a matrix and compute. That route is what Davie and Reeds exhausted; improving it has produced gains of order $10^{-12}$ at best, because the hard instances are high-dimensional Gaussian objects whose $\mathrm{OPT}$ is itself hard to bound tightly. The route taken here avoids instances entirely, and its difficulty lies elsewhere: a constraint on a single scheme is worthless unless it survives averaging over schemes and passing to limits of schemes of growing dimension, since only then does the Naor–Regev optimality theorem convert it into a statement about $K_G$. Constraints that are nonlinear in the scheme do not survive that passage, which is why the target inequality is affine in $(b_1,b_3)$. For the upper bound, the difficulty is that the improvement is genuinely asymptotic: it comes from a limit of schemes of growing dimension rather than any fixed low-dimensional partition, and the final margin of $3.47\times10^{-4}$ is certified numerically rather than in closed form.

Formalization scope

$\mathrm{OPT}(A)$ and $\mathrm{SDP}(A)$ are defined as suprema of explicitly described sets of reals, over matrices indexed by Fin m and Fin n with real entries; the sign vectors are real-valued functions constrained to take the values $1$ and $-1$, and the relaxation quantifies over unit vectors of EuclideanSpace ℝ (Fin d) for an existentially quantified $d$, so no dimension bound is built in. The empty-index cases $m=0$ or $n=0$ are included and give value $0$ on both sides. $K_G$ is the infimum of the set of Grothendieck bounds; that set is nonempty precisely by Grothendieck's inequality, which is itself a milestone, and it is bounded below, so the infimum is not a junk value.

A Krivine scheme is a structure carrying two measurable $\pm1$-valued functions on Fin k → ℝ, each odd almost everywhere. Almost-everywhere oddness is forced: no $\pm1$-valued function satisfies $f(-0)=-f(0)$ at the origin, so a pointwise requirement would make the structure empty and every statement about schemes vacuous. With the null-set relaxation the half-space partition is a scheme in every dimension $k\ge1$, and the definition file constructs it, pinning down non-vacuity; dimension $k=0$ admits no scheme. The correlation function is the explicit double Gaussian integral against the correlated-pair density, scaled by $\pi/2$, and the coefficients $b_1,b_3$ are read off as $H'(0)$ and $H'''(0)/6$ — where $H$ fails to be three times differentiable at $0$ these are the ambient junk value $0$, which a solver should keep in mind when reading the coefficient milestones.

No trivializing reading is available for the goal: it pins $K_G$ between two explicit numerical constants, so it can be satisfied neither vacuously nor by a degenerate convention. Solvers should be aware that the source paper states its two theorems in abridged form and refers to its companion paper for the full proofs, and that the further bounds reported there — the stronger lower rungs $27\pi/49$ and $51\pi/92$, and the upper values $1.781801841033$ and $1.7813319810625639$ — are explicitly described as system-tested but not author-verified; they are deliberately outside this mission's milestone list.

Selected references

• A. Grothendieck, Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79.
• J.-L. Krivine, Sur la constante de Grothendieck, C. R. Acad. Sci. Paris (1977).
• M. Braverman, K. Makarychev, Y. Makarychev, A. Naor, The Grothendieck constant is strictly smaller than Krivine's bound, FOCS 2011, 453–462. https://doi.org/10.1109/FOCS.2011.77
• A. Naor, O. Regev, Krivine schemes are optimal, Proc. Amer. Math. Soc. 142 (2014), 4315–4320. https://doi.org/10.1090/S0002-9939-2014-12145-3
• N. Alon, A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), 787–803. https://doi.org/10.1137/S0097539704441629
• A. Li, R. Saha, A. Xue, S. Chaudhuri, A. Klivans, P. K. Kothari, R. Meka, Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human–AI Mathematical Collaboration, arXiv:2608.11195v3, 2026. https://arxiv.org/abs/2608.11195
• R. Saha, A. Li, A. Xue, S. Chaudhuri, A. Klivans, P. K. Kothari, R. Meka, New upper and lower bounds for the Grothendieck constant, 2026 (companion paper containing the full proofs).

Motivation

Addition and multiplication interact in rigid ways: a finite set of numbers that is highly structured with respect to one operation (an arithmetic progression, say) tends to be unstructured with respect to the other (a geometric progression). The sum–product problem asks for the sharp quantitative form of this principle. It was posed by Erdős and Szemerédi in 1983 (Erdős Problem 52) and has since become a central question of additive combinatorics, with applications in incidence geometry, exponential sum estimates, expanders and randomness extraction.

Timeline.

• 1983 — Erdős and Szemerédi show that $\max(|A+A|,|AA|)\ge c|A|^{1+\delta}$ for some absolute $\delta>0$ and every finite set of integers $A$, and conjecture exponent $2-\varepsilon$.
• 1997 — Nathanson obtains the explicit exponent $1+\tfrac1{31}$; Ford (1998) improves it to $1+\tfrac1{15}$.
• 1997 — Elekes, using the Szemerédi–Trotter incidence theorem, proves $|A+A|\,|AA|\gg|A|^{5/2}$ for finite sets of reals, hence exponent $5/4$.
• 2009 — Solymosi proves $|A+A|^2|AA|\gg |A|^4/\log|A|$ for finite sets of positive reals, hence exponent $4/3$ up to a logarithmic factor.
• 2015–2022 — Konyagin and Shkredov first break the $4/3$ barrier (exponent $4/3+c$ for a small explicit $c>0$); after several improvements, Rudnev and Stevens reach $4/3+2/1167$ up to logarithmic factors.

The conjecture itself remains open.

Setting

For a finite set $A\subset\mathbb Z$ define the sumset and product set

For nonempty $A$ both contain at least $|A|$ elements and at most $\binom{|A|+1}{2}$. The quantity of interest is $\max(|A+A|,|AA|)$ as a function of $|A|$.

Formalization targets

Goal (Erdős–Szemerédi conjecture)

For every $0<\varepsilon<1$ there is $C_\varepsilon>0$ such that for every finite set $A\subset\mathbb Z$,

Known lower bounds (milestones, weakest to strongest)

Sharpness

The $\varepsilon$ cannot be removed: there is no $C>0$ with $\max(|A+A|,|AA|)\ge C|A|^2$ for all $A$ (take $A=\{1,\dots,n\}$; the multiplication table $|AA|$ is $o(n^2)$ by Erdős).

Significance

A proof of the goal would settle the sharp form of the sum–product phenomenon over $\mathbb Z$. Sum–product estimates are an input to incidence bounds, to Bourgain–Katz–Tao-type results over finite fields, and to explicit constructions in theoretical computer science; improvements of the exponent over $\mathbb R$ have come together with new incidence-geometric tools.

Formalization status: the milestones are published theorems (Erdős–Szemerédi, Elekes, Solymosi, Rudnev–Stevens, Erdős's multiplication table bound), but their proofs are not known to be formalized in Lean/Mathlib. The Szemerédi–Trotter theorem, multiplicative energy, and the Elekes and Solymosi arguments are reusable infrastructure. The goal itself is an open problem.

Difficulty

Incidence-geometric methods (Szemerédi–Trotter and its descendants) naturally produce exponents near $4/3$, and passing beyond $4/3$ has required intricate higher-energy arguments yielding only small gains. None of the existing approaches is known to reach exponents close to $2$; even over $\mathbb Z$, where arithmetic structure is available, the best general bounds are the real-number ones.

Formalization scope

Sets are Finset ℤ; $A+A$ and $AA$ are Mathlib's pointwise sumset and product set (open scoped Pointwise), and cardinalities are cast to $\mathbb R$. Powers are real powers (Real.rpow). The empty set is allowed; the hypothesis $\varepsilon<1$ keeps every exponent positive, so the empty set contributes the trivial inequality $0\ge 0$ rather than a junk value $0^0=1$. The constant $C$ may depend on $\varepsilon$ but not on $A$. The Solymosi milestone is stated for $|A|\ge2$ so that $\log|A|>0$.

The statements are for integer sets only; results proved over $\mathbb R$ specialise to them. Contributions of general-purpose infrastructure (Szemerédi–Trotter over $\mathbb R$, multiplicative energy, bounds for the multiplication table) are welcome.

Selected references

• P. Erdős, E. Szemerédi, On sums and products of integers, Studies in Pure Mathematics, Birkhäuser, 1983, 213–218.
• M. B. Nathanson, On sums and products of integers, Proc. Amer. Math. Soc. 125 (1997), 9–16.
• K. Ford, Sums and products from a finite set of real numbers, Ramanujan J. 2 (1998), 59–66.
• G. Elekes, On the number of sums and products, Acta Arith. 81 (1997), 365–367.
• J. Solymosi, Bounding multiplicative energy by the sumset, Adv. Math. 222 (2009), 402–408. https://arxiv.org/abs/0806.1040
• S. V. Konyagin, I. D. Shkredov, On sum sets of sets having small product set, Proc. Steklov Inst. Math. 290 (2015), 288–299. https://arxiv.org/abs/1503.05771
• M. Rudnev, S. Stevens, An update on the sum-product problem, Math. Proc. Cambridge Philos. Soc. 173 (2022), 411–430. https://arxiv.org/abs/2005.11145
• Erdős Problem 52, https://www.erdosproblems.com/52

Motivation

A set $A$ of positive integers is pairwise coprime if $\gcd(a,b)=1$ for all distinct $a,b\in A$. The primes are the model example, and a recurring theme in Erdős's combinatorial number theory is that pairwise coprime sets cannot do much better than the primes on natural additive or harmonic statistics. Erdős Problem 1210 asks for a sharp version of this principle for the harmonic weight $1/(n-a)$, which measures how densely a coprime set can crowd the point $n$ from below.

Timeline.

• 1977. In [Er77c, p.64] Erdős posed a question about the primes $q_1<\dots<q_k$ in an interval $(n,m]$: is $\sum_i 1/(q_i-n)<\sum_{p<m-n}1/p+O(1)$?
• 1980. In [Er80, p.112] he wrote that he had "not stated [this] quite correctly" in [Er77c] and posed the question for arbitrary pairwise coprime sets $A\subseteq[1,n)$, which is the form recorded as Problem 1210.
• 2026. On the erdosproblems.com forum, a reduction to a counting bound for $A\cap[n-x,n)$ was suggested; it was then observed that this counting bound would itself imply an open inequality of the type $\pi(x+y)\le\pi(x)+\pi(y)+O(y/(\log y)^2)$ (compare Problem 855). The problem remains open.

Setting

Fix a natural number $n$. Consider finite sets $A$ of integers with $1\le a<n$ for every $a\in A$, and with $\gcd(a,b)=1$ for all distinct $a,b\in A$. For such a set define the reciprocal gap sum

Every term is at most $1$, and the element $a=n-d$ contributes $1/d$. Write $\sum_{p<n}1/p$ for the sum of reciprocals of the primes below $n$; by Mertens' theorem it equals $\log\log n+O(1)$. Throughout, $\pi(x)$ denotes the number of primes $p\le x$.

Target

The goal of the mission is the affirmative answer to Problem 1210: there is an absolute constant $C$ such that

for every $n$ and every pairwise coprime $A\subseteq[1,n)$. A negative answer is equally welcome and is recorded by disproving the goal statement.

The milestones are:

1. Small prime factors. For pairwise coprime $A$, at most $\pi(x)$ elements of $A\cap[n-x,n)$ have a prime factor $\le x$.
2. Partial summation reduction. If $|A\cap[n-x,n)|\le\pi(x)+O(x/(\log x)^2)$ uniformly, then the goal holds.
3. The [Er77c] variant. For the primes $q_i$ in $(n,m]$, $\sum_i 1/(q_i-n)<\sum_{p<m-n}1/p+O(1)$.

Significance

The result itself. An affirmative answer would say that, for the weight $1/(n-a)$, no pairwise coprime set beats the primes by more than a constant, and would give a quantitative form of the heuristic that coprime sets behave like sets of primes near a point. A negative answer would exhibit coprime sets that concentrate near $n$ more efficiently than the primes do in the harmonic sense. The [Er77c] variant concerns only primes, and relates the distribution of primes just above $n$ to the primes below the interval length $m-n$.

Formalizing it. Neither the goal nor the [Er77c] variant is known. The mission produces Lean statements checked against the source, a reduction (milestone 2), to be verified in Lean, that isolates exactly which counting estimate would suffice, and the elementary coprimality lemma (milestone 1). These pin down what a proof or disproof must supply.

Difficulty

The natural first attempt splits $A\cap[n-x,n)$ into elements with a prime factor $\le x$, of which there are at most $\pi(x)$, and $x$-rough elements, and then hopes that sieve bounds make the rough part $O(x/(\log x)^2)$. The obstruction is that $A$ may contain many primes in $[n-x,n)$. Bounding the number of primes in a short interval $[n-x,n)$ by $\pi(x)+O(x/(\log x)^2)$ is a form of the second Hardy–Littlewood conjecture $\pi(x+y)\le\pi(x)+\pi(y)$, which is open and known to be incompatible, in its exact form, with the prime $k$-tuples conjecture. So the counting route in milestone 2 needs input on primes in short intervals beyond current knowledge, and any proof of the goal must either supply such input or avoid pointwise counting.

Formalization scope

All objects are elementary: $A$ is a Finset ℕ, coprimality is Nat.Coprime, primes are Nat.Prime, $\pi$ is Nat.primeCounting, and the sums are real-valued. The source's $O(1)$ is encoded as an existentially quantified real constant $C$ chosen before $n$ and $A$. The source asks a yes/no question; each statement is posed in its affirmative form, and a disproof (a proof of the negation) settles the negative answer. The standing hypothesis $1\le a<n$ means every denominator $n-a$ is at least $1$, so no division-by-zero default can make the statement trivial. The window $[n-x,n)$ is written as $a\ge n-x$ with truncated natural subtraction together with $a<n$.

No new definitions are required. Useful reusable contributions include Mertens-type estimates for $\sum_{p<n}1/p$, partial summation lemmas for finite sums over $\mathbb N$, and upper bounds for primes in short intervals.

Selected references

• P. Erdős, Problems and results on combinatorial number theory. III, Number Theory Day (Proc. Conf., Rockefeller Univ., New York, 1976), (1977), 43–72. [Er77c]
• P. Erdős, A survey of problems in combinatorial number theory, Ann. Discrete Math. (1980), 89–115. [Er80]
• T. F. Bloom, Erdős Problem #1210, https://www.erdosproblems.com/1210 , and discussion thread https://www.erdosproblems.com/forum/thread/1210
• Formal Conjectures project, ErdosProblems/1210.lean, https://github.com/google-deepmind/formal-conjectures

Motivation

Which sets of positive integers are forced to contain long arithmetic progressions? Van der Waerden (1927) showed that in any finite colouring of $\mathbb N$ some colour class does; Erdős and Turán (1936) asked for a density version, which became Szemerédi's theorem. Erdős then proposed the strongest natural size condition: divergence of the reciprocal sum. Erdős Problem #3 (erdosproblems.com/3) asks whether every $A\subseteq\mathbb N$ with $\sum_{n\in A}1/n=\infty$ contains arbitrarily long arithmetic progressions. Erdős attached one of his largest prizes to it. The primes are the motivating example: $\sum_p 1/p=\infty$, so a positive answer would contain the Green–Tao theorem.

Timeline.

• 1936 — Erdős and Turán conjecture that sets of positive density contain arbitrarily long progressions.
• 1953 — Roth proves the case $k=3$ of the density conjecture by Fourier analysis.
• 1975 — Szemerédi proves the density conjecture for all $k$.
• 2001 — Gowers gives the first quantitative bounds for all $k$: $r_k(N)\ll N/(\log\log N)^{c_k}$.
• 2008 — Green and Tao prove that the primes contain arbitrarily long progressions.
• 2020 — Bloom and Sisask prove $r_3(N)\ll N/(\log N)^{1+c}$, which settles the case $k=3$ of Erdős Problem #3.
• 2023 — Kelley and Meka prove $r_3(N)\le N\exp(-c(\log N)^{1/12})$.
• 2024 — Leng, Sah and Sawhney prove $r_k(N)\le N\exp(-(\log\log N)^{c_k})$ for every $k\ge5$.

The problem is open for every $k\ge4$.

Setting

A set $S\subseteq\mathbb N$ is an arithmetic progression of length $k$ if $|S|=k$ and $S=\{a,a+d,\dots,a+(k-1)d\}$ for some $a,d\in\mathbb N$ (for $k\ge2$ the size condition forces $d>0$). For $k,N\in\mathbb N$, $r_k(N)$ denotes the largest size of a subset of $\{1,\dots,N\}$ containing no arithmetic progression of length $k$. A set $A$ has divergent reciprocal sum if $\sum_{n\in A}1/n=\infty$.

Formalization targets

Goal (Erdős Problem #3)

For every $A\subseteq\mathbb N$,

This is the formal-conjectures statement erdos_3 with its answer(sorry) instantiated to the conjectured answer yes. A disproof of the goal on the platform settles the problem negatively.

Milestones

• Szemerédi's theorem for sets of positive upper density (the density case), and the existing platform statement $r_k(N)=o(N)$.
• The Green–Tao theorem (the case $A=$ primes).
• The Bloom–Sisask bound on $r_3(N)$ and its corollary, the case $k=3$ of the goal; the Kelley–Meka bound (existing platform statement).
• The Leng–Sah–Sawhney bound for $k\ge5$.
• The partial-summation reduction: bounds $r_k(N)\le N/(\log N)^{1+c_k}$ for all $k\ge3$ imply the goal.

Significance

A positive answer would be a common strengthening of Szemerédi's theorem and the Green–Tao theorem, obtained from a single size condition with no arithmetic structure. Through the reduction milestone, it is closely tied to the quantitative theory of $r_k(N)$: bounds of the shape $N/(\log N)^{1+c}$ for every $k$ would suffice. Formalizing the milestones would also give reusable Lean statements of Szemerédi-type theorems in a common language.

Difficulty

Divergence of $\sum 1/n$ is a very weak condition: such sets can have density zero, and the natural approach through $r_k(N)$ requires bounds just past $N/\log N$. For $k=3$ this barrier was only broken in 2020. For $k\ge4$ the best known bounds (Leng–Sah–Sawhney) save only a power of $\log\log N$ in the exponent, far from what is needed. The Green–Tao method uses pseudorandom majorants specific to the primes and does not apply to arbitrary sets.

Formalization scope

All statements import the published definition file Erdos142Basic, which reproduces the formal-conjectures definitions IsAPOfLengthWith, IsAPOfLength and the counting function r k N (over $\{1,\dots,N\}$). The reciprocal-sum hypothesis is ¬ Summable (fun a : A ↦ 1 / (a : ℝ)); the element $0$, if present, contributes $1/0=0$. "Arbitrarily long" is written as ∃ᶠ k in atTop, which is equivalent to "every length" because sub-progressions of progressions are progressions. Bounds stated in the literature with $\ll$ are written without a multiplicative constant and with "for all sufficiently large $N$"; the constant can be absorbed into the exponent. Contributions formalizing partial summation over sets of naturals and the equivalence of the "frequently" and "for every $k$" forms are welcome.

Selected references

• P. Erdős and P. Turán, On some sequences of integers, J. London Math. Soc. 11 (1936).
• K. F. Roth, On certain sets of integers, J. London Math. Soc. 28 (1953).
• E. Szemerédi, On sets of integers containing no k elements in arithmetic progression, Acta Arith. 27 (1975).
• W. T. Gowers, A new proof of Szemerédi's theorem, Geom. Funct. Anal. 11 (2001).
• B. Green and T. Tao, The primes contain arbitrarily long arithmetic progressions, Ann. of Math. 167 (2008).
• T. F. Bloom and O. Sisask, Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions, arXiv:2007.03528 (2020).
• Z. Kelley and R. Meka, Strong bounds for 3-progressions, FOCS 2023, arXiv:2302.05537.
• J. Leng, A. Sah and M. Sawhney, Improved bounds for Szemerédi's theorem, arXiv:2402.17995 (2024).
• T. F. Bloom, Erdős Problem #3, https://www.erdosproblems.com/3

Motivation

A sunflower (also called a $\Delta$-system) with $k$ petals is a family of $k$ sets whose pairwise intersections are all equal to one common set, the kernel. In 1960 Erdős and Rado proved the sunflower lemma: every sufficiently large family of $n$-element sets contains a sunflower with $k$ petals, and they asked how large "sufficiently large" must be (Erdős–Rado 1960). The conjecture that the threshold is only exponential in $n$ is one of Erdős' best-known problems in extremal combinatorics; it is listed as Erdős Problem 20, and Erdős offered a $1000 prize for it. Sunflower bounds are used, for example, in Razborov's monotone circuit lower bounds and in the study of set systems with restricted intersections.

Timeline.

• 1960 — Erdős and Rado prove $(k-1)^n < f(n,k) \le (k-1)^n\, n! + 1$ and conjecture $f(n,k) \le c_k^{\,n}$ (ErRa60).
• 2019 — Alweiss, Lovett, Wu and Zhang prove $f(n,k) \le (C k^3 \log n \log\log n)^n$, the first bound of the form $(\log n)^{n(1+o(1))}$ for fixed $k$ (arXiv:1908.08483).
• 2020 — Rao simplifies the argument via Shannon's noiseless coding theorem and obtains $(\alpha k \log(kn))^n$ (arXiv:1909.04774); Tao gives an entropy proof of the same bound.
• 2021 — Bell, Chueluecha and Warnke obtain $f(n,k) \le (C k \log n)^n$ for $n,k \ge 2$ (arXiv:2009.09327).

The conjecture itself remains open, even for $k = 3$.

Setting

Fix natural numbers $n$ (the uniformity) and $k$ (the number of petals). A family $\mathcal F$ of sets is $n$-uniform if every member of $\mathcal F$ has exactly $n$ elements. A subfamily $\mathcal S \subseteq \mathcal F$ is a $k$-sunflower if $|\mathcal S| = k$ and there is a set $Y$ with $A \cap B = Y$ for all distinct $A, B \in \mathcal S$.

The sunflower threshold $f(n,k)$ is the least natural number $m$ such that every $n$-uniform family $\mathcal F$ (over any ground set) with $|\mathcal F| \ge m$ contains a $k$-sunflower.

Formalization targets

Goal — the sunflower conjecture (Erdős Problem 20)

The constants $c_k$ are left unspecified; only the exponential shape in $n$ is asked for. A disproof (the negation of this statement) would equally settle the problem.

Milestones from the literature

1. Erdős–Rado upper bound: $f(n,k) \le (k-1)^n\, n! + 1$ for $n \ge 1$, $k \ge 2$.
2. Erdős–Rado lower bound: $(k-1)^n < f(n,k)$ for $n \ge 1$, $k \ge 2$.
3. Rao's bound: there is $\alpha > 1$ with $f(n,k) \le (\alpha k \log(kn))^n + 1$ for $n \ge 1$, $k \ge 2$.
4. Bell–Chueluecha–Warnke bound: there is $C \ge 4$ with $f(n,k) \le (C k \log n)^n$ for $n, k \ge 2$.

A supporting sanity check, $f(0,1) = 1$, is taken from the source formalization.

Significance

A positive answer would show that sunflower-free $n$-uniform families have at most exponential size, the correct order of magnitude by the Erdős–Rado lower bound; this would sharpen every application that currently loses a $\log n$ factor per coordinate, including monotone circuit lower bounds. A negative answer would show the $(\log n)^n$-type bounds of 2019–2021 are essentially the truth.

On the formal side, the Erdős–Rado upper bound has a Lean formalization recorded in the source file; the lower-bound construction and the spread-family / coding arguments behind the Rao and Bell–Chueluecha–Warnke bounds are, as far as this proposal records, not yet formalized. Formalizing them produces reusable infrastructure on spread families and random-subset (or entropy) arguments.

Difficulty

The classical induction on $n$ (pick a maximal family of pairwise disjoint members; if it is small, some element lies in many members, recurse on the link) loses a factor of about $n$ at each of $n$ steps, which is where $n!$ comes from. The modern arguments replace the recursion by an analysis of spread families, but each still loses a factor $\log n$ per level, and no known technique removes it. The case $k = 3$ is already open.

Formalization scope

• The ground set is an arbitrary type in the lowest universe; set families are Set (Set α) and sizes are measured with Set.ncard, which returns $0$ on infinite sets. Consequently, for $n \ge 1$ only finite members can be "$n$-element", and the condition $m \le |\mathcal F|$ with $m \ge 1$ only applies to finite families. All targets assume $n \ge 1$ (except the sanity check), so the $n = 0$ quirks do not affect them.
• $f(n,k)$ is defined as an infimum over natural numbers; if no admissible $m$ existed the infimum would be $0$. The Erdős–Rado upper bound shows the admissible set is non-empty for $n \ge 1$.
• Logarithms are natural logarithms; changing the base only rescales the unspecified constants.
• The goal is stated as the positive claim of the conjecture, not as a yes/no answer(·) statement.

Contributions of general lemmas on sunflowers, spread families and the Erdős–Rado construction are welcome and reusable beyond this mission.

Selected references

• P. Erdős, R. Rado, Intersection theorems for systems of sets, J. London Math. Soc. 35 (1960), 85–90. doi:10.1112/jlms/s1-35.1.85
• R. Alweiss, S. Lovett, K. Wu, J. Zhang, Improved bounds for the sunflower lemma, Annals of Mathematics 194 (2021). arXiv:1908.08483
• A. Rao, Coding for sunflowers, Discrete Analysis 2020:2. arXiv:1909.04774
• T. Bell, S. Chueluecha, L. Warnke, Note on sunflowers, Discrete Mathematics 344 (2021). arXiv:2009.09327
• Erdős Problem 20. erdosproblems.com/20

Motivation

A set of integers is a Sidon set if all of its pairwise sums $a+b$ ($a\le b$) are different. Sidon, in connection with Fourier analysis, asked how dense such sets can be, and the question became one of the standard problems of additive combinatorics. Let

A counting argument shows $h(N)\le (1+o(1))\sqrt{2N}$, and the true order was settled early: $h(N)\sim\sqrt N$. What remains open is the size of the error term $h(N)-\sqrt N$. Erdős and Turán asked whether it is smaller than every power of $N$; Erdős offered $1000 for this problem (Erdős Problem #30), and it is also Problem 31 on Green's list of open problems and problem C9 in Guy's Unsolved Problems in Number Theory.

Timeline.

• 1938 — Singer constructs, for every prime power $q$, a set of $q+1$ residues modulo $q^2+q+1$ with all differences distinct. Combined with the density of primes this gives $h(N)\ge(1-o(1))\sqrt N$ (Singer 1938).
• 1941 — Erdős and Turán prove $h(N)\le N^{1/2}+O(N^{1/4})$ (Erdős–Turán 1941).
• 1969 — Lindström gives an alternative proof with the explicit bound $h(N)\le N^{1/2}+N^{1/4}+1$ (Lindström 1969).
• 2021 — Balogh, Füredi and Roy lower the constant: $h(N)\le N^{1/2}+0.998N^{1/4}$ for large $N$ (arXiv:2103.15850).
• 2022 — O'Bryant: $h(N)\le N^{1/2}+0.99703N^{1/4}$ for large $N$ (arXiv:2207.07800).
• 2023 — Carter, Hunter and O'Bryant: $h(N)\le N^{1/2}+0.98183N^{1/4}+O(1)$, with substantial computer assistance (arXiv:2310.20032).

No upper bound with an error exponent below $1/4$ is known, and no lower bound of the form $h(N)\ge\sqrt N-O(N^{\varepsilon})$ for every $\varepsilon>0$ is known either.

Setting

A set $A$ in an additive commutative monoid is Sidon if for all $i_1,j_1,i_2,j_2\in A$,

For a finite set $X$, $\operatorname{maxSidon}(X)$ is the largest size of a Sidon subset of $X$ (the empty set is Sidon, so this is well defined), and

The first values are $h(1),\dots,h(15)=1,2,2,3,3,3,4,4,4,4,4,5,5,5,5$ (OEIS A143824).

Formalization targets

Goal (Erdős Problem #30)

This is a two-sided statement: it asks both for an upper bound $h(N)\le\sqrt N+C_\varepsilon N^\varepsilon$ and for a matching lower bound $h(N)\ge\sqrt N-C_\varepsilon N^\varepsilon$ for large $N$. Erdős asked it as a yes/no question; the goal fixes the conjectured answer yes, so a disproof on the platform settles the question negatively.

Milestones (known results, weakest to strongest)

1. Singer's construction: $h(q^2+q+1)\ge q+1$ for every prime power $q$.
2. Singer's lower bound: $h(N)\ge(1-\varepsilon)\sqrt N$ for every $\varepsilon>0$ and all large $N$.
3. Erdős–Turán / Lindström: $h(N)\le\sqrt N+N^{1/4}+1$ for all $N$.
4. Balogh–Füredi–Roy: $h(N)\le\sqrt N+0.998N^{1/4}$ for all large $N$.
5. O'Bryant: $h(N)\le\sqrt N+0.99703N^{1/4}$ for all large $N$.
6. Carter–Hunter–O'Bryant: $h(N)\le\sqrt N+0.98183N^{1/4}+C$ for an absolute constant $C$.

Significance

The result itself. An affirmative answer would pin $h(N)$ down to $\sqrt N$ up to a sub-polynomial error, in both directions; Erdős even speculated that $h(N)=\sqrt N+O(1)$ might hold, while remarking that this is perhaps too optimistic. A negative answer would show that the Singer-type constructions or the counting upper bounds are off by a power of $N$. Either answer would be the first change in the exponent of the error term since 1941.

Formalizing it. The goal is open. All milestones are published theorems. The platform already contains weaker related results in other formalizations (for example the order-of-magnitude bounds $c\sqrt N\le \max|A|\le\sqrt{2N}+1$ for Sidon subsets of an initial segment, and the Erdős–Turán construction); the sharp bounds listed as milestones are not stated there for this $h$. The upper bounds of Balogh–Füredi–Roy and O'Bryant are elementary but delicate optimizations, and the Carter–Hunter–O'Bryant bound relies on a large computation, so formalizing it is a substantial verification task in its own right.

Difficulty

For the upper bound, every known argument counts differences $a-a'$ in short windows and loses at the scale $N^{1/4}$; improvements since 1941 only change the constant in front of $N^{1/4}$. For the lower bound, the constructions (Singer, Bose, Ruzsa) produce Sidon sets of size about $\sqrt p$ in a modulus $p$ of size about $N$, and the loss comes from the gap between $N$ and the nearest admissible modulus; bringing it below $N^\varepsilon$ requires either new constructions or information about primes in very short intervals that is far beyond current knowledge.

Formalization scope

Sidon sets are formalized for sets in an arbitrary additive commutative monoid, with the definition, the decidability instance and $\operatorname{maxSidon}$ transcribed from the formal-conjectures library (definitions IsSidon, Finset.maxSidonSubsetCard, and Erdos30.h in FormalConjectures/ErdosProblems/30.lean), placed in the namespace Erdos30. The value $h(N)$ is a natural number cast to $\mathbb R$; $\sqrt{\cdot}$ is the real square root and $N^{\varepsilon}$, $N^{1/4}$ are real powers of $N\ge 0$. The goal's $O(\cdot)$ is Mathlib's Asymptotics.IsBigO along atTop on $\mathbb N$. The goal is not trivialized by any junk value: $h$ is a genuine finite maximum, and the $O(\cdot)$ statement concerns all large $N$.

Useful infrastructure: basic lemmas on Sidon sets (hereditary under subsets, translation invariance, distinct differences), finite projective geometry or Bose's construction for the lower bounds, and prime gaps (Bertrand's postulate suffices for $h(N)\ge c\sqrt N$ with $c<1$; a prime number theorem in short intervals is needed for $1-o(1)$). Contributions of reusable Sidon-set lemmas are welcome.