Combinatorics

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

Motivation

All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an $n$-vertex weighted directed graph. Floyd–Warshall solves it in $O(n^3)$ time, and for decades no algorithm beat $n^{3-\delta}$ for any constant $\delta>0$ on graphs with polynomially bounded integer weights. In 2026, Alman and Vassilevska Williams (arXiv:2610.06783) gave a deterministic $O(n^{2.99942})$ algorithm, the campaign's first entry. Later entries tightened the accounting to $2.9983$ and $2.99791$.

This entry records the deterministic exponent $2.996001$. It roughly doubles the saving below $3$ compared with $2.99791$, and it matches what was previously only known with randomized hashing.

Setting

The model is the campaign's fixed deterministic word RAM (foundation mission: Truly Subcubic APSP on a Word RAM). A finite program uses add, subtract and multiply modulo $2^W$, indirect load and store, a sign branch, and accept or reject, on words of width $W \ge b(\log_2 n + 1)$. Inputs have integer weights of absolute value at most $n^\kappa$ for a fixed $\kappa$, and there are no negative cycles. The machine has no source of randomness; the algorithm behind this entry is deterministic.

Formalization target

The goal is the campaign template with the value $2.996001$:

$$\texttt{TrulySubcubicAPSP.APSP.SolvedInTime}\ 2.996001,$$

which says there is a deterministic word-RAM program that solves APSP in $O(n^{2.996001})$ steps.

How the bound arises

The algebraic core is the thin-product data structure of Alman and Vassilevska Williams: for an $N\times D$ by $D\times N$ integer product it answers requested entries $W$ in $\tilde O(N^2D^{-\Gamma} + N D^{a} + |W| D^{q})$. Two local refinements of that construction sharpen the exponents:

1. Pruned encodings. Encoding branches with more than $m$ copies of the distinguished symbol $P_0$ are never materialized, giving $a(c) = \bigl(\tfrac12 cH(1/c) + (c-1)\ln 3\bigr)/\ln 4$.
2. Exact binomial tail. The box preprocessing is bounded by its actual binomial sum, giving $\Gamma(c,\theta) = \bigl(cH(1/c) - cH((1-\theta)/c) - \theta\ln 9\bigr)/\ln 4$, with $q(\theta) = \bigl(H(\theta)+\theta\ln 9\bigr)/\ln 4$.

The main new step is a deterministic filtering reduction. Moduli are chosen one small prime factor at a time, using exact thin-product witness counts to certify positive answers and to eliminate whole blocks of unresolved queries. Repeated filtering removes the need to scan individual modular witnesses, which was the bottleneck of earlier deterministic reductions (the prime-by-prime idea is suggested in footnote 9 of the source paper, after Fischer, Kaliciak and Polak). With middle blocks of size $n^{\varepsilon/2}$ this yields all-edges Exact Triangle in $n^{3-\delta+o(1)}$, where

$$\delta = \min\{\varepsilon\Gamma,\ 1-\varepsilon a,\ \varepsilon(1/2-q)\},$$

and deterministic bit scaling transfers the bound to min-plus product and APSP with polylogarithmic overhead.

The exact rational parameters $c = 21.2733$, $\theta = 0.111731$ and $\varepsilon = 0.056846$ satisfy the thin regime $\varepsilon(a+\Gamma) < 1$ with margin $1.16\times10^{-6}$, and give $\delta > 0.00399928$. Hence APSP runs in $n^{2.99600072+o(1)}$, and the gap $2.996001 - 2.99600072 > 0$ absorbs the subpolynomial factor.

Significance

This is the first deterministic entry near $2.996$. Earlier analyses reached about $2.99601$ only by repeating random-prime hashing, which this word-RAM model cannot express. The deterministic filtering closes that gap.

Selected references

• J. Alman and V. Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs (2026). https://arxiv.org/abs/2610.06783
• Deterministic APSP in $O(n^{2.996001})$: an explicit refinement of the thin-product method, technical note, 6 October 2026. This is the source of $2.996001$ and has not been peer reviewed.

Motivation

