Graph Theory

Motivation

Drawing all edges between two vertex classes creates unavoidable intersections. The Zarankiewicz target asks for the exact best crossing count with both part sizes variable. The source manuscript presents the surrounding research claim.

Setting

The complete bipartite graph has vertex type Fin m⊕Fin n and one edge for every pair in Fin m×Fin n. Admissible plane drawings use simple continuous arcs, distinct vertices, finitely many proper double crossings and no triple crossings.

Formalization target

For every m,n>0, prove there is a drawing with exactly

$$Z(m,n)=\left\lfloor\frac m2\right\rfloor\left\lfloor\frac{m-1}2\right\rfloor\left\lfloor\frac n2\right\rfloor\left\lfloor\frac{n-1}2\right\rfloor$$

crossing points, and every admissible drawing has at least Z(m,n) crossings.

The selected formal target is OAI.Zarankiewicz.mainTarget_proof.

Significance and status

The formal target includes both an attaining drawing and the universal lower bound. Small positive part sizes remain in scope. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The best known construction alone cannot establish optimality. The lower bound must allow arbitrary continuous edge arcs and repeated crossings of a pair of edges.

Formalization scope

Proper intersections use local coordinate-axis charts. Counted objects are crossing points, not merely pairs of edges that meet. The formula is implemented by axisPairs(r)=(r/2)((r−1)/2) in natural arithmetic. Tangencies, overlaps and triple crossings are excluded by the drawing model.

Selected references

• OpenAI, The crossing number of complete bipartite graphs, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

The complete graph forces many crossings in any plane drawing. The mission seeks the exact ordinary crossing number rather than one drawing’s upper bound. The source manuscript presents the surrounding research claim.

Setting

An admissible drawing uses distinct vertex points and injective continuous edge paths whose interiors avoid vertices. Intersections are finitely many proper double crossings, with no triple crossing. Every crossing point is counted, including repeated meetings of a pair of edges.

Formalization target

For n≥3, prove

$$\operatorname{cr}(K_n)=\frac14\left\lfloor\frac n2\right\rfloor\left\lfloor\frac{n-1}2\right\rfloor\left\lfloor\frac{n-2}2\right\rfloor\left\lfloor\frac{n-3}2\right\rfloor.$$

The selected formal target is OAI.Paper170.complete_graph_crossing_number.

Significance and status

The target fixes the exact minimum across the full continuous-drawing class. It does not restrict edges to straight segments or impose a special layout. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

An explicit drawing establishes only an upper bound. The equality also requires a bound valid for all admissible topological drawings.

Formalization scope

The graph uses ordered endpoint pairs with increasing indices. Proper crossings are defined through local open partial homeomorphisms taking the two traces to coordinate axes. The ordinary crossing number is the natural infimum of crossing counts; hill uses natural subtraction and division. The selected theorem starts at n=3.

Selected references

• OpenAI, The crossing number of complete graphs, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Sampling a graph with a prescribed degree vector requires moving among realizations without changing degrees. The switch chain performs local edge replacements and asks whether these suffice for rapid global mixing. The source manuscript presents the surrounding research claim.

Setting

States are simple undirected labeled graphs realizing a graphical vector d on n≥4 vertices. The lazy switch chain stays put with probability one half and otherwise proposes one ordered replacement between distinct perfect matchings on four vertices, rejecting invalid proposals.

Formalization target

Prove

$$\tau_{TV}(1/4)\le2n^8,$$

with mixing time zero for a singleton state space. When more than one state exists, prove the spectral-gap lower bound 1/(24n²·binom(n,4)).

The selected formal target is OAI.Problem315.switch_chain_main.

Significance and status

The goal covers every graphical degree sequence under the stated degree bound, without regularity or density restrictions. Connectivity and explicit exponential total-variation decay are available supporting targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Connectivity gives eventual communication but no polynomial rate. The estimate must be uniform across degree vectors and initial graphs.

Formalization scope

The kernel is defined by exact counts of four-vertex proposals, and total variation is the finite half-ℓ₁ distance from uniform measure. The main theorem contains the singleton case explicitly. The manuscript’s exact sampler is not an additional published target here.

Selected references

• OpenAI, Polynomial mixing of the switch chain for every graphical degree sequence, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

A uniform spanning tree of a finite connected graph is a spanning tree chosen uniformly at random. On an infinite graph one takes limits along finite pieces: the free uniform spanning forest (FUSF) is the weak limit of uniform spanning trees of an increasing sequence of finite connected subgraphs, with no boundary identification. Uniform spanning forests connect random walks, electrical networks, determinantal processes and $\ell^2$-Betti numbers of groups.

A random object on a graph is a factor of IID if it can be produced by one measurable rule from independent uniform labels on the vertices, in a way that commutes with all graph symmetries. Such representations are the measure-theoretic analogue of local algorithms, and they are central in ergodic theory of group actions. Whether the FUSF is a factor of IID was raised by Lyons at Oberwolfach in 2013, and Timár's 2025 paper describes the unrestricted question as open.

Timeline

• 1991. Pemantle constructs infinite-volume uniform spanning trees on $\mathbb Z^d$ (Ann. Probab., 1991; arXiv:math/0404043).
• 2001. Benjamini, Lyons, Peres and Schramm develop the general theory of free and wired uniform spanning forests; on transient graphs the wired forest is a factor of IID via Wilson's algorithm rooted at infinity (doi:10.1214/aop/1008956321).
• 2003. Lyons develops determinantal probability measures on countable sets (doi:10.1007/s10240-003-0016-0).
• 2009. Borcea, Brändén and Liggett introduce strongly Rayleigh measures and their negative-dependence theory (doi:10.1090/S0894-0347-08-00618-8).
• 2013. Lyons discusses the FUSF factor question for Cayley graphs (doi:10.4171/OWR/2013/42).
• 2016. Lyons and Thom prove Bernoulli isomorphism for equivariant determinantal measures on amenable Cayley graphs and ask a broader determinantal factor question (doi:10.1017/etds.2014.70).
• 2022. Nam, Sly and Zhang give FIID codings of free Ising measures on regular trees through Brownian-driven systems (doi:10.1007/s00220-021-04260-2).
• 2025. Timár proves FIID representability of the free forest on recurrent and invariantly amenable unimodular random graphs (doi:10.1007/s11856-025-2884-1).

The source of this mission, an OpenAI preprint dated September 25, 2026, proves the unrestricted statement with one rule for all graphs.

Setting

Let $G$ be an infinite, connected, locally finite, simple, undirected graph. For a finite connected subgraph $H$, let $\mathrm{UST}_H$ be the uniform law on spanning trees of $H$. For finite connected subgraphs $H_1\subseteq H_2\subseteq\cdots$ whose edges exhaust $E(G)$, the laws $\mathrm{UST}_{H_n}$ (edges outside $H_n$ absent) converge weakly; the limit $\mathrm{FUSF}_G$ on $\{0,1\}^{E(G)}$ does not depend on the exhaustion (Proposition 2.2).

A rule $\Phi(G,U,e)\in\{0,1\}$ takes a graph, real vertex labels $U=(U_v)$ and an edge. It is equivariant if $\Phi(\sigma G,\sigma U,\sigma e)=\Phi(G,U,e)$ for every isomorphism $\sigma$, and root independent if it uses no distinguished vertex.

A law $\mu$ on $\{0,1\}^F$, $F$ finite, is strongly Rayleigh if $\sum_x\mu(x)\prod_iz_i^{x_i}\ne0$ whenever all $\operatorname{Im}z_i>0$; on a countable set, every finite marginal must be strongly Rayleigh.

Formalization targets

Milestones (strongly Rayleigh processes, Section 6)

