Motivation

An edge partition into cliques compresses the adjacency structure of a graph into complete pieces without allowing any edge to be counted twice. Erdős Problem 81 asks for the asymptotically sharp upper bound on the number of pieces needed when the graph is chordal. Chordal graphs have strong elimination structure, but that structure does not make the partition parameter additive under arbitrary edge deletion, and obtaining a linear error term remains substantially stronger than identifying the leading quadratic coefficient.

Erdős, Ordman, and Zalcstein studied clique partitions of chordal graphs in 1993. Their examples already exhibit the $n^2/6$ scale, while their general upper estimate had a larger quadratic coefficient. Later dense-packing results of Haxell–Rödl and Yuster compare fractional and integer triangle packings with an $o(n^2)$ gap. The project candidate combines that interface with chordal elimination arguments to formulate a uniform $n^2/6+o(n^2)$ milestone. It does not supply the $O(n)$ remainder asked for by the root.

Setting

A finite simple graph is chordal when it has no induced cycle of length greater than three. The Lean definition uses the equivalent perfect-elimination form: vertices admit an injective ranking such that the later neighbors of every vertex form a clique.

An edge partition into cliques is a finite family $\mathcal P$ of complete vertex sets such that every edge of $G$ belongs to exactly one member of $\mathcal P$. Members may share vertices but may not share edges. Write $\operatorname{cp}(G)$ for the minimum possible number of pieces.

The asymptotic notation

$$\frac{n^2}{6}+O(n)$$

means that there are constants $C>0$ and $n_0\ge1$, chosen independently of $G$ and $n$, such that every chordal $n$-vertex graph with $n\ge n_0$ has a clique partition with at most $n^2/6+Cn$ pieces.

Formalization targets

Erdős Problem 81

The root theorem is

$$\exists C>0\ \exists n_0\ge1\ \forall n\ge n_0\ \forall G\text{ chordal on }n\text{ vertices}, \qquad \operatorname{cp}(G)\le \frac{n^2}{6}+Cn.$$

The quantifier order is essential: $C$ and $n_0$ are universal and cannot depend on the graph.

Leading-coefficient milestone

The supporting target records the weaker uniform statement

$$\forall\varepsilon>0\ \exists n_0\ \forall n\ge n_0\ \forall G\text{ chordal on }n\text{ vertices}, \qquad \operatorname{cp}(G)\le \left(\frac16+\varepsilon\right)n^2.$$

This is the precise $n^2/6+o(n^2)$ form. It is not equivalent to the root: choosing $\varepsilon=1/n$ is invalid because the cutoff may depend on the fixed value of $\varepsilon$.

Significance

The root would determine the clique-partition extremum for chordal graphs up to a linear remainder, matching the scale of the complete-split examples that motivate the coefficient $1/6$. It would refine a leading-order asymptotic theorem into a uniform estimate strong enough to distinguish second-order behavior.

Formalization creates a clean interface among perfect elimination orderings, exact edge partitions, fractional edge-and-triangle decompositions, and integer triangle packings. It also forces the proof to distinguish a partition from a cover and original graph order from the order of any auxiliary hypergraph. These definitions can support other decomposition problems on chordal and split graphs.

Difficulty

Perfect elimination does not by itself give the sharp partition count. Greedily taking maximal cliques may overlap in edges or accumulate too many singleton pieces. Similarly, a fractional edge-and-triangle partition can achieve the right leading coefficient while integer rounding loses $o(n^2)$ pieces; the root requires that loss to be only $O(n)$.

The dense-packing theorem has quantifiers of the form “for every fixed $\varepsilon>0$ there exists $N(\varepsilon)$.” It therefore yields a uniform subquadratic error but no linear error. Any proof of the root must add a chordal-specific rounding or extremal reduction rather than treating the general packing theorem as if its $\varepsilon$ could vary with $n$.

Formalization scope

Graphs are finite and simple. Chordality is encoded by existence of a perfect-elimination ranking, including disconnected and edgeless graphs. A clique piece is a finite vertex set that spans a complete subgraph. Exactness means every actual edge occurs in exactly one piece; no nonedge can occur inside a piece. Bounds are compared in $\mathbb R$ so the displayed asymptotic expressions retain their conventional form, while the number of parts remains a natural number.

The candidate derivation of the leading coefficient imports finite linear-programming duality and the Haxell–Rödl/Yuster fixed-triangle packing approximation. It is candidate_only, not an admitted result or kernel proof. Contributions may formalize the perfect-elimination lemmas, the fractional compression, the uniform packing interface, complete-split lower examples, or the root linear rounding theorem. A result for edge-and-triangle pieces only, a fractional partition, or one fixed order must not be presented as the unrestricted integer clique-partition theorem.

Selected references

