Combinatorics

Motivation

Plünnecke-type inequalities turn information about a set and one product (or sum) of it into bounds on all of its iterated products. In an abelian group, Plünnecke's theorem (Plünnecke 1970) and its extension by Ruzsa say that $|A + A| \le \alpha|A|$ implies $|hA| \le \alpha^h |A|$ for every $h$. Such bounds are a basic tool in additive combinatorics, and their non-abelian analogues are used in the study of growth in groups (for example Helfgott's work on $\mathrm{SL}_2(\mathbb{Z}/p\mathbb{Z})$).

Without commutativity the abelian statement is false. Petridis recalls the standard example (p. 2): let $H$ be a subgroup and $x$ an element with $|HxH| = |H|^2$, and put $A = H \cup \{x\}$; then $|AA| \le 3|A|$ while $|AAA| \ge (|A|-1)^2$. Small doubling alone therefore says nothing about tripling.

Timeline.

• 1970. Plünnecke proves the abelian inequality by a graph-theoretic method (Plünnecke 1970); Ruzsa later rediscovers and extends it.
• 2006. Ruzsa observes that an extra hypothesis is needed in the non-abelian case: in addition to $|AB| \le \alpha|A|$ one must assume $|AbB| \le \alpha|A|$ for all $b \in B$ (Ruzsa, Cardinality questions about sumsets, CRM Proc. Lecture Notes, 2006).
• 2008. Tao proves the case $A = B$ (Tao 2008): if $|BB| \le \alpha|B|$ and $|BbB| \le \alpha|B|$ for every $b \in B$, then $|B^h| \le \alpha^{ch}|B|$ for an absolute constant $c$ that is not computed (Theorem 1.3 of the present paper).
• 2010. Ruzsa asks for an explicit value of $c$ (Towards a noncommutative Plünnecke-type inequality, in An Irregular Mind, Bolyai Soc. Math. Stud. 21, 2010).
• 2011–2012. Petridis gives explicit exponents, $|B^h| \le \alpha^{8h-17}\beta^{h-2}|B|$, so $c = 9$ suffices (arXiv:1101.3507v3, Theorem 1.6; Combinatorica 32, 2012).

Setting

Let $G$ be a group, not necessarily abelian, and let $B$ be a finite subset of $G$. Write $|X|$ for the number of elements of a finite set $X$. For finite sets $X, Y \subseteq G$ the product set is $XY = \{xy : x \in X,\ y \in Y\}$, and the inverse set is $X^{-1} = \{x^{-1} : x \in X\}$. For $h \ge 1$, $B^h = B \cdots B$ is the product of $h$ copies of $B$. For $b \in G$, $BbB = \{b_1 b\, b_2 : b_1, b_2 \in B\}$.

The two hypotheses of the mission, for real numbers $\alpha$ and $\beta$, are

$$|BB| \le \alpha|B| \qquad\text{and}\qquad |BbB| \le \beta|B| \ \text{ for every } b \in B.$$

The first is small doubling; the second says that every two-sided "translate" $BbB$ is small. In an abelian group $BbB = bBB$ has the same size as $BB$, so the second hypothesis follows from the first with $\beta = \alpha$.

The proof uses an auxiliary set: a nonempty $A \subseteq B$ that grows minimally under right multiplication by $B$, meaning $|AB|/|A| \le |ZB|/|Z|$ for every nonempty $Z \subseteq B$.

Formalization targets

Goal: Theorem 1.6 (p. 4)

For every integer $h > 2$,

$$|B^h| \le \alpha^{8h-17}\,\beta^{h-2}\,|B|.$$

Milestones, in the order the proof uses them

1. Display (6) (p. 9): for $A \subseteq B$ nonempty and minimally growing, $|BAB| \le \alpha^2|B|$.
2. Corollary 4.3 (p. 8): for any finite $A, B$ with $|BB| \le \alpha|B|$ and $|BAB| \le \alpha^2|B|$, $\;|BA^{-1}AB^{-1}| \le \alpha^6|B|$.
3. Display (8) (p. 10): for $T \subseteq B$ with $|T| \le \alpha$, $\;|BTB| \le \alpha\beta|B|$.
4. Theorem 4.4 (p. 9): $|BBB| \le \alpha^7\beta|B|$, the case $h = 3$ of the goal.
5. Display (9) (p. 10): with $A$ as in (6) and $T \subseteq B$, $|T| \le \alpha$, $B \subseteq A^{-1}AT$: $\;|B^h| \le \alpha^6|BTB^{h-2}|$ for $h > 2$.
6. Display (10) (p. 10): $|BTB^{h-2}| \le \alpha\beta|B^{-1}B^{h-2}|$ for $h > 2$.
7. Display (11) (p. 10): $|B^{-1}B^{h-2}| \le \alpha|B^{h-1}|$ for $h > 2$.
8. Inductive step (p. 11): $|B^h| \le \alpha^8\beta|B^{h-1}|$ for $h > 2$.

Significance