• Lemma 6.1: for strongly Rayleigh $\mu$ and tilts $\mu_h$, $\partial p_i/\partial h_j=\operatorname{Cov}_{\mu_h}(X_i,X_j)$ and $\sum_j|\partial p_i/\partial h_j|\le2p_i(1-p_i)\le\tfrac12$.
• Theorem 1.3: an invariant strongly Rayleigh law on $\{0,1\}^\Gamma$, $\Gamma$ a countable group, is an equivariant factor of IID.
• Inputs to Corollary 1.4: finite determinantal laws with $0\le K\le I$ exist and are strongly Rayleigh; on a countable set the determinantal law of a positive contraction exists and is unique.
• Corollary 1.4: invariant determinantal laws on countable groups are factors of IID, in particular when $K_{gh,gk}=K_{h,k}$.

Goal: Theorem 1.1

$$\exists\ \Phi\ \text{Borel, equivariant, root independent}:\quad \forall G,\quad \{e:\Phi(G,U,e)=1\}\sim\mathrm{FUSF}_G\quad\text{for IID Uniform}[0,1]\ U.$$

The Lean statement OAI.Problem336.fusf_is_factor_iid is open on the platform.

Significance

Theorem 1.1 answers the FUSF factor question without amenability, transience, unimodularity, degree bounds or moment assumptions, and with a single rule for all graphs; Corollary 1.2 gives the factor statement under every unimodular random graph law. Theorem 1.3 and Corollary 1.4 extend the method to all invariant strongly Rayleigh and determinantal processes on countable groups, addressing the regular-action case of the Lyons–Thom question. The paper asserts an ordinary Borel factor, not a finitary one.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Formalization would also provide uniform spanning trees, the free forest limit, strongly Rayleigh measures and determinantal laws as reusable Lean objects.

Difficulty

Previous constructions use structure that is absent in general: Wilson's algorithm works for the wired forest on transient graphs, and Timár's construction needs monotone limits along a hyperfinite exhaustion. A factor must produce one exact sample of the infinite-volume law while controlling all edges jointly, and equivariance forbids any choice of root or ordering. The paper's route observes the forest through independent Brownian noises and must show that the posterior drift has a uniformly Lipschitz response to the observations even when the fields are unbounded over the graph.

Formalization scope

• Graphs are coded on vertex set $\mathbb N$ by symmetric irreflexive ℕ → ℕ → Bool; edges are pairs $u<v$; a connected graph on $\mathbb N$ is automatically infinite. Equivariance is invariance under every permutation of $\mathbb N$ applied to graph, labels and edge.
• RuleBorel is joint measurability of $\Phi$ in the product σ-algebras.
• IsVertexIID requires the label coordinates to have independent Uniform$[0,1]$ finite-dimensional laws (with $s=\varnothing$ this forces a probability measure).
• HasFUSFLaw asks that every cylinder probability (edges in $A$ present, edges in $B$ absent) be the limit of the corresponding uniform-spanning-tree ratio along every exhaustion by finite connected subgraphs covering all edges.
• The strongly Rayleigh and determinantal milestones use ProbabilityMeasure (Γ → Bool), left translation $(\tau_ga)_h=a_{g^{-1}h}$, i.i.d. labels in Set.Icc 0 1 via Measure.infinitePi, and Hermitian kernels with $0\le\langle c,Kc\rangle\le\|c\|^2$ on finitely supported vectors.

A complete development needs the matrix-tree theorem and Kirchhoff formulas, weak limits on $\{0,1\}^{E}$, Brownian motion and a Borel Picard iteration for the decoder, and the Borcea–Brändén–Liggett theory. Contributions formalizing Proposition 2.2 (free exhaustion limit), Lemma 2.3 (finite-field forest response) and Proposition 4.2 (sampling from independent Brownian paths) are welcome.

Selected references

• OpenAI, The free uniform spanning forest is a factor of IID, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026.pdf
• I. Benjamini, R. Lyons, Y. Peres, O. Schramm, Uniform spanning forests, Ann. Probab., 2001. https://doi.org/10.1214/aop/1008956321
• R. Lyons, ℓ²-Betti numbers, cost, and the free uniform spanning forest, Oberwolfach Reports, 2013. https://doi.org/10.4171/OWR/2013/42
• Á. Timár, Factor of iid's through stochastic domination, Israel J. Math., 2025. https://doi.org/10.1007/s11856-025-2884-1
• R. Lyons, A. Thom, Invariant coupling of determinantal measures on sofic groups, Ergodic Theory Dynam. Systems, 2016. https://doi.org/10.1017/etds.2014.70
• R. Lyons, Determinantal probability measures, Publ. Math. IHÉS, 2003. https://doi.org/10.1007/s10240-003-0016-0
• J. Borcea, P. Brändén, T. M. Liggett, Negative dependence and the geometry of polynomials, J. Amer. Math. Soc., 2009. https://doi.org/10.1090/S0894-0347-08-00618-8
• D. Nam, A. Sly, L. Zhang, Ising model on trees and factors of IID, Comm. Math. Phys., 2022. https://doi.org/10.1007/s00220-021-04260-2
• R. Pemantle, Choosing a spanning tree for the integer lattice uniformly, Ann. Probab., 1991. https://arxiv.org/abs/math/0404043

Motivation

In Bernoulli bond percolation on a graph $G=(V,E)$, each edge is kept (open) independently with probability $p$. As $p$ grows, an infinite connected component of open edges appears at the critical probability $p_c(G)$. The criticality problem asks whether an infinite cluster can already exist at $p_c$. A negative answer means the phase transition is continuous. Benjamini and Schramm (1996) conjectured that, on every graph with a large symmetry group and $p_c<1$, there is no infinite cluster at $p_c$. The question contains the famous open case of $\mathbb Z^3$ and connects percolation to geometric group theory, since Cayley graphs of finitely generated groups are the main examples.

Timeline

• 1957. Broadbent and Hammersley introduce percolation (doi:10.1017/S0305004100032680).
• 1960, 1980. Harris and Kesten settle nearest-neighbour bond percolation on $\mathbb Z^2$, including $\theta(p_c)=0$ (doi:10.1017/S0305004100034241, doi:10.1007/BF01197577).
• 1986–1987. Menshikov and Aizenman–Barsky prove sharpness of the subcritical phase; this does not settle behaviour at $p_c$ (doi:10.1007/BF01212322).
• 1990. Hara and Slade prove mean-field behaviour, including $\theta(p_c)=0$, for $\mathbb Z^d$ in sufficiently high dimension (doi:10.1007/BF02108785).
• 1996. Benjamini and Schramm formulate the conjecture for quasi-transitive graphs with $p_c<1$ (doi:10.1214/ECP.v1-978).
• 1999. Benjamini, Lyons, Peres and Schramm prove it for nonamenable graphs with a unimodular quasi-transitive action (doi:10.1214/aop/1022677450).
• 2006. Timár excludes infinitely many infinite critical clusters on nonunimodular transitive graphs (doi:10.1214/009117906000000494).
• 2016. Hutchcroft proves the conjecture for every quasi-transitive graph of exponential growth (arXiv:1605.05301). Duminil-Copin, Sidoravicius and Tassion treat slabs (doi:10.1002/cpa.21641).
• 2017. Fitzner and van der Hofstad reach nearest-neighbour $\mathbb Z^d$, $d\ge11$ (arXiv:1506.07977).
• 2021. Hermon and Hutchcroft cover certain groups of intermediate growth (arXiv:1809.11112).
• 2024. Kozma and Nitzan reduce the $\mathbb Z^d$ case to a conjectured gluing inequality (arXiv:2401.12397).
• 2026. Public, non-peer-reviewed announcements report AI-assisted proofs for $\mathbb Z^d$, including a reported Lean formalization of the lattice case (Leder, August 2026).

The source of this mission is an OpenAI preprint dated September 24, 2026, which treats the remaining subexponential-growth case for all quasi-transitive graphs.

Setting