• P. Erdős, E. T. Ordman, and Y. Zalcstein, Clique Partitions of Chordal Graphs, Combinatorics, Probability and Computing 2(4), 1993. https://doi.org/10.1017/S0963548300000808
• P. E. Haxell and V. Rödl, Integer and Fractional Packings in Dense Graphs, Combinatorica 21, 2001. https://doi.org/10.1007/s004930170003
• R. Yuster, Integer and fractional packing of families of graphs, 2003. https://arxiv.org/abs/math/0305350
• Erdős Problems, Problem 81. https://www.erdosproblems.com/81

Egyptian fractions and the Erdős–Straus question

A unit fraction is the reciprocal of a positive integer. The Erdős–Straus conjecture asks whether the particularly simple rational number $4/n$ always admits an expansion with three such terms. Its difficulty lies in obtaining a fixed number of terms for every denominator: general algorithms for Egyptian fractions do not give this three-term guarantee.

The conjecture is open. This mission adopts the exact statement maintained as Erdős Problem 242. It aims to formalize established reductions and provide a precise frontier for further work; it does not present a proof of the universal conjecture.

The historical formulations vary. Erdős’s 1950 paper, pp. 193–195, discusses distinct unit fractions and attributes the conjecture jointly to himself and Straus. His 1961 problem I.32, p. 238, allows positive denominators without specifying distinctness, while the 1979 statement, problem 9, p. 70, explicitly orders distinct denominators. The earliest published discussion may be Obláth’s 1950 paper, submitted in 1948; it attributes the question to Erdős, as explained by Bloom–Elsholtz, pp. 238–239.

The main developments relevant here are:

• 1950: Obláth’s sufficient condition using a prime divisor of $n+1$ congruent to $3$ modulo $4$.
• 1965–1969: Yamamoto’s congruence analysis and Mordell’s exposition reduce the remaining prime cases to six classes modulo $840$.
• 1970–1971: Vaughan bounds the density of possible exceptions; Terzi develops a stronger congruence sieve modulo $120120$.
• 2013–2022: Elsholtz–Tao analyze representation counts and soluble polynomial congruences; Bloom–Elsholtz give an explicit equivalent covering formulation.
• 2025: Computational verification is reported through $10^{18}$. Pomerance–Weingartner study the more general Erdős–Straus–Schinzel problem, including quantitative dependence on a variable numerator.

The exact property

For a natural number $n$, write $\mathrm{IsErdosStraus}(n)$ for the following literal property:

$$\exists x,y,z\in\mathbb N,\qquad 1\le x<y<z,\qquad \frac4n=\frac1x+\frac1y+\frac1z.$$

Every fraction is evaluated in $\mathbb Q$. The predicate contains only these witnesses, inequalities, and equality. The required range of the conjecture is $n>2$; distinctness is part of the mathematical target. In particular, the prime $2$ cannot simply be imported from a formulation permitting repeated denominators. The boundary value $n=3$ is included, with denominators $1,4,12$.

Formalization targets

The unresolved root goal is

$$\forall n\in\mathbb N,\quad n>2\Longrightarrow\mathrm{IsErdosStraus}(n).$$

The supporting milestones concern established mathematics. Denominator clearing relates the rational equation to $4xyz=n(yz+xz+xy)$ under strict positivity. Positive scaling transports a solution for $n$ to one for $kn$ while preserving the strict order. An explicit even-number family supplies the case needed for the prime reduction.

The elementary families cover $3\mid n$, $n\equiv2\pmod3$, $n\equiv3\pmod4$, and $n\equiv5\pmod8$, with the displayed witnesses and their integrality and strict ordering recorded in separate statements. Together with the even case, they solve every $n>2$ outside $1\pmod{24}$. The useful reduction is an equivalence between the root goal and its restriction to primes $p\equiv1\pmod{24}$; the ordinary prime reduction is also stated separately. The classical scaling and residue observations are discussed in Bloom–Elsholtz, p. 239.

Obláth’s milestone says that $\mathrm{IsErdosStraus}(n)$ holds for $n>2$ whenever $n+1$ has a prime divisor $q\equiv3\pmod4$. This condition is explicitly recorded in the introduction of Pomerance–Weingartner, which identifies the original Obláth reference. The exact distinctness requirement is retained in this mission.

The Mordell–Yamamoto milestone asks for a decomposition for every prime $p>2$ satisfying

$$p\bmod840\notin\{1,121,169,289,361,529\}.$$

The actual existence claim is the theorem to prove. It has no hypothesis asserting that these classes are covered. Yamamoto’s original paper, §§3–4, pp. 42–46, supplies the congruence framework and prints this residual list. The same list appears in the current Erdős Problems record. The list printed on p. 239 of Bloom–Elsholtz instead contains $49$ and omits $529$; that discrepant list is not used here. The historical papers often permit repeated denominators, so producing distinct ordered witnesses is an explicit part of the formalization obligation.