The result. Theorem 1.6 is a non-abelian Plünnecke inequality with explicit, linear-in-$h$ exponents. Taking $\beta \le \alpha$ (Tao's setting) gives $|B^h| \le \alpha^{9h}|B|$, so the constant $c$ in Tao's theorem can be taken to be $9$, answering Ruzsa's request for an explicit value. Bounds of this shape are the standard way to pass from control of a few products of a set to control of all of its products.

Formalizing it. The result is proved on paper; this mission produces a machine-checked proof. Mathlib already contains the abelian Plünnecke–Ruzsa inequality, Ruzsa's triangle inequality and covering lemma for arbitrary groups, and the Plünnecke–Petridis inequality (Proposition 2.1 of the paper), but no non-abelian bound on $|B^h|$ under the two hypotheses above. The milestone statements (6)–(11) are each short calculations from these tools and are reusable for other non-abelian product-set estimates.

Difficulty

The obvious argument is to iterate the doubling bound, as in the abelian case. This fails: the example $A = H \cup \{x\}$ shows that $|BB|$ does not control $|BBB|$ in a non-abelian group, so the second hypothesis has to enter, and it controls only products with a single element in the middle. The difficulty is to bring that hypothesis to bear on $B^h$, whose factors are all copies of $B$, while losing only a bounded power of $\alpha$ and $\beta$ per additional factor and keeping the order of the factors fixed throughout: any step that silently commutes two factors is invalid. The exponents $8h-17$ and $h-2$ are exactly what the paper's bookkeeping yields; a looser chain gives a worse but still linear exponent (the paper notes $\alpha^9\beta$ for $|BBB|$ via a different route, p. 10).

Formalization scope

All statements live in the namespace PlunneckeType.Tao and use Mathlib's pointwise Finset operations under open scoped Pointwise, in a group {G : Type*} [Group G] [DecidableEq G], never CommGroup.

• $XY$ is X * Y, $X^{-1}$ is X⁻¹, $B^h$ is B ^ h, and $BbB$ is B * {b} * B, with the single element in the middle. Products keep the order printed in the paper.
• Cardinalities are #X cast to ℝ; $\alpha, \beta$ are real numbers with no sign hypotheses. If $B$ is nonempty the hypotheses force $\alpha, \beta \ge 1$; if $B$ is empty every statement reads $0 \le 0$.
• $h$ is a natural number with 2 < h. Under this hypothesis the natural-number exponents 8 * h - 17 and h - 2, and the powers B ^ (h - 1), B ^ (h - 2), are exact. The goal does not claim $h = 2$, where the printed exponent would be negative.
• The minimal-growth condition is written cross-multiplied, $|AB|\,|Z| \le |ZB|\,|A|$ for every nonempty $Z \subseteq B$, with $A$ nonempty: the ratio $|ZB|/|Z|$ is defined only for nonempty sets, and with $A = \emptyset$ the condition would hold vacuously.
• Theorem 1.6 is stated for a non-commutative Group. A version for commutative groups, or one that adds a hypothesis implying commutativity of the relevant products, is a different and weaker theorem and does not count.

Recorded deviations from the printed text: Theorem 1.6 reads "Let $B$ be finite a set" (word order; kept verbatim in the milestone text); the strategy paragraph on p. 9 says "cover the middle copy of $B$ by $A^{-1}AX$", where the set is $A^{-1}AT$; display (11)'s lead-in writes "$Y = B-1$" for $Y = B^{-1}$. The Lean statements use the intended mathematics.

Tools solvers will find in Mathlib (Mathlib/Combinatorics/Additive/): Finset.pluennecke_petridis_inequality_mul (Proposition 2.1), Finset.ruzsa_triangle_inequality_mul_mulInv_mul and its variants (Lemma 4.2, up to Finset.card_inv), Finset.ruzsa_covering_mul (Lemma 4.1, after inverting), Finset.card_singleton_mul, Finset.card_mul_singleton. Lemmas 4.1 and 4.2 are cited results of Ruzsa and are not items of this mission. Proofs of any milestone, and any reusable lemmas on non-abelian product sets, are welcome.

Selected references

• G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups, arXiv:1101.3507v3, 2011; Combinatorica 32 (2012). https://arxiv.org/abs/1101.3507 · https://doi.org/10.1007/s00493-012-2818-5
• T. Tao, Product set estimates for non-commutative groups, Combinatorica 28 (2008) 547–594. https://arxiv.org/abs/math/0601431
• H. Plünnecke, Eine zahlentheoretische Anwendung der Graphtheorie, J. Reine Angew. Math. 243 (1970) 171–183. https://doi.org/10.1515/crll.1970.243.171
• I. Z. Ruzsa, Towards a noncommutative Plünnecke-type inequality, in I. Bárány and J. Solymosi (eds.), An Irregular Mind: Szemerédi is 70, Bolyai Soc. Math. Stud. 21, Springer, 2010 (reference [14] of Petridis).
• I. Z. Ruzsa, Cardinality questions about sumsets, in A. Granville, M. B. Nathanson and J. Solymosi (eds.), Additive Combinatorics, CRM Proceedings & Lecture Notes, AMS, 2006 (reference [12] of Petridis).

Motivation

Plünnecke–Ruzsa inequalities bound the size of iterated sumsets: if $A$ and $B$ are finite subsets of an abelian group with $|A+B| \le \alpha|A|$, then $|hB| \le \alpha^h|A|$ for every $h$, where $hB = B + \dots + B$. They are a basic tool of additive combinatorics, used in Freiman-type structure theorems, sum–product estimates and the study of approximate groups. Plünnecke's original proof went through a graph-theoretic argument; Ruzsa simplified and extended it.

G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups (arXiv:1101.3507v3, 2011; Combinatorica 32, 2012, doi:10.1007/s00493-012-2818-5), gave a short, purely combinatorial proof. Its core (Proposition 2.1, p. 5) is that a subset $X \subseteq A$ minimising $|XB|/|X|$ satisfies $|CXB| \le \alpha|CX|$ for every finite $C$, in any group.

In a non-abelian group the hypothesis $|AB| \le \alpha|A|$ alone does not control $|AB^h|$ or $|B^h|$. Tao (Product set estimates for non-commutative groups, Combinatorica 28, 2008) showed that an extra condition on triple products restores polynomial bounds, without explicit exponents. Petridis' §4 makes Tao's bound explicit for a single set; this mission is §5 of the paper, which treats two sets $A$ and $B$ of comparable size.

Timeline:

• 1970: Plünnecke, graph-theoretic inequalities for sumsets in abelian groups.
• 1989: Ruzsa, simplified proof and the inequality $|mB - nB| \le \alpha^{m+n}|A|$.
• 2008: Tao, Plünnecke-type estimates in non-commutative groups under a triple-product hypothesis.
• 2011: Petridis, the minimal-growth argument; explicit non-abelian bounds (Theorems 1.6 and 1.7).

Setting

Let $G$ be a group, written multiplicatively and not necessarily commutative. For finite subsets $X, Y \subseteq G$ write

$$XY = \{xy : x \in X,\ y \in Y\}, \qquad X^{-1} = \{x^{-1} : x \in X\},$$

$|X|$ for the number of elements, $B^h = B \cdots B$ ($h$ factors), and $AbB = A\{b\}B$ for $b \in G$. The order of factors matters: $SB^h$ multiplies $S$ on the left of $B^h$.

The three hypotheses of the mission are, for finite $A, B \subseteq G$ and real numbers $\alpha, \beta, \gamma$:

1. $|AB| \le \alpha|A|$ (small product set);
2. $|AbB| \le \beta|A|$ for every $b \in B$ (small triple products);
3. $|A| \le \gamma|B|$ (comparable sizes).

A minimal-growth subset of $A$ (with respect to $B$) is a nonempty $S \subseteq A$ with $|SB|/|S| \le |ZB|/|Z|$ for every nonempty $Z \subseteq A$. In Lean this is written cross-multiplied: $|SB|\,|Z| \le |ZB|\,|S|$.

Formalization targets

Goal: Theorem 1.7 (p. 4)

If $A$ is nonempty and (1)–(3) hold, there is a nonempty $S \subseteq A$ such that for every integer $h > 1$

$$|SB^{h}| \le \alpha^{8h-9}\beta^{h-1}\gamma^{4h-5}\,|S|.$$

The same $S$ serves every $h$.

Milestones (in the order the proof uses them)

• (12) (p. 12): for a minimal-growth $S$ under (1), $|CSB| \le \alpha|CS|$ for every finite $C$.
• Corollary 5.1 (p. 11): if $B \ne \emptyset$ and $|CSB| \le \alpha|CS|$ for every finite $C$, then

$$|SS^{-1}SS^{-1}| \le \alpha^{6}\left(\frac{|S|}{|B|}\right)^{3}|S|.$$

• (14) (p. 12): under (2), for $S \subseteq A$, $T \subseteq B$, $|T| \le \alpha$, $B \ne \emptyset$: $|STB| \le \alpha\beta|A|$.
• Proposition 5.2 (p. 12): under (1)–(3), a minimal-growth $S$ satisfies $|SBB| \le \alpha^{7}\beta\gamma^{3}|S|$ — the case $h = 2$ of the goal.
• Inductive step (proof of Theorem 1.7, p. 13): under the same hypotheses, for every $h \ge 2$,

$$|SB^{h}| \le \alpha^{8}\beta\gamma^{4}\,|SB^{h-1}|.$$

Significance

Theorem 1.7 extends the Plünnecke–Ruzsa inequality to non-abelian groups with explicit exponents, under hypotheses that are checkable on $A$ and $B$ alone. Bounds of this kind feed into the theory of approximate groups, where polynomial dependence on the doubling constants is what keeps later structure theorems quantitative. The witness $S$ is a large-enough piece of $A$ on which all powers of $B$ grow at a controlled rate, which is the form in which such bounds are used.

The result is proved in the paper. Mathlib formalizes Petridis' Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul, in any group) and the abelian Plünnecke–Ruzsa inequalities (Finset.pluennecke_ruzsa_inequality_*, for commutative groups), but not the non-abelian estimates of §5. This mission adds them: the corollary on $SS^{-1}SS^{-1}$, the comparable-size bound for $SBB$, and the full Theorem 1.7. Companion missions of this series formalize the abelian Theorem 3.1 and the explicit form of Tao's theorem (Theorem 1.6).

Difficulty

The abelian argument iterates $|CXB| \le \alpha|CX|$ with $C = B^{h-1}$, which needs $XB^{h-1}B = B^{h-1}XB$, i.e. commutativity. In a non-abelian group $S$ and powers of $B$ cannot be reordered, so the bound on $|CSB|$ does not iterate directly. A second obstacle is that the hypotheses control products of $A$ and $B$, while the induction needs control of sets such as $SS^{-1}SS^{-1}$ and $B^{-1}B^{h-1}$, built from inverses; the hypotheses say nothing directly about such sets, and every passage between them and products of $A$ and $B$ costs further powers of $\alpha$ and $\gamma$, which is why the exponents grow like $8h$ and $4h$ rather than $h$. The abelian bound $\alpha^h$ should not be expected to transfer unchanged.

Formalization scope

All statements use Mathlib's pointwise Finset algebra under open scoped Pointwise, in {G : Type*} [Group G] [DecidableEq G] — never CommGroup. $XY$ is X * Y, $AbB$ is A * {b} * B, $SB^h$ is S * B ^ h with B ^ 0 = {1}, $X^{-1}$ is X⁻¹. Cardinalities are cast to ℝ; $\alpha, \beta, \gamma$ are arbitrary reals, with no sign hypotheses beyond what the page states. Exponents are natural numbers, exact under 1 < h (goal) and 2 ≤ h (inductive step).

Conventions committed to:

• Nonempty witness. The page says "there exists $S \subseteq A$"; every product with $\emptyset$ is empty, so $S = \emptyset$ would make the statement trivially true. The paper's $S$ minimises a ratio defined only for nonempty sets, so the goal assumes $A \ne \emptyset$ and asserts $S \ne \emptyset$; a formalization without this is ruled out.
• Minimality is cross-multiplied and ranges over nonempty $Z \subseteq A$.
• Division by $|B|$. Corollary 5.1 assumes $B \ne \emptyset$, since Lean's $x/0 = 0$ would make it false otherwise; display (14), stated on its own, also assumes $B \ne \emptyset$, which the paper's condition (3) supplies.
• Typos recorded, not encoded. Proposition 5.2 says "sets in a finite group"; it is formalized for finite sets in any group, as in Theorem 1.7. The proof of Theorem 1.7 prints "$B \subseteq A^{-1}AT$" for $B \subseteq S^{-1}ST$ and "$|SB^h| \subseteq |SS^{-1}STB^{h-1}|$" for an inclusion of sets; neither affects a statement.

Proof tools available in Mathlib: Ruzsa's covering lemma (Lemma 4.1 of the paper, Finset.ruzsa_covering_mul), Ruzsa's triangle inequality (Lemma 4.2, Finset.ruzsa_triangle_inequality_mul_mulInv_mul and siblings, with Finset.card_inv), Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul), and Finset.card_singleton_mul. No new definitions are needed. Proofs of any milestone are welcome; the inequalities (15)–(17) of p. 13 are natural auxiliary lemmas for the inductive step.

Selected references

• G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups, arXiv:1101.3507v3, 2011; Combinatorica 32 (2012). https://arxiv.org/abs/1101.3507
• T. Tao, Product set estimates for non-commutative groups, Combinatorica 28 (2008) 547–594. https://arxiv.org/abs/math/0601431
• I. Z. Ruzsa, An application of graph theory to additive number theory, Scripta Math. 3 (1989) 97–109.
• H. Plünnecke, Eine zahlentheoretische Anwendung der Graphentheorie, J. Reine Angew. Math. 243 (1970) 171–183. https://doi.org/10.1515/crll.1970.243.171
• W. T. Gowers, A new way of proving sumset estimates, blog post, 2011. https://gowers.wordpress.com/2011/02/10/a-new-way-of-proving-sumset-estimates/