A graph here has vertex set $V$ and a set $E$ of labelled bonds, each with a pair of endpoints; loops and parallel bonds are allowed. It is locally finite if each vertex lies in finitely many bonds, connected if any two vertices are joined by a path, and quasi-transitive if its automorphism group (bijections of vertices and of bonds respecting endpoints) has finitely many orbits on $V$. Examples include $\mathbb Z^d$ and every Cayley graph of a finitely generated group.

For $p\in[0,1]$, let $\mathbb P_p$ be the law of a random set $\omega\subseteq E$ containing each bond independently with probability $p$. The cluster $C_x(\omega)$ of $x$ is the set of vertices joined to $x$ by a finite path of bonds in $\omega$ (including $x$). Define

$$p_c(G)=\inf\{p\in[0,1]:\ \mathbb P_p(\exists x,\ |C_x|=\infty)>0\}.$$

Formalization targets

Goal: Theorem 1.1

For every infinite, connected, locally finite, quasi-transitive graph $G$,

$$p_c(G)<1\ \Longrightarrow\ \mathbb P_{p_c(G)}\bigl(\exists x\in V:\ |C_x|=\infty\bigr)=0.$$

The hypothesis $p_c<1$ is necessary, since at $p=1$ every infinite connected graph percolates. The Lean statement OAI.CriticalPercolation.BondGraph.no_percolation_at_criticality is open on the platform.

Significance

Theorem 1.1 resolves the Benjamini–Schramm criticality conjecture for Bernoulli bond percolation, and in particular gives $\theta(p_c)=0$ on $\mathbb Z^d$ for every $d\ge2$ (Corollary 10.1, p. 39), including the long-open case $d=3$. With Hutchcroft's exponential-growth theorem, the remaining work is the subexponential case, divided into superpolynomial growth and growth bounded by a polynomial along a sequence of scales. As a consequence the percolation probability is continuous at $p_c$ on every such graph.

The result is proved in an OpenAI preprint that has not been peer reviewed. No machine-checked proof of the general quasi-transitive statement exists; the reported Lean formalization concerns only nearest-neighbour $\mathbb Z^d$. A formal proof would also certify the structural input (Tessera–Tointon's finitary structure theorem) as used here.

Difficulty

The obvious strategy, renormalization from large finite boxes, needs a gluing inequality to connect independently found large clusters, and it needs coordinates: on a general quasi-transitive graph there is no lattice to place boxes in. Planar duality is unavailable, the lace expansion needs high dimension, and Hutchcroft's argument uses exponential growth essentially. In the superpolynomial case one must rule out two large distinct clusters adjacent across an edge; in the polynomial case one needs nilpotent-group coordinates (Gromov, Trofimov, Tessera–Tointon) and a two-direction corridor exploration in which conditional failure probabilities stay uniformly small. Neither uniqueness of the infinite cluster nor independence across coarse blocks can be assumed.

Formalization scope

• BondGraph V E stores ends : E → Sym2 V; loops and parallel bonds are allowed. LocallyFinite counts bonds at each vertex. Clusters use SimpleGraph.fromEdgeSet of the open bonds, so loops are discarded and parallel bonds collapse; reachability includes the zero-length path.
• Aut consists of a vertex bijection and a bond bijection that commute with ends; QuasiTransitive says some finite set of vertices meets every orbit.
• law p is ProbabilityTheory.setBernoulli Set.univ p on Set E: each bond retained independently with probability p : unitInterval.
• criticalProbability is sInf in unitInterval of $\{p:\mathbb P_p(\text{percolates})>0\}$; if the set were empty this would be $1$, which hpc excludes.
• percolates is the event that some cluster is infinite; the conclusion says it has measure $0$ at $p_c$.

A complete development needs Bernoulli product measures, Harris–FKG and conditional correlation inequalities, Hutchcroft's exponential-growth theorem, volume-growth theory of quasi-transitive graphs, and the Gromov–Trofimov–Tessera–Tointon structure theory. Each of these is reusable well beyond this mission. Contributions formalizing Proposition 3.1 (two-cluster bound), Theorem 6.1 (joint gluing), Theorem 7.1 (criticality with a nilpotent quotient action) or Proposition 9.3 (subcritical exploration), or the cited Theorem 2.2 (Hutchcroft), are welcome.

Selected references

• OpenAI, No percolation at criticality on quasi-transitive graphs, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/No-percolation-at-criticality-on-quasi-transitive-graphs-September-24-2026/paper.pdf
• I. Benjamini, O. Schramm, Percolation beyond $\mathbb Z^d$, many questions and a few answers, Electron. Commun. Probab., 1996. https://doi.org/10.1214/ECP.v1-978
• I. Benjamini, R. Lyons, Y. Peres, O. Schramm, Critical percolation on any nonamenable group has no infinite clusters, Ann. Probab., 1999. https://doi.org/10.1214/aop/1022677450
• T. Hutchcroft, Critical percolation on any quasi-transitive graph of exponential growth has no infinite clusters, C. R. Math., 2016. https://doi.org/10.1016/j.crma.2016.07.013
• J. Hermon, T. Hutchcroft, No percolation at criticality on certain groups of intermediate growth, IMRN, 2021. https://doi.org/10.1093/imrn/rnz265
• R. Tessera, M. C. H. Tointon, A finitary structure theorem for vertex-transitive graphs of polynomial growth, Combinatorica, 2021. https://doi.org/10.1007/s00493-020-4295-6
• G. Kozma, S. Nitzan, A reduction of the θ(p_c)=0 problem to a conjectured inequality, preprint, 2024. https://arxiv.org/abs/2401.12397
• T. Hara, G. Slade, Mean-field critical behaviour for percolation in high dimensions, Comm. Math. Phys., 1990. https://doi.org/10.1007/BF02108785
• H. Kesten, The critical probability of bond percolation on the square lattice equals 1/2, Comm. Math. Phys., 1980. https://doi.org/10.1007/BF01197577
• Á. Timár, Percolation on nonunimodular transitive graphs, Ann. Probab., 2006. https://doi.org/10.1214/009117906000000494

Motivation

The Ramsey number $R(H,J)$ is the least $N$ such that every red–blue colouring of the edges of $K_N$ contains a red copy of $H$ or a blue copy of $J$. For a cycle $C_m$ against a clique $K_n$ there is a simple lower-bound construction: take $n-1$ disjoint red cliques of order $m-1$ with all edges between them blue. It has $(m-1)(n-1)$ vertices, no red $C_m$ (each red component is too small) and no blue $K_n$ (a blue clique meets each red clique at most once). In 1978 Erdős, Faudree, Rousseau and Schelp conjectured that this construction is optimal whenever $m\ge n\ge3$, apart from $R(C_3,K_3)=6$. Cycle–complete Ramsey numbers are among the few families where exact values are expected over a whole parameter range, and the conjecture has been attacked case by case for decades.

This mission asks for a formal proof of the full conjecture as stated 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. Part of the proof is a finite case analysis of 3,099 parameter-pattern instances carried out by two exact programs that accompany the paper.

Background

• 1971 — Chartrand and Schuster settle $n=3$ (Bull. AMS 1971).
• 1973 — Bondy and Erdős prove the formula for $m\ge n^2-2$ (JCTB 1973).
• 1978 — Erdős, Faudree, Rousseau and Schelp state the conjecture (J. Graph Theory 1978).
• 1999–2008 — The full range for $n=4$ (Yang–Huang–Zhang, Australas. J. Combin. 1999), $n=5$ (Bollobás et al., Australas. J. Combin. 2000), $n=6$ (Schiermeyer, JGT 2003), $n=7$ (Chen–Cheng–Zhang, Eur. J. Combin. 2008).
• 2005 — Nikiforov proves the formula for $n\ge4$, $m\ge4n+2$ (CPC 2005).
• 2007–2023 — Partial results for $n=8$, including $R(C_8,K_8)$ (Discrete Math. 2009) and $R(C_9,K_8)$ (ISRN Algebra 2011).
• 2021 — Keevash, Long and Skokan prove the formula for $m\ge C\log n/\log\log n$, leaving finitely many open pairs (IMRN 2021).
• September 2026 — The OpenAI preprint claims all remaining pairs (Theorem 1.1, p. 2).

Setting

All graphs are finite and simple. $C_m$ is the cycle on exactly $m$ vertices and $K_n$ the complete graph on $n$ vertices. Identify a red–blue colouring of $K_N$ with its red graph $G$ on $N$ vertices; the blue graph is the complement $\overline G$. A copy of $H$ in $G$ is an injective homomorphism $H\to G$ (copies need not be induced). The Ramsey property $\mathcal R(m,n,N)$ says: every graph $G$ on $N$ vertices contains $C_m$ or its complement contains $K_n$. Then

$$R(C_m,K_n)=\min\{N:\ \mathcal R(m,n,N)\}.$$

Formalization targets

Goal: Theorem 1.1 (p. 2)

For all integers $m\ge n\ge 3$ with $(m,n)\ne(3,3)$,

$$R(C_m,K_n)=(m-1)(n-1)+1,$$

and $R(C_3,K_3)=6$.

Significance

The result itself. It completes a programme that over five decades settled the conjecture for $n\le7$, for long cycles, and for all sufficiently large $n$ by Keevash–Long–Skokan; the preprint's contribution is the remaining finite but large set of pairs. Since Keevash–Long–Skokan's constant is not explicit, the preprint gives a structural reduction that does not need a numerical value of it.

Formalizing it. The statement uses only Mathlib's cycleGraph, complete graphs, complements and subgraph containment. A formal proof would have to certify both the structural lemmas (independent-set expansion, a large-clique lemma, optimal path systems) and the finite verification of 3,099 pattern instances, which the preprint currently delegates to two programs with deduction traces. Bringing such a computation inside a proof assistant is itself a worthwhile contribution. Neither $R(C_m,K_n)$ for general parameters nor any of the previously known infinite families has a machine-checked proof.

Difficulty

The lower bound is the explicit construction above; the work is the upper bound for exact cycle length $m$. Methods that find long cycles (Pósa rotation, Chvátal–Erdős) produce cycles of length at least $m$, not exactly $m$, and forbidding exactly one cycle length gives weak structural information. The preprint passes to a minimal counterexample with independent-set expansion (Lemma 2.2, p. 4), finds a clique of order $\max\{3,\lfloor k/2\rfloor\}$ with $k=m-1$ (Theorem 3.1, p. 5), and optimizes systems of paths through that clique so that every improvement would close a cycle of order exactly $m$. Cliques of order $t\ge9$ are excluded by hand (Proposition 8.4, p. 24); the remaining $3\le t\le8$, $5\le k\le17$ need the finite verification of Section 9 (Proposition 9.1, p. 26).

Formalization scope

• RamseyProperty m n N: for every G : SimpleGraph (Fin N), cycleGraph m ⊑ G or (⊤ : SimpleGraph (Fin n)) ⊑ Gᶜ, where ⊑ is Mathlib's subgraph containment (injective homomorphism, non-induced).
• cycleCliqueRamsey m n = sInf {N | RamseyProperty m n N} in ℕ. If the set were empty, sInf would return 0; the goal's equalities exclude that, so a proof must exhibit the Ramsey property.
• The goal quantifies over integers $m,n$ with $3\le n\le m$, $(m,n)\ne(3,3)$, converting with toNat (harmless since both are at least $3$), and separately states cycleCliqueRamsey 3 3 = 6.
• cycleGraph m on Fin m is the $m$-cycle for $m\ge3$.

Welcome contributions: a verified checker for the pattern enumeration of Section 9, and the classical small cases ($n=3$, Bondy–Erdős for $m\ge n^2-2$).

Selected references

• OpenAI, Cycle–clique Ramsey numbers, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Cycle-clique-Ramsey-numbers-September-25-2026/Cycle-clique-Ramsey-numbers-September-25-2026.pdf
• P. Erdős, R. J. Faudree, C. C. Rousseau, R. H. Schelp, On cycle–complete graph Ramsey numbers, J. Graph Theory 2 (1978). https://doi.org/10.1002/jgt.3190020107
• J. A. Bondy, P. Erdős, Ramsey numbers for cycles in graphs, J. Combin. Theory Ser. B (1973). https://doi.org/10.1016/S0095-8956(73)80005-X
• G. Chartrand, S. Schuster, On the existence of specified cycles in complementary graphs, Bull. Amer. Math. Soc. (1971). https://doi.org/10.1090/S0002-9904-1971-12832-X
• I. Schiermeyer, All cycle-complete graph Ramsey numbers r(C_m,K_6), J. Graph Theory (2003). https://doi.org/10.1002/jgt.10145
• V. Nikiforov, The cycle-complete graph Ramsey numbers, Combin. Probab. Comput. (2005). https://doi.org/10.1017/S096354830400642X
• Y. Chen, T. C. E. Cheng, Y. Zhang, The Ramsey numbers R(C_m,K_7) and R(C_7,K_8), European J. Combin. (2008). https://doi.org/10.1016/j.ejc.2007.05.007
• P. Keevash, E. Long, J. Skokan, Cycle-complete Ramsey numbers, Int. Math. Res. Not. (2021). https://doi.org/10.1093/imrn/rnz119
• V. Chvátal, P. Erdős, A note on Hamiltonian circuits, Discrete Math. (1972). https://doi.org/10.1016/0012-365X(72)90079-9

Motivation

A thin spanning tree of a graph is a spanning tree that uses only a small fraction of the edges of every cut. Thin trees were introduced for the asymmetric traveling salesman problem: Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that a thin tree of low cost can be augmented into a cheap tour, giving an $O(\log n/\log\log n)$-approximation (doi:10.1287/opre.2017.1603). Goddyn conjectured that high edge connectivity forces thin trees; the strong thin tree conjecture asks for thinness $C/k$ in every $k$-edge-connected multigraph. For applications one wants not just existence but an efficient algorithm that finds such a tree, also when parallel-edge multiplicities are huge and written in binary.

Background. The maximum-entropy rounding of Asadpour et al. constructs $O(\log n/(k\log\log n))$-thin trees. Oveis Gharan and Saberi constructed $O(1/k)$-thin trees on planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan proved existence of $\mathrm{poly}(\log\log n)/k$-thin trees in general (2015, arXiv:1411.4613), without a polynomial-time construction. Klein and Olver (2023, doi:10.1109/FOCS57990.2023.00011) and Klein, Olver and Yeoh (2026, doi:10.4230/LIPIcs.ICALP.2026.129) handled laminar families and near-minimum cuts. A companion OpenAI preprint claims the existence statement of the strong conjecture.

The source of this mission, an OpenAI preprint dated September 23, 2026, claims a deterministic polynomial-time construction.

Setting

Graphs are finite undirected loopless multigraphs; parallel copies count separately. For $\varnothing\ne S\subsetneq V(G)$, $\delta_G(S)$ is the multiset of edges with exactly one endpoint in $S$, and $G$ is $k$-edge-connected if $|\delta_G(S)|\ge k$ for every such $S$. A spanning tree $T$ is $\alpha$-thin if $|\delta_T(S)|\le\alpha|\delta_G(S)|$ for all such $S$. Two input formats are allowed: an explicit list of labelled edge copies, or a list of endpoint pairs with multiplicities written in binary (so the number of edges can be exponential in the input length). Running time is measured in the total binary input length.

Formalization targets

Goal: Theorem 1.1 (algorithmic strong thin trees)

There is an absolute constant $C$ and a deterministic algorithm that, given $k\ge1$ and a $k$-edge-connected multigraph $G$ on at least one vertex (in either format), returns in time polynomial in the input length a spanning tree $T$ with

$$|\delta_T(S)|\le\frac Ck\,|\delta_G(S)|\qquad(\varnothing\ne S\subsetneq V(G)),$$

returning the empty tree for a one-vertex graph. Lean: OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees, open on the platform.

Significance

The theorem would give an algorithmic resolution of the strong thin tree conjecture: not only do $C/k$-thin trees exist, they can be found deterministically in polynomial time, even for exponentially many parallel edges. It also yields simultaneous cost-and-cut rounding (Corollary 7.1): from a fractional point whose mass on every cut is at least one, a tree in its support with every cut load and total cost within constant factors, with no metric assumption on costs. The order $1/k$ is optimal. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Existence proofs for thin trees go through the Marcus–Spielman–Srivastava interlacing-families theorem and a fixed-point argument, neither of which is constructive: they show that some choice works without locating it. The algorithm must replace these by explicit, rational, polynomially sized computations (checked signings, rational positive semidefinite decompositions, bounded denominators) and must work with binary multiplicities, where even listing the edges is exponential. Certifying thinness on all exponentially many cuts must also be done without enumerating them.

Formalization scope

• Graphs: StrongThinTree.MultiGraph n m (vertices Fin n, edges Fin m, loopless). Inputs are ExplicitInput or BinaryInput (ordered, distinct endpoint pairs with multiplicities); a binary input's edge copies are Σ i, Fin (multiplicity i).
• Valid x: $n\ge1$, $k\ge1$ and EdgeConnected k.
• The machine model is CurrentKS.Machine: a deterministic machine with finitely many binary stacks and a finite instruction table, run for a fuel bound. Inputs and outputs are self-delimiting binary encodings (CurrentKS.encodeNat).
• AlgorithmicStrongThinTrees: ∃ C > 0, ∃ M a degree, 0 < a ∧ ∀ x, Valid x → after a * (len + 1)^degree steps M has halted and its output stack encodes a duplicate-free edge list forming a ThinTree C k; for $n=1$ the output is empty.
• One machine and one polynomial serve all inputs in both formats.

Needed infrastructure: the existence theory of the companion mission, a model of deterministic computation with polynomial-time bounds, exact rational linear algebra, and constructive spectral sparsification. Contributions formalizing Proposition 2.5, Proposition 3.1, Lemma 6.1, Theorem A.1 (rational rank-one signing) or Corollary 7.1 are welcome.

Selected references

• OpenAI, A polynomial-time construction of strong thin trees, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-polynomial-time-construction-of-strong-thin-trees-September-23-2026/paper.pdf
• OpenAI, The strong thin tree conjecture, preprint, September 23, 2026.
• 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
• 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
• O. Svensson, J. Tarnawski, L. A. Végh, A constant-factor approximation algorithm for the asymmetric traveling salesman problem, J. ACM, 2020. https://doi.org/10.1145/3424306

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: the Shareshian–Wachs elementary-positivity conjecture

The chromatic symmetric function of a graph, introduced by Stanley, records all proper colorings of the graph with infinitely many colors as a symmetric function; it refines the chromatic polynomial. Whether it expands with nonnegative coefficients in the basis of elementary symmetric functions ("$e$-positivity") is a central question in algebraic combinatorics. The Stanley–Stembridge conjecture (1993) predicted $e$-positivity for incomparability graphs of $(3+1)$-free posets; it arose from positivity questions for immanants of Jacobi–Trudi matrices. Shareshian and Wachs introduced a $q$-graded refinement, the chromatic quasisymmetric function, which tracks ascents of colorings along edges, and conjectured that for natural unit interval graphs its elementary coefficients are polynomials in $q$ with nonnegative integer coefficients. The $q$-refinement is tied to geometry: it describes the graded representation of the symmetric group on the cohomology of regular semisimple Hessenberg varieties.

Timeline

• 1993 — Stanley and Stembridge formulate the $e$-positivity conjecture for $(3+1)$-free posets (J. Combin. Theory Ser. A 1993); Haiman's immanant results imply Schur positivity (JAMS 1993).
• 1995 — Stanley introduces the chromatic symmetric function (Adv. Math. 1995).
• 1996 — Gasharov gives a positive Schur expansion via poset tableaux (Discrete Math. 1996).
• 2012/2016 — Shareshian and Wachs introduce the chromatic quasisymmetric function, prove its symmetry and Schur positivity for natural unit interval graphs, and conjecture elementary positivity over $\mathbb N[q]$ and the Hessenberg connection (Configuration Spaces 2012; Adv. Math. 2016).
• 2013 — Guay-Paquet reduces the Stanley–Stembridge conjecture to unit interval orders (arXiv:1306.2400).
• 2015 — Athanasiadis gives a power-sum expansion (Electron. J. Combin. 2015).
• 2016–2018 — Brosnan–Chow (Adv. Math. 2018) and Guay-Paquet (arXiv:1601.05498) prove the Hessenberg representation identity.
• 2019–2023 — Positivity for substantial subfamilies: abelian Hessenberg varieties (Harada–Precup 2019), explicit expansions (Cho–Huh 2019), melting lollipops (Huh–Nam–Yoo 2020), abelian Dyck paths via $q$-rook theory (Colmenarejo–Morales–Panova 2023); the modular law of Abreu and Nigro (J. Combin. Theory Ser. A 2021).
• 2024–2025 — Hikita proves the Stanley–Stembridge conjecture ($q=1$) via a probabilistic formula (arXiv:2410.12758); his weights do not give coefficientwise positivity in $\mathbb N[q]$. Griffin, Mellit, Romero, Weigl and Wen give an independent proof (arXiv:2504.06936).
• 2026 — The OpenAI preprint Elementary positivity of chromatic quasisymmetric functions (OpenAI Math Release, September 24, 2026) claims elementary positivity over $\mathbb N[q]$ for all natural unit interval graphs, with an explicit permutation witness. It has not been peer reviewed and its theorem is not formally verified.

Setting

Let $h:[n]\to[n]$ be weakly increasing with $i\le h(i)$. The natural unit interval graph $G=G(h)$ has vertices $[n]=\{1,\dots,n\}$ and edges $\{i,j\}$ with $i<j\le h(i)$. A proper coloring $f:[n]\to\mathbb N_{>0}$ gives different colors to adjacent vertices, and $\operatorname{asc}_G(f)$ counts edges $\{a<b\}$ with $f(a)<f(b)$. The chromatic quasisymmetric function is

$$\chi_G(X;q)=\sum_{f\ \text{proper}} q^{\operatorname{asc}_G(f)}\prod_{a=1}^n x_{f(a)} .$$

For a partition $\lambda$, $e_\lambda=\prod_i e_{\lambda_i}$ with $e_k=\sum_{i_1<\dots<i_k}x_{i_1}\cdots x_{i_k}$. Let $D^0_G$ be the set of permutations $\sigma$ (as words $\sigma_1\cdots\sigma_n$) such that every adjacent descent $\sigma_i>\sigma_{i+1}$ is an edge, and $\operatorname{ginv}_G(\sigma)$ the number of inversions $i<j$, $\sigma_i>\sigma_j$, with $\{\sigma_i,\sigma_j\}$ an edge.

In Lean (namespace OAI.ElementaryPositivity), NaturalUnitIntervalGraph n stores a monotone extensive h : Fin n → Fin n; chromatic r is $\chi_G$ in $r$ variables as an MvPolynomial (Fin r) (Polynomial ℕ); Nondescent and graphInversions define $D^0_G$ and $\operatorname{ginv}_G$; a PermutationWitness is a map $\theta:D^0_G\to\{\lambda\vdash n\}$ together with the identity below in every number $r$ of variables, using Mathlib's MvPolynomial.esymmPart.

Formalization targets

Goal: elementary positivity with a permutation witness (Theorem 1.1)

For every $n$ and every natural unit interval graph $G$ on $[n]$ there is a map $\theta_G:D^0_G\to\{\lambda\vdash n\}$ with

$$\chi_G(X;q)=\sum_{\sigma\in D^0_G} q^{\operatorname{ginv}_G(\sigma)}\,e_{\theta_G(\sigma)}(X).$$

In particular every elementary coefficient of $\chi_G$ lies in $\mathbb N[q]$. The goal is published on the platform with status Open.

Significance

The result itself. The theorem resolves the elementary-positivity part of the Shareshian–Wachs conjecture, and at $q=1$, via Guay-Paquet's reduction, recovers the Stanley–Stembridge conjecture first proved by Hikita. It is stronger than positivity: it gives a combinatorial witness, assigning each permutation of $D^0_G$ an elementary partition while preserving its graph-inversion weight. Through the Brosnan–Chow/Guay-Paquet identity, it implies that each graded piece of the cohomology of a regular semisimple Hessenberg variety is a direct sum of Young permutation modules with multiplicities counted by the witness (Corollary 1.2). Elementary unimodality, the other part of the Shareshian–Wachs conjecture, is not addressed.

Formalizing it. The statement is a finite polynomial identity for each $n$, $G$ and $r$, fully expressible with Mathlib's multivariate polynomials and elementary symmetric polynomials. A machine-checked proof would certify a long bijective argument (walls, triangle moves, witness completion) with many case distinctions.

Difficulty

The coloring definition already has nonnegative coefficients in the monomial basis, but rewriting in the elementary basis involves subtraction, so positivity is not visible from the definition. Earlier positive formulas (Schur expansions, power-sum expansions, the acyclic-orientation formula) group partitions or work at $q=1$, and Hikita's probabilistic formula has rational $q$-weights that are only positive at real $q>0$, not coefficientwise. A proof over $\mathbb N[q]$ must produce, for each elementary partition and each power of $q$, a nonnegative integer count, uniformly over all graphs.

Formalization scope

• Graphs are encoded by h : Fin n → Fin n monotone with i ≤ h i (zero-indexed); edges are $i<j\le h(i)$ in either order.
• Colorings use $r$ colors Fin r and the identity is required for every $r\in\mathbb N$, which is equivalent to the identity of symmetric functions since both sides are homogeneous of degree $n$.
• Coefficients live in Polynomial ℕ, so nonnegativity in $\mathbb N[q]$ is built into the statement; the witness theta is an arbitrary function on the finite set $D^0_G$. The source's additional assertion that $\theta_G$ is produced by a deterministic terminating procedure is not encoded, but any such function on a finite set is computable by search, so nothing of mathematical substance is lost.
• Needed infrastructure: symmetric functions in finitely many variables, elementary basis manipulations, and bijections on ordered independent-set collections. These are reusable for other chromatic-function and LLT-positivity problems.

Selected references

• R. P. Stanley and J. R. Stembridge, On immanants of Jacobi–Trudi matrices and permutations with restricted position, J. Combin. Theory Ser. A 62 (1993). https://doi.org/10.1016/0097-3165(93)90048-D
• R. P. Stanley, A symmetric function generalization of the chromatic polynomial of a graph, Adv. Math. 111 (1995), 166–194. https://doi.org/10.1006/aima.1995.1020
• J. Shareshian and M. L. Wachs, Chromatic quasisymmetric functions, Adv. Math. 295 (2016). https://doi.org/10.1016/j.aim.2015.12.018
• M. Guay-Paquet, A modular law for the chromatic symmetric functions of (3+1)-free posets, arXiv:1306.2400 (2013). https://arxiv.org/abs/1306.2400v1
• P. Brosnan and T. Y. Chow, Unit interval orders and the dot action on the cohomology of regular semisimple Hessenberg varieties, Adv. Math. 329 (2018), 955–1001. https://doi.org/10.1016/j.aim.2018.02.020
• A. Abreu and A. Nigro, Chromatic symmetric functions from the modular law, J. Combin. Theory Ser. A 180 (2021). https://doi.org/10.1016/j.jcta.2021.105407
• T. Hikita, A proof of the Stanley–Stembridge conjecture, arXiv:2410.12758 (2024, revised 2025). https://arxiv.org/abs/2410.12758v2
• S. T. Griffin, A. Mellit, M. Romero, K. Weigl and J. J. Wen, On Macdonald expansions of q-chromatic symmetric functions and the Stanley–Stembridge conjecture, arXiv:2504.06936 (2025). https://arxiv.org/abs/2504.06936v1
• OpenAI, Elementary positivity of chromatic quasisymmetric functions, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2; Corollary 1.2, p. 4). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Elementary-Positivity-of-Chromatic-Quasisymmetric-Functions-September-24-2026/paper.pdf