What these results provide

The elementary infrastructure gives reusable certificates and transports for exact rational decompositions. The reductions identify a mathematically meaningful remaining domain without assuming the conjecture. Completion of the modulo-$840$ milestone would leave the prime cases in its six residual classes as the classical research frontier; those classes are not asserted to consist of counterexamples.

Later targets include Terzi’s 1971 sieve, whose publisher abstract reports 198 residual classes modulo $120120$, and Vaughan’s density theorem, bounding the exceptional count by $X\exp(-c(\log X)^{2/3})$ for a positive constant $c$. Neither is a core Lean statement in this draft. No unaudited list of 198 classes is supplied.

Elsholtz–Tao provide counting results and a classification of polynomially soluble congruences. Bloom–Elsholtz, Theorem 1, pp. 239–240, characterize their conjecture by coverage of all primes by classes

$$-a/c\pmod{4acd-1}\quad(a,c,d\ge1),$$

or

$$-(4c^2d+1)/k\pmod{4cd}\quad(c,d,k\ge1,\ k\mid4c^2d+1).$$

Here division by $c$ denotes a modular inverse; division by $k$ is exact integer division. The authors are Bloom and Elsholtz, not Bradford and Elsholtz. This is a later formalization target: an initial core theorem is not included until the translation between that paper’s denominator convention and the present strict convention is separately formalized. Pomerance–Weingartner address growing numerators in the generalized problem; their exceptions are not counterexamples to the fixed numerator $4$ conjecture.

The remaining difficulty

Congruence identities prove infinite families only when the identities and their arithmetic hypotheses are established for arbitrary parameters. Checking finitely many representatives with a search program does not prove that all future values in an arithmetic progression work. Density estimates also allow an exceptional set and therefore do not settle the universal statement.

The current record cites Mihnea–Bogdan (2025) for computational verification through $10^{18}$. This is reported computational evidence, not a Lean-certified theorem in this mission. No universal conclusion or periodicity assertion is inferred from it.

Formalization scope

The development uses natural-number denominators, exact rational arithmetic, integer polynomial identities, divisibility, primality, and natural-number remainders. Definitions are transparent. The root is not hidden in a typeclass, structure field, certificate, or extra assumption, and its quantifier is not bounded. The existing Google DeepMind transcription is a statement reference, not an imported proof.

The draft targets Mathlib 0df444a360eaa60ab8c11dca51a86af692955474 with Lean 4.33.1. Every proposed statement has been locally elaborated and supplied with an independent read-back. Statement elaboration with sorry is not proof verification. The accompanying local proof audit distinguishes the proved supporting results from the open root and the remaining modulo-$840$ formalization task.

Selected references

• Erdős, Az … egyenlet egész számú megoldásairól, Mat. Lapok 1 (1950), 192–210; original scan.
• Erdős–Graham, Old and New Problems and Results in Combinatorial Number Theory (1980), chapter IV; author’s institutional scan.
• Obláth, Sur l’équation diophantienne $4/n=1/x_1+1/x_2+1/x_3$, Mathesis 59 (1950), 308–316; bibliographic record, also cited in Pomerance–Weingartner.
• Yamamoto, On the Diophantine Equation $4/n=1/x+1/y+1/z$, Mem. Fac. Sci. Kyushu Univ. A 19 (1965), 37–47; original paper.
• Mordell, Diophantine Equations, Academic Press (1969), chapter 30, pp. 287–290; publisher record.
• Terzi (1971), Vaughan (1970), Elsholtz–Tao (2013), Bloom–Elsholtz (2022), Mihnea–Bogdan (2025), and Pomerance–Weingartner (2025/2026): primary sources linked at their statements above.

Motivation

A unit fraction is the reciprocal $1/n$ of a positive integer. The number $1$ can be written as a sum of distinct unit fractions in infinitely many ways — $1 = \tfrac12+\tfrac13+\tfrac16$, $1 = \tfrac12+\tfrac14+\tfrac16+\tfrac1{12}$, and so on — and the combinatorics of such representations is one of the oldest recurring themes in Erdős's problem lists. Most questions in the area concern size: how many terms are needed, how small the largest denominator can be, how large the smallest one must be. Erdős Problem 287 asks instead about the shape of a representation: how tightly can the denominators be packed?

Order the denominators increasingly and look at their consecutive differences. For $1 = \tfrac12+\tfrac13+\tfrac16$ the differences are $1$ and $3$. The question is whether a difference of at least $3$ must always occur, in every representation of $1$, no matter how many terms it has. The problem is recorded in Erdős and Graham's 1980 problem book (ErGr80, p. 33) and was selected for the booklet of favourite problems prepared for the 1999 Budapest conference on Erdős's mathematics ([Va99, 1.15]). It remains open.