Motivation

Compatibility of independently chosen row and column permutations controls how two families of local symmetries overlap. The source connects a weighted compatibility estimate to Thorp spectral bounds. The source is OpenAI's September 2026 manuscript.

Setting

A row system chooses a permutation in each row of an $A$ by $D$ array; a column system chooses a permutation in each column. They are compatible when their combined routing remains injective down each column. Nonnegative weights may bias each local permutation.

Formalization targets

$$\operatorname{WeightedCompatibility}(w,v)\le e^{C_0n^{54/100}}\prod_i M_\theta(w_i)\prod_j M_\theta(v_j),\qquad\theta=1-L/\log\sqrt n.$$

The proposition WeightedCompatibilityTheorem holds. Here, for natural numbers A and D, Rows assigns to each i in Fin A a permutation of Fin D, and Cols assigns to each j in Fin D a permutation of Fin A; a pair (r,c) is Compatible if for every column j the map i ↦ c(r_i(j))(i) is injective. The weightedCompatibility of real weight families w (indexed by i and a permutation of Fin D) and v (indexed by k and a permutation of Fin A) is (AD)! / ((D!)^A (A!)^D) times the uniform mean, over all pairs (r,c), of the indicator of compatibility times ∏_i w_i(r_i) ∏_k v_k(c_k). The marginalFactor for θ and a weight function u is the θ-th power of the uniform mean of u^(1/θ). The stated claim is that there exist reals L, C₀, m₀ > 0 such that for all natural numbers A and D, with n = AD, m = √n and θ = 1 − L/log m, whenever m ≥ m₀, θ > 0, and both A and D lie between m/2 and 2m, then for all nonnegative weight families w and v, weightedCompatibility(A,D,w,v) ≤ exp(C₀ n^(54/100)) · ∏_i marginalFactor(θ, w_i) · ∏_k marginalFactor(θ, v_k).

The goal is OAI.ThorpCompatibility.weightedCompatibility_main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• remaining main.

Significance

The formal goal is an entropy-type inequality for arbitrary nonnegative local weights in sufficiently large balanced rectangles. It supplies a concrete combinatorial estimate that can support spectral analysis. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The compatibility indicator couples all row and column choices. A product of separate marginal expectations loses the injectivity constraint and cannot directly recover the stated exponent.

Formalization scope

The rectangle satisfies $n=AD$, with both side lengths between $\sqrt n/2$ and $2\sqrt n$. The theorem existentially chooses positive $L,C_0,m_0$ and assumes positive $\theta$. The marginal factor is the $\theta$th power of the uniform mean of the weight to power $1/\theta$.

The shared definitions are supplied by ThorpRemaining, ThorpWeightedCompatibility. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Compatibility entropy and the spectrum of a Thorp sweep, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

An external force rewards self-avoiding walks whose endpoints move in a chosen direction. The source studies critical honeycomb scaling; the available formal goal supplies existence of the forced free-energy limit. The source is OpenAI's September 2026 manuscript.

Setting

For an $n$-step self-avoiding walk, the endpoint displacement is embedded in the complex plane. Its projection onto $e$ is the real part of $\overline e$ times that displacement. The partition sum weights the walk by critical activity to the $n$th power and an exponential force reward.

Formalization targets

$$\frac1n\log\!\sum_{\gamma\in\operatorname{SAW}_n(o)}\rho^n e^{s\operatorname{Re}(\overline e\,\Delta\gamma)}\longrightarrow F(o,e,s),\qquad\rho=(2+\sqrt2)^{-1/2}.$$

For every starting vertex o of the honeycomb lattice, every complex number e and every real number s, the sequence logPartition(o,e,s)(n) converges as n tends to infinity to freeEnergy(o,e,s). Here vertices are triangular-up or triangular-down sites labeled by integer column and row, each up vertex being adjacent to three down vertices and vice versa, with planar positions given in the complex plane. saws(o,n) is the set of self-avoiding walks of n steps from o, meaning vertex lists with no repetition. For such a walk γ, its displacement is the position of its endpoint minus the position of o, and its projection onto e is the real part of conj(e) times the displacement. The partition function is the sum over γ in saws(o,n) of ρ^n exp(s times that projection), with ρ = 1/√(2+√2). logPartition is log of this partition function divided by n, and freeEnergy is defined as the limit of logPartition at infinity, using Lean's limUnder convention. The statement therefore asserts that this limit exists and equals freeEnergy; it is a stated theorem whose proof is admitted in the source.

The goal is OAI.HoneycombForce.logPartition_tendsto.

Significance

The conclusion makes the defined free energy an actual convergent limit for every starting point, direction parameter, and real force. It establishes the thermodynamic quantity underlying later asymptotic questions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Finite sums at each length do not guarantee convergence after normalization. Self-avoidance couples concatenated pieces, so ordinary independent-product arguments are unavailable without additional work.

Formalization scope

The target allows any complex $e$ and real $s$, without a unit-direction restriction. Length counts steps, and walk lists contain $n+1$ distinct vertices. The spatial exponent, thermal laws, and small-force exponent from the manuscript are not attached conclusions.

The shared definitions are supplied by HoneycombFreeEnergy. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Renewal and changes of law for critical honeycomb walks, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Finite matroid packing and covering principles connect disjoint spanning sets with independent covers. The source seeks a concrete obstruction to extending the unrestricted principle to infinite ground sets. The source is OpenAI's September 2026 manuscript.

Setting

A matroid records independent subsets and their closure. A packing/covering partition divides the common ground set into a part with disjoint spanning sets in restrictions and a part covered by independent sets in contractions. Self-duality means equality with the dual on the same labelled ground set.

Formalization targets

$$\exists M_0,M_1\text{ on a countably infinite }E:\quad M_i^*=M_i,\quad I_0\cup I_1\ne E\text{ for every independent pair},\quad\neg\operatorname{HasPackingCovering}(M_0,M_1).$$

The ground type E = ℤ × D, where D is the type of pairs consisting of a natural number m and a Boolean function on Boolean m-tuples, is countable and infinite, and that there exist two matroids M₀ and M₁ on E, each with ground set all of E, each equal to its own dual, such that no independent set of M₀ and independent set of M₁ have union all of E. Yet the pair fails HasPackingCovering. That predicate asks for a partition of the common ground set into P and C, two disjoint subsets S₀ and S₁ of P that are spanning in the restrictions M₀|P and M₁|P respectively, and subsets I₀ and I₁ of C that are independent in the contractions of M₀ and M₁ onto C (the dual of the restriction of the dual to C), with I₀ ∪ I₁ = C. So the theorem asserts a countably infinite pair of self-dual matroids with no such packing-covering decomposition.

The goal is OAI.InfiniteMatroidCounterexample.main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• partitional intersection counterexample.
• separate covering packing counterexamples.

Significance

The goal simultaneously supplies a countable infinite example, failure of a full independent cover, and failure of every mixed partition. Additional attached statements treat partitional matroids, intersection, and the separate packing and covering assertions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Failure of a full independent cover does not by itself exclude a mixed partition. The matroids must satisfy the infinite independence axioms, including maximal extension, throughout the construction.

Formalization scope

The ground type is the fixed product of integers with finite Boolean-function data. Mathlib matroids have ground set equal to the entire type in the goal. The two source definition groups have overlapping declarations and remain separate reference groups, with no aggregate import.

The shared definitions are supplied by InfiniteMatroid, InfiniteMatroidCorollaries. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, A Counterexample to the Infinite Matroid Packing/Covering Conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Excluding a fixed clique should force independent sets larger than those guaranteed by average degree alone. The source asks for the full logarithmic improvement uniformly across graph sizes. The source is OpenAI's September 2026 manuscript.

Setting

An independent set contains no adjacent pair. Write $n$ for the number of vertices, $d=2|E|/n$ for average degree, and $α(G)$ for the largest independent-set size. A graph is clique-free of order $r$ when it contains no $r$ pairwise adjacent vertices.

Formalization targets

$$\forall r\ge4\ \exists c_r>0:\quad \alpha(G)\ge c_r\frac{n\log d}{d}\qquad(d\ge2,\ G\text{ is }K_r\text{-free}).$$

For every natural number r ≥ 4, there is a real constant c > 0 such that the following holds for every finite simple graph G on a vertex type V (a Fintype). Here the average degree d(G) is defined as 2|E(G)|/|V|, twice the number of edges divided by the number of vertices (as a real number). If G contains no clique of size r (it is r-clique-free) and d(G) ≥ 2, then the independence number α(G), the maximum size of an independent set, satisfies α(G) ≥ c · |V| · log(d(G)) / d(G), where log is the natural logarithm of real numbers. The constant c may depend on r but not on G.

The goal is OAI.CliqueFreeLog.logarithmic_independence_bound.

Significance

The bound improves the general inverse-degree scale by a factor of natural logarithmic size. The constant may depend on the forbidden clique but must work for every input graph. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The condition forbids ordinary cliques rather than imposing bounded complexity on every neighborhood. Estimates using maximum degree alone do not establish the stated average-degree bound.

Formalization scope

The representation is Mathlib SimpleGraph on a finite type. Real.log is the natural logarithm and the hypothesis $d\ge2$ keeps its argument and the denominator positive. The empty graph is excluded by that hypothesis.

The shared definitions are supplied by CliqueFreeLog. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, A logarithmic independence bound for clique-free graphs, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Graph homomorphism inequalities compare the frequency of a fixed pattern with what edge density predicts. The mission asks for one finite host graph violating the proposed bound for a specified bipartite pattern. The source manuscript presents the surrounding research claim.

Setting

The pattern H is the incidence graph between thirteen points and twenty-two explicitly listed triples, giving thirty-five vertices and sixty-six edges. Homomorphism density counts all edge-preserving maps, including noninjective maps, divided by the number of all vertex maps.

Formalization target

Construct a positive-size finite simple host G with at least one edge such that

$$t(H,G)<p(G)^{66},\qquad p(G)=\frac{2|E(G)|}{|V(G)|^2}.$$

The selected formal target is OAI.SidorenkoCounterexample.main.

Significance and status

The counterexample uses the exact supplied pattern rather than an unspecified bipartite graph. A finite host makes the density comparison an ordinary finite counting statement. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The required strict inequality concerns all homomorphisms, not only embeddings. The host must have an edge so the assertion cannot be replaced by a zero-density degeneracy.

Formalization scope

H is built from the published table of twenty-two triples. Hosts use Fin size, and both graph counts and real density normalizations are fixed. The manuscript’s forcing-conjecture consequence is not an attached formal target.

Selected references

• OpenAI, A counterexample to Sidorenko's conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Finite patterns fit inside positive-measure sets after a sufficiently small affine change. The dyadic similarity problem asks whether one particular infinite pattern can be excluded even from compact sets of nearly full measure. The source manuscript presents the surrounding research claim.

Setting

The dyadic sequence is D={2⁻ⁿ:n≥1}. Its affine copies are x+sD with arbitrary x∈ℝ and nonzero signed scale s. The ambient measure is Lebesgue measure on the real line.

Formalization target

For every 0<η<1, construct a compact E⊆[0,1] with

$$|E|>1-\eta,\qquad\forall x\in\mathbb R\;\forall s\ne0\;\exists n\ge1,\quad x+s2^{-n}\notin E.$$

The same E must avoid every translation and both signs of dilation.

The selected formal target is OAI.Problem310.dyadic_affine_avoidance.

Significance and status

The result concerns the dyadic sequence specifically, with a stronger near-full-measure conclusion than merely finding one positive-measure avoiding set. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Excluding a countable collection of copies does not handle the continuum of scales and centers. Finite initial segments cannot replace the entire sequence.

Formalization scope

The definition dyadicPoint accepts n=0, but the theorem explicitly chooses n≥1. Measure is ENNReal-valued and compares with ENNReal.ofReal(1−η). Compactness and interval containment are required conclusions. General infinite sets are outside this selected target.

Selected references

• OpenAI, The dyadic case of the Erdős similarity conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Add random clauses one at a time to a Boolean formula on $n$ variables until it first becomes unsatisfiable. The index $H_n$ of that first failure is the satisfiability hitting time of random $k$-SAT. Its mean, divided by $n$, converges to the satisfiability threshold; its variance measures the width of the transition window. Friedgut's sharp-threshold theorem shows the window is $o(n)$, but quantitative widths have remained far from the $\sqrt n$ scale suggested by lower bounds. This mission asks for the order of the variance of $H_n$ for every fixed $k\ge3$.

Timeline

• 1981. Efron and Stein prove their variance inequality, the basic tool for fluctuation bounds of functions of independent inputs (doi:10.1214/aos/1176345462).
• 1999. Friedgut, with an appendix by Bourgain, proves a sharp threshold sequence for each fixed $k$ (doi:10.1090/S0894-0347-99-00305-7).
• 2002. Wilson proves an $\Omega_k(\sqrt n)$ separation of central quantiles for the proper-clause model (doi:10.1002/rsa.10050).
• 2005. Boucheron, Bousquet, Lugosi and Massart give moment inequalities for functions of independent variables (doi:10.1214/009117904000000856).
• 2022. Ding, Sly and Sun prove the satisfiability conjecture for large $k$ (doi:10.4007/annals.2022.196.1.1).
• 2026. Carenini proves an $O_{k,\eta}(n/\log n)$ window (ECCC TR26-145, arXiv:2609.26222) and then a polynomial window $O_{k,\eta}(n^{1/2+1/k})$ with variance $O_k(n^{1+2/k})$, resolving the satisfiability conjecture for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026); priority for that resolution belongs to Carenini. A companion OpenAI preprint gives an alternative proof of the limiting threshold.

The source of this mission is an OpenAI preprint dated September 27, 2026.

Setting

Fix $k\ge3$ and $n\ge k$. A proper $k$-clause is an OR of literals on $k$ distinct variables; let $C_1,C_2,\dots$ be independent uniform choices among the $2^k\binom nk$ signed proper clauses (signs fair, whole clauses may repeat). Put

$$F_m=C_1\wedge\dots\wedge C_m,\qquad F_0=\text{true},\qquad H_n=\min\{m\ge1:\ F_m\ \text{unsatisfiable}\},$$

and, for fixed $B>0$, the capped hitting time $T_{n,B}=\min\{H_n,\lfloor Bn\rfloor\}$. Since each assignment survives a clause with probability $1-2^{-k}$, $H_n$ is a.s. finite with all moments. Write

$$\ell_k(n)=\begin{cases}\log(en),&k=3,\\1,&k\ge4,\end{cases}\qquad U_k=\frac{\log2}{-\log(1-2^{-k})}.$$

Formalization targets

Goal: Theorem 1.1

There are constants $C_k,c_k>0$ with

$$\operatorname{Var}(H_n)\le C_k\,n\,\ell_k(n)\quad(n\ge k),\qquad \operatorname{Var}(H_n)\ge c_kn\quad(n\ \text{large}),$$

and for every fixed $B>0$ a constant $C_{k,B}$ with $\operatorname{Var}(T_{n,B})\le C_{k,B}\,n\,\ell_k(n)$; if $B>U_k$ then also $\operatorname{Var}(T_{n,B})\ge c_kn$ for large $n$. Hence $\operatorname{Var}(H_n)=\Theta_k(n)$ for $k\ge4$. Lean: OAI.RandomKSAT.variance_main, open on the platform.

Milestone: Propositions A.1–A.2 (optimality of exponents)

The killing-probability exponent $\beta=k/(k-1)$ in the lifetime bound $\tau_k(S)q_d(S)^\beta\le C_kd^\beta$ (Proposition 2.3) cannot be decreased, and the block-error term $g^{-(k-1)}$ in the replacement lemma cannot be improved to $o(g^{-(k-1)})$ uniformly. Lean: OAI.RandomKSAT.sharpness.

Significance

For $k\ge4$ the theorem determines the variance of the hitting time up to constants, so the transition window has width $\Theta_k(\sqrt n)$ in the variance sense, matching Wilson's lower bound and improving Carenini's $O_k(n^{1+2/k})$ variance bound. For $k=3$ it leaves only a logarithmic gap, closed in a companion OpenAI preprint. Chebyshev's inequality then gives concentration of $H_n$ about $\mathbb EH_n$ at scale $\sqrt{n\ell_k(n)}$.

The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.

Difficulty

The Efron–Stein inequality reduces the upper bound to the expected squared delay caused by deleting one clause, which counts pairs of prefixes at which that clause is pivotal. Controlling this occupation time requires a uniform estimate relating how quickly a set of assignments is killed by shorter $(k-1)$-clauses to its lifetime under $k$-clauses, valid for every assignment set with no lower cutoff. Earlier arguments truncate the number of clauses incident to the deleted clause's variables at a logarithmic level, which costs a logarithm; keeping that number as a random parameter without destroying independence is the main obstacle. Appendix A shows the relevant exponents are sharp.

Formalization scope

• Clause n k is a dependent pair of a $k$-element Finset (Fin n) and a sign vector on it; clauseLaw is uniform; streamLaw is the infinite product (Measure.infinitePi).
• firstFailure ω is the least $m$ with an unsatisfiable prefix, valued in ℕ∞; H = (firstFailure ω).toNat; T B ω = (min (firstFailure ω) ⌊Bn⌋).toNat. The infinite case has probability zero.
• variance is ProbabilityTheory.variance under streamLaw n k; ell, U are as displayed.
• In the milestone, blockKill u s S g is the probability that $g$ independent proper $s$-clauses kill $S$, and lifetime u k S $=\sum_m\mathbb P(S\text{ survives }m\text{ clauses})$ is $\tau_k(S)$.

Infrastructure: product measures on clause streams, Efron–Stein, conditioning on incidence patterns. Formalizations of Proposition 2.3 (lifetime from shorter-clause killing), Proposition 4.3 (conditional squared delay), Corollary 5.2 and Proposition 6.2 (linear variance lower bound) are welcome.

Selected references

• OpenAI, Variance of the Random k-SAT Hitting Time, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Variance-of-the-Random-k-SAT-Hitting-Time-September-27-2026/article.pdf
• OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
• G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
• G. Carenini, The scaling window of random k-SAT, ECCC TR26-145, 2026. https://arxiv.org/abs/2609.26222
• E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
• D. B. Wilson, On the critical exponents of random k-SAT, Random Structures Algorithms, 2002. https://doi.org/10.1002/rsa.10050
• J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
• B. Efron, C. Stein, The jackknife estimate of variance, Ann. Statist., 1981. https://doi.org/10.1214/aos/1176345462
• S. Boucheron, O. Bousquet, G. Lugosi, P. Massart, Moment inequalities for functions of independent random variables, Ann. Probab., 2005. https://doi.org/10.1214/009117904000000856

Motivation

A random $k$-SAT formula on $n$ Boolean variables is a conjunction of $m$ independent random clauses, each an OR of $k$ literals on distinct variables. As the clause density $m/n$ grows, the formula changes from almost surely satisfiable to almost surely unsatisfiable. Random $k$-SAT is a central model in probabilistic combinatorics, the theory of algorithms and statistical physics: its threshold is where hard instances are expected to concentrate, and it is a proving ground for methods from spin-glass theory. The satisfiability conjecture, formulated explicitly by Chvátal and Reed, asserts that for each fixed $k$ the transition happens at a limiting density $\alpha_k$ that does not drift with $n$.

Timeline

• 1992. Chvátal and Reed settle $k=2$ and formulate the conjecture for every fixed clause size (doi:10.1109/SFCS.1992.267789); Goerdt gives an independent proof for $k=2$ (doi:10.1006/jcss.1996.0081).
• 1999. Friedgut, with an appendix by Bourgain, proves a sharp transition around a sequence of densities, leaving open whether the sequence converges (doi:10.1090/S0894-0347-99-00305-7).
• 2002, 2006. Mézard, Parisi and Zecchina, and Mertens, Mézard and Zecchina, predict threshold values via the cavity method (doi:10.1126/science.1073287, doi:10.1002/rsa.20090).
• 2004. Achlioptas and Peres prove bounds $2^k\log2-O(k)$ (doi:10.1090/S0894-0347-04-00464-3).
• 2013, 2014. Bayati, Gamarnik and Tetali develop combinatorial interpolation for sparse random structures (doi:10.1214/12-AOP816); Abbe and Montanari study concentration of solution counts (doi:10.1002/rsa.20501).
• 2016. Coja-Oghlan and Panagiotou locate the threshold sequence within $o_k(1)$ of $2^k\log2-(1+\log2)/2$ (doi:10.1016/j.aim.2015.11.007).
• 2022. Ding, Sly and Sun prove the conjecture for all sufficiently large $k$, with the 1RSB value (doi:10.4007/annals.2022.196.1.1).
• 2026. Carenini proves a polynomial scaling window and resolves the conjecture for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026; https://eccc.weizmann.ac.il/report/2026/229/). Priority for the resolution belongs to Carenini.

The source of this mission is an OpenAI preprint dated September 25, 2026, which gives an alternative proof of the existence of the limiting threshold.

Setting

Fix $k\ge3$. For $n\ge k$, a proper $k$-clause chooses $k$ distinct variables among $x_1,\dots,x_n$ uniformly and gives each an independent fair sign, so each of the $2^k\binom nk$ clauses is equally likely. Let $C_1,C_2,\dots$ be independent such clauses (sampled with replacement: two positions may hold the same clause) and

$$F_{n,m}=\bigwedge_{i=1}^mC_i,\qquad P_n(m)=\mathbb P(F_{n,m}\ \text{is satisfiable}),\qquad P_n(0)=1 .$$

The ratio $c=m/n$ is the clause density.

Formalization targets

Goal: Theorem 1.1

For every fixed integer $k\ge3$ there is $\alpha_k\in(0,\infty)$ such that

$$\lim_{n\to\infty}P_n(\lfloor cn\rfloor)=\begin{cases}1,&0\le c<\alpha_k,\\ 0,&c>\alpha_k.\end{cases}$$

No assertion is made at $c=\alpha_k$, and the value of $\alpha_k$ is not identified. Lean: OAI.FixedClauseThreshold.main, open on the platform.

Significance

The theorem settles, for every fixed $k\ge3$, the existence half of the threshold question: Friedgut's sharp transition happens at a location that converges. Previously this was known only for large $k$ (Ding–Sly–Sun) and for $k=2$. Existence is a prerequisite for questions about the value of $\alpha_k$, its computability, and the fluctuations of the satisfiability hitting time, which companion OpenAI preprints address. The proof here proceeds through concentration of a capped last satisfiable index and a comparison between system sizes; it does not rely on Carenini's window.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

A sharp-threshold theorem gives a narrow window at each $n$ but no control of how the window's center moves with $n$. Convergence needs a comparison between different system sizes, and interpolation methods from spin-glass theory deliver free-energy bounds, not hard satisfiability statements, and often only for even arity. The center must also be shown to concentrate polynomially, which requires bounding how many variables are forced along the clause process.

Formalization scope

• ProperClause n k is a function Fin n → Option Bool with exactly $k$ defined entries; some b at $i$ is the literal satisfied when $\sigma_i=b$.
• Formula n k m := Fin m → ProperClause n k (ordered, with replacement); properSATProbability n k m is the exact ratio of satisfiable formulas to all formulas, which equals $P_n(m)$ under the uniform product law.
• Degenerate sizes: $m=0$ gives probability $1$; for $n<k$ and $m>0$ the ensemble is empty and the ratio is $0$ by convention, affecting only finitely many $n$.
• HasLimitingThreshold k asserts $\exists\,\alpha>0$ with limits $1$ for $0\le c<\alpha$ and $0$ for $c>\alpha$ at $m=\lfloor cn\rfloor$.

Infrastructure: finite counting of formulas, Efron–Stein-type variance bounds, a deterministic concentration-to-convergence lemma (Theorem 5.1), and the Poisson/interpolation comparison with the transfer back to proper clauses. Formalizations of Proposition 2.2 (integrated forcing), Proposition 3.3 (polynomial concentration) and Theorem 5.1 are welcome.

Selected references

• OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
• G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
• V. Chvátal, B. Reed, Mick gets some (the odds are on his side), FOCS 1992. https://doi.org/10.1109/SFCS.1992.267789
• E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
• D. Achlioptas, Y. Peres, The threshold for random k-SAT is $2^k\log2-O(k)$, J. Amer. Math. Soc., 2004. https://doi.org/10.1090/S0894-0347-04-00464-3
• A. Coja-Oghlan, K. Panagiotou, The asymptotic k-SAT threshold, Adv. Math., 2016. https://doi.org/10.1016/j.aim.2015.11.007
• J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
• M. Bayati, D. Gamarnik, P. Tetali, Combinatorial approach to the interpolation method and scaling limits in sparse random graphs, Ann. Probab., 2013. https://doi.org/10.1214/12-AOP816
• E. Abbe, A. Montanari, On the concentration of the number of solutions of random satisfiability formulas, Random Structures Algorithms, 2014. https://doi.org/10.1002/rsa.20501

Motivation

In a Maker–Breaker achievement game, two players alternately claim cells of a board; Maker wins by owning every cell of some copy of a fixed shape, and Breaker only tries to prevent this. Polyomino achievement games on the infinite square grid, introduced by Frank Harary, ask which small polyominoes are winners (Maker can force a copy) and which are losers (Breaker can prevent it forever). The six-cell shape Snaky is the long-standing hard case: Maker was known to win with a one-stone handicap or in higher dimensions, but the ordinary planar game without handicap remained undecided.

Timeline

• 2004. Sieben shows that Snaky is a winner in 41 dimensions and records earlier handicap-two strategies of Harary, Harborth and Seemann, as well as the non-existence of a pairing strategy for Breaker (Integers 4, 2004).
• 2007. Halupczok and Schlage-Puchta prove that Snaky wins in three dimensions, loses on an $8\times8$ board, and has planar handicap number at most one (Integers 7, 2007). Ito and Miyagawa give another handicap-one construction.
• 2008. Sieben develops proof trees for weak achievement games and gives a finite proof sequence for the handicap-one win, describing the ordinary planar problem as undecided (Integers 8, 2008).
• 2011. Csernenszky, Martin and Pluhár give a computer-free proof that Breaker has no pairing defense for Snaky (Integers 11, 2011).
• 2023, 2025. Shaik, Mayer-Eichberger, van de Pol and Saffidine study QBF encodings of finite Maker–Breaker games, including Snaky on a $5\times5$ board (arXiv:2301.07345); Boucher and Villemaire treat strong achievement games (doi:10.21428/594757db.6ae0c84a).

The source of this mission, an OpenAI preprint dated September 25, 2026, settles the ordinary planar game: Snaky is a winner, within 21 Maker moves.

Setting

The board is $\mathbb Z^2$, initially empty. Snaky is

$$S=\{(0,0),(1,0),(2,0),(3,0),(3,1),(4,1)\}.$$

An allowed copy is $t+R(S)$ with $t\in\mathbb Z^2$ and $R$ one of the eight $2\times2$ signed permutation matrices (rotations by quarter turns and reflections; no scaling). Maker moves first; then Breaker and Maker alternate, each claiming one previously unclaimed cell. Maker wins when it owns all cells of an allowed copy.

A Maker policy is a rule that, given the current position, returns an unclaimed cell. In the fixed-endpoint formulation, the policy keeps claiming fresh cells even after a win, and one asks that after Maker's $N$-th claim its set of cells contain an allowed copy whenever Breaker's first $N-1$ replies were legal.

Formalization targets

Milestone: Proposition 10 (finite identities of the 35-move certificate)

A pure computation on a printed certificate of 616 cards: card counts, 1,837 placement terms, required-set/envelope/height data of four interface cards, and uniform bounds for all cards.

Milestone: Theorem 11

$$\exists\ \text{Maker policy}\ \sigma:\ \text{every legal play} \Rightarrow \text{an allowed copy of } S \text{ within } 35 \text{ Maker claims}.$$

Goal: Theorem 1

$$\exists\ \text{Maker policy}\ \sigma:\ \text{every legal play} \Rightarrow \text{an allowed copy of } S \text{ within } 21 \text{ Maker claims}.$$

The Lean statement OAI.SnakyPrototype.snaky_winning_strategy_21_with_legal_states is open on the platform.

Significance

Theorem 1 decides the ordinary planar Snaky game, recorded as undecided by Sieben (2008), and gives an explicit bound of 21 Maker moves (a win by the 41st individual turn). It also gives a win on the finite $17\times17$ board (Corollary 6), and removes the handicap from the earlier handicap-one strategies. The paper does not claim the bound 21 is optimal or address the strong game in which both players seek a copy.

The result is proved in an OpenAI preprint that has not been peer reviewed. Its correctness rests on a soundness lemma for a composition rule together with large finite certificates checked by standalone programs. A machine-checked proof would replace this combination of informal soundness argument and external computation by a single certified statement.

Difficulty

The board is infinite and Breaker may play anywhere, so no finite game-tree search applies directly: a proof must cover all Breaker replies, including those far from the action. Pairing strategies, the usual tool for proving shapes are losers, are known to fail for Snaky, but that does not give Maker a strategy. The certificate approach needs a composition rule whose soundness accounts for arbitrary previous ownership on both sides; the move count must be the number of actual Maker claims, including any replacement moves.

Formalization scope

• Cells are ℤ × ℤ; snaky is the six-cell set above and HasSnaky M asks for r : Fin 8, t : Cell with snaky.image (placement r t) ⊆ M, where orient lists all eight signed permutations.
• A Policy is a function of a move counter, the Maker set and the Breaker set; it must never return an owned cell. playState σ N β ∅ ∅ k is the position after $k$ Maker claims and $k$ Breaker replies.
• LegalRepliesBeforeFinal σ N β ∅ ∅ constrains only the first $N-1$ Breaker replies; the theorems conclude a copy of $S$, exactly $N$ Maker cells, and disjointness of the two players' sets throughout.
• The certificate milestone stores the cards as an Array Entry and computes rowAt i (required set, envelope, height) by the composition recursion; it is a decidable statement about explicit finite data.

A trivializing reading is ruled out: the policy is required to be legal on all inputs, and Breaker's replies are arbitrary legal cells of the infinite board. A complete development needs a soundness proof for the composition rule (Lemma 3) and verified evaluation of the certificates; the policy, game and certificate infrastructure is shared between the 21- and 35-move statements. Contributions formalizing Lemma 3, Proposition 5 (the 21-move certificate identities) and Corollary 6 are welcome.

Selected references

• OpenAI, Snaky in 21 Maker moves, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Snaky-in-21-Maker-moves-September-25-2026/article.pdf
• N. Sieben, Snaky is a 41-dimensional winner, Integers 4, 2004. https://math.colgate.edu/~integers/eg5/eg5.pdf
• I. Halupczok, J.-C. Schlage-Puchta, Achieving Snaky, Integers 7, 2007. https://math.colgate.edu/~integers/hg2/hg2.pdf
• N. Sieben, Proof trees for weak achievement games, Integers 8, 2008. https://math.colgate.edu/~integers/ig7/ig7.pdf
• H. Ito, H. Miyagawa, Snaky is a winner with one handicap, 8th Hellenic European Conference on Computer Mathematics and its Applications, 2007.
• A. Csernenszky, R. R. Martin, A. Pluhár, On the complexity of Chooser–Picker positional games, Integers 11, 2011. https://math.colgate.edu/~integers/lg2/lg2.pdf
• I. Shaik, V. Mayer-Eichberger, J. van de Pol, A. Saffidine, Implicit state and goals in QBF encodings for positional games, preprint, 2023. https://arxiv.org/abs/2301.07345
• S. Boucher, R. Villemaire, The QBF Cover encoding for Harary's Tic-Tac-Toe, Canadian Conference on AI, 2025. https://doi.org/10.21428/594757db.6ae0c84a

Motivation

When does the Erdős–Rényi random graph $G(n,p)$ contain a copy of a prescribed graph $H$? A necessary condition is visible from first moments: if some subgraph $F\subseteq H$ has expected copy count below a constant, then $H$ is unlikely to appear. Kahn and Kalai conjectured in 2007 that this elementary obstruction determines the containment threshold up to a logarithmic factor, uniformly over all target graphs, including spanning ones such as perfect matchings, Hamilton cycles or cubes (CPC 2007). Their abstract conjecture for general increasing families (the "first" conjecture) was proved by Park and Pham; the graph-specific "second" conjecture compares the threshold with the smaller, purely subgraph-count-based graph expectation threshold, and is not implied by the abstract theorem.

This mission asks for a formal proof of the second Kahn–Kalai conjecture with explicit constants, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1960–1981 — Erdős and Rényi's evolution of random graphs (1960) and perfect matchings (1966); Bollobás determines thresholds for fixed subgraphs (Math. Proc. Camb. Phil. Soc. 1981).
• 2007 — Kahn and Kalai state both conjectures (CPC 2007).
• 2010 — Talagrand introduces fractional expectation thresholds (STOC 2010).
• 2021 — Frankston, Kahn, Narayanan and Park prove $p_c=O(q_f\log\ell)$ (Annals 2021), building on the sunflower methods of Alweiss–Lovett–Wu–Zhang (Annals 2021).
• 2022–2025 — Mossel, Niles-Weed, Sun and Zadik obtain a single-log bound for a modified graph threshold (arXiv:2209.03326) and a Bayesian proof of the spread lemma (RSA 2025).
• 2024 — Park and Pham prove the abstract Kahn–Kalai conjecture (JAMS 2024).
• 2025 — Dubroff, Kahn and Park prove $p_c=O(p_E\log^3n)$ and special cases (arXiv:2508.14269, arXiv:2510.02005).
• 2026 — Tran reduces the loss to $O(\log^2(2e(H)))$ and proves the conjecture for trees and other classes (arXiv:2609.20546); the OpenAI preprint claims the general case (Theorem 1.1, p. 1).

Setting

For finite simple graphs $G,F$ let $N(G,F)$ be the number of subgraphs of $G$ isomorphic to $F$ (ordinary, non-induced copies). $G(n,p)$ is the random graph on $[n]$ with each of the $\binom n2$ edges present independently with probability $p$. For a graph $H$ with at least one edge and at most $n$ vertices,

$$p_c(n,H)=\inf\{p\in[0,1]:\ \Pr[N(G(n,p),H)>0]\ge\tfrac12\},$$ $$p_E(n,H)=\inf\{p\in[0,1]:\ \mathbb E\,N(G(n,p),F)\ge\tfrac12\ \text{for every subgraph }F\subseteq H\}.$$

The first is the containment threshold, the second the graph expectation threshold; always $p_E\le p_c$. Write $h=e(H)$ for the number of edges.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every $n\ge2$ and every finite simple graph $H$ with $h\ge1$ edges and at most $n$ vertices,

$$p_c(n,H)\ \le\ \min\bigl\{1,\ 2048\,e^{50}\,p_E(n,H)\,(1+\log_2 h)\bigr\},\qquad p_c(n,H)\ \le\ 6144\,e^{50}\,p_E(n,H)\log_2 n .$$

The constants are explicit and universal; $H$ may vary with $n$.

Significance

The result itself. The bound says that, up to a universal constant times $\log h$, the only obstruction to containing $H$ is a subgraph with too few expected copies. The logarithm cannot be removed: for a perfect matching $p_E=\Theta(1/n)$ while $p_c=\Theta(\log n/n)$, because isolated vertices must disappear. This settles the problem left by the abstract Park–Pham theorem, whose bound is in terms of the possibly larger integral expectation threshold of the family of graphs containing $H$.

Formalizing it. Both thresholds are finite, explicit optimization problems over Bernoulli product measures on the edges of $K_n$, so the statement is fully elementary. Mathlib has SimpleGraph.copyCount but no random-graph or threshold theory; the spread-family resampling lemma and the tree covering theorem would be reusable for other threshold results (Park–Pham, Frankston–Kahn–Narayanan–Park). No machine-checked proof of any Kahn–Kalai-type theorem is known.

Difficulty

The abstract theorem compares $p_c$ with the integral expectation threshold of the family $\mathcal F_H$ of edge sets containing a copy of $H$, and covers of $\mathcal F_H$ may be much cheaper than the copies of a single subgraph, so it does not give a bound in terms of $p_E$. Previous graph-specific approaches lost extra logarithms because each conditional extension step paid the sampling cost again. The preprint (Section 1.2, pp. 3) builds a tree of nested subgraph extensions with geometrically growing, pairwise disjoint labels along each path, and must reuse one random set at every level of the tree while keeping the spread property under conditioning (Theorem 3.1, p. 6).

Formalization scope

• $G(n,p)$ is encoded as a Bernoulli product weight on Finset (Edge n), where Edge n is the type of non-diagonal Sym2 (Fin n); expectations and probabilities are finite sums, defined for every real $p$ but used only on $[0,1]$.
• expectedCopies and containmentProbability use Mathlib's copyCount of the graph built from the edge set; both are ordinary (non-induced) copies.
• criticalThreshold and expectationThreshold are sInf over $p\in[0,1]$; the sets are nonempty (they contain $p=1$ when $H$ has at most $n$ vertices), so the infima are the true thresholds. The expectation constraint ranges over all H.Subgraphs, including subgraphs with isolated vertices, whose constraints are automatically satisfied.
• $H$ is a SimpleGraph on an arbitrary finite type V with Fintype.card V ≤ n, 2 ≤ n and at least one edge; logTwo is $\log x/\log 2$.
• The constants $2048e^{50}$ and $6144e^{50}$ are hard-coded, as in the source.

Selected references

• OpenAI, The second Kahn–Kalai conjecture, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-second-Kahn-Kalai-conjecture-September-24-2026/paper.pdf
• J. Kahn, G. Kalai, Thresholds and expectation thresholds, Combin. Probab. Comput. 16 (2007), 495–502. https://doi.org/10.1017/S0963548307008474
• J. Park, H. T. Pham, A proof of the Kahn–Kalai conjecture, J. Amer. Math. Soc. 37 (2024), 235–243. https://doi.org/10.1090/jams/1028
• K. Frankston, J. Kahn, B. Narayanan, J. Park, Thresholds versus fractional expectation-thresholds, Ann. of Math. 194 (2021), 475–495. https://doi.org/10.4007/annals.2021.194.2.2
• R. Alweiss, S. Lovett, K. Wu, J. Zhang, Improved bounds for the sunflower lemma, Ann. of Math. 194 (2021), 795–815. https://doi.org/10.4007/annals.2021.194.3.5
• M. Talagrand, Are many small sets explicitly small?, STOC 2010. https://doi.org/10.1145/1806689.1806693
• E. Mossel, J. Niles-Weed, N. Sun, I. Zadik, On the second Kahn–Kalai conjecture, arXiv:2209.03326 (2022). https://arxiv.org/abs/2209.03326v1
• E. Mossel, J. Niles-Weed, N. Sun, I. Zadik, A Bayesian proof of the spread lemma, Random Structures Algorithms 66 (2025), e70008. https://doi.org/10.1002/rsa.70008
• Q. Dubroff, J. Kahn, J. Park, On the "second" Kahn–Kalai conjecture, arXiv:2508.14269 (2025). https://arxiv.org/abs/2508.14269v1
• T. Tran, Fractional expectation thresholds and the "second" Kahn–Kalai conjecture, arXiv:2609.20546 (2026). https://arxiv.org/abs/2609.20546v2
• B. Bollobás, Threshold functions for small subgraphs, Math. Proc. Cambridge Philos. Soc. 90 (1981), 197–206. https://doi.org/10.1017/S0305004100058655

Motivation

Sensitivity and block sensitivity are two of the basic complexity measures of a Boolean function $f:\{0,1\}^n\to\{0,1\}$. Sensitivity counts how many single-bit flips change the value; block sensitivity allows disjoint groups of bits to be flipped together. Block sensitivity is polynomially related to decision-tree complexity, certificate complexity, degree and quantum query complexity, so the question of how it compares with sensitivity (the Sensitivity Conjecture, from Nisan's 1989 work on CREW PRAMs) decides whether sensitivity belongs to that same family. Huang's 2019 theorem settled the polynomial question: $\mathrm{bs}(f)\le s(f)^4$. Nisan and Szegedy had suggested the stronger bound $\mathrm{bs}(f)\le s(f)^2$, and the best known separations were quadratic.

This mission asks for a formal proof that no quadratic bound holds, as claimed in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1989 — Nisan introduces block sensitivity and records Rubinstein's quadratic separation (STOC 1989).
• 1994 — Nisan and Szegedy suggest $\mathrm{bs}(f)\le s(f)^2$ (Comput. Complexity 1994).
• 1995 — Rubinstein's function: $\mathrm{bs}(f)=\tfrac12 s(f)^2$ (Combinatorica 1995).
• 2011 — Virza improves to $\tfrac12s^2+\tfrac12s$ (IPL 2011); Ambainis and Sun reach $\tfrac23s^2-\tfrac13s$ (arXiv:1108.3494).
• 2013–2014 — Tal studies composition as an amplification tool (ITCS 2013); Ambainis and Prūsis note that a seed with $\mathrm{bs}>s^2$ would give a superquadratic power separation by iteration (ECCC TR14-027).
• 2019 — Huang proves $\mathrm{bs}(f)\le s(f)^4$ (Annals 2019); Wellens later sharpens the constant (Discrete Analysis 2022).
• 2026 — Meiburg shows block sensitivity can exceed spectral sensitivity squared (arXiv:2608.00851).
• September 2026 — The OpenAI preprint claims $\mathrm{bs}(f)/s(f)^2$ is unbounded, and $\mathrm{bs}\ge s^\alpha$ for a fixed $\alpha>2$.

Setting

For $x\in\{0,1\}^n$ and $B\subseteq[n]$, let $x^B$ be $x$ with the coordinates in $B$ flipped. For a total Boolean function $f$,

$$s(f,x)=\#\{a\in[n]: f(x^{\{a\}})\ne f(x)\},\qquad s(f)=\max_x s(f,x),$$

and $\mathrm{bs}(f,x)$ is the largest number of pairwise disjoint nonempty sets $B_1,\dots,B_m$ with $f(x^{B_j})\ne f(x)$ for every $j$; $\mathrm{bs}(f)=\max_x\mathrm{bs}(f,x)$. Always $s(f)\le\mathrm{bs}(f)$, and a nonconstant $f$ has $s(f)\ge1$.

Formalization targets

Goal: the quantitative form of Theorem 1.1 (p. 2)

For every integer $d\ge1$ there are $n\ge1$ and a nonconstant $f:\{0,1\}^n\to\{0,1\}$ with $f(0,\dots,0)=0$ and

$$\frac{\mathrm{bs}(f)}{s(f)^2}\ \ge\ \frac{2^d}{4(d+2)^2}.$$

Since the right side tends to infinity, for every $C>0$ some nonconstant $f$ has $\mathrm{bs}(f)>C\,s(f)^2$, which is the first sentence of Theorem 1.1. The goal does not include the fixed-exponent statement of Corollary 4.3 (p. 10).

Significance

The result itself. It refutes the quadratic strengthening of the Sensitivity Conjecture suggested by Nisan and Szegedy and leaves the true exponent between $2$ and $4$: Huang's theorem gives $\mathrm{bs}\le s^4$, while Corollary 4.3 of the preprint gives functions with $\mathrm{bs}(f,0)\ge s(f)^\alpha$ for some $\alpha>2$ and unbounded block sensitivity. Because spectral sensitivity is at most sensitivity, the separation also strengthens Meiburg's spectral result.

Formalizing it. The objects are finite and elementary, so a formal proof is a complete certificate of an explicit combinatorial construction. Huang's theorem has been formalized in Lean; a formal proof here would place the lower side of the gap on the same footing.

Difficulty

Known separations compose small gadgets, and composition multiplies both measures in a way that keeps the exponent at $2$. To break it, a recursion must grow the number of disjoint sensitive blocks by a factor $\approx 2M^2$ per level while ordinary sensitivity grows by only $\approx M$. The preprint's nested predicates on a labelled tournament (Section 2) achieve this, but a single bit flip can repair a failed gate condition only by changing two child predicates at once. Controlling sensitivity therefore requires tracking these joint sensitivities alongside ordinary ones at every input, not only at the input where the blocks are found (Proposition 3.1, p. 5), and the random edge labelling must exclude dense local configurations (Lemma 2.1, p. 3).

Formalization scope

• Inputs are Fin n → Bool; flip x B flips the coordinates in a Finset. sensitivity and blockSensitivity are Finset.sup over all inputs of the local counts; block families are finsets of pairwise disjoint nonempty finsets, each of which changes the value.
• The ratio is computed in ℝ. Nonconstancy (∃ x y, f x ≠ f y) forces $s(f)\ge1$, so the division is genuine.
• The extra clause $f(0)=0$ is not in the printed Theorem 1.1, but the constructed function satisfies it (the predicates vanish at zero, Lemma 2.3, p. 5, and the proof of Corollary 4.3 uses $f(0)=0$), so it is a faithful strengthening rather than an added assumption.
• Nothing is vacuous: $d\ge1$ is satisfiable and the conclusion asks for an explicit function.

Welcome contributions: a reusable library of Boolean-function complexity measures (sensitivity, block sensitivity, certificate complexity) and composition lemmas such as Lemma 4.2 (p. 9).

Selected references

• OpenAI, A superquadratic separation between sensitivity and block sensitivity, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-superquadratic-separation-between-sensitivity-and-block-sensitivity-September-25-2026/paper.pdf
• N. Nisan, CREW PRAMs and decision trees, STOC 1989. https://doi.org/10.1145/73007.73038
• N. Nisan, M. Szegedy, On the degree of Boolean functions as real polynomials, Comput. Complexity (1994). https://doi.org/10.1007/BF01263419
• D. Rubinstein, Sensitivity vs. block sensitivity of Boolean functions, Combinatorica (1995). https://doi.org/10.1007/BF01200762
• M. Virza, Sensitivity versus block sensitivity of Boolean functions, Inform. Process. Lett. (2011). https://doi.org/10.1016/j.ipl.2011.02.001
• A. Ambainis, X. Sun, New separation between s(f) and bs(f), arXiv:1108.3494 (2011). https://arxiv.org/abs/1108.3494v1
• A. Tal, Properties and applications of Boolean function composition, ITCS 2013. https://doi.org/10.1145/2422436.2422485
• A. Ambainis, K. Prūsis, A tight lower bound on certificate complexity in terms of block sensitivity and sensitivity, ECCC TR14-027 (2014). https://eccc.weizmann.ac.il/report/2014/027/revision/1/download
• H. Huang, Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture, Ann. of Math. 190 (2019). https://doi.org/10.4007/annals.2019.190.3.6
• J. Wellens, Relationships between the number of inputs and other complexity measures of Boolean functions, Discrete Analysis (2022). https://doi.org/10.19086/da.57741
• S. Aaronson, S. Ben-David, R. Kothari, et al., Degree vs. approximate degree and quantum implications of Huang's sensitivity theorem, STOC 2021. https://doi.org/10.1145/3406325.3451047
• A. Meiburg, Block sensitivity can exceed spectral sensitivity squared, arXiv:2608.00851 (2026). https://arxiv.org/html/2608.00851v1

Motivation: how short can an Egyptian fraction be?

An Egyptian-fraction expansion writes a positive rational number as a sum of distinct unit fractions $1/n$. Every fraction $a/b$ with $1\le a<b$ has one, by the greedy algorithm, but greedy expansions can be long. The basic quantitative question is how many terms are needed in the worst case for a fixed denominator $b$. Let $N(a,b)$ be the least length of an expansion of $a/b$ with denominators $\ge2$, and $N(b)=\max_{1\le a<b}N(a,b)$. Erdős proved in 1950 that $N(b)\ll\log b/\log\log b$, showed that $N(b)\gg\log\log b$ (already for $a=b-1$), and conjectured that the double-logarithmic order is correct. The question appears in Erdős–Graham's 1980 problem book and as Erdős Problem 304. The same circle of questions asks how many expansions of $1$ with exactly $k$ terms exist, and which integers can appear as denominators in them (Erdős Problem 293).

Timeline

• 1940 — Nakayama studies $N(a,b)$ through arithmetic criteria for expansions with few terms (Tohoku Math. J. 46).
• 1950 — Erdős reports de Bruijn's bound $N(b)\ll\log b/\log\log\log b$, improves it to $N(b)\ll\log b/\log\log b$, proves the lower bound $N(b)\gg\log\log b$, and conjectures the matching upper bound (Mat. Lapok 1950).
• 1980 — Erdős and Graham restate the problem and ask for estimates of the number of $k$-term expansions of $1$ and for the least missing denominator (Old and New Problems…).
• 1985 — Vose proves $N(b)\ll\sqrt{\log b}$ (Bull. LMS 17).
• 1990 — Tenenbaum and Yokota give length $(1+\varepsilon)\log b/\log\log b$ with denominators $O(b(\log b)^2\log\log b)$ (J. Number Theory).
• 2014–2021 — Konyagin proves a lower bound for the number $F(k)$ of $k$-term expansions of $1$ with $\log\log F(k)\gg k/\log k$ (Mat. Zametki); Elsholtz extends it to restricted denominators (Q. J. Math.); Elsholtz and Planitzer prove $\log\log F(k)=O(k)$ (Bull. LMS).
• 2026 — van Doorn and Tang prove $v(k)\ge\exp(ck^2)$ for the least missing denominator (Math. Proc. Cambridge Philos. Soc.).
• 2026 — An OpenAI preprint, Short Egyptian fractions (OpenAI Math Release, September 25, 2026), claims $N(b)\asymp\log\log b$, settling Erdős's conjecture, together with $\log\log F(k)\asymp k$ and $\log\log v(k)\asymp k$. It has not been peer reviewed, and its proofs are not formally verified.

Setting

For integers $1\le a<b$, an expansion of $a/b$ is a finite list $2\le n_1<\dots<n_k$ of integers with

$$\frac ab=\frac1{n_1}+\dots+\frac1{n_k}.$$

The fraction need not be in lowest terms and the denominators are unbounded. $N(a,b)$ is the least such $k$, and

$$N(b)=\max_{1\le a<b}N(a,b).$$

For $k\ge1$, $F(k)$ is the number of tuples $1\le n_1<\dots<n_k$ with $\sum 1/n_i=1$; $D_k$ is the set of integers $m\ge2$ occurring as some $n_i$ in such a tuple; and $v(k)=\min(\{2,3,\dots\}\setminus D_k)$.

Formalization targets

Goal: the optimal order of the shortest expansions (Theorem 1.1)

Every $a/b$ with $1\le a<b$ has an expansion, and there are absolute constants $c_1,c_2>0$ and $b_0$ such that for every $b\ge b_0$

$$c_1\log\log b\;\le\;N(b)\;\le\;c_2\log\log b .$$

No values of the constants are fixed. The goal statement is published on the platform with status Open.

Milestones

• Theorem 1.1, second formulation, stated with the definitions shared by the corollaries below.
• Corollary 1.2: there are $c,C>0$ and $k_0$ with $ck\le\log\log F(k)\le Ck$ for every $k\ge k_0$.
• Lemma 7.2: for $r\ge3$, any exact $r$-term expansion of $1$ containing the denominator $m$ can be lengthened to an exact $(r+1)$-term expansion still containing $m$; hence $D_r\subseteq D_{r+1}$.
• Proposition 8.1: for every $\varepsilon>0$, every sufficiently large $m$ is a denominator in an expansion of $1$ with at most $(257/\log2+\varepsilon)\log\log m$ terms.
• Corollary 1.3: eventually $\exp(\exp(k/600))\le v(k)\le1+k^{2^{k-1}}$, and $\log2/257\le\liminf_k \log\log v(k)/k\le\limsup_k\log\log v(k)/k\le\log2$.

Significance

The result itself. Theorem 1.1 answers Erdős's 1950 conjecture (Erdős Problem 304) affirmatively. The lower bound is classical; the content is the uniform upper bound for every numerator. As consequences, the paper determines the double-logarithmic order of the number of representations of $1$ (Corollary 1.2) and of the least integer absent from all $k$-term expansions of $1$ (Corollary 1.3), improving van Doorn–Tang's $\exp(ck^2)$ lower bound to a double exponential.

Formalizing it. All statements are elementary, with no analytic objects beyond logarithms, so a formal proof would give a complete machine-checked account of a problem from Erdős's list. The proof uses residue distribution of divisors, uniform divisor moments and a probabilistic construction, none of which is machine-checked. The elementary pieces — finiteness of $F(k)$, the denominator bound $n_i\le k^{2^{i-1}}$, and the padding lemma — are independently checkable and useful for other unit-fraction problems.

Difficulty

The greedy algorithm and divisor methods (Erdős; Tenenbaum–Yokota) lose a factor $\log b/(\log\log b)^2$ because they treat each numerator individually. The proof instead builds an auxiliary denominator $M$ for which almost every numerator in a large range has a short expansion, and descends through $O(\log\log b)$ ranges. The obstacle is that the exceptional numerators at each level could accumulate during the descent; controlling them requires a uniform moment bound for small divisors in shifted intervals. For Corollary 1.3, an additional difficulty is that the exact term $1/m$ must survive every operation that lengthens the expansion.

Formalization scope

• The goal uses OAI.ShortEgyptian: expansions are List ℕ that are strictly increasing (Pairwise (· < ·)), with entries $\ge2$ and rational sum $a/b$; minLength a b is an sInf and maxMinLength b the maximum over $1\le a<b$. The existence conjunct guarantees that sInf is taken over a nonempty set, so the bounds cannot hold through a junk value.
• The Problem337 milestones use Fin k → ℕ tuples (StrictMono, entries $\ge2$ for $a/b$ and $\ge1$ for expansions of $1$); $F(k)$ is Set.ncard, and $v(k)$ is sInf of the missing denominators. Finiteness of $D_k$ and of the expansion sets, which make these values meaningful, are separate statements in the proposal. In Corollary 1.3 the slopes are real liminf/limsup, accompanied by the explicit eventual bounds.
• Logarithms are Real.log; all constants are existential, apart from the explicit $600$, $257/\log 2$ and $\log2$ of the source.
• Needed infrastructure: divisor-counting and residue-distribution estimates, elementary prime-number bounds (the counting corollary uses the prime number theorem), and finite probabilistic constructions. Contributions proving the elementary pieces are welcome.

Selected references

• M. Nakayama, On the decomposition of a rational number into "Stammbrüche", Tohoku Math. J. 46 (1940). https://www.jstage.jst.go.jp/article/tmj1911/46/0/46_0_1/_article/-char/en
• P. Erdős, Az $1/x_1+1/x_2+\dots+1/x_n=a/b$ egyenlet egész számú megoldásairól, Mat. Lapok (1950). https://users.renyi.hu/~p_erdos/1950-02.pdf
• P. Erdős and R. L. Graham, Old and New Problems and Results in Combinatorial Number Theory, 1980. https://mathweb.ucsd.edu/~ronspubs/80_11_number_theory.pdf
• T. F. Bloom, Erdős Problem 304. https://www.erdosproblems.com/304
• M. D. Vose, Egyptian fractions, Bull. London Math. Soc. 17 (1985). https://doi.org/10.1112/blms/17.1.21
• G. Tenenbaum and H. Yokota, Length and denominators of Egyptian fractions, III, J. Number Theory (1990). https://doi.org/10.1016/0022-314X(90)90109-5
• S. V. Konyagin, Double exponential lower bound for the number of representations of unity by Egyptian fractions, Mat. Zametki (2014). https://doi.org/10.4213/mzm10417
• C. Elsholtz and S. Planitzer, Sums of four and more unit fractions and approximate parametrizations, Bull. London Math. Soc. (2021). https://doi.org/10.1112/blms.12452
• W. van Doorn and Q. Tang, The smallest denominator not contained in a unit fraction decomposition of 1 with fixed length, Math. Proc. Cambridge Philos. Soc. (2026). https://doi.org/10.1017/S0305004126102102
• OpenAI, Short Egyptian fractions, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 2; Corollaries 1.2–1.3, p. 3; Lemma 7.2, p. 26; Proposition 8.1, p. 27). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Short-Egyptian-fractions-September-25-2026/Short-Egyptian-fractions-September-25-2026.pdf