All missions

Motivation

How efficiently can the edges of a graph be split into cycles? Some single edges must be allowed, since a forest has no cycles at all, and a tree on $n$ vertices already needs $n-1$ single-edge parts. The Erdős–Gallai cycle decomposition conjecture asserts that this is essentially the only obstruction: every graph on $n$ vertices can have its edge set partitioned into $O(n)$ simple cycles and single edges. Equivalently, every graph with all degrees even partitions into $O(n)$ cycles. The problem is a basic question about edge decompositions, and the partial bounds $O(n\log n)$, $O(n\log\log n)$ and $O(n\log^*n)$ trace several decades of progress on it.

This mission asks for a formal proof of the linear bound, 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

• 1966 — Erdős, Goodman and Pósa record the problem and an $O(n\log n)$ bound, distinguishing covers from edge-disjoint partitions (Canad. J. Math. 1966).
• 1968 — Lovász: every graph on $n$ vertices partitions into at most $\lfloor n/2\rfloor$ paths and cycles (On covering of graphs, 1968).
• 1985 — Pyber shows that $n-1$ cycles and edges suffice to cover (not partition) every graph (Combinatorica 1985).
• 2014 — Conlon, Fox and Sudakov prove $O(n\log\log n)$ in general and linear bounds for random graphs and graphs of linear minimum degree (RSA 2014).
• 2015–2021 — Asymptotically sharp counts for random graphs (Korándi–Krivelevich–Sudakov, CPC 2015); $(3/2+\delta)n$ for dense graphs (Girão–Granet–Kühn–Osthus, J. LMS 2021).
• 2024 — Bucić and Montgomery prove $O(n\log^*n)$ (Adv. Math. 2024).
• 2025 — Akbari, Aloni, Beikmohammadi and Clow prove $n-1$ for maximum degree at most four (arXiv:2509.01901).
• September 2026 — The OpenAI preprint claims the linear bound (Theorem 1.1, p. 1).

Setting

A finite simple graph $G$ has vertex set of size $n$ and edge set $E(G)$ of unordered pairs of distinct vertices. A cycle is a closed walk of length at least $3$ with no repeated vertices except the endpoints; its edge set is the set of edges it traverses. A cycle-and-edge decomposition of $G$ into $k$ parts is a family $E_1,\dots,E_k$ of pairwise disjoint subsets of $E(G)$ with union $E(G)$, where each $E_i$ is either the edge set of a cycle of $G$ or a single edge of $G$. Parts may share vertices; isolated vertices need not be covered; for an edgeless graph $k=0$ is allowed.

Formalization targets

Goal: Theorem 1.1 (p. 1)

There is an absolute constant $C>0$ such that for every $n$ and every simple graph $G$ on $n$ vertices,

$$G\ \text{has a cycle-and-edge decomposition into at most } Cn \text{ parts}.$$

The value of $C$ is left unspecified, which keeps the goal stable under future improvements of the constant (the best possible constant is at least $3/2$, by complete bipartite examples).

Significance

The result itself. The order $n$ is optimal (trees). The theorem implies that every Eulerian graph (all degrees even) partitions into $O(n)$ cycles (Corollary 1.2, p. 2), and via known equivalences it gives the sharp $\Delta(G)/2+\delta n$ cycle bound for Eulerian graphs satisfying a large-cut condition. It removes the last iterated-logarithm loss from the Bucić–Montgomery bound.

Formalizing it. The statement uses only Mathlib's SimpleGraph.Walk.IsCycle and edge sets, so it is a clean combinatorial target. A complete development needs Lovász's path-cycle decomposition theorem, the Aharoni–Haxell hypergraph matching theorem, expansion and routing lemmas, and binomial tail bounds; all are reusable in extremal graph theory. No machine-checked proof of any $o(n\log n)$ bound is known.

Difficulty