Timeline. The weaker statement that some difference must be at least $2$ — equivalently, that $1$ is never the sum of the reciprocals of a block of consecutive integers — is classical. Theisinger (1915) proved that the harmonic number $H_n$ is not an integer for $n \ge 2$, using Bertrand's postulate. Kürschák (1918) introduced the $2$-adic argument that proves the general block statement: for $m \le n-2$, the difference $H_n - H_m$ is not an integer. Erdős's 1932 paper [Er32], whose title translates as "A generalisation of an elementary number-theoretic theorem of Kürschák", extends the result from blocks of consecutive integers to arithmetic progressions; the erdosproblems.com entry for Problem 287 cites it for the difference-$\ge 2$ bound. Nothing stronger appears to be known: the passage from $2$ to $3$ is the open part, and no partial result is recorded in the entry beyond a conditional one, namely that the conjecture would follow for all but finitely many exceptions if it were known that for every large $N$ there is a prime $p \in [N, 2N]$ with $(p+1)/2$ also prime.

Setting

Fix an integer $k \ge 2$ and integers

$$1 < n_1 < n_2 < \cdots < n_k$$

with

$$1 \;=\; \frac{1}{n_1} + \frac{1}{n_2} + \cdots + \frac{1}{n_k},$$

the sum taken in $\mathbb{Q}$. Call such a tuple a representation of length $k$. The denominators are strictly increasing, hence distinct, and all exceed $1$: the value $n_1 = 1$ is excluded because $1/1$ already exhausts the total. The gaps of the representation are the $k-1$ consecutive differences $n_{i+1} - n_i$ for $1 \le i \le k-1$, and its maximal gap is $\max_i (n_{i+1} - n_i)$.

Representations exist for every $k \ge 3$, and for $k = 1$ only the excluded $n_1 = 1$; no representation of length $2$ exists. Examples: $(2,3,6)$ with gaps $1, 3$; $(2,4,6,12)$ with gaps $2,2,6$; $(3,4,6,10,12,15)$ with gaps $1,2,4,2,3$.

Formalization targets

Goal — Erdős Problem 287

$$\text{every representation } 1 < n_1 < \cdots < n_k \ (k \ge 2) \text{ of } 1 \text{ satisfies } \max_{1 \le i < k} (n_{i+1} - n_i) \;\ge\; 3.$$

This is the open conjecture, stated with no bound on $k$ and no restriction on the denominators beyond those in Setting. It is the weakest form that captures the question: asserting a bound for one particular $k$, or for denominators in some range, would be a different and strictly easier statement.

Milestone — the gap-two bound (Kürschák; Erdős [Er32])

$$\text{every representation satisfies } \max_{1 \le i < k}(n_{i+1} - n_i) \;\ge\; 2.$$

Equivalently: no block of two or more consecutive integers has reciprocals summing to $1$. This is closed mathematics and the natural first target.

Milestone — the classical block theorem (Kürschák)

$$\text{for } n \ge 1 \text{ and } k \ge 2, \qquad \sum_{i=0}^{k-1} \frac{1}{n+i} \notin \mathbb{Z}.$$

The gap-two bound is an immediate consequence, since a representation all of whose gaps equal $1$ is exactly a block of consecutive integers.

Milestone — sharpness

$$1 = \tfrac12+\tfrac13+\tfrac16 \text{ is a representation all of whose gaps are at most } 3.$$

So the constant $3$ in the goal is optimal and cannot be replaced by $4$.

Significance

The result itself. A positive answer would say that a representation of $1$ by unit fractions can never have all its denominators within distance $2$ of each other — a structural constraint of a kind that the size-based results in this area do not provide. The conditional route recorded on the problem page is instructive about where the difficulty sits: it reduces the conjecture, up to finitely many exceptions, to the existence of primes $p$ in $[N,2N]$ with $(p+1)/2$ prime, a statement of Bertrand-with-extra-structure type that is itself out of reach of current technology. A direct proof would therefore either bypass that route or resolve the conjecture for the remaining cases by different means.

Formalizing it. The gap-two bound and the block theorem behind it are closed mathematics, so the honest description of that part of this mission is formalization, not research. It is nevertheless not already available: Mathlib proves Theisinger's case harmonic_not_int, that $H_n \notin \mathbb{Z}$ for $n \ge 2$, but not Kürschák's block version $H_n - H_m \notin \mathbb{Z}$, which is the form Problem 287 needs. Supplying it is a genuine strengthening of the library's existing development and is reusable for any question about reciprocal sums over intervals. The goal itself is open, and this mission does not claim otherwise: it is registered with an open proof, and the milestones are what a solver can realistically close today.

Difficulty