Motivation

A vertex cover of a hypergraph $H$ 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. In an $r$-partite $r$-uniform hypergraph the vertices are split into $r$ parts and every edge contains exactly one vertex from each part. Ryser's covering conjecture asserts

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

For $r=2$ it is Kőnig's theorem, so it proposes a higher-dimensional analogue of the most basic min–max theorem of bipartite matching theory. In the intersecting case ($\nu=1$) it asks for a cover of size $r-1$, and it is equivalent to Gyárfás's conjecture that $r-1$ monochromatic trees cover any $r$-edge-coloured complete graph.

Background. An equivalent formulation appears in Henderson's 1971 thesis (doi:10.7907/J1Z1-SK19). Aharoni proved the case $r=3$ in 2001 (doi:10.1007/s004930170001); Gyárfás and Tuza settled the intersecting case through $r=5$; Haxell and Scott (2012) proved $\tau\le(r-\epsilon)\nu$ for $r=4,5$ (doi:10.37236/1175); Francetić, Herke, McKay and Wanless (2017) handled linear intersecting hypergraphs through rank nine (doi:10.1016/j.ejc.2016.10.004); Bishnoi, Das, Morris and Szabó (2021) treated $t$-intersecting hypergraphs (doi:10.1016/j.jcta.2020.105366). Truncated projective planes give equality whenever $r-1$ is a prime power; equality examples were studied by Mansour, Song and Yuster (2009, doi:10.1007/s00373-008-0821-9), Aharoni, Barát and Wanless (2016, doi:10.1007/s00373-015-1575-9) and Abu-Khazneh, Barát, Pokrovskiy and Szabó (2019, doi:10.1016/j.jcta.2018.07.011). Clow, Haxell and Mohar disproved Lovász's stronger matching-reduction conjecture at $r=3$ (doi:10.1007/s00493-026-00220-3), without contradicting Ryser's inequality.

The source of this mission, an OpenAI preprint dated September 23, 2026, claims intersecting counterexamples for ranks $r=s^n+1$.

Setting

A finite hypergraph is a finite set of edges, each a finite set of vertices. It is $r$-partite $r$-uniform if there is a map assigning each vertex one of $r$ parts such that every edge contains exactly one vertex of each part. It is intersecting if it is nonempty and any two distinct edges share a vertex, so $\nu(H)=1$. Every edge of an intersecting hypergraph is itself a cover, so $\tau(H)\le r$ always; a counterexample to Ryser's conjecture in the intersecting case needs $\tau(H)=r$.

Formalization targets

Milestone: special case of Theorem 1.1

There are a prime $p>5$ with $p\equiv2\pmod3$ and $N$ such that for every prime $n\ge N$, $n>2$, an intersecting $(p^n+1)$-partite $(p^n+1)$-uniform hypergraph with $\nu=1$ and $\tau=p^n+1$ exists.

Goal: Theorem 1.1

There is $s_0$ such that for every prime $s\ge s_0$ with $s\equiv2\pmod 3$ there is $n_0(s)\ge3$ such that for every odd $n\ge n_0(s)$, with $q=s^n$, there is a finite intersecting $(q+1)$-partite $(q+1)$-uniform hypergraph $H$ with

$$\tau(H)=q+1>q=(r-1)\,\nu(H).$$

In particular infinitely many ranks fail. Lean: OAI.RyserOdd.eventualOddFailures_and_infinite, open on the platform.

Significance

The theorem would disprove Ryser's conjecture in its intersecting case, and through the standard transfer (Corollary 1.2) also Gyárfás's monochromatic tree-cover conjecture, for the ranks $s^n+1$. The value $\tau=r$ is the maximum possible. A companion preprint of the same family covers a different range of ranks (prime $q$, with balanced parts); the two constructions are independent apart from three elementary estimates. Thresholds are not numerical. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

The truncated-plane examples sit exactly at $\tau=r-1$, and covers may mix vertices from different parts, so enlarging individual parts does not help. One must insert exceptional edges that destroy every cover of size $q$ while preserving the intersecting property. Ruling out all small covers requires showing that any small cover contains almost a full pencil of lines, which over $\mathbb F_{s^n}$ needs an incidence bound with a power saving (a Bourgain–Katz–Tao-type sum–product estimate) valid in fields whose proper subfields are small. This is where odd exponents and the congruence $s\equiv2\pmod3$ enter.

Formalization scope

• Hypergraph V := Finset (Finset V) over a finite type V with decidable equality.
• RPartiteUniform r H: some part : V → Fin r with exactly one vertex of each part in every edge. Uniform r H: every edge has r vertices.
• Intersecting: distinct edges meet. matchingNumber is the maximal size of a pairwise disjoint subfamily; coverNumber is sInf of cover sizes, and existence of a cover is asserted separately so the sInf is not the empty-set default.
• ExplicitFailureAt r packages all of these with $\nu=1$, $\tau=r$ and $(r-1)\nu<\tau$; the goal asserts it for the stated ranks and that the set of failing ranks is infinite.

Needed infrastructure: finite fields $\mathbb F_{s^n}$ and their projective planes, incidence and sum–product estimates, and probabilistic selection arguments. Contributions formalizing Theorem 2.1 (uniform incidence saving), Lemma 3.2 (line covers after random deletions) or Theorem 4.1 (compatible translates from independent pools) are welcome.

Selected references

• OpenAI, A counterexample to Ryser's covering conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Counterexample-to-Rysers-Covering-Conjecture-September-23-2026/paper.pdf
• J. R. Henderson, Permutation decompositions of (0,1)-matrices and decomposition transversals, PhD thesis, 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
• J. Bourgain, N. Katz, T. Tao, A sum-product estimate in finite fields, and applications, Geom. Funct. Anal., 2004. https://doi.org/10.1007/s00039-004-0451-1
• A. Clow, P. Haxell, B. Mohar, A counterexample to a conjecture of Lovász, Combinatorica, 2026. https://doi.org/10.1007/s00493-026-00220-3
• OpenAI, Balanced counterexamples to Ryser's conjecture at prime orders, preprint, September 27, 2026.

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

Weisfeiler–Leman (WL) refinement compares two graphs by repeatedly refining colors of ordered vertex $k$-tuples. For every fixed dimension $k$ this is a polynomial-time procedure, with running time $n^{O(k)}$. When $k$ is part of the input, that computation is no longer polynomial, and the complexity of deciding the outcome becomes a question in its own right. Seppelt (2024) proved coNP-hardness and recorded Berkholz's question whether the problem is EXPTIME-complete.

This preprint answers that question for the joint-update convention: deciding $k$-WL equivalence of two explicit graphs with $k$ in binary is EXPTIME-complete, even on connected graphs of maximum degree three.

Background

• 1968. Weisfeiler and Leman introduce the refinement method.
• 1982. Luks shows isomorphism of graphs of bounded degree is decidable in polynomial time.
• 1992. Cai, Fürer and Immerman construct degree-three graphs with small color classes that remain indistinguishable with linearly many counting variables.
• 2019. Kiefer and Neuen record the joint-update convention and its bijective $(k+1)$-pebble game characterization.
• 2024–2025. Seppelt, and independently Lichter, Raßmann and Schweitzer, prove coNP-hardness of WL equivalence with the dimension as input. Grohe, Lichter, Neuen and Schweitzer compress CFI graphs to obtain long refinement sequences.
• 2026. The OpenAI preprint Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs (dated September 25, 2026) proves EXPTIME-completeness; companion preprints treat identification and fixed-dimension time lower bounds. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Graphs are finite, simple, undirected and uncolored, given by adjacency matrices. In the joint-update convention a $k$-tuple's initial color records equalities and adjacencies among its entries; each round adjoins to the old color the multiset, over replacement vertices $z$, of the vector of $k$ old colors obtained by replacing each coordinate in turn by $z$. Color names are common to both graphs, and $G \equiv_k H$ means their $k$-tuple color histograms agree at every round.

The language $\mathrm{WL}$ consists of encodings $(G, H, k)$ with $k \ge 2$ in binary and $G \equiv_k H$. The language $\mathrm{SubWL}$ additionally requires $G$ and $H$ to be connected, of the same positive order, and of maximum degree at most three. Malformed encodings are excluded.

In Lean (OAI.VariableWL), Graph is a SimpleGraph on Fin order, color and histogram implement the joint update by recursion on rounds, pairCode concatenates the two graph codes (order header plus row-major matrix) and the code of $k$, and complexity classes are defined from an explicit deterministic Turing machine model with OutputsWithin, InEXPTIME, PolytimeReduces and EXPTIMEComplete.

Formalization targets

Goal: Theorem 1.1

Both $\mathrm{WL}$ and $\mathrm{SubWL}$ are EXPTIME-complete under deterministic polynomial-time many-one reductions:

$$\mathrm{WL},\ \mathrm{SubWL} \in \mathrm{EXPTIME}, \qquad L \le_p \mathrm{WL} \text{ and } L \le_p \mathrm{SubWL} \text{ for every } L \in \mathrm{EXPTIME}.$$

Significance

The result. Theorem 1.1 resolves the question recorded by Seppelt and strengthens the known coNP-hardness to EXPTIME-completeness. The subcubic case is notable because isomorphism of bounded-degree graphs is polynomial-time (Luks), yet equivalence under refinement at a supplied dimension remains EXPTIME-complete for degree three; nonisomorphic graphs can be equivalent. Corollary 8.3 shows hardness persists with $k$ in unary.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The uniform computation interface developed here is reused by the companion identification paper, so a formalization would serve both missions.

Difficulty

Membership requires showing that the dimension can be capped before allocating tuple tables (Lemma 2.2), since $k$ may exceed the graph order. Hardness requires simulating an arbitrary exponential-time computation by a graph pair whose WL equivalence at a polynomially encoded dimension reflects acceptance. Because the number of address coordinates grows with the input, fixed-dimension constructions with dimension-dependent constants do not give a uniform polynomial-time reduction, and in the subcubic case colors must be realized by uncolored degree-three gadgets that a winning strategy still recognizes.

Formalization scope

• Graphs: SimpleGraph (Fin order); Subcubic bounds every vertex degree by three; SubWL also demands positive equal orders and connectivity.
• Equivalence quantifies over all rounds $s$; colors are nested Multiset types.
• Dimension $k \ge 2$ is encoded in binary after a unary length header.
• The Turing machine model is explicit; EXPTIME bounds are $2^{c(n+1)^d}$ and reductions run in $c(n+1)^d$ steps.

The statement is not trivial: both membership and hardness are required for both languages.

Needed infrastructure: the bijective game characterization (Lemma 2.4), product-circuit compilation (Proposition 3.2), the general and subcubic realizations (Propositions 5.1 and 7.1) and the uniform compiler (Proposition 8.2). Contributions toward any of these are welcome.

Selected references

• OpenAI, Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Variable-dimension-Weisfeiler-Leman-equivalence-on-general-and-subcubic-graphs-September-25-2026/paper.pdf
• OpenAI, The complexity of identifying a graph by Weisfeiler–Leman refinement, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/main/preprints/The-complexity-of-identifying-a-graph-by-Weisfeiler-Leman-refinement-September-25-2026/paper.pdf
• B. Weisfeiler, A. Leman, The Reduction of a Graph to Canonical Form and the Algebra Which Appears Therein, 1968. https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
• J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
• E. M. Luks, Isomorphism of Graphs of Bounded Valence Can Be Tested in Polynomial Time, J. Comput. Syst. Sci. 25 (1982). https://doi.org/10.1016/0022-0000(82)90009-5
• S. Kiefer, D. Neuen, The Power of the Weisfeiler–Leman Algorithm to Decompose Graphs, MFCS 2019.
• T. Seppelt, An Algorithmic Meta Theorem for Homomorphism Indistinguishability, MFCS 2024.
• M. Lichter, S. Raßmann, P. Schweitzer, Computational Complexity of the Weisfeiler–Leman Dimension, CSL 2025. https://doi.org/10.4230/LIPIcs.CSL.2025.13
• M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978

Motivation

The Weisfeiler–Leman (WL) method colors $k$-tuples of vertices by repeatedly recording their local extension patterns; two graphs are $k$-WL equivalent when the stable color histograms agree. For each fixed $k$ the direct algorithm runs in time $n^{O(k)}$: there are $n^k$ tuples and polynomially many refinement rounds. The question is whether the growing exponent is necessary for any algorithm deciding the equivalence relation, not just for implementations of refinement.

This preprint proves that it is, unconditionally: for every sufficiently large fixed $k$, every deterministic sequential decider for $k$-WL equivalence needs time $n^{ck}$ at every sufficiently large graph order, without assuming the Exponential Time Hypothesis.

Background

• 1966. Hennie and Stearns use padded machine indices and clocked self-simulation in their time-hierarchy proof.
• 1968. Weisfeiler and Leman introduce the refinement method.
• 1992. Cai, Fürer and Immerman's parity constructions establish limits of bounded-variable graph identification.
• 1996. Hella introduces the bijective pebble game characterizing counting-logic equivalence.
• 1999. Grohe proves equivalence in finite-variable logics is complete for polynomial time.
• 2013. Berkholz proves unconditional time lower bounds with exponent linear in the number of pebbles for existential pebble games.
• 2024–2025. Seppelt, and Lichter, Raßmann and Schweitzer, prove coNP-hardness of WL equivalence when the dimension is part of the input. Grohe, Lichter, Neuen and Schweitzer prove $\Omega_k(n^{k/2})$ lower bounds on the number of refinement rounds via compressed CFI graphs; such bounds do not constrain other algorithms deciding the equivalence.
• 2026. The OpenAI preprint Unconditional time lower bounds for Weisfeiler–Leman equivalence (dated September 25, 2026) proves the bound stated below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Graphs are finite, simple, undirected and uncolored, given as $n \times n$ adjacency matrices. For a $k$-tuple, the initial color records coordinate equalities and adjacencies. Each refinement step keeps the old color and adds, in the joint convention, the multiset over vertices $z$ of the $k$-vectors of colors obtained by replacing each coordinate by $z$; in the separate convention, one such multiset per coordinate. Two $n$-vertex graphs are $k$-WL equivalent if their color histograms agree at every round.

A decider for a convention and dimension $k$ is a deterministic machine that halts on every encoded pair of $n$-vertex graphs and accepts exactly the equivalent pairs. Its worst-case time $T_A(n)$ is the maximum running time over pairs of $n$-vertex graphs (optionally restricted to connected graphs of diameter at most two).

In Lean (OAI.WLTime), Graph n is a symmetric loopless Boolean matrix on Fin n, tupleColor and histogram define both conventions by recursion on rounds, Equivalent compares all rounds, encodePair encodes $n$ and both matrices, and machines are either multitape Turing machines (TM) or logarithmic-word RAMs (RAM) whose word operations are themselves implemented by Turing machines in time polynomial in the word length.

Formalization targets

Goal: Theorem 1.1

There are absolute constants $c > 0$ and $k_0$ such that for every fixed $k \ge k_0$, either convention, either input class (all graphs, or connected graphs of diameter at most two) and every correct deterministic decider $A$ in either machine model, there is $n_0 = n_0(A, k)$ with

$$T_A(n) \ge n^{ck} \qquad \text{for every } n \ge n_0 .$$

The exponent constant $c$ is independent of $k$ and of the program; the threshold $n_0$ may depend on both. The bound holds at every large order, not only infinitely often.

Significance

The result. Theorem 1.1 rules out any running time $f(k)\,n^{g(k)}$ with $g(k) = o(k)$, unconditionally. Earlier lower bounds either concerned the number of refinement rounds, assumed ETH, or treated the dimension as part of the input (coNP- and EXPTIME-hardness), which does not give a fixed-dimension exponent. It covers both standard update conventions and the restricted class of diameter-two graphs.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The Lean statement fixes explicit machine models, so a proof would include a verified padded diagonalization (Theorem 5.2), a verified computation-to-graph reduction (Theorem 4.3) and a verified compressed consistency construction (Theorem 3.2).

Difficulty

Unconditional time lower bounds in concrete models are rare; the only general technique is diagonalization, which yields hard languages but not hard natural problems. The proof must therefore transfer a diagonal language to WL equivalence through a reduction that is efficient enough to preserve an exponent linear in $k$. A polynomial-time computation with exponent proportional to $k$ has too many addressed locations to list in a small reduction, and local consistency is symmetric whereas a computation must propagate information forward without forcing false predecessors to become true.

Formalization scope

• Decides A c k p requires halting and correctness on every pair in the input class at every order $n$; worstTime is a Finset.sup over pairs in the class.
• Diameter two includes $n > 0$ and every pair of vertices equal, adjacent, or with a common neighbour (hence connected).
• Turing machines have finitely many tapes, states and symbols; RAM words have $O(\log(n+2))$ bits, and RAM instructions are fixed finite programs whose word operations carry a polynomial-time implementation.
• Time is a natural number; the bound $n^{ck}$ is compared in ℝ.

The statement is not vacuous: correct deciders exist (direct refinement), so the conclusion constrains real algorithms.

Needed infrastructure: bijective pebble games and their equivalence with refinement (Lemma 2.3), Turing machine simulation and clocking, and the graph constructions of Sections 3–4. Contributions toward any of these components are welcome.

Selected references

• OpenAI, Unconditional time lower bounds for Weisfeiler–Leman equivalence, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence-September-25-2026/paper.pdf
• B. Weisfeiler, A. Leman, The Reduction of a Graph to Canonical Form and the Algebra Which Appears Therein, 1968. https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
• J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
• L. Hella, Logical Hierarchies in PTIME, Information and Computation 129 (1996). https://doi.org/10.1006/inco.1996.0070
• F. C. Hennie, R. E. Stearns, Two-Tape Simulation of Multitape Turing Machines, J. ACM 13 (1966). https://doi.org/10.1145/321356.321362
• C. Berkholz, Lower Bounds for Existential Pebble Games and k-Consistency Tests, Logical Methods in Computer Science 9 (2013).
• M. Grohe, Equivalence in Finite-Variable Logics Is Complete for Polynomial Time, Combinatorica 19 (1999). https://doi.org/10.1007/s004939970004
• M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978
• M. Lichter, S. Raßmann, P. Schweitzer, Computational Complexity of the Weisfeiler–Leman Dimension, arXiv:2402.11531, 2024. https://arxiv.org/abs/2402.11531
• T. Seppelt, An Algorithmic Meta Theorem for Homomorphism Indistinguishability, MFCS 2024.