Covering is easy (Pyber's $n-1$ bound), but a cover does not yield a partition: deleting repeated edges can break cycles into many paths. For partitions, the standard strategy decomposes the graph into expanding pieces at a sequence of scales, and paying a cost proportional to the full order at every scale accumulates a factor from the number of scales — this is where the $\log\log n$ and $\log^*n$ losses come from. The preprint (Introduction, pp. 2–3) charges the work on a prefix of scales to a single expanding layer and saves a fixed fraction of vertices by identifying pairs, then lifts quotient cycles back with reserved edge-disjoint routes (Lemma 3.1, p. 5); keeping a separate assignment for each original edge throughout is what makes the induction close.

Formalization scope

• Graphs are SimpleGraph (Fin n) for arbitrary n (including 0 and edgeless graphs).
• CycleOrSingleEdge G s: either $s$ is p.edgeSet for some p : G.Walk v v with p.IsCycle (Mathlib cycles have length at least $3$), or $s=\{e\}$ for an edge $e\in G$.
• EdgeDecomposition G k: parts indexed by Fin k, each a cycle or single edge, pairwise disjoint, with union G.edgeSet.
• MainStatement: $\exists C>0,\ \forall n\ \forall G,\ \exists k,$ EdgeDecomposition G k $\wedge\ k\le Cn$.
• Trivializations are ruled out: parts must be nonempty edge sets of the required shape and must exactly partition the edge set, so the count $k$ is a genuine count.

Selected references

• OpenAI, A linear cycle-and-edge decomposition of every graph, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026/main.pdf
• P. Erdős, A. W. Goodman, L. Pósa, The representation of a graph by set intersections, Canad. J. Math. 18 (1966). https://doi.org/10.4153/CJM-1966-014-3
• L. Lovász, On covering of graphs, Theory of Graphs (Proc. Colloq. Tihany, 1966), 1968.
• L. Pyber, An Erdős–Gallai conjecture, Combinatorica 5 (1985). https://doi.org/10.1007/BF02579444
• D. Conlon, J. Fox, B. Sudakov, Cycle packing, Random Structures Algorithms (2014). https://doi.org/10.1002/rsa.20574
• D. Korándi, M. Krivelevich, B. Sudakov, Decomposing random graphs into few cycles and edges, Combin. Probab. Comput. (2015). https://doi.org/10.1017/S0963548314000844
• A. Girão, B. Granet, D. Kühn, D. Osthus, Path and cycle decompositions of dense graphs, J. London Math. Soc. (2021). https://doi.org/10.1112/jlms.12455
• M. Bucić, R. Montgomery, Towards the Erdős–Gallai cycle decomposition conjecture, Adv. Math. (2024). https://doi.org/10.1016/j.aim.2023.109434
• R. Aharoni, P. Haxell, Hall's theorem for hypergraphs, J. Graph Theory 35 (2000). https://doi.org/10.1002/1097-0118(200010)35:2<83::AID-JGT2>3.0.CO;2-V
• S. Akbari, J. Aloni, A. Beikmohammadi, A. Clow, Tight bounds for cycle-edge decompositions and covers, arXiv:2509.01901 (2025). https://arxiv.org/abs/2509.01901v2

Motivation: high-dimensional analogues of expander graphs

An expander graph is a sparse graph in which every set of vertices has a large edge boundary relative to its size. Expanders with bounded degree are a basic tool across combinatorics, computer science and group theory. High-dimensional expanders are simplicial complexes that extend this behavior to faces of every dimension, and coboundary expansion over $\mathbb F_2$ is the strongest of the standard notions: the coboundary of any set of $i$-faces must be large unless the set is already close to a coboundary. Gromov connected such filling inequalities with topological overlap of maps to Euclidean space. The basic existence question is whether there are arbitrarily large complexes of fixed dimension with bounded vertex degree and uniform coboundary expansion in every degree.

Background and timeline

• 2006–2009 — Linial–Meshulam (Combinatorica 2006) and Meshulam–Wallach (Random Struct. Alg. 2009) develop the coisoperimetric viewpoint through random complexes.
• 2010 — Gromov connects cohomological filling inequalities with topological overlap and asks for large complexes with bounded vertex incidence and uniform filling bounds (GAFA 2010, §§2.3–2.5, 2.14).
• 2015 — Lubotzky and Meshulam construct random Latin-square coboundary expanders in dimension two, with bounded codimension-one degree (Adv. Math. 2015).
• 2016 — Kaufman, Kazhdan and Lubotzky prove cosystolic and topological expansion for two-dimensional skeleta of Ramanujan complexes, with bounded vertex degree (GAFA 2016).
• 2019 — Lubotzky, Luria and Rosenthal construct random Steiner-system coboundary expanders in every dimension, again with bounded codimension-one degree but growing vertex degree (Discrete Comput. Geom. 2019).
• 2024 — Evra and Kaufman obtain bounded-degree cosystolic expanders in every dimension (JAMS 2024); cosystolic expansion allows nonzero cohomology.
• 2025 — Chapman and Lubotzky prove existence of bounded-degree two-dimensional coboundary expanders over $\mathbb F_2$ and state the general problem (Adv. Math. 2025, Problem 1.3, Theorem 1.9); Kaufman–Oppenheim–Weinberger (arXiv:2411.02819) prove degree-one coboundary expansion for coset complexes; Oppenheim and Valentiner-Branth prove cosystolic expansion for Kac–Moody–Steinberg complexes (arXiv:2504.05823).
• 2026 — The OpenAI preprint Bounded-degree coboundary expanders in every dimension (OpenAI Math Release, September 24, 2026) claims bounded-degree $\mathbb F_2$ coboundary expanders in every dimension $d\ge3$. It has not been peer reviewed and its theorem is not formally verified.

Setting

A finite simplicial complex $Y$ is a downward-closed family of finite sets (faces) of vertices; $Y(i)$ denotes the faces with $i+1$ vertices. $Y$ is pure of dimension $s$ if it has $s$-faces and every face lies in one. An $i$-cochain is a function $f:Y(i)\to\mathbb F_2$; its coboundary is $(\delta_if)(\tau)=\sum_{\sigma\subset\tau,\,|\sigma|=i+1}f(\sigma)$. Let $B^i(Y)=\operatorname{im}\delta_{i-1}$, with $B^0(Y)$ the constant functions. Faces are weighted by

$$w_i(\sigma)=\frac{\#\{\tau\in Y(s):\sigma\subseteq\tau\}}{\binom{s+1}{i+1}|Y(s)|},\qquad \|f\|_{i}=\sum_{\sigma:\,f(\sigma)\ne0}w_i(\sigma),$$

so $\|f\|_i$ is the probability that $f$ is nonzero on a random $i$-face of a uniformly random top face, and $\operatorname{dist}_i(f,A)=\min_{a\in A}\|f-a\|_i$.

In Lean (namespace OAI.CoboundaryExpanders), a Complex has vertex set Fin vertexCount, a Finset of faces that is downward closed and contains every singleton; Pure, Connected (connected $1$-skeleton), weight, norm, coboundary, coboundaries and distance follow these definitions, and topDegree X d v counts $d$-faces containing $v$.

Formalization targets

Goal: bounded-degree coboundary expanders (Theorem 1.1)

For every $d\ge3$ there are $D<\infty$, $\varepsilon>0$ and finite connected pure $d$-dimensional complexes $X_m$ with $|X_m(0)|\to\infty$, every vertex in at most $D$ faces of dimension $d$, and

$$\|\delta_if\|_{X_m,i+1}\ \ge\ \varepsilon\,\operatorname{dist}_{X_m,i}\bigl(f,B^i(X_m)\bigr)\qquad(f\in C^i(X_m;\mathbb F_2),\ 0\le i<d),$$

with constants independent of $m$, $i$ and $f$. The Lean goal is published on the platform with status Open.

Significance

The result itself. Together with the classical graph case and the Chapman–Lubotzky two-dimensional theorem, Theorem 1.1 gives bounded-degree $\mathbb F_2$ coboundary expanders in every positive dimension, answering the existence question in the form stated by Chapman and Lubotzky. Earlier bounded-vertex-degree constructions gave cosystolic expansion, which permits nonvanishing cohomology, or degree-one expansion only; earlier coboundary expanders in all dimensions had vertex degrees growing with size. Coboundary expansion in all degrees implies vanishing $\mathbb F_2$-cohomology below the top dimension, the property Gromov related to topological overlap.

Formalizing it. The definitions are elementary finite combinatorics, so the statement is completely precise; the proof combines group-theoretic coset complexes over $\mathrm{SL}_N(k[t])$, congruence quotients and a quantitative cosystolic input. A formal proof would require formalizing that input (Oppenheim–Valentiner-Branth), which is substantial.

Difficulty

Coboundary expansion requires two things at once: a quantitative isoperimetric inequality against cocycles (cosystolic expansion) and exact vanishing of $H^i(X_m;\mathbb F_2)$ for every $i<d$. Random constructions give vanishing cohomology but force growing vertex degree; algebraic bounded-degree constructions (Ramanujan complexes, coset complexes) give the quantitative inequality but typically have nonzero cohomology that cannot be controlled uniformly. A cocycle that is not a coboundary has zero coboundary and positive distance, so any nonzero cohomology class destroys the inequality. The difficulty is a family of bounded-degree complexes whose cohomology vanishes in every degree below $d$, uniformly along the tower.

Formalization scope

• Vertices are Fin vertexCount and every vertex is a face; faces are Finsets, and an $i$-face has exactly $i+1$ vertices.
• Purity requires at least one $d$-face; connectivity is of the $1$-skeleton and requires a nonempty vertex set, so empty or disconnected complexes do not satisfy the hypotheses.
• Cochains are ZMod 2-valued; $B^0$ is the constant cochains (reduced cohomology in degree $0$). Distance is a real sInf over the image of a nonempty finite set, hence a minimum.
• The inequality is required for every $i<d$ and every cochain, with $D$ and $\varepsilon$ chosen before the sequence and depending only on $d$. Only $d\ge3$ is asserted; dimensions $1$ and $2$ are separate known results.
• Needed infrastructure: coset complexes, local spectral expansion and cosystolic expansion theorems, and cohomology of congruence quotients. A library of simplicial cochain complexes over $\mathbb F_2$ would be reusable for many high-dimensional-expansion problems.

Selected references

• N. Linial and R. Meshulam, Homological connectivity of random 2-complexes, Combinatorica 26 (2006). https://doi.org/10.1007/s00493-006-0027-9
• R. Meshulam and N. Wallach, Homological connectivity of random k-dimensional complexes, Random Structures Algorithms 34 (2009). https://doi.org/10.1002/rsa.20238
• M. Gromov, Singularities, expanders and topology of maps. Part 2, Geom. Funct. Anal. 20 (2010), 416–526. https://doi.org/10.1007/s00039-010-0073-8
• A. Lubotzky and R. Meshulam, Random Latin squares and 2-dimensional expanders, Adv. Math. 272 (2015). https://doi.org/10.1016/j.aim.2014.12.015
• T. Kaufman, D. Kazhdan and A. Lubotzky, Isoperimetric inequalities for Ramanujan complexes and topological expanders, Geom. Funct. Anal. 26 (2016). https://doi.org/10.1007/s00039-016-0362-y
• A. Lubotzky, Z. Luria and R. Rosenthal, Random Steiner systems and bounded degree coboundary expanders of every dimension, Discrete Comput. Geom. 62 (2019). https://doi.org/10.1007/s00454-018-9991-2
• S. Evra and T. Kaufman, Bounded degree cosystolic expanders of every dimension, J. Amer. Math. Soc. 37 (2024). https://doi.org/10.1090/jams/1019
• M. Chapman and A. Lubotzky, Stability of homomorphisms, coverings and cocycles II: Examples, applications and open problems, Adv. Math. 463 (2025). https://doi.org/10.1016/j.aim.2025.110117
• T. Kaufman, I. Oppenheim and S. Weinberger, Coboundary expansion of coset complexes, arXiv:2411.02819 (STOC 2025). https://arxiv.org/abs/2411.02819v1
• I. Oppenheim and I. Valentiner-Branth, New cosystolic high-dimensional expanders from KMS groups, arXiv:2504.05823. https://arxiv.org/abs/2504.05823v2
• OpenAI, Bounded-degree coboundary expanders in every dimension, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Bounded-degree-coboundary-expanders-in-every-dimension-September-24-2026/paper.pdf

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

A spanning tree keeps a graph connected with as few edges as possible. A spanning tree is thin if, in addition, it uses only a small fraction of the edges of every cut. Thin trees were introduced as a tool for the asymmetric traveling salesman problem (ATSP): Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that thin trees, together with cost control, can be augmented cheaply into tours, which gave an $O(\log n/\log\log n)$-approximation (doi:10.1287/opre.2017.1603). Goddyn's thin tree conjecture asks whether high edge connectivity alone forces an $\varepsilon$-thin spanning tree, independently of the number of vertices; the strong form asks for thinness $C/k$ in a $k$-edge-connected graph.

Background. Goddyn recorded the conjecture in a 2004 problem list. The Nash–Williams–Tutte theorem (1961) gives $\lfloor k/2\rfloor$ edge-disjoint spanning trees in a $k$-edge-connected graph (doi:10.1112/jlms/s1-36.1.445, doi:10.1112/jlms/s1-36.1.221), so each cut is used about $2/k$ times on average, but no single tree need be good for every cut. Oveis Gharan and Saberi proved the bound for planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan obtained thinness $\mathrm{poly}(\log\log n)/k$ in general (2015, arXiv:1411.4613), using the Marcus–Spielman–Srivastava interlacing-families method (doi:10.4007/annals.2015.182.1.8). Klein and Olver handled any prescribed laminar family of cuts (2023, doi:10.1109/FOCS57990.2023.00011), and Klein, Olver and Yeoh controlled all near-minimum cuts (2026, doi:10.4230/LIPIcs.ICALP.2026.129). Constant-factor ATSP approximations were obtained by other means (Svensson–Tarnawski–Végh 2020, doi:10.1145/3424306; Traub–Vygen 2022, doi:10.1137/20M1339313), but the thin tree question stayed unresolved.

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the strong thin tree conjecture.

Setting

Let $G=(V,E)$ be a finite undirected multigraph without loops; parallel edges are counted separately. For a nonempty proper subset $\varnothing\ne S\subsetneq V$, let $\delta_G(S)$ be the set of edges with exactly one endpoint in $S$. $G$ is $k$-edge-connected if $|\delta_G(S)|\ge k$ for every such $S$. For an edge set $T\subseteq E$, $\delta_T(S)=\delta_G(S)\cap T$. A spanning tree $T$ is $\alpha$-thin if $|\delta_T(S)|\le\alpha|\delta_G(S)|$ for every nonempty proper $S$.

Formalization targets

Goal: Theorem 1.1 (strong thin trees)

There is a universal constant $C>0$ such that for every $k\ge1$, every finite loopless $k$-edge-connected multigraph with at least two vertices has a spanning tree $T$ with

$$|\delta_T(S)|\le\frac{C}{k}\,|\delta_G(S)|\qquad(\varnothing\ne S\subsetneq V).$$

Lean: OAI.StrongThinTree.strongThinTree, open on the platform.

Significance

The order $1/k$ is optimal (two vertices joined by $k$ parallel edges). The theorem would settle both Goddyn's thin tree conjecture and its strong form, removing the $\mathrm{poly}(\log\log n)$ loss of Anari–Oveis Gharan. It shows that connectivity alone controls all cuts at once, and gives a structural route to ATSP integrality-gap bounds through thin trees. An algorithmic version (deterministic polynomial-time construction) is the subject of the companion mission in this family. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Averaging over a Nash–Williams–Tutte packing controls each cut on average but not all cuts simultaneously: there are exponentially many cuts and a union bound over them loses a factor depending on $n$. Spectral approaches control all cuts via a matrix inequality, but spectrally thin trees need not exist when some edges have large effective resistance, which is why previous spectral arguments lost $\log\log n$ factors. One must instead keep a large tree packing on low-resistance edges through a sequence of sparsifications whose relative losses stay bounded.

Formalization scope

• MultiGraph n m: vertices Fin n, edges Fin m with endpoint maps and a looplessness proof; parallel edges are distinct edges.
• cut G T S: the edges of T with exactly one endpoint in S. Connected G T: every nonempty proper S is crossed by T. SpanningTree G T: T connected and every proper deletion disconnects.
• EdgeConnected G k: every nonempty proper cut has at least k edges.
• MainStatement: ∃ C > 0, ∀ k ≥ 1, ∀ n ≥ 2, ∀ G k-edge-connected, ∃ T spanning tree, ∀ S nonempty proper, |cut T S| ≤ (C/k)|cut G S| (real arithmetic).

Needed infrastructure: graph Laplacians and effective resistance, the Nash–Williams–Tutte theorem, the Marcus–Spielman–Srivastava mixed-characteristic-polynomial bound, and a Brouwer-type fixed point theorem (the paper proves the finite-dimensional case via Sperner's lemma). Contributions formalizing Theorem 2.3 (Nash–Williams–Tutte), Theorem 3.2, Theorem 4.1, Proposition 6.2 or Theorem A.1 are welcome.

Selected references

• OpenAI, The strong thin tree conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-strong-thin-tree-conjecture-September-23-2026/paper.pdf
• L. A. Goddyn, Some open problems I like, problem list, 2004.
• A. Asadpour, M. X. Goemans, A. Mądry, S. Oveis Gharan, A. Saberi, An O(log n/log log n)-approximation algorithm for the asymmetric traveling salesman problem, Oper. Res., 2017. https://doi.org/10.1287/opre.2017.1603
• N. Anari, S. Oveis Gharan, Effective-resistance-reducing flows, spectrally thin trees, and asymmetric TSP, FOCS, 2015. https://arxiv.org/abs/1411.4613
• A. W. Marcus, D. A. Spielman, N. Srivastava, Interlacing families II: mixed characteristic polynomials and the Kadison–Singer problem, Ann. of Math., 2015. https://doi.org/10.4007/annals.2015.182.1.8
• S. Oveis Gharan, A. Saberi, The asymmetric traveling salesman problem on graphs with bounded genus, SODA, 2011. https://doi.org/10.1137/1.9781611973082.75
• N. Klein, N. Olver, Thin trees for laminar families, FOCS, 2023. https://doi.org/10.1109/FOCS57990.2023.00011
• N. Klein, N. Olver, Z. S. Yeoh, Thin trees for near minimum cuts, ICALP, 2026. https://doi.org/10.4230/LIPIcs.ICALP.2026.129
• C. St. J. A. Nash-Williams, Edge-disjoint spanning trees of finite graphs, J. London Math. Soc., 1961. https://doi.org/10.1112/jlms/s1-36.1.445

Motivation: the logarithmic factor in $r(s,t)$

For integers $s,t\ge2$ the Ramsey number $r(s,t)$ is the least $N$ such that every simple graph on $N$ vertices contains a clique of order $s$ or an independent set of order $t$. Ramsey's theorem guarantees these numbers are finite. In the off-diagonal regime, $s$ is fixed and $t\to\infty$; the classical upper bounds give $r(s,t)=O_s\!\left(t^{s-1}/(\log t)^{s-2}\right)$, while for a long time lower-bound constructions did not reach the power $t^{s-1}$. Once the power was settled, the remaining question was the power of $\log t$.

Timeline

• 1930 — Ramsey proves finiteness of these numbers (Ramsey 1930, Thm B).
• 1935 — Erdős and Szekeres: $r(s,t)\le\binom{s+t-2}{s-1}=O_s(t^{s-1})$ (Erdős–Szekeres 1935).
• 1977 — Spencer's local-lemma construction: $r(s,t)=\Omega_s\big((t/\log t)^{(s+1)/2}\big)$ (Spencer 1977).
• 1980 — Ajtai, Komlós and Szemerédi: $r(s,t)=O_s\big(t^{s-1}/(\log t)^{s-2}\big)$ (AKS 1980).
• 1995 — Kim: $r(3,t)=\Theta(t^2/\log t)$ (Kim 1995).
• 2001 — Li, Rousseau and Zang: upper leading coefficient $1+o(1)$ (Li–Rousseau–Zang 2001).
• 2010 — Bohman and Keevash, via the random $K_s$-free process: $r(s,t)=\Omega_s\big(t^{(s+1)/2}(\log t)^{1/(s-2)-(s+1)/2}\big)$ (Bohman–Keevash 2010, Thm 1.2).
• 2024 — Mubayi and Verstraëte show that suitable optimally pseudorandom $K_s$-free graphs would give $t^{s-1}/(\log t)^{2s-4}$ (Mubayi–Verstraëte 2024); Mattheus and Verstraëte prove $r(4,t)=\Omega(t^3/(\log t)^4)$ (Mattheus–Verstraëte 2024).
• 2026 — Bradač proves $r(s,t)\ge c_s\,t^{s-1}/(\log t)^{2s-4}$ for every $s\ge3$, fixing the polynomial exponent (Bradač 2026, Thm 1.1).
• 2026 — An OpenAI preprint, Sharp logarithmic exponents for fixed off-diagonal Ramsey numbers (OpenAI Math Release, September 24, 2026), claims $r(s,t)=t^{s-1}/(\log t)^{s-2+o(1)}$ for every fixed $s\ge6$; a companion preprint treats $s=5$. Neither has been peer reviewed, and the main theorem is not formally verified.

Setting

A graph on $N$ vertices is a SimpleGraph (Fin N). The Lean development defines

• RamseyProperty s t N: every graph on Fin N has an $s$-clique, or its complement has a $t$-clique (an independent set of size $t$);
• ramsey s t := sInf {N | RamseyProperty s t N}, the Ramsey number $r(s,t)$.

All logarithms are natural; real powers of $\log t$ use Real.rpow.

Formalization targets

Goal: sharp logarithmic exponent for every fixed $s\ge6$

For every integer $s\ge6$ there is $C_s>0$ such that for every $\varepsilon>0$ and every sufficiently large $t$ (threshold depending on $s,\varepsilon$)

$$\frac{t^{s-1}}{(\log t)^{s-2+\varepsilon}}\ \le\ r(s,t)\ \le\ C_s\,\frac{t^{s-1}}{(\log t)^{s-2}}, \qquad\text{and}\qquad \lim_{t\to\infty}\frac{(s-1)\log t-\log r(s,t)}{\log\log t}=s-2 .$$

This is Theorem 1.1 of the source, formalized as main (s) (hs : 6 ≤ s) : MainBounds s ∧ MainLimit s. The goal is published on the platform with status Open; no machine-checked proof exists.

Significance

The result itself. Together with the companion $s=5$ preprint and the earlier results for $s=3,4$ on the polynomial exponent, the theorem identifies the exact power of $\log t$ in $r(s,t)$ up to $(\log t)^{o(1)}$ for each fixed $s$: the classical AKS upper bound is sharp in its logarithmic exponent. It does not give a matching constant-factor lower bound. The main new ingredient is a prime-indexed construction (Theorem 1.2 of the source): for fixed $d\ge5$ and large primes $q$, a $K_{d+1}$-free graph on $\lfloor q^d\log q\rfloor$ vertices with independence number below $q(\log q)^{1+\eta}$, built from random incident point–hyperplane flags of $\mathrm{PG}(d,q)$.

Formalizing it. The upper half is classical (Proposition 7.3 of the source restates the AKS estimate for all fixed $s$). The lower half is a long argument combining finite projective geometry, entropy of a selected subsequence, and incidence bounds in positive characteristic; formal verification would independently check an unrefereed claim.

Difficulty

Bradač's projective graph has the right number of vertices but its independent sets were only controlled up to logarithmic exponent $2s-4$. Improving to $s-2+o(1)$ requires bounding long independent sequences in a random stream of flags. A union bound over sequences loses too much, and a sequence selected from the random stream need not have independent or uniform flags. The source pays for this with an entropy lower bound on the selected sequence and a compression upper bound, which in turn requires a description theorem for sparse point–hyperplane pairs in arbitrary dimension (repeated projections and a high-rank two-row description based on a finite-field Zariski-closure inequality of Nie and Wang).

Formalization scope

• Graphs are SimpleGraph (Fin N); independent sets are cliques of the complement graph. ramsey is an sInf, equal to $r(s,t)$ because the defining set is nonempty by Ramsey's theorem.
• MainBounds s fixes one $C>0$ (depending on $s$) before quantifying over $\varepsilon$; natural subtraction s - 1, s - 2 is harmless because $s\ge6$. MainLimit s is a Filter.Tendsto over natural $t$.
• The case $s=5$ belongs to the companion preprint and is not part of this goal; $s=3,4$ are not covered.
• Needed infrastructure: projective spaces over $\mathbb F_q$, Shannon entropy and conditional entropy, concentration inequalities, polynomial-method incidence bounds over finite fields, and AKS-type independent-set bounds for locally sparse graphs. The incidence and entropy layers are reusable.

Selected references

• F. P. Ramsey, On a problem of formal logic, Proc. London Math. Soc. (2) 30 (1930), 264–286. https://doi.org/10.1112/plms/s2-30.1.264
• P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Math. 2 (1935), 463–470. https://www.numdam.org/item/CM_1935__2__463_0/
• J. Spencer, Asymptotic lower bounds for Ramsey functions, Discrete Math. 20 (1977), 69–76. https://doi.org/10.1016/0012-365X(77)90044-9
• M. Ajtai, J. Komlós and E. Szemerédi, A note on Ramsey numbers, J. Combin. Theory Ser. A 29 (1980), 354–360. https://doi.org/10.1016/0097-3165(80)90030-8
• J. H. Kim, The Ramsey number R(3,t) has order of magnitude t²/log t, Random Structures Algorithms 7 (1995), 173–207. https://doi.org/10.1002/rsa.3240070302
• Y. Li, C. C. Rousseau and W. Zang, Asymptotic upper bounds for Ramsey functions, Graphs Combin. 17 (2001), 123–128. https://doi.org/10.1007/s003730170060
• T. Bohman and P. Keevash, The early evolution of the H-free process, Invent. Math. 181 (2010), 291–336. https://doi.org/10.1007/s00222-010-0247-x
• D. Mubayi and J. Verstraëte, A note on pseudorandom Ramsey graphs, J. Eur. Math. Soc. 26 (2024), 153–161. https://doi.org/10.4171/JEMS/1359
• S. Mattheus and J. Verstraëte, The asymptotics of r(4,t), Ann. of Math. 199 (2024), 919–941. https://doi.org/10.4007/annals.2024.199.2.8
• D. Bradač, Off-diagonal Ramsey numbers, arXiv:2605.28793 (2026). https://arxiv.org/abs/2605.28793v3
• Z. Nie and A. Y. Wang, Hilbert functions and the finite degree Zariski closure in finite field combinatorial geometry, J. Combin. Theory Ser. A 134 (2015), 196–220. https://doi.org/10.1016/j.jcta.2015.03.011
• OpenAI, Sharp logarithmic exponents for fixed off-diagonal Ramsey numbers, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-Logarithmic-Exponents-for-Fixed-Off-Diagonal-Ramsey-Numbers-September-24-2026/paper.pdf

Motivation: the growth of off-diagonal Ramsey numbers

For integers $s,t\ge 2$ the Ramsey number $r(s,t)$ is the least $n$ such that every simple graph on $n$ vertices contains either a complete subgraph $K_s$ or an independent set of $t$ vertices. Determining how $r(s,t)$ grows when $s$ is fixed and $t\to\infty$ is one of the central problems of extremal and probabilistic combinatorics: upper bounds come from counting and local density arguments, lower bounds require explicit or random constructions of $K_s$-free graphs with no large independent set, and for decades the two sides did not even agree on the power of $t$.

Timeline

• 1935 — Erdős and Szekeres prove $r(s,t)\le\binom{s+t-2}{s-1}$ (Erdős–Szekeres 1935).
• 1977 — Spencer's local-lemma method gives $r(5,t)\gtrsim (t/\log t)^3$ (Spencer 1977).
• 1980 — Ajtai, Komlós and Szemerédi improve the fixed-$s$ upper bound to $O(t^{s-1}/(\log t)^{s-2})$ (AKS 1980).
• 1995 — Kim shows $r(3,t)$ has order $t^2/\log t$ (Kim 1995).
• 2001 — Li, Rousseau and Zang obtain upper leading constant $1+o(1)$ for fixed $s$ (Li–Rousseau–Zang 2001).
• 2010 — Bohman and Keevash's analysis of the $K_5$-free process gives $r(5,t)\gtrsim t^3/(\log t)^{8/3}$ (Bohman–Keevash 2010, Thm 1.2).
• 2024 — Mattheus and Verstraëte prove $r(4,t)\ge c\,t^3/(\log t)^4$ via Hermitian unitals, settling the power of $t$ for $s=4$ (Mattheus–Verstraëte 2024).
• 2026 — Bradač's projective construction gives $r(s,t)\ge c_s\,t^{s-1}/(\log t)^{2s-4}$ for all $s\ge3$; for $s=5$ the logarithmic exponent is $6$ (Bradač 2026, Thm 1.1).
• 2026 — An OpenAI preprint, The sharp logarithmic exponent of r(5,t) (OpenAI Math Release, September 24, 2026), claims $r(5,t)=t^4/(\log t)^{3+o(1)}$, closing the gap between exponent $6$ and the AKS-type exponent $3$. The preprint has not been peer reviewed and its main theorem is not formally verified.

Setting

A graph on $n$ vertices is a SimpleGraph (Fin n). A $k$-clique is a set of $k$ pairwise adjacent vertices and a $k$-independent set a set of $k$ pairwise non-adjacent vertices. The Lean development defines

• RamseyProperty s t n: every simple graph on Fin n has an $s$-clique or a $t$-independent set;
• ramsey s t := sInf {n | RamseyProperty s t n}, the Ramsey number $r(s,t)$.

All logarithms are natural.

Formalization targets

Goal: sharp bounds and logarithmic exponent for $r(5,t)$

There is an absolute constant $C>0$ such that for every $\varepsilon>0$ and all sufficiently large $t$ (threshold depending on $\varepsilon$)

$$\frac{t^4}{(\log t)^{3+\varepsilon}}\ \le\ r(5,t)\ \le\ C\,\frac{t^4}{(\log t)^3},$$

and consequently

$$\lim_{t\to\infty}\frac{4\log t-\log r(5,t)}{\log\log t}=3 .$$

This is Theorem 1.1 of the source, formalized as SharpBounds ∧ SharpExponent. The goal is published on the platform with status Open; no machine-checked proof exists.

Significance

The result itself. The theorem determines $r(5,t)$ up to a factor $(\log t)^{o(1)}$, the first case beyond $s=4$ in which the logarithmic exponent of a fixed off-diagonal Ramsey number is known. It shows that the classical upper-bound exponent $s-2=3$ is the truth for $s=5$, and it leaves open only a constant-factor asymptotic for $t^4/(\log t)^3$. The lower-bound construction (random incident point–hyperplane pairs in projective space $\mathrm{PG}(4,q)$, ordered by position) together with its entropy/compression analysis is the new part.

Formalizing it. The upper bound is an elementary argument (triangle-free independent-set bounds plus random sampling), stated separately in the source as Theorem 2.1 for all $t\ge2$; its formalization is a self-contained milestone. The lower bound is a long probabilistic and finite-geometric argument whose formal verification would independently certify an unrefereed claim.

Difficulty

The lower bound needs a $K_5$-free graph on about $t^4/(\log t)^{3+\varepsilon}$ vertices with no independent set of size $t$. Random graph processes lose logarithmic factors and even the power of $t$; Bradač's projective graph has the right power but its independent sets were only controlled to logarithmic exponent $6$. The obstacle is to bound long independent sequences in a random stream of flags: a direct union bound over sequences is far too weak, and the selected sequence can have a heavily biased law. The source handles this with an entropy lower bound and a matching compression (description) upper bound that relies on a new theorem about sparse point–hyperplane incidences.

Formalization scope

• Graphs are SimpleGraph (Fin n); cliques and independent sets use Mathlib's IsNClique and IsNIndepSet. ramsey is an sInf, which is the true Ramsey number because the defining set is nonempty by Ramsey's theorem; a proof must use that nonemptiness rather than the junk value 0.
• SharpBounds fixes one $C>0$ before $\varepsilon$; the threshold $t_0$ may depend on $\varepsilon$. The power $(\log t)^{3+\varepsilon}$ is Real.rpow. SharpExponent is a Filter.Tendsto statement over natural $t$ with real logarithms.
• Needed infrastructure: finite projective geometry over $\mathbb F_q$, entropy and conditional entropy of finite random variables, concentration inequalities, and independent-set bounds for triangle-free graphs (Shearer/AKS type). The upper-bound half and the triangle-free bounds are reusable in other Ramsey formalizations.

Selected references

• P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Math. 2 (1935), 463–470. https://www.numdam.org/item/CM_1935__2__463_0/
• J. Spencer, Asymptotic lower bounds for Ramsey functions, Discrete Math. 20 (1977), 69–76. https://doi.org/10.1016/0012-365X(77)90044-9
• M. Ajtai, J. Komlós and E. Szemerédi, A note on Ramsey numbers, J. Combin. Theory Ser. A 29 (1980), 354–360. https://doi.org/10.1016/0097-3165(80)90030-8
• J. H. Kim, The Ramsey number R(3,t) has order of magnitude t²/log t, Random Structures Algorithms 7 (1995), 173–207. https://doi.org/10.1002/rsa.3240070302
• Y. Li, C. C. Rousseau and W. Zang, Asymptotic upper bounds for Ramsey functions, Graphs Combin. 17 (2001), 123–128. https://doi.org/10.1007/s003730170060
• T. Bohman and P. Keevash, The early evolution of the H-free process, Invent. Math. 181 (2010), 291–336. https://doi.org/10.1007/s00222-010-0247-x
• S. Mattheus and J. Verstraëte, The asymptotics of r(4,t), Ann. of Math. 199 (2024), 919–941. https://doi.org/10.4007/annals.2024.199.2.8
• D. Bradač, Off-diagonal Ramsey numbers, arXiv:2605.28793 (2026). https://arxiv.org/abs/2605.28793v3
• OpenAI, The sharp logarithmic exponent of r(5,t), OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Sharp-Logarithmic-Exponent-of-r-5-t-September-24-2026/paper.pdf

Motivation

Kazhdan–Lusztig polynomials $P_{u,b}(q)$ are integer polynomials attached to pairs $u\le b$ of elements of a Coxeter group. They were introduced through the canonical basis of the Hecke algebra (Kazhdan–Lusztig, 1979). For Weyl groups they compute local intersection cohomology of Schubert varieties, and they enter the Kazhdan–Lusztig conjectures on characters of highest-weight representations. Their definition uses the simple generators of the group, yet in every known example $P_{u,b}$ seemed to depend only on the Bruhat interval $[u,b]$ as an abstract partially ordered set. The combinatorial invariance conjecture, attributed to Lusztig and Dyer, asserts this: if two Bruhat intervals, possibly in different Coxeter groups, are isomorphic as posets, their Kazhdan–Lusztig polynomials coincide.

This mission asks for a formal proof of the conjecture, 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

• 1979–1980 — Kazhdan and Lusztig define the polynomials (Invent. Math. 1979) and interpret them via Schubert varieties (Proc. Sympos. Pure Math. 36, 1980).
• 1987–1993 — Dyer's thesis and papers on reflection subgroups and the Bruhat graph (J. Algebra 1990; Compositio 1991); the conjecture's published formulation for finite Coxeter systems and the reconstruction of the Bruhat graph from the interval order.
• 2000–2006 — Lower intervals $[1,b]$: du Cloux (Adv. Math. 2003), Brenti for symmetric groups (EJC 2004), and for all Coxeter systems Brenti–Caselli–Marietti (Adv. Math. 2006) and Delanoy (J. Alg. Combin. 2006).
• 2001–2014 — Moment-graph and Soergel-bimodule machinery: Braden–MacPherson (Math. Ann. 2001), Fiebig (Trans. AMS 2008), Soergel (J. Inst. Math. Jussieu 2007), Elias–Williamson (Annals 2014).
• 2007–2021 — Short intervals (Incitti, JCTA 2007); the coefficient of $q$ in simply-laced type (Patimo, IMRN 2021).
• 2022–2026 — Hypercube decompositions guided by machine learning (Blundell–Buesing–Davies–Veličković–Williamson, Represent. Theory 2022); Barkley–Gaetz (Math. Ann. 2025; IMRN 2026); Barkley–Gaetz–Lam: invariance of the $q$-coefficient in general and full invariance up to rank six (arXiv:2601.07793); Esposito–Marietti–Stella up to rank ten in finite Weyl groups (arXiv:2509.16433).
• September 2026 — The OpenAI preprint claims the full conjecture for arbitrary Coxeter systems (Theorem 1.1, p. 2).

Setting

A Coxeter system $(W,S)$ is a group $W$ with a generating set $S$ of involutions subject only to relations $(st)^{m_{st}}=1$. Write $\ell$ for word length in $S$. A reflection is a conjugate of an element of $S$. Bruhat order is the partial order generated by $x<tx$ whenever $t$ is a reflection and $\ell(tx)>\ell(x)$; the interval $[u,b]=\{x:u\le x\le b\}$ is finite and graded of rank $\ell(b)-\ell(u)$, even when $W$ is infinite. The equal-parameter R-polynomials $R_{x,y}$ and Kazhdan–Lusztig polynomials $P_{x,y}$ are the unique families with $R_{x,x}=P_{x,x}=1$, $R_{x,y}=P_{x,y}=0$ unless $x\le y$, the recursion: for $s\in S$ with $sy<y$,

$$R_{x,y}=\begin{cases}R_{sx,sy}, & sx<x,\\ (q-1)R_{x,sy}+q\,R_{sx,sy}, & sx>x,\end{cases}$$

the degree bound $\deg P_{x,y}<(\ell(y)-\ell(x))/2$ for $x<y$, and the inversion formula

$$q^{\ell(y)-\ell(x)}P_{x,y}(q^{-1})=\sum_{x\le z\le y}R_{x,z}(q)\,P_{z,y}(q).$$

Formalization targets

Goal: Theorem 1.1 (p. 2)

Let $(W,S)$ and $(W',S')$ be arbitrary Coxeter systems, $u\le b$ in $W$ and $u'\le b'$ in $W'$. If $\iota:[u,b]\to[u',b']$ is an isomorphism of posets (a bijection preserving and reflecting order), then

$$P^{W}_{u,b}(q)=P^{W'}_{u',b'}(q).$$

The isomorphism carries no labels or root data; the groups may be infinite and noncrystallographic.

Significance

The result itself. It shows that a Kazhdan–Lusztig polynomial, defined algebraically from the Hecke algebra, is determined by a finite poset. Restricting $\iota$ to subintervals gives the same for every $P_{x,y}$ with $u\le x\le y\le b$, and hence for the R-polynomials (Corollary 6.1, p. 29). For Weyl groups this means that local intersection cohomology of Schubert varieties is determined by the Bruhat poset. It settles a question open since the 1980s that had been verified only for lower intervals, short intervals, low ranks, and single coefficients.

Formalizing it. Mathlib has Coxeter systems and their length function but no Bruhat order, Hecke algebra, or Kazhdan–Lusztig theory. The proof uses reflection orders (Dyer's path formula, Theorem 2.2, p. 7), Braden–MacPherson moment-graph sheaves over a reflection-faithful real realization (Theorem 2.3, p. 8), and the Elias–Williamson character theorem as external inputs. Building these would be a substantial, reusable contribution to formal representation theory.

Difficulty

The defining recursion uses a simple generator $s$ with $sy<y$, but a poset isomorphism need not carry simple generators or reflections to anything recognisable, and need not respect root labels. Dyer's reconstruction recovers all reflection edges of the Bruhat graph from the order (Theorem 3.4, p. 12) but not their labels. Lanini's moment-graph invariance requires compatible label automorphisms, which an abstract isomorphism does not provide. The preprint therefore keeps the two realizations separate, transports reflection orders through maximal dihedral subintervals (Proposition 3.5, p. 13), counts later edges exactly, and compares images of edges in two different sheaves by a reciprocal inequality that is then forced to be an equality (Sections 5–6).

Formalization scope

• Coxeter systems are Mathlib CoxeterSystem M W for arbitrary index types and groups; the two systems may live in different universes.
• BruhatLE is the reflexive–transitive closure of $x\to tx$ with $t$ a reflection and $\ell(x)<\ell(tx)$, i.e. strong Bruhat order (not weak order). Interval cs u b carries this order; ι is an order isomorphism ≃o.
• klPolynomial is the second component of Classical.epsilon (NormalizedKL cs), where NormalizedKL encodes exactly the normalization above (R-recursion with left multiplication, diagonal and vanishing conditions, $2\deg P<\ell(y)-\ell(x)$, and the inversion formula with Polynomial.reflect). Existence and uniqueness of such families is the classical Kazhdan–Lusztig theorem, and a proof of the goal has to establish them, since otherwise Classical.epsilon returns an arbitrary pair.
• Sums over intervals use finsum; intervals are finite, so this is the ordinary sum.
• The hypotheses $u\le b$, $u'\le b'$ are explicit; there is no vacuous reading.

Welcome contributions: Bruhat order and its basic properties (subword property, finiteness of intervals), R-polynomials, and existence and uniqueness of Kazhdan–Lusztig polynomials for arbitrary Coxeter systems.

Selected references

• OpenAI, Combinatorial invariance of Kazhdan–Lusztig polynomials, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Combinatorial-Invariance-of-Kazhdan-Lusztig-Polynomials-September-24-2026/paper.pdf
• D. Kazhdan, G. Lusztig, Representations of Coxeter groups and Hecke algebras, Invent. Math. 53 (1979), 165–184. https://doi.org/10.1007/BF01390031
• M. Dyer, On the "Bruhat graph" of a Coxeter system, Compositio Math. 78 (1991), 185–191. https://www.numdam.org/item/CM_1991__78_2_185_0/
• F. Brenti, F. Caselli, M. Marietti, Special matchings and Kazhdan–Lusztig polynomials, Adv. Math. 202 (2006), 555–601. https://doi.org/10.1016/j.aim.2005.01.011
• E. Delanoy, Combinatorial invariance of Kazhdan–Lusztig polynomials on intervals starting from the identity, J. Algebraic Combin. 24 (2006), 437–463. https://doi.org/10.1007/s10801-006-0014-7
• F. du Cloux, Rigidity of Schubert closures and invariance of Kazhdan–Lusztig polynomials, Adv. Math. 180 (2003), 146–175. https://doi.org/10.1016/S0001-8708(02)00100-7
• T. Braden, R. MacPherson, From moment graphs to intersection cohomology, Math. Ann. 321 (2001), 533–551. https://doi.org/10.1007/s002080100232
• B. Elias, G. Williamson, The Hodge theory of Soergel bimodules, Ann. of Math. 180 (2014), 1089–1136. https://doi.org/10.4007/annals.2014.180.3.6
• C. Blundell, L. Buesing, A. Davies, P. Veličković, G. Williamson, Towards combinatorial invariance for Kazhdan–Lusztig polynomials, Represent. Theory 26 (2022), 1145–1191. https://doi.org/10.1090/ert/624
• G. T. Barkley, C. Gaetz, T. Lam, Combinatorial invariance for the coefficient of q in Kazhdan–Lusztig polynomials, arXiv:2601.07793 (2026). https://arxiv.org/abs/2601.07793v2
• A. Björner, F. Brenti, Combinatorics of Coxeter Groups, GTM 231, Springer, 2005. https://doi.org/10.1007/3-540-27596-7

Motivation

The unit-distance problem of Erdős asks how many pairs among $n$ points in the plane can be at distance exactly one. By rescaling, this is the same as asking how often a single distance can repeat. It is one of the central extremal questions of combinatorial geometry and a benchmark for incidence methods. The bound $u(n)=O(n^{4/3})$ of Spencer, Szemerédi and Trotter (1984) has resisted improvement of its exponent for four decades, and the same exponent is sharp for the closely related Szemerédi–Trotter point–line incidence theorem, so any improvement must use geometry specific to circles in the Euclidean plane.

This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims a fixed power saving: $u(n)=O(n^{\beta})$ for some absolute $\beta<4/3$. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).

Background

• 1946 — Erdős introduces the problem and the lattice lower bound $n^{1+c/\log\log n}$ (Amer. Math. Monthly 1946).
• 1982–1983 — The crossing inequality of Ajtai, Chvátal, Newborn and Szemerédi (1982) and Leighton (1983).
• 1984 — Spencer, Szemerédi and Trotter prove $u(n)=O(n^{4/3})$ (Unit distances in the Euclidean plane, Graph Theory and Combinatorics, 1984).
• 1997 — Székely's crossing-number proof and incidence theorem for curves (CPC 1997).
• 2022 — Ágoston and Pálvölgyi improve the leading constant (Studia Sci. Math. Hungar. 2022).
• 2026 — Pach, Raz and Solymosi obtain a logarithmic improvement conditional on a rigidity conjecture (SoCG 2026). Erdős's conjecture $u(n)=n^{1+o(1)}$ is disproved by an OpenAI construction with $n^{1+\varepsilon}$ unit distances, simplified by Alon, Bloom, Gowers, Litt et al. (arXiv:2605.20695) and sharpened by Sawin to $n^{1.014114}$ (arXiv:2605.20579).
• September 2026 — The OpenAI preprint claims the upper exponent can be lowered below $4/3$ (Theorem 1.1, p. 1).

Setting

For a finite set $X\subset\mathbb R^2$ let

$$u(X)=\#\bigl\{\{x,y\}\subset X:\ \|x-y\|=1\bigr\},$$

the number of unordered pairs of distinct points at Euclidean distance one, and let

$$u(n)=\max_{X\subset\mathbb R^2,\ |X|=n}u(X).$$

The maximum exists because $u(X)\le\binom n2$.

Formalization targets

Goal: Theorem 1.1 (p. 1)

There are absolute constants $0<C<\infty$ and $1\le\beta<4/3$ such that

$$u(n)\le C\,n^{\beta}\qquad\text{for every integer }n\ge0.$$

Equivalently, $u(n)=O(n^{4/3-\delta})$ for an absolute $\delta>0$. The goal leaves $C$ and $\beta$ unspecified, so it is stable under any later numerical improvement.

Significance

The result itself. It answers the long-standing question of whether the Spencer–Szemerédi–Trotter exponent $4/3$ can be lowered by a fixed amount. Combined with the recent lower bounds $u(n)\ge n^{1+\varepsilon}$ along a sequence, it confines the true exponent to an interval strictly inside $(1,4/3)$. Because point–line incidences do attain $n^{4/3}$, the result also isolates a genuine difference between unit circles and lines in incidence geometry.

Formalizing it. The proof combines random cuttings in the Clarkson–Shor framework, an entropy-based prediction lemma, the product formula and absolute heights of algebraic numbers, and an algebraic obstruction using derivations and valuations of function fields. A formal proof would add these to Mathlib and would also require the $O(n^{4/3})$ bound itself (via the crossing lemma) as background. No machine-checked unit-distance bound beyond trivial ones is known.

Difficulty

Every known proof of $O(n^{4/3})$ uses only two combinatorial properties of unit circles (two circles meet in at most two points; two points lie on at most two unit circles), and those properties are shared by systems attaining $n^{4/3}$, so no argument using only them can save a power. The saving must exploit arithmetic or algebraic rigidity of the Euclidean metric. In the preprint the scheme is a contradiction argument on a hypothetical sequence with $t^{4-o(1)}$ unit pairs among $t^3$ points: transfer to number fields, measure edge-jump profiles at all absolute values, and show that either a bounded-scale configuration violates a determinant identity (Proposition 4.4, p. 19) or a dense pair graph with low-height rectangle products arises, which is excluded algebraically (Proposition 8.1, p. 42). The hard step is transferring concentration from predicted states to actual points under the true edge and history laws (Lemma 6.2, p. 29).

Formalization scope

• Points are in EuclideanSpace ℝ (Fin 2); unitPairCount X counts elements of X.sym2 (unordered pairs, diagonal included but never at distance $1$) with dist = 1.
• u n is the natural-number sSup of unitPairCount X over $n$-element Finsets; the set is nonempty and bounded by $\binom n2$, so it is the true maximum.
• The goal is ∃ C β : ℝ, 0 < C ∧ 1 ≤ β ∧ β < 4/3 ∧ ∀ n, (u n : ℝ) ≤ C * n ^ β with real-power exponent. At $n=0$ both sides vanish.
• There is no trivialization: $\beta<4/3$ is strict and the bound must hold for every $n$ with constants independent of the configuration.

Selected references

• OpenAI, A power saving for planar unit distances, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-power-saving-for-planar-unit-distances-September-23-2026/paper.pdf
• P. Erdős, On sets of distances of n points, Amer. Math. Monthly 53 (1946), 248–250. https://doi.org/10.1080/00029890.1946.11991674
• J. Spencer, E. Szemerédi, W. T. Trotter, Unit distances in the Euclidean plane, Graph Theory and Combinatorics (1984). https://trotter.math.gatech.edu/papers/44.pdf
• L. A. Székely, Crossing numbers and hard Erdős problems in discrete geometry, Combin. Probab. Comput. (1997). https://doi.org/10.1017/S0963548397002976
• P. Ágoston, D. Pálvölgyi, An improved constant factor for the unit distance problem, Studia Sci. Math. Hungar. (2022). https://doi.org/10.1556/012.2022.01517
• J. Pach, O. E. Raz, J. Solymosi, Erdős's unit distance problem and rigidity, SoCG 2026. https://doi.org/10.4230/LIPIcs.SoCG.2026.83
• N. Alon, T. F. Bloom, W. T. Gowers, D. Litt et al., Remarks on the disproof of the unit distance conjecture, arXiv:2605.20695 (2026). https://arxiv.org/abs/2605.20695v1
• W. Sawin, An explicit lower bound for the unit distance problem, arXiv:2605.20579 (2026). https://arxiv.org/abs/2605.20579v1
• K. L. Clarkson, P. W. Shor, Applications of random sampling in computational geometry, II, Discrete Comput. Geom. (1989). https://doi.org/10.1007/BF02187740
• N. H. Katz, G. Tardos, A new entropy inequality for the Erdős distance problem, Contemp. Math. 342 (2004). https://doi.org/10.1090/conm/342/06136

Motivation

Erdős's distinct-distance problems ask how few different distances $n$ points in the plane can determine. The global version, which counts all distances between all pairs, was essentially settled by Guth and Katz, who proved that every $n$-point planar set determines at least $cn/\log n$ distinct distances (Annals 2015), matching the square lattice up to a $\sqrt{\log n}$ factor. The pinned version asks for many distances measured from a single point: given $P$, is there a pin $x\in P$ from which almost $n$ distinct distances are visible? The weak pinned Erdős conjecture asserts that for every $\varepsilon>0$ some pin sees at least $n^{1-\varepsilon}$ distinct distances. Erdős stated the question in 1957 (Michigan Math. J. 1957, Problem 16). Pinned bounds are a standard test for incidence-geometric methods, since Guth–Katz controls only the union of distances over all pins.

This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims that large repeated-distance fibres are rare at almost every pin and deduces the weak pinned conjecture. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).

Background

• 1946 — Erdős introduces the distinct-distance problem and the $\sqrt{\log n}$ lattice example (Amer. Math. Monthly 1946).
• 1957 — Erdős asks the pinned question (Michigan Math. J. 1957).
• 2001 — Solymosi and Tóth prove a pinned lower bound of order $n^{6/7}$ (DCG 2001).
• 2003–2004 — Tardos improves the exponent with entropy inequalities (Adv. Math. 2003); Katz and Tardos reach every exponent below $\frac{48-14e}{55-16e}=0.8641\ldots$ (Contemp. Math. 342, 2004).
• 2015 — Guth and Katz prove the global bound $cn/\log n$ (Annals 2015).
• September 2026 — The OpenAI preprint claims the weak pinned conjecture (Theorem 1.1 and Corollary 1.2, p. 2).

Setting

Let $P\subset\mathbb R^2$ be a finite set with $|P|=n\ge2$. For distinct $x,y\in P$, the distance fibre size is

$$k_P(x,y)=\#\{z\in P\setminus\{x\}:\ \|z-x\|=\|y-x\|\},$$

the number of points of $P$ at the same distance from the pin $x$ as $y$ (it counts $y$ itself). Each pair uses its own pin; pairs sharing a numerical distance but with different pins are not pooled. For $s>0$ define

$$F_n(s)=\sup_{P\subset\mathbb R^2,\ |P|=n}\ \frac{\#\{(x,y)\in P^2:\ x\ne y,\ k_P(x,y)\ge n^s\}}{n(n-1)},$$

the largest possible fraction of ordered distinct pairs that lie in a distance fibre of size at least $n^s$.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every fixed $s>0$,

$$F_n(s)\longrightarrow0\qquad(n\to\infty).$$

The convergence is uniform over all configurations; no separation, general-position or coordinate hypothesis is imposed, and no rate is claimed.

Significance

The result itself. Corollary 1.2 (p. 2) follows in a few lines: for every $\varepsilon>0$, the fraction of pins $x\in P$ with fewer than $n^{1-\varepsilon}$ distinct distances tends to $0$ uniformly in $P$, so all but $o(n)$ points see at least $n^{1-\varepsilon}$ distances. This settles the weak pinned conjecture, improving the previous best exponent $0.8641\ldots$ to $1-\varepsilon$. An exceptional set is unavoidable: the centre of a circle carrying the other points sees one distance. The sharper conjecture of order $n/\sqrt{\log n}$ at a pin is not addressed.

Formalizing it. The proof combines transfer for real closed fields (to move a configuration into a number field), the product formula over all places of a number field, random nested grids, and weak compactness of probability measures. A formal proof would exercise Mathlib's number-field and measure-theory libraries in combination, and the statement itself is elementary enough to audit easily. No machine-checked pinned-distance bound is known.

Difficulty

Incidence bounds (Szemerédi–Trotter type) and entropy inequalities give pinned exponents strictly below $1$, and the obstruction is structural: they count incidences globally, while the pinned problem needs control at individual pins. The preprint (pp. 3–4) proceeds by contradiction and uses that squared distance factors as $(Z_1(y)-Z_1(x))(Z_2(y)-Z_2(x))$ with $Z_{1,2}=u\pm iv$, so on a fibre one coordinate is a fractional linear function of the other. Turning the product formula into usable information requires an exact additive overlap identity for nested partitions at every absolute value (Section 3), with the field and its degree unbounded along the sequence, and then a limiting argument that rules out non-atomic fibre maps (Lemma 7.1, p. 25).

Formalization scope

• Points are in EuclideanSpace ℝ (Fin 2); configurations are Finsets. k P x y counts (P.erase x).filter (dist z x = dist y x).
• richPairs P s is the set of ordered pairs $(x,y)\in P\times P$ with $x\ne y$ and $n^s\le k_P(x,y)$; pairFraction divides by $n(n-1)$ as a real.
• F n s is the sSup over all $n$-point sets of pairFraction for $n\ge2$ and is defined as 0 for $n<2$. For $n\ge2$ the set of values is nonempty and contained in $[0,1]$, so sSup is the true supremum.
• The goal is Tendsto (fun n => F n s) atTop (𝓝 0) for each fixed s > 0; it is not vacuous, since $F_n(s)$ is a genuine supremum over all configurations.
• Corollary 1.2 (the counting statement about pins) is not part of the goal; it is an elementary consequence.

Selected references

• OpenAI, The weak pinned planar distance theorem, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-weak-pinned-planar-distance-theorem-September-23-2026/paper.pdf
• P. Erdős, On sets of distances of n points, Amer. Math. Monthly 53 (1946), 248–250. https://doi.org/10.1080/00029890.1946.11991674
• P. Erdős, Some unsolved problems, Michigan Math. J. 4 (1957), 291–300. https://doi.org/10.1307/mmj/1028997963
• J. Solymosi, C. D. Tóth, Distinct distances in the plane, Discrete Comput. Geom. 25 (2001), 629–634. https://doi.org/10.1007/s00454-001-0009-z
• G. Tardos, On distinct sums and distinct distances, Adv. Math. 180 (2003), 275–289. https://doi.org/10.1016/S0001-8708(03)00004-5
• N. H. Katz, G. Tardos, A new entropy inequality for the Erdős distance problem, Contemp. Math. 342 (2004). https://doi.org/10.1090/conm/342/06136
• L. Guth, N. H. Katz, On the Erdős distinct distances problem in the plane, Ann. of Math. 181 (2015), 155–190. https://doi.org/10.4007/annals.2015.181.1.2
• B. Lund, G. Petridis, Bisectors and pinned distances, Discrete Comput. Geom. 64 (2020), 995–1012. https://doi.org/10.1007/s00454-019-00122-w

Motivation

A vertex cover of a hypergraph is a set of vertices meeting every edge; the covering number $\tau(H)$ is the minimum size of a cover, and the matching number $\nu(H)$ is the maximum number of pairwise disjoint edges. An $r$-partite $r$-uniform hypergraph has $r$ disjoint vertex parts, and every edge takes exactly one vertex from each part. Ryser's covering conjecture asserts that every such hypergraph satisfies

$$\tau(H)\le(r-1)\,\nu(H).$$

For $r=2$ this is Kőnig's theorem for bipartite graphs, so the conjecture is a proposed higher-dimensional Kőnig theorem. Its intersecting case ($\nu=1$, bound $r-1$) is equivalent to Gyárfás's conjecture that every $r$-edge-coloured complete graph can be covered by $r-1$ monochromatic trees, which connects it to Ramsey-type covering problems.

Timeline

• 1971. Henderson's thesis contains an equivalent formulation of the conjecture (doi:10.7907/J1Z1-SK19); Best and Wanless discuss its attribution to Ryser (arXiv:1801.02893).
• 1983. Tuza proves the intersecting case for $r=5$; Gyárfás had handled $r\le4$ (historical account in Király–Tóthmérész, doi:10.37236/6448).
• 1991. Erdős, Gyárfás and Pyber record the equivalence with the monochromatic tree-cover formulation (doi:10.1016/0095-8956(91)90007-7).
• 2001. Aharoni proves the full case $r=3$ (doi:10.1007/s004930170001).
• 2012. Haxell and Scott prove $\tau\le(r-\varepsilon_r)\nu$ for $r=4,5$ (doi:10.37236/1175).
• 2017. Francetić, Herke, McKay and Wanless verify the linear intersecting case through rank nine (doi:10.1016/j.ejc.2016.10.004); Haxell and Scott construct intersecting examples with $\tau\ge r-4$ (doi:10.37236/6460).
• 2019. Abu-Khazneh, Barát, Pokrovskiy and Szabó construct intersecting $(q+2)$-partite hypergraphs with $\tau=q+1$, matching the conjectured bound, for prime powers $q$ (doi:10.1016/j.jcta.2018.07.011).
• 2025–2026. Clow, Haxell and Mohar disprove Lovász's stronger deletion conjecture at $r=3$ (doi:10.1007/s00493-026-00220-3); those examples do not contradict Ryser's bound.

The source of this mission, an OpenAI preprint dated September 27, 2026, claims counterexamples to the conjecture itself, already in the intersecting case and with all parts of equal size.

Setting

Fix $r=q+1$. A $(q+1)$-partite $(q+1)$-uniform hypergraph on parts $V_1,\dots,V_{q+1}$ is given by its edge set, each edge choosing one vertex in every part. It is intersecting if it has at least one edge and any two edges share a vertex (necessarily in the same part). A vertex is nonisolated if it lies in some edge. For an intersecting hypergraph $\nu(H)=1$, so Ryser's conjecture predicts $\tau(H)\le q$.

The natural extremal example comes from the affine plane $\mathbb F_q^2$: one part per direction, one vertex per line, one edge per point. It is intersecting with $\tau=q$, attaining the conjectured bound.

Formalization targets

Goal: Theorem 1.1

There is $q_0$ such that for every prime $q\ge q_0$ there exists a finite intersecting $(q+1)$-partite $(q+1)$-uniform hypergraph $H$ with

$$|V_1|=\dots=|V_{q+1}|=q+1,\qquad \tau(H)=q+1,$$

and every vertex lies in an edge. Lean: OAI.Balanced.main_result, open on the platform.

Significance

Since $\nu(H)=1$ and $\tau(H)=q+1>q=r-1$, the theorem would disprove Ryser's conjecture for infinitely many $r$, in its intersecting case. The value $\tau=r$ is the largest possible for an intersecting $r$-uniform hypergraph (any edge is a cover), and the part sizes $q+1$ are the smallest compatible with $\tau=r$, so the examples are extremal in both respects. Via the standard transfer (Corollary 1.2) they also disprove Gyárfás's tree-cover conjecture for $r=q+1$ colours. The threshold $q_0$ is not explicit. A companion preprint of the same family gives counterexamples over extension fields without balance. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

The affine-plane example sits exactly at the conjectured bound, and its minimum covers are rigid (parallel classes). Raising $\tau$ by one requires adding edges that destroy every $q$-element cover while keeping the hypergraph intersecting and keeping only $q+1$ vertices per part; adding a new part, as Abu-Khazneh et al. did, changes $r$ and only reaches equality. Verifying that no cover of size $q$ survives requires controlling all small sets of lines, which the paper does with stability results for line covers in prime-order planes and a probabilistic selection.

Formalization scope

• PartiteHypergraph r n has vertex set Fin r × Fin n and edges a Finset (Fin r → Fin n); an edge $e$ contains the vertices $(i,e(i))$.
• Intersecting: edges nonempty and any two edges agree in some coordinate. Nonisolated: every $(i,v)$ lies in some edge. HasCoverNumber H k: some cover has exactly $k$ vertices and every cover has at least $k$.
• MainResult: ∃ q₀, ∀ q ≥ q₀, q.Prime → ∃ H : PartiteHypergraph (q+1) (q+1), Intersecting ∧ Nonisolated ∧ HasCoverNumber (q+1).
• Finite fields of prime order are available in Mathlib as ZMod q.

Contributions formalizing the deterministic reduction (Proposition 2.1), the stability of affine line covers (Lemma 3.3, building on Szőnyi–Weiner), or the selection step (Proposition 5.1) are welcome, as is the monochromatic tree-cover corollary.

Selected references

• OpenAI, Balanced counterexamples to Ryser's conjecture at prime orders, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Balanced-Counterexamples-to-Rysers-Conjecture-at-Prime-Orders-September-27-2026/paper.pdf
• J. R. Henderson, Permutation decompositions of (0,1)-matrices and decomposition transversals, PhD thesis, Caltech, 1971. https://doi.org/10.7907/J1Z1-SK19
• R. Aharoni, Ryser's conjecture for tripartite 3-graphs, Combinatorica, 2001. https://doi.org/10.1007/s004930170001
• P. Haxell, A. Scott, On Ryser's conjecture, Electron. J. Combin., 2012. https://doi.org/10.37236/1175
• N. Francetić, S. Herke, B. D. McKay, I. M. Wanless, On Ryser's conjecture for linear intersecting multipartite hypergraphs, European J. Combin., 2017. https://doi.org/10.1016/j.ejc.2016.10.004
• A. Abu-Khazneh, J. Barát, A. Pokrovskiy, T. Szabó, A family of extremal hypergraphs for Ryser's conjecture, J. Combin. Theory Ser. A, 2019. https://doi.org/10.1016/j.jcta.2018.07.011
• P. Erdős, A. Gyárfás, L. Pyber, Vertex coverings by monochromatic cycles and trees, J. Combin. Theory Ser. B, 1991. https://doi.org/10.1016/0095-8956(91)90007-7
• Z. Király, L. Tóthmérész, On Ryser's conjecture for t-intersecting and degree-bounded hypergraphs, Electron. J. Combin., 2017. https://doi.org/10.37236/6448

Motivation

Van der Waerden's theorem (1927) says that for every number of colours $r$ and every length $k$, every $r$-colouring of a long enough interval of integers contains a monochromatic arithmetic progression of length $k$. The van der Waerden number $W_r(k)$ is the least such interval length. Its upper bounds were for a long time not even primitive recursive (Shelah 1988 gave the first primitive recursive bound; Gowers 2001 gave a tower-type bound), while lower bounds stayed close to exponential, $W_2(k)\gtrsim 2^k$. Erdős asked whether $W_2(k)^{1/k}\to\infty$, i.e. whether the growth is genuinely faster than any exponential. Lower bounds on $W_r(k)$ correspond to long colourings with no monochromatic progression and are a central quantitative question in Ramsey theory.

Timeline

• 1927. Van der Waerden proves finiteness of $W_r(k)$.
• 1952 and 1962. Erdős–Rado (doi:10.1112/plms/s3-2.1.417) and Schmidt (doi:10.1215/S0012-7094-62-02914-9) obtain early exponential-type lower bounds.
• 1968. Berlekamp proves $W_2(p+1)>p\,2^p$ for primes $p$ by an algebraic construction (doi:10.4153/CMB-1968-047-7).
• 1975. Erdős and Lovász introduce the local lemma, a standard tool for such colourings.
• 1980. Erdős asks for $\lim_k W_2(k)^{1/k}=\infty$ (doi:10.1016/S0167-5060(08)70697-6).
• 1990. Szabó proves $W_2(k)\ge 2^k/k^{\varepsilon}$ (doi:10.1002/rsa.3240010307).
• 2016. Kozik and Shabanov prove $W_r(k)\ge\beta r^{k-1}$ uniformly (doi:10.1016/j.jctb.2015.09.004).
• 2025. Hunter improves the exponential base for fixed $r\ge5$ (doi:10.1007/s11856-025-2735-0).
• 2026. Fox and Hunter prove superexponential growth for three colours, $W_3(k)>2^{k\log^*k/4}$ (arXiv:2606.02541); Campos, Fox and Schildkraut prove $W_2(k)\ge(1-o(1))k2^{k-1}$ (arXiv:2608.20824).

For two colours, superexponential growth had not been established. The source of this mission, an OpenAI preprint dated September 23, 2026, claims a bound of the form $k^{ck\log r}$ uniformly in $r\ge2$.

Setting

For positive integers $r,k$, $W_r(k)$ is the least positive integer $N$ such that every map $\{1,\dots,N\}\to\{1,\dots,r\}$ is constant on some progression

$$a,\ a+d,\ \dots,\ a+(k-1)d,\qquad a,d\ge1,\quad a+(k-1)d\le N.$$

Colourings may use fewer than $r$ colours.

Formalization targets

Goal: Theorem 1.1

There is an absolute $K_0$ such that for every $k\ge K_0$ and every $r\ge2$,

$$W_r(k)\ >\ k^{\,c\,k\lfloor\log_2 r\rfloor},\qquad c=10^{-5}.$$

In particular $W_r(k)^{1/k}\to\infty$ for each fixed $r\ge2$. The constant $c$ is the paper's and is not optimized. The Lean statement OAI.QuantitativeVanDerWaerden.uniform_lower_bound is open on the platform.

Significance

The theorem gives a quantitative positive answer to Erdős's superexponential-growth question for two colours, and is stronger than the statement $W_2(k)/2^k\to\infty$ settled by Campos–Fox–Schildkraut. It is uniform in the number of colours with a single threshold $K_0$, which complements the Fox–Hunter bounds that require many colours relative to $k$. The bound is still far from the best upper bounds, which are tower-type.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would certify an explicit colouring construction together with a probabilistic (local-lemma) argument.

Difficulty

Random colourings with the local lemma give only $W_r(k)\gtrsim r^{k}/\mathrm{poly}(k)$: the number of $k$-term progressions in $[N]$ is of order $N^2$, and each is monochromatic with probability $r^{1-k}$, which caps the length at exponential size. Algebraic constructions such as Berlekamp's gain only a factor $p$. A superexponential bound needs colourings with structure that kills most progressions deterministically, while the remaining progressions are few enough to be destroyed randomly, uniformly down to two colours.

Formalization scope

• MonoAP c k a d: the colour of $a+jd$ equals the colour of $a$ for $j<k$; HasMonoAP c k N: some $d>0$ with $a+(k-1)d<N$.
• IsRamsey α k N: every colouring ℕ → α has a monochromatic $k$-AP in $\{0,\dots,N-1\}$ (equivalent to the paper's $[N]$ after a shift).
• W r k is the sInf of positive Ramsey $N$ for colours Fin r. If no such $N$ existed this would be $0$ and the goal's strict inequality would fail, so the goal implicitly includes van der Waerden's theorem.
• The exponent uses Nat.log 2 r $=\lfloor\log_2 r\rfloor$ and the real constant 1/100000.

A complete development needs van der Waerden's theorem (or at least finiteness), a finite asymmetric local lemma, and the paper's explicit adaptive-mesh colourings and counting of affine signatures. Contributions formalizing Lemma 4.1 (finite asymmetric local lemma) or Theorem 6.3 (a cyclic two-colouring) are welcome.

Selected references

• OpenAI, Quantitative Superexponential Bounds for van der Waerden Numbers, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Quantitative-Superexponential-Bounds-for-van-der-Waerden-Numbers-September-23-2026/paper.pdf
• P. Erdős, A survey of problems in combinatorial number theory, Ann. Discrete Math., 1980. https://doi.org/10.1016/S0167-5060(08)70697-6
• E. R. Berlekamp, A construction for partitions which avoid long arithmetic progressions, Canad. Math. Bull., 1968. https://doi.org/10.4153/CMB-1968-047-7
• Z. Szabó, An application of Lovász' local lemma: a new lower bound for the van der Waerden number, Random Structures Algorithms, 1990. https://doi.org/10.1002/rsa.3240010307
• J. Kozik, D. Shabanov, Improved algorithms for colorings of simple hypergraphs and applications, J. Combin. Theory Ser. B, 2016. https://doi.org/10.1016/j.jctb.2015.09.004
• J. Fox, Z. Hunter, Three-color van der Waerden numbers grow super-exponentially, preprint, 2026. https://arxiv.org/abs/2606.02541
• M. Campos, J. Fox, C. Schildkraut, A new lower bound for two-color van der Waerden numbers, preprint, 2026. https://arxiv.org/abs/2608.20824
• S. Shelah, Primitive recursive bounds for van der Waerden numbers, J. Amer. Math. Soc., 1988. https://doi.org/10.1090/S0894-0347-1988-0929498-X
• W. T. Gowers, A new proof of Szemerédi's theorem, Geom. Funct. Anal., 2001. https://doi.org/10.1007/s00039-001-0332-9