The obvious first idea — bound the number of terms, then check finitely many cases — fails immediately, because $k$ is unbounded: representations of $1$ exist with arbitrarily many terms, so no finite computation can settle the conjecture. The second idea, extending the $2$-adic argument that gives the gap-two bound, also fails, and instructively. That argument works because a block of consecutive integers contains exactly one element of maximal $2$-adic valuation, which leaves the total with negative valuation. Once gaps of size $2$ are permitted the denominators may be chosen to avoid that configuration — for instance all even, as in $(2,4,6,12)$ — and the valuation obstruction disappears. There is no evident replacement prime or weighting that rules out all gap-$\le 2$ configurations simultaneously, and the conditional result quoted above suggests why: the known routes pass through the distribution of primes in short intervals with a multiplicative side condition, rather than through a congruence obstruction.

Formalization scope

A representation is encoded as a function $f : \mathbb{N} \to \mathbb{N}$ together with the hypotheses ∀ i < k, 1 < f i and ∀ i j, i < j → j < k → f i < f j, and the requirement ∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1. Only the values of $f$ below $k$ are constrained; the function is not required to be monotone or bounded elsewhere, and nothing outside the window is used. The conclusion is ∃ i, i + 1 < k ∧ 3 ≤ f (i + 1) - f i, the existential form of "the maximal gap is at least $3$"; the subtraction is natural-number subtraction, which is harmless because $f$ is increasing on the window, so no truncation can occur. The sum is a rational equality, not an approximation.

The statement admits no trivializing reading. The hypothesis 1 < f i is essential and is not vacuous — dropping it would admit $f\,0 = 1$, $k = 1$; the strict monotonicity is what makes the gaps well defined and the denominators distinct; and k ≥ 2 guarantees that at least one gap exists, so the conclusion is not an empty existential. Asserting exactly $3$ rather than at least $3$ would be false, as $(2,4,6,12)$ has a gap of $6$.

Infrastructure: the block theorem is proved from Mathlib's padicNorm and padicValNat API — padicNorm.add_eq_max_of_ne, padicNorm.sum_lt', padicNorm.not_int_of_not_padic_int, pow_padicValNat_dvd and pow_succ_padicValNat_not_dvd — and needs no new definitions. That development is reusable beyond this mission and is a candidate for upstreaming to Mathlib alongside harmonic_not_int. Contributions are welcome on any milestone independently; a formalization of the conditional reduction to primes $p$ with $(p+1)/2$ prime would also be a valuable addition, and is not included as a milestone here only because the problem page states it too briefly to formalize faithfully without consulting a primary source.

Selected references

• P. Erdős, Egy Kürschák-féle elemi számelméleti tétel általánosítása (A generalisation of an elementary number-theoretic theorem of Kürschák), Mat. és Phys. Lapok 39 (1932), 17–24.
• P. Erdős and R. L. Graham, Old and new problems and results in combinatorial number theory, Monographies de L'Enseignement Mathématique, Geneva, 1980, p. 33. scan
• Various, Some of Paul's favorite problems, booklet for the conference "Paul Erdős and his mathematics", Budapest, July 1999, item 1.15.
• K. Conrad, The $p$-adic growth of harmonic sums, expository notes (Theorem 2 is Kürschák's block theorem, with the $2$-adic proof). pdf
• T. F. Bloom, Erdős Problem #287, erdosproblems.com/287.

Motivation

Erdős asked, repeatedly and with a rising price tag, for an asymptotic formula for the largest subset of $\{1,\dots,N\}$ that contains no arithmetic progression of a given length. He offered 1000 dollars for it in [Er97c] and 10000 dollars in [Er81, p.4], where he called the question "probably enormously difficult"; elsewhere he described it as "probably unattackable at present". Most of modern additive combinatorics — the density increment method, the triangle removal lemma, Gowers uniformity norms, the arithmetic regularity lemma — grew out of attempts on this single question, and the answer is still unknown, even in the first non-trivial case $k=3$.

Timeline.

• 1936: Erdős and Turán conjecture that $r_k(N)=o(N)$ for every $k$.
• 1946: Behrend constructs large progression-free sets, giving $r_3(N)\ge N\exp(-c\sqrt{\log N})$.
• 1953: Roth proves $r_3(N)=o(N)$, with the quantitative form $r_3(N)\ll N/\log\log N$.
• 1961: Rankin generalises Behrend, giving $r_k(N)\ge N\exp(-c_k(\log N)^{1/(k-1)})$.
• 1969, 1975: Szemerédi proves $r_4(N)=o(N)$ and then $r_k(N)=o(N)$ for all $k$, settling Erdős–Turán.
• 1977: Furstenberg reproves Szemerédi's theorem ergodically, with no effective bound.
• 1998, 2001: Gowers introduces uniformity norms and obtains $r_k(N)\ll N(\log\log N)^{-c_k}$, the first effective bound for general $k$.
• 2017: Green and Tao obtain $r_4(N)\ll N(\log N)^{-c}$.
• 2020: Bloom and Sisask obtain $r_3(N)\ll N(\log N)^{-1-c}$, the first bound past the $N/\log N$ barrier.
• 2023: Kelley and Meka obtain $r_3(N)\le N\exp(-c(\log N)^{1/12})$.
• 2024: Leng, Sah and Sawhney obtain $r_k(N)\ll N\exp(-(\log\log N)^{c_k})$ for $k\ge5$.

Every upper bound in this list is still astronomically far from Behrend's lower bound, and no candidate asymptotic formula has been proposed for any $k\ge3$.

Setting

Fix an integer $k$. A non-trivial $k$-term arithmetic progression is a list $a,\,a+d,\,a+2d,\dots,a+(k-1)d$ of natural numbers with common difference $d>0$; the requirement $d>0$ is what "non-trivial" means, and it forces the $k$ terms to be distinct. A finite set $A\subseteq\mathbb N$ is $k$-AP-free if it contains no such progression. Write

$$r_k(N)\;=\;\max\bigl\{\,|A| \;:\; A\subseteq\{1,\dots,N\},\ A\ \text{is}\ k\text{-AP-free}\,\bigr\}.$$

The mission takes its formal definition of $r_k$ verbatim from the formal-conjectures entry for this problem, so that the goal below is literally the statement recorded there. In that development a set is called free of progressions of length $l$ when every subset of it that is an arithmetic progression of length $l$ forces $l\le1$. Progressions of length $0$ and $1$ count as trivial, so under that convention every set is free of them and $r_0(N)=r_1(N)=N$; the interesting range begins at $k\ge2$. Every statement in this mission that depends on the convention carries an explicit hypothesis on $k$.

On that range, $r_k(N)$ is non-decreasing in both $N$ and $k$, satisfies $r_k(M+N)\le r_k(M)+r_k(N)$, and hence, by Fekete's subadditivity lemma, $r_k(N)/N$ converges. Szemerédi's theorem is the statement that the limit is $0$; the whole difficulty of this mission lies in how fast it goes to $0$.

Formalization targets

Goal

$$r_k(N)\;=\;o_k\!\left(\frac{N}{\log N}\right)\qquad\text{for every }k>1 .$$

This is erdos_142.variants.lower of the formal-conjectures file for Erdős 142, reproduced binder for binder, over that file's own definition of $r_k$.

The headline theorem in that file, erdos_142, states $r_k(N)=\Theta(f)$ with the comparison function left as an answer(sorry) placeholder, and the same is true of its variants.upper and variants.three. Those are not closed propositions and cannot serve as a mission goal: the literal request of Erdős Problem #142 — "prove an asymptotic formula for $r_k(N)$" — has no known right-hand side for any $k\ge3$, which is exactly why the file leaves a hole there. variants.lower is the one formalizable target in the file, and it is also the strongest precisely-stated form the problem page attaches to #142: Erdős offered 5000 dollars for (essentially) exactly it, as recorded under Erdős Problem #3. It is known for $k=3$ — it follows from Bloom–Sisask 2020, and a fortiori from Kelley–Meka 2023 — trivial for $k=2$, where $r_2(N)=1$, and open for every $k\ge4$. It fixes no constants, so no future improvement can invalidate it.

A weaker open question

$$\frac{r_k(n)}{r_{k+1}(n)}\longrightarrow 0\qquad\text{for some }k\ge3 .$$

Erdős remarked in [Er80, p.92] that even this separation between consecutive progression lengths is not known. Here [Er80] is the erdosproblems.com bibliography key for Erdős's 1980 paper; it is a citation, not a pointer to Erdős Problem #80, which is an unrelated question about books in graphs. This statement has no counterpart in formal-conjectures: the file for #142 contains only the $\Theta$, $o$ and $O$ variants above, and the only two files in that repository that mention $r_k$ at all are the ones for #142 and #139.

Significance

Proving $r_k(N)=o_k(N/\log N)$ for all $k$ yields, by a standard summation argument, Erdős's conjecture that every $A\subseteq\mathbb N$ with $\sum_{a\in A}1/a=\infty$ contains arbitrarily long arithmetic progressions — the 5000-dollar Erdős Problem #3, of which the Green–Tao theorem on primes is the best-known special case. Below that threshold, quantitative bounds on $r_k$ control the density at which progressions must appear in any concrete set, and are the input to results on progressions in the primes, in sumsets, and in sparse random subsets of the integers.

Formalization status is uneven, and this mission is designed around that gap. Mathlib already contains the $k=3$ theory in a usable form: the predicate ThreeAPFree, the Roth number rothNumberNat, its subadditivity, and a complete formalization of Behrend's construction (Behrend.roth_lower_bound). Mathlib does not contain Roth's theorem, Szemerédi's theorem, or any of the modern upper bounds; to the best of current knowledge none of Roth, Szemerédi, Gowers, Green–Tao, Kelley–Meka or Leng–Sah–Sawhney has a machine-checked proof anywhere. The formal-conjectures entry states the problem but proves nothing: every declaration in it is a sorry. Two of this mission's targets are taken from that repository — the goal from its file for #142, and the Szemerédi milestone from its file for #139, which uses the same $r_k$; those are the only two files there that mention $r_k$. The milestones therefore split cleanly: the first six are reachable now on top of Mathlib, and the last five are open formalization projects of independent value.

Difficulty

Every known upper bound for $r_k$ runs a density increment: if $A\subseteq\{1,\dots,N\}$ of density $\delta$ has no $k$-term progression, find a long subprogression on which $A$ has density $\delta(1+c(\delta))$, and iterate. The bound this produces is governed entirely by two quantities — how large the increment $c(\delta)$ is, and how much of the interval survives one step. For $k\ge4$ the increment is extracted from an inverse theorem for the Gowers $U^{k-1}$-norm, and the best available correlation bounds there are quasipolynomial in $\delta$; iterating a quasipolynomial increment cannot do better than $N\exp(-(\log\log N)^{c})$, which is nowhere near $N/\log N$. Reaching $N/\log N$ requires an increment with polynomial dependence on $\delta$ together with a subprogression of polynomial length, and that combination is currently available only for $k=3$, through the sifting and almost-periodicity machinery of Kelley–Meka. No soft or averaging argument can substitute: Behrend's construction shows the truth at $k=3$ is $N\exp(-\Theta(\sqrt{\log N}))$, so the answer is not a power of $\log N$ and cannot be produced by any argument whose output has that shape.

Formalization scope

The mission's definition file Erdos142Basic carries two layers, and every statement in the mission is written against them.

1. The source definitions, ported verbatim. IsAPOfLengthWith, IsAPOfLength, IsAPOfLengthFree and r are the declarations of the formal-conjectures entry, transcribed unchanged into the mission's namespace: a set is an arithmetic progression of length $l$ with first term $a$ and difference $d$ when it has exactly $l$ elements and equals $\{a+nd : n<l\}$; it is free of length-$l$ progressions when every progression of length $l$ inside it forces $l\le1$; and $r_k(N)$ is the supremum of $|S|$ over subsets $S\subseteq\{1,\dots,N\}$ free of length-$k$ progressions. The ground set is Finset.Icc 1 N, and the supremum is sSup over $\mathbb N$; the file proves the two facts that make it a genuine maximum (le_r and r_le).

2. An elementary handle. HasAP k A is ∃ a d, 0 < d ∧ ∀ i < k, a + i * d ∈ A, and APFree k A its negation. This form carries no cardinality side condition in $\mathbb N\cup\{\infty\}$ and is what a solver actually wants to induct on. The first milestone is exactly the bridge between the two layers.

Two consequences of the source convention are worth stating plainly, because the prose is silent about them. Length-$0$ and length-$1$ progressions are trivial, so every set is free of them and $r_0(N)=r_1(N)=N$; monotonicity of $r_k$ in $k$ therefore holds only from $k\ge2$ onward, and the corresponding milestone carries that hypothesis. Asymptotic statements use Asymptotics.IsLittleO and Filter.atTop over $\mathbb N$ with real-valued casts, and real division is Lean's, so (N : ℝ) / Real.log N is $0$ at $N=1$; this is invisible to atTop.

A trivializing formalization is ruled out by construction: one milestone asserts $r_3(N)=$ rothNumberNat N, pinning this development against Mathlib's independently written definition of the Roth number, so a vacuous or mis-quantified notion of progression-freeness cannot survive. That milestone, the bridge milestone above it, and the monotonicity milestone have all been checked to be provable before this proposal was drafted.

A full development needs: discrete Fourier analysis on $\mathbb Z/N\mathbb Z$, Bohr sets and their regularity, the arithmetic regularity lemma, Gowers uniformity norms and the inverse theorem for them, and — for the lower bounds — sphere-counting in high-dimensional boxes (already in Mathlib via Behrend). All of this is reusable well beyond this mission. Contributions of any kind are welcome, including partial results: quantitative bounds weaker than the cited ones, the $k=3$ case of a general-$k$ milestone, and reusable Fourier-analytic infrastructure are all valuable even when they do not close a milestone.

Selected references

• Erdős Problem #142. https://www.erdosproblems.com/142
• Erdős Problem #3. https://www.erdosproblems.com/3
• Erdős Problem #139 (Szemerédi's theorem in the $r_k$ formulation), linked from #142. https://www.erdosproblems.com/139
• Google DeepMind, formal-conjectures, FormalConjectures/ErdosProblems/142.lean — the source of the goal statement and of the definition of $r_k$. https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.lean
• F. A. Behrend, On sets of integers which contain no three terms in arithmetical progression, Proc. Nat. Acad. Sci. USA 32 (1946), 331–332. https://doi.org/10.1073/pnas.32.12.331
• K. F. Roth, On certain sets of integers, J. London Math. Soc. 28 (1953), 104–109. https://doi.org/10.1112/jlms/s1-28.1.104
• R. A. Rankin, Sets of integers containing not more than a given number of terms in arithmetical progression, Proc. Roy. Soc. Edinburgh Sect. A 65 (1961), 332–344.
• E. Szemerédi, On sets of integers containing no $k$ elements in arithmetic progression, Acta Arith. 27 (1975), 199–245. https://doi.org/10.4064/aa-27-1-199-245
• W. T. Gowers, A new proof of Szemerédi's theorem, Geom. Funct. Anal. 11 (2001), 465–588. https://doi.org/10.1007/s00039-001-0332-9
• B. Green and T. Tao, New bounds for Szemerédi's theorem, III: A polylogarithmic bound for $r_4(N)$, Mathematika 63 (2017), 944–1040. https://arxiv.org/abs/1705.01703
• T. F. Bloom and O. Sisask, Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions, arXiv:2007.03528. https://arxiv.org/abs/2007.03528
• Z. Kelley and R. Meka, Strong bounds for 3-progressions, arXiv:2302.05537. https://arxiv.org/abs/2302.05537
• J. Leng, A. Sah and M. Sawhney, Improved bounds for Szemerédi's theorem, arXiv:2402.17995. https://arxiv.org/abs/2402.17995

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

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

$$A+A=\{a+b : a,b\in A\},\qquad AA=\{ab : a,b\in A\}.$$

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$,

$$\max(|A+A|,|AA|)\ \ge\ C_\varepsilon\,|A|^{2-\varepsilon}.$$

Known lower bounds (milestones, weakest to strongest)

$$|A+A|\ge 2|A|-1,\qquad \max(|A+A|,|AA|)\gg|A|^{1+\delta},\qquad \gg|A|^{5/4},\qquad \gg\frac{|A|^{4/3}}{(\log|A|)^{1/3}},\qquad \gg_\varepsilon |A|^{4/3+2/1167-\varepsilon}.$$

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

$$S_n(A)=\sum_{a\in A}\frac{1}{n-a}.$$

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

$$S_n(A)\;\le\;\sum_{p<n}\frac1p+C$$

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$,

$$\sum_{n\in A}\frac1n=\infty\ \Longrightarrow\ A\ \text{contains arithmetic progressions of arbitrarily large length}.$$

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)

$$\exists\, c:\mathbb N\to\mathbb N\quad \forall n \ge 1,\ \forall k:\qquad f(n,k) < c_k^{\,n}.$$

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

$$h(N)=\max\{|A| : A\subseteq\{1,\dots,N\},\ A \text{ Sidon}\}.$$

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$,

$$i_1+i_2=j_1+j_2\ \Longrightarrow\ (i_1=j_1\wedge i_2=j_2)\ \vee\ (i_1=j_2\wedge i_2=j_1).$$

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

$$h(N)=\operatorname{maxSidon}(\{1,2,\dots,N\}),\qquad h(0)=0.$$

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)

$$\forall\varepsilon>0:\qquad h(N)-\sqrt N = O\!\left(N^{\varepsilon}\right)\quad(N\to\infty).$$

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.

Selected references

• J. Singer, A theorem in finite projective geometry and some applications to number theory, Trans. Amer. Math. Soc. 43 (1938), 377–385. https://doi.org/10.1090/S0002-9947-1938-1501951-4
• P. Erdős and P. Turán, On a problem of Sidon in additive number theory, and on some related problems, J. London Math. Soc. 16 (1941), 212–215. https://doi.org/10.1112/jlms/s1-16.4.212
• B. Lindström, An inequality for $B_2$-sequences, J. Combin. Theory 6 (1969), 211–212. https://doi.org/10.1016/S0021-9800(69)80124-9
• J. Balogh, Z. Füredi and S. Roy, An upper bound on the size of Sidon sets, Amer. Math. Monthly (2023). https://arxiv.org/abs/2103.15850
• K. O'Bryant, On the size of finite Sidon sets (2022). https://arxiv.org/abs/2207.07800
• D. Carter, Z. Hunter and K. O'Bryant, On the diameter of finite Sidon sets (2023). https://arxiv.org/abs/2310.20032
• K. O'Bryant, A complete annotated bibliography of work related to Sidon sequences, Electron. J. Combin. DS11 (2004). https://arxiv.org/abs/math/0407117
• T. F. Bloom, Erdős Problem #30, https://www.erdosproblems.com/30
• Google DeepMind, formal-conjectures, FormalConjectures/ErdosProblems/30.lean. https://github.com/google-deepmind/formal-conjectures