A submodular function on a finite set $V$ is a function $f$ on subsets of $V$ with $f(X \cup Y) + f(X \cap Y) \le f(X) + f(Y)$. Minimizing such a function is one of the central tractable problems of combinatorial optimization: it contains minimum cuts in directed graphs, matroid intersection and polymatroid problems, and many scheduling and facility-location subproblems. Grötschel, Lovász and Schrijver showed in 1981 that it can be done in polynomial time with the ellipsoid method; in 2000, Schrijver (JCTB 80, 346–355) and, simultaneously, Iwata, Fleischer and Fujishige (J. ACM 48, 2001) gave the first combinatorial strongly polynomial algorithms.

In many applications the function is not defined on all subsets of $V$ but only on a ring family: a collection closed under union and intersection, such as the order ideals of a precedence relation in scheduling, or the sets of a closure system. The last section of Schrijver's paper (§6, pp. 353–354) shows that nothing is lost: any algorithm minimizing submodular functions on all subsets of $V$ also minimizes a submodular function given only on a ring family. This mission formalizes that reduction.

Setting

Let $V$ be a finite set. A collection $\mathcal C$ of subsets of $V$ is a ring family if $X \cup Y \in \mathcal C$ and $X \cap Y \in \mathcal C$ whenever $X, Y \in \mathcal C$. A real function $f$ is submodular on $\mathcal C$ if

$$f(X \cup Y) + f(X \cap Y) \le f(X) + f(Y) \qquad (X, Y \in \mathcal C).$$

Following the paper, $\mathcal C$ is normalized: $\emptyset \in \mathcal C$, $V \in \mathcal C$, and $M_u \ne M_v$ for all $u \ne v$, where $M_v$ is the smallest set of $\mathcal C$ containing $v$. (Elements with the same $M_v$ can be identified.) Under this normalization $\mathcal C$ is the family of lower ideals of a partial order on $V$.

For $X \subseteq V$, the closure $\overline X$ is the smallest set of $\mathcal C$ containing $X$. For $v \in V$, $L_v$ is the largest set of $\mathcal C$ not containing $v$. The paper defines weights

$$c(v) := \max\{0,\ f(L_v) - f(L_v \cup \{v\})\} \qquad (23)$$

with the modular extension $c(X) := \sum_{v \in X} c(v)$, and the function on all subsets of $V$

$$g(X) := f(\overline X) + c(\overline X) \qquad (X \subseteq V). \qquad (26)$$

In Lean, $V$ is a type with [Fintype V] [DecidableEq V], subsets are Finset V, $\mathcal C$ is C : Set (Finset V), and the objects above are IsRingFamily C, SubmodularOn C f, closure C X, M C v, L C v, cw C f v (for $c(v)$), csum C f X (for $c(X)$) and g C f X, all in the namespace SchrijverSFM.Ring.

Formalization targets

Goal: the reduction

Under the normalization above, for $f$ submodular on $\mathcal C$:

$$g \text{ is submodular on all subsets of } V,$$

and, if $U \subseteq V$ minimizes $g(U) - c(U)$ over all subsets of $V$, then $\overline U \in \mathcal C$ and

$$f(\overline U) \le f(T) \qquad \text{for all } T \in \mathcal C.$$

Both conjuncts are needed: the second alone follows almost from the definitions, while the first is what makes an all-subsets algorithm applicable to $g - c$ in the first place.

Milestones

1. $\mathcal C$ is the collection of all lower ideals of some partial order on $V$ (p. 353).
2. $L_v$ is the largest set in $\mathcal C$ not containing $v$, equal to the union of the $M_u$ not containing $v$, and $L_v \cup \{v\} \in \mathcal C$ (p. 353, (23)).
3. The one-element step (25): $f(X) \le f(Y) + c(v)$ for $X, Y \in \mathcal C$, $Y = X \cup \{v\}$, $v \notin X$.
4. Monotonicity (24): $f(Y) + c(Y) \ge f(X) + c(X)$ for $X \subseteq Y$ in $\mathcal C$.
5. The closure identities $\overline X \cup \overline Y = \overline{X \cup Y}$ and $\overline X \cap \overline Y \supseteq \overline{X \cap Y}$.
6. Display (27): $g$ is submodular.
7. Transfer of minimizers: if $U$ minimizes $g - c$ over $2^V$, then $\overline U$ minimizes $f$ over $\mathcal C$.

Significance

The reduction means that a single algorithm for unconstrained submodular minimization serves for every ring family, given only the sets $M_v$. This is how ring-family constrained problems (for example minimum-cost closures and precedence-constrained scheduling objectives) are routinely handed to general submodular-minimization codes, and it is the standard justification for stating submodular minimization algorithms over $2^V$ only.

On the formal side, the mission produces a small reusable layer on ring families of finite sets (closure operator, the lower-ideal representation, the largest set avoiding an element) together with the monotonization trick (24), which is of independent use whenever a function on a lattice of sets has to be made monotone by a modular correction. The result is classical and its proof in the paper is complete; to our knowledge no machine-checked version exists. Companion mission I of this series formalizes the algorithm of §§2–5 itself; this mission does not depend on it, since the algorithm enters only as the hypothesis that a minimizer $U$ of $g - c$ is given.

Difficulty

Every step is elementary, but two points are easy to get wrong. First, (24) is proved on the page by assuming $Y = X \cup \{v\}$; reducing the general case $X \subseteq Y$ to such one-element steps inside $\mathcal C$ requires the normalization $M_u \ne M_v$: without it a ring family can jump by more than one element (for $\mathcal C = \{\emptyset, V\}$ with $|V| = 2$ the inequality (24) fails for suitable $f$). Second, the weights $c(v)$ evaluate $f$ at $L_v \cup \{v\}$, which belongs to $\mathcal C$ only because of the same normalization; a formalization that drops it lets values of $f$ outside $\mathcal C$ leak into $c$ and $g$. The submodularity proof (27) also needs the asymmetric closure facts — equality for unions but only containment for intersections — which is exactly why the monotonicity (24) is required.

Formalization scope

• $V$ is a finite type with decidable equality; subsets are Finset V; $\mathcal C$ is a Set (Finset V).
• $f$ is a real function on all of Finset V; only its values on $\mathcal C$ matter, and under the hypotheses no other value enters $c$, $g$ or the conclusions. The paper allows any ordered field; the formalization uses $\mathbb R$.
• The normalization of p. 353 is assumed as hypotheses: ∅ ∈ C, Finset.univ ∈ C, and M C u ≠ M C v for u ≠ v. No hypothesis $f(\emptyset) = 0$ is made; §6 does not use it.
• The closure is the intersection (Finset.inf) of the sets of $\mathcal C$ containing $X$, and $L_v$ the union (Finset.sup) of the sets of $\mathcal C$ avoiding $v$; their default values on an empty family are never reached under the hypotheses.
• $c(X)$ is the modular extension $\sum_{v \in X} c(v)$; the $\max\{0, \cdot\}$ in (23) is kept, so $c \ge 0$.
• Submodularity of $g$ on all subsets is the published platform definition NonmonotoneSubmod.Shared.Submodular.
• Not formalized: the running-time claims of §6 ("we can find $c$ by $2|V|$ oracle calls", strongly polynomial time) and the oracle model; there is no machine model.
• The goal does not assume (24) or (27), and it is not the minimizer-transfer statement alone, which would be near-definitional.

Contributions welcome: proofs of the milestones in the order listed, general lemmas on closure operators of ring families of Finsets, and the lower-ideal representation, which is reusable beyond this mission.

Selected references

• A. Schrijver, A combinatorial algorithm minimizing submodular functions in strongly polynomial time, J. Combin. Theory Ser. B 80 (2000), 346–355. https://doi.org/10.1006/jctb.2000.1989
• S. Iwata, L. Fleischer, S. Fujishige, A combinatorial strongly polynomial algorithm for minimizing submodular functions, J. ACM 48 (2001), 761–777. https://doi.org/10.1145/502090.502096
• M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981), 169–197. https://doi.org/10.1007/BF02579273