Prove2Me
← Collections

OAI Math

All of openAI's results.

https://github.com/openai/math

317 missions

Missions

81–100 of 317
Completed
AnalysisDynamical Systems·Captain: wurtle

Boundedness and persistence of weakly reversible mass-action systemsResearch Paper

Motivation: can a weakly reversible reaction network lose a species or blow up?

Chemical reaction network theory studies the polynomial differential equations that describe concentrations of interacting species under mass-action kinetics, where each reaction proceeds at a rate proportional to the product of the concentrations of its reactants. A central theme is which properties of the dynamics are forced by the structure of the reaction graph alone, independently of the (usually unknown) rate constants. Weak reversibility — every reaction can be undone by some directed path of reactions — is the main structural condition in this theory. Two long-standing conjectures ask whether weak reversibility alone guarantees that no species dies out (persistence) and that no concentration grows without bound (boundedness). These questions matter for systems biology and chemical engineering, where extinction of a species or unbounded growth would contradict the modeled behavior, and they are closely tied to the global attractor conjecture for complex-balanced systems.

Timeline

  • 1972 — Horn and Jackson develop the equilibrium and stability theory of complex-balanced mass-action systems (ARMA 1972); Horn (ARMA 1972) and Feinberg (ARMA 1972) give complex-balancing criteria and the deficiency-zero analysis.
  • 1987 — Feinberg formulates the expectation that a positive trajectory of a weakly reversible system cannot converge to a boundary point (Chem. Eng. Sci. 1987, Remark 6.1.E).
  • 2010 — August and Barahona state the general boundedness and persistence conclusion (IFAC 2010); the source identifies a gap in one step of their proof (p. 2).
  • 2011 — Anderson separates the boundedness conjecture from the persistence conjecture and proves boundedness for a single linkage class (J. Math. Chem. 2011); he also proves the global attractor conjecture in the single-linkage case (SIAM J. Appl. Math. 2011).
  • 2012–2013 — Pantea proves persistence of bounded trajectories when the stoichiometric subspace has dimension two (SIAM J. Math. Anal. 2012); Craciun, Nazarov and Pantea prove boundedness, persistence and permanence for two-species systems (SIAM J. Appl. Math. 2013).
  • 2014 — Gopalkrishnan, Miller and Shiu prove permanence for strongly endotactic systems (SIAM J. Appl. Dyn. Syst. 2014).
  • 2019–2020 — Boros proves every positive stoichiometric class of a weakly reversible system contains a positive equilibrium (SIAM J. Math. Anal. 2019); Boros and Hofbauer reprove single-linkage permanence (SIAM J. Appl. Dyn. Syst. 2020).
  • 2026 — Craciun's revised toric-differential-inclusion approach gives persistence for bounded trajectories (arXiv:1501.02860v3).
  • 2026 — The OpenAI preprint Boundedness and persistence of weakly reversible mass-action systems (OpenAI Math Release, September 25, 2026) claims both conjectures for constant positive rates in every dimension. It has not been peer reviewed and its theorem is not formally verified.

Setting

Fix d≥1d\ge1 species. A reaction network consists of a finite set of complexes C⊂Z≥0d\mathcal C\subset\mathbb Z_{\ge0}^d and a set R\mathcal R of reactions y→y′y\to y' with y,y′∈Cy,y'\in\mathcal C, y≠y′y\neq y'. It is weakly reversible if for every reaction y→y′y\to y' there is a directed path of reactions from y′y' back to yy. Given positive rate constants κy→y′>0\kappa_{y\to y'}>0, the mass-action system is

x˙=f(x)=∑y→y′∈Rκy→y′ xy (y′−y),xy=∏i=1dxiyi.\dot x = f(x)=\sum_{y\to y'\in\mathcal R}\kappa_{y\to y'}\,x^{y}\,(y'-y),\qquad x^y=\prod_{i=1}^d x_i^{y_i}.

A positive trajectory is persistent if lim inf⁡t→∞xi(t)>0\liminf_{t\to\infty}x_i(t)>0 for every ii.

In Lean (namespace OAI.Problem326), a ReactionNetwork d has a Finset of complexes in Fin d → ℕ and a Finset of reactions between them with distinct source and target; WeaklyReversible is Relation.TransGen reachability from target back to source; massAction N κ is the vector field above; and IsGlobalForwardSolution N κ x0 x means x(0)=x0x(0)=x_0 and xx has derivative f(x(t))f(x(t)) at every t≥0t\ge0.

Formalization targets

Goal: global existence, boundedness and persistence (Theorem 1.1)

Let d≥1d\ge1, let the network be weakly reversible and all rates positive. For every x0∈R>0dx^0\in\mathbb R_{>0}^d the solution with x(0)=x0x(0)=x^0 exists for all t≥0t\ge0, and there is ε∈(0,1)\varepsilon\in(0,1), depending on the network, the rates and x0x^0, such that

ε≤xi(t)≤ε−1(t≥0, 1≤i≤d).\varepsilon\le x_i(t)\le\varepsilon^{-1}\qquad(t\ge0,\ 1\le i\le d).

The goal is published on the platform with status Open.

Significance

The result itself. The theorem proves the boundedness conjecture and the persistence conjecture together, for arbitrary constant positive rates, any number of linkage classes and any number of species; earlier results needed a single linkage class, two species, or a two-dimensional stoichiometric subspace. It applies whether or not the stoichiometric compatibility class is bounded. Combined with complex balance, it yields convergence to the unique positive equilibrium in each class (the global attractor conclusion; Remark 3.5, p. 15). The proof also produces, for each positive initial point, a compact convex forward-invariant polytope in the open orthant (Proposition 3.3, p. 13), which gives a short proof of Boros's existence theorem for positive equilibria (Corollary 3.4, p. 14).

Formalizing it. Statements about reaction networks quantify over all networks and all rates, so they are a natural fit for formal verification; the history includes a published proof with a gap in one step. A machine-checked proof would settle the status of the general theorem independently of that history.

Difficulty

The natural approach is to find a Lyapunov function or an invariant region whose boundary each reaction crosses inward. Individual reactions need not point inward across any fixed face, and near the orthant boundary and at infinity different monomials dominate in different regions, with ties between monomials that an arbitrary choice of face normal can reverse. The argument must control the combined flux across cuts of the reaction graph using the return paths given by weak reversibility, and must do so simultaneously for small and large concentrations; a naive comparison of monomials by total degree fails, as the source's example 2A⇄B2A\rightleftarrows B with (a,b)=(T,T3)(a,b)=(T,T^3) shows.

Formalization scope

  • Complexes are vectors in Fin d → ℕ, so exponents are nonnegative integers and ff is a polynomial vector field on Rd\mathbb R^d; the reaction set is a Finset with source ≠ target. Empty reaction sets and isolated complexes are allowed, as in the source.
  • Rates are a function on reactions with ∀ e, 0 < κ e; d>0d>0 is a hypothesis.
  • The conclusion asserts existence of some global forward solution and bounds for every global forward solution from x0x^0 (uniqueness is therefore not assumed). Solutions are functions ℝ → (Fin d → ℝ) with HasDerivAt at every t≥0t\ge0, including a two-sided derivative at t=0t=0.
  • The same ε\varepsilon works for all t≥0t\ge0 and all species; it may depend on x0x^0. No uniformity over initial points is claimed.
  • Needed infrastructure: Picard–Lindelöf for polynomial fields, forward invariance of convex polytopes (Nagumo-type tangency conditions), and graph-cut flux estimates. ODE invariance tools are reusable beyond this mission.

Selected references

2 thms2 active usersReviewed
Completed
Dynamical SystemsPure Mathematics·Captain: wurtle

Ergodicity of triangular billiards with an irrational angleResearch Paper

Motivation

A billiard in a polygon is a point moving at unit speed inside the table and reflecting off the sides by the law "angle of incidence equals angle of reflection". It is one of the simplest Hamiltonian systems and a standard model in mathematical physics; triangles also model two point masses colliding on a segment. The natural invariant probability measure is normalized area times uniform direction, and the basic question is ergodicity: are the only flow-invariant sets of measure 00 or 11? For polygons with angles that are rational multiples of π\pi the answer is no (the phase space splits into invariant surfaces, one for each family of directions). For triangles with an irrational angle the question has been open for every individual triangle, with only generic or specially approximable examples known.

Timeline

  • 1975. Zemlyakov and Katok construct the phase space, show that vertex-hitting trajectories form a null set, and prove topological transitivity for irrational polygons (doi:10.1007/BF01818045).
  • 1986. Kerckhoff, Masur and Smillie prove unique ergodicity in almost every direction for rational polygons, and ergodicity of the full flow for a dense GδG_\delta set of polygons (doi:10.2307/1971280).
  • 1997. Vorobets gives an explicit approximation condition implying ergodicity, with examples including irrational right triangles (doi:10.1070/SM1997v188n03ABEH000211).
  • 2002. Masur and Tabachnikov survey rational billiards and flat structures (doi:10.1016/S1874-575X(02)80015-7).
  • 2014 and 2022. Numerical studies of irrational right triangles and irrational isosceles triangles raise doubts about ergodicity (doi:10.1103/PhysRevE.89.042918, doi:10.1103/PhysRevE.105.L012201).
  • 2025. Forni and Moll develop a cohomological-equation framework for flat surfaces with cone points, proving constancy of sufficiently regular invariant functions under non-rational holonomy (arXiv:2510.18128).
  • 2026. Chaika and Forni prove weak mixing for a dense GδG_\delta set of nn-gons (doi:10.4007/annals.2026.203.3.1).

The source of this mission, an OpenAI preprint dated September 25, 2026, claims ergodicity for every triangle with at least one irrational angle.

Setting

Let QQ be the open interior of a nondegenerate triangle in R2\mathbb R^2 with angles α,β,γ\alpha,\beta,\gamma. The phase space is Q×S1Q\times S^1 (position and unit direction). The billiard flow Φt\Phi_t moves a state in a straight line at unit speed; on reaching an open side it reflects the direction across that side (tangential component preserved, normal component reversed). Trajectories that hit a vertex, in either time direction, have no continuation and are discarded; they form a null set. The invariant probability measure is

dμ=dA dθ2π Area(Q).d\mu=\frac{dA\,d\theta}{2\pi\,\mathrm{Area}(Q)}.

Φt\Phi_t is ergodic if every measurable AA with μ(Φt−1A △ A)=0\mu(\Phi_t^{-1}A\,\triangle\,A)=0 for all t∈Rt\in\mathbb R has μ(A)∈{0,1}\mu(A)\in\{0,1\}.

Formalization targets

Goal: Theorem 1

If at least one of α/π\alpha/\pi, β/π\beta/\pi, γ/π\gamma/\pi is irrational, then the billiard flow on Q×S1Q\times S^1 is ergodic for μ\mu:

μ(Φt−1A △ A)=0  ∀t∈R⟹μ(A)∈{0,1}.\mu(\Phi_t^{-1}A\,\triangle\,A)=0\ \ \forall t\in\mathbb R\quad\Longrightarrow\quad\mu(A)\in\{0,1\}.

The Lean statement OAI.TriangularBilliards.irrational_triangle_billiard also asks for the standard well-posedness facts (almost every state has a unique complete trajectory avoiding vertices, each Φt\Phi_t preserves μ\mu, and Φs+t=Φs∘Φt\Phi_{s+t}=\Phi_s\circ\Phi_t almost everywhere), so that the ergodicity clause is about the actual billiard flow. It is open on the platform.

Significance

The theorem settles ergodicity for the entire class of triangles with an irrational angle, including triangles with one rational and two irrational angles, with no genericity or Diophantine condition; earlier results gave ergodicity only for a residual set or for tables with exceptionally fast rational approximations. It also contradicts the non-ergodicity suggested by numerical experiments, which can now be attributed to slow convergence. The paper derives interior and boundary quantum ergodicity of Dirichlet and Neumann eigenbases and growth of nodal-domain counts for these triangles. The claim is ergodicity only, not mixing or unique ergodicity.

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

Difficulty

Triangle sides are straight, so there is no dispersing curvature to drive hyperbolicity, and trajectories near vertices have no continuous continuation. Rational-approximation arguments (Kerckhoff–Masur–Smillie, Vorobets) only reach generic or specially approximable tables. The Forni–Moll framework shows that invariant functions with horizontal Sobolev regularity are constant under non-rational holonomy, but a bounded invariant indicator has no such regularity a priori: one obtains an L2L^2 gradient for each angular Fourier coefficient separately, not a square-summable family, and must show each of these gradients vanishes.

Formalization scope

  • A Triangle is three affinely independent points of ℂ; table is the interior of their convex hull; side i is an open segment; angle i is the interior angle at vertex i via InnerProductGeometry.angle.
  • Phase space is ℂ × Circle with the product of normalized area on the table and the uniform angular probability (pushforward of normalized Lebesgue measure on [0,2π)[0,2\pi)).
  • A FlightChain is a bi-infinite strictly increasing sequence of collision times, unbounded in both directions, with collisions in open sides, straight flights through the open table, and specular reflection reflect across the side tangent. billiardFlow follows the unique chain if one exists and is the identity otherwise; the theorem must prove the singular set is null.
  • Ergodicity is stated for measurable sets with μ(Φt−1A△A)=0\mu(\Phi_t^{-1}A\triangle A)=0 for every real tt.

A complete development needs the geometry of unfolding, the null measure of vertex-hitting trajectories, Liouville measure preservation for billiards, angular Fourier decomposition on the doubled triangle, and holonomy arguments. Formalizing the well-posedness clauses alone (measure preservation and the a.e. flow property) is reusable for all polygonal billiards and is a welcome first contribution.

Selected references

2 thms2 active usersReviewed
Algebraic TopologyCombinatoricsDiscrete Geometry·Captain: wurtle

A nine-dimensional counterexample to Borsuk's covering assertionResearch Paper

Motivation

In 1933 Borsuk asked whether every bounded set of positive diameter in Rd\mathbb R^d can be split into d+1d+1 pieces of strictly smaller diameter. The answer is yes in dimensions d≤3d\le3 and for smooth convex bodies, and a regular simplex shows that d+1d+1 pieces may be necessary. Kahn and Kalai showed in 1993 that the answer is no in high dimensions, and since then the question has been: in which dimensions does Borsuk's assertion first fail? The smallest known counterexample dimension measures how far our understanding of diameter partitions extends; it has been reduced from 13251325 to 6363 by combinatorial constructions, while the assertion is open in all dimensions between 44 and the current record.

Timeline

The source of this mission, an OpenAI preprint dated September 23, 2026, claims a counterexample in dimension 99.

Setting

For a bounded set YY of positive diameter, b(Y)b(Y) is the least number of subsets of strictly smaller diameter that cover YY (covers and partitions give the same number). Borsuk's assertion in Rd\mathbb R^d is that b(Y)≤d+1b(Y)\le d+1 for every such Y⊂RdY\subset\mathbb R^d.

Let Sym4(R)\mathrm{Sym}_4(\mathbb R) be the real symmetric 4×44\times4 matrices with the Frobenius norm ∥A∥F2=tr⁡(A2)=∑i,jAij2\|A\|_F^2=\operatorname{tr}(A^2)=\sum_{i,j}A_{ij}^2. The trace-one hyperplane {tr⁡A=1}\{\operatorname{tr}A=1\} in Sym4(R)\mathrm{Sym}_4(\mathbb R) is a 99-dimensional affine Euclidean space. For a unit vector u∈R4u\in\mathbb R^4, uuTuu^{\mathsf T} is the orthogonal projector onto the line Ru\mathbb Ru. Two such projectors are at distance 2\sqrt2 exactly when the lines are orthogonal.

Formalization targets

Goal: Theorem 1.1

The set

X={uuT:u∈R4, ∥u∥=1}⊂{A∈Sym4(R):tr⁡A=1}X=\{uu^{\mathsf T}:u\in\mathbb R^4,\ \|u\|=1\}\subset\{A\in\mathrm{Sym}_4(\mathbb R):\operatorname{tr}A=1\}

is compact, has Frobenius diameter 2\sqrt2, and cannot be covered by ten subsets of diameter strictly less than 2\sqrt2. Hence b(X)≥11>9+1b(X)\ge11>9+1 and Borsuk's assertion fails in dimension 99. The Lean statement OAI.BorsukNine.main_theorem is open on the platform.

Significance

The theorem lowers the smallest known counterexample dimension for Borsuk's conjecture from 6363 to 99, and the paper extends it to compact counterexamples in every dimension d≥9d\ge9 (Corollary 7.1). Unlike previous counterexamples, which are finite point sets built from codes or strongly regular graphs, the witness is a continuum: the image of real projective 33-space under the projector embedding. The theorem does not determine the smallest failing dimension (the assertion remains undecided in dimensions 44 to 88) or the exact value of b(X)b(X).

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would combine metric geometry, an algebraic-topological degree argument and a finite combinatorial obstruction.

Difficulty

Previous counterexamples use finite sets where a counting argument (Frankl–Wilson type) forces many parts; such counting gives nothing for a 99-dimensional continuum. For XX, a cover by ten small sets corresponds to ten nonnegative functions on RP3\mathbb{RP}^3 summing to one, with orthogonal lines never sharing a positive coordinate. One would like to use the minimal number of vertices of a triangulation of RP3\mathbb{RP}^3 (Walkup: eleven), but the positive-support complex arising from such functions is not a triangulation, so its face structure has to be derived from the map itself.

Formalization scope

  • Vectors are EuclideanSpace ℝ (Fin 4); matrices are EuclideanSpace ℝ (Fin 4 × Fin 4), whose norm is the Frobenius norm. projector u has entries uiuju_iu_j.
  • projectorSet is the image of the unit sphere; traceOneSymmetric is the set of symmetric matrices of trace 11.
  • HasTenSmallCover: ten subsets of projectorSet covering it, each with Metric.diam < √2. Requiring the pieces to lie in XX loses no generality, and keeps Metric.diam away from its default value for unbounded sets.
  • The goal is the conjunction: IsCompact projectorSet, containment in traceOneSymmetric, Metric.diam projectorSet = √2, and ¬ HasTenSmallCover.

A complete development needs partitions of unity, mod-two degree of odd maps on spheres, local preimage counting, and a finite combinatorial case analysis on labelled supports. The finite combinatorial part (Sections 5–6) and Lemma 2.4 (reduction to strict gaps) are self-contained and welcome first contributions.

Selected references

2 thms1 active userReviewed
CombinatoricsDiscrete GeometryGraph Theory·Captain: wurtle

The Euclidean plane is not five-colorableResearch Paper

Motivation

The Hadwiger–Nelson problem asks for the chromatic number of the plane χ(R2)\chi(\mathbb R^2): the least number of colours needed to colour every point of the Euclidean plane so that any two points at distance exactly 11 receive different colours. Equivalently, it is the chromatic number of the infinite graph whose vertices are the points of the plane and whose edges are the unit-distance pairs. Since 1950 the answer has been known to lie between 44 and 77, and it is one of the best known open problems in combinatorial geometry. Its difficulty is that the colour classes may be arbitrary sets: no measurability or regularity is assumed, so analytic tools that work for measurable colourings do not apply directly.

This mission asks for a formal proof that five colours do not suffice, as claimed in an OpenAI preprint dated September 23, 2026 (source), so that 6≤χ(R2)≤76\le\chi(\mathbb R^2)\le7. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

  • 1950 — Nelson poses the problem and observes χ≥4\chi\ge4; Isbell finds a hexagonal 77-colouring (recounted by Soifer, Mathematics Competitions 2003).
  • 1951 — de Bruijn and Erdős: an infinite graph is kk-colourable iff every finite subgraph is (Indag. Math. 1951).
  • 1961 — Hadwiger publishes the problem with bounds 44 and 77 (Elem. Math. 1961); the Moser spindle gives a 7-vertex obstruction to three colours (Canad. Math. Bull. 1961).
  • 1973–2005 — Woodall studies region colourings (JCTA 1973); Townsend proves map-type colourings need six colours (JCTA 1981; Geombinatorics 2005).
  • 1981 — Falconer proves that measurable colourings need at least five colours (JCTA 1981).
  • 2018–2020 — de Grey constructs a finite unit-distance graph that is not 44-colourable, so χ≥5\chi\ge5 (arXiv:1804.02385); Heule and Parts shrink it (arXiv:1805.12181, arXiv:2010.12665); Exoo–Ismailescu give another proof (DCG 2020).
  • 2025 — Sokolov and Voronov prove seven colours are needed for polygonal map-type colourings (arXiv:2502.01958).
  • September 2026 — The OpenAI preprint claims χ(R2)≥6\chi(\mathbb R^2)\ge6 for arbitrary colourings (Theorem 1.1, p. 2).

Setting

A proper kk-colouring of the plane is any function c:R2→{1,…,k}c:\mathbb R^2\to\{1,\dots,k\} such that c(x)≠c(y)c(x)\ne c(y) whenever ∥x−y∥=1\|x-y\|=1, with ∥⋅∥\|\cdot\| the Euclidean norm. No measurability, continuity or regularity of the colour classes c−1(i)c^{-1}(i) is assumed. χ(R2)\chi(\mathbb R^2) is the least kk admitting a proper kk-colouring.

Formalization targets

Milestone: the upper bound χ(R2)≤7\chi(\mathbb R^2)\le7 (Theorem 1.1, p. 2)

There is a proper 77-colouring of the plane: colour the Voronoi hexagons of a triangular lattice (circumradius r=2/5r=2/5) by the seven cosets of an index-seven similar sublattice, assigning boundary points to any incident hexagon. This classical construction is reproved in the deduction of Theorem 1.1 (pp. 2–3), including all boundary points.

Goal: no proper five-colouring (Theorem 1.1, p. 2)

There is no function c:R2→{1,…,5}c:\mathbb R^2\to\{1,\dots,5\} with c(x)≠c(y)c(x)\ne c(y) whenever ∥x−y∥=1\|x-y\|=1. Together with the milestone this gives 6≤χ(R2)≤76\le\chi(\mathbb R^2)\le7.

Significance

The result itself. It raises the lower bound for the chromatic number of the plane from five (de Grey, 2018) to six, leaving only 66 and 77. Unlike de Grey's bound it is not witnessed by a finite graph; the proof transfers the problem to measurable colourings for every number of colours (Theorem 1.3, p. 2) and then excludes weak measurable five-colourings (Theorem 1.4, p. 2). The transfer theorem is of independent interest: in ZFC, a proper kk-colouring exists iff a weak measurable kk-colouring does. The preprint also derives a positive lower bound on the invariant-mean frequency of monochromatic unit pairs for every five-colouring (Corollary 1.5, p. 5).

Formalizing it. The statements are elementary, but the proof uses ergodic theory (a Furstenberg–Zimmer compact-extension tower and rigidity of invariant measures on a character group, Theorem 2.3, p. 6), spectral theory, density points, Fourier decay of circle measure, and planar topology. A formal proof would remove any doubt about a long and varied argument. The finite-graph bound χ≥5\chi\ge5 has been checked by SAT solvers, but no formal proof of a bound that is not witnessed by a finite graph is known.

Difficulty

By de Bruijn–Erdős, χ≥6\chi\ge6 is equivalent to the existence of a finite unit-distance graph that is not 55-colourable, but no such graph is known, and SAT-based searches have not produced one. Measurable methods (Falconer's density-point argument) cannot be applied to arbitrary colour classes, and a measurable colouring can have boundaries far too irregular for map-type interface arguments such as Townsend's or Sokolov–Voronov's. The preprint must therefore (i) produce measurable data from an arbitrary colouring without losing the unit-distance exclusions, via invariant averaging over algebraic rotations and translations and the rigidity Theorem 2.3, and (ii) construct the connected interfaces needed for a geometric contradiction from measure estimates alone (Sections 5–7), before excluding label cycles of length 33, 44 and 55 (Section 8).

Formalization scope

  • The goal works in ℂ with ‖p - q‖ = 1; a colouring is any function ℂ → Fin 5. ProperColoring 5 c requires distinct colours at every unit-distance pair. No measurability is assumed, so the statement is about arbitrary colourings, as in the source.
  • The milestone works in EuclideanSpace ℝ (Fin 2) with dist x y = 1 and asks for some c : Plane → Fin 7; the two planes are isometric.
  • Both statements are in ZFC-style classical Lean; no choice-free reading is intended. Neither is vacuous.

Welcome contributions: the de Bruijn–Erdős compactness theorem, the Moser spindle, Lebesgue density points in R2\mathbb R^2, and the measurable/unrestricted transfer of Theorem 1.3.

Selected references

10 thms2 active usersReviewed
Completed
CombinatoricsNumber Theory·Captain: wurtle

Quantitative Superexponential Bounds for van der Waerden NumbersResearch Paper

Motivation

Van der Waerden's theorem (1927) says that for every number of colours rr and every length kk, every rr-colouring of a long enough interval of integers contains a monochromatic arithmetic progression of length kk. The van der Waerden number Wr(k)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, W2(k)≳2kW_2(k)\gtrsim 2^k. Erdős asked whether W2(k)1/k→∞W_2(k)^{1/k}\to\infty, i.e. whether the growth is genuinely faster than any exponential. Lower bounds on Wr(k)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 Wr(k)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 W2(p+1)>p 2pW_2(p+1)>p\,2^p for primes pp 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⁡kW2(k)1/k=∞\lim_k W_2(k)^{1/k}=\infty (doi:10.1016/S0167-5060(08)70697-6).
  • 1990. Szabó proves W2(k)≥2k/kεW_2(k)\ge 2^k/k^{\varepsilon} (doi:10.1002/rsa.3240010307).
  • 2016. Kozik and Shabanov prove Wr(k)≥βrk−1W_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≥5r\ge5 (doi:10.1007/s11856-025-2735-0).
  • 2026. Fox and Hunter prove superexponential growth for three colours, W3(k)>2klog⁡∗k/4W_3(k)>2^{k\log^*k/4} (arXiv:2606.02541); Campos, Fox and Schildkraut prove W2(k)≥(1−o(1))k2k−1W_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 kcklog⁡rk^{ck\log r} uniformly in r≥2r\ge2.

Setting

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

a, a+d, …, a+(k−1)d,a,d≥1,a+(k−1)d≤N.a,\ a+d,\ \dots,\ a+(k-1)d,\qquad a,d\ge1,\quad a+(k-1)d\le N.

Colourings may use fewer than rr colours.

Formalization targets

Goal: Theorem 1.1

There is an absolute K0K_0 such that for every k≥K0k\ge K_0 and every r≥2r\ge2,

Wr(k) > k c k⌊log⁡2r⌋,c=10−5.W_r(k)\ >\ k^{\,c\,k\lfloor\log_2 r\rfloor},\qquad c=10^{-5}.

In particular Wr(k)1/k→∞W_r(k)^{1/k}\to\infty for each fixed r≥2r\ge2. The constant cc 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 W2(k)/2k→∞W_2(k)/2^k\to\infty settled by Campos–Fox–Schildkraut. It is uniform in the number of colours with a single threshold K0K_0, which complements the Fox–Hunter bounds that require many colours relative to kk. 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 Wr(k)≳rk/poly(k)W_r(k)\gtrsim r^{k}/\mathrm{poly}(k): the number of kk-term progressions in [N][N] is of order N2N^2, and each is monochromatic with probability r1−kr^{1-k}, which caps the length at exponential size. Algebraic constructions such as Berlekamp's gain only a factor pp. 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+jda+jd equals the colour of aa for j<kj<k; HasMonoAP c k N: some d>0d>0 with a+(k−1)d<Na+(k-1)d<N.
  • IsRamsey α k N: every colouring ℕ → α has a monochromatic kk-AP in {0,…,N−1}\{0,\dots,N-1\} (equivalent to the paper's [N][N] after a shift).
  • W r k is the sInf of positive Ramsey NN for colours Fin r. If no such NN existed this would be 00 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 =⌊log⁡2r⌋=\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

2 thms1 active userReviewed
CombinatoricsGraph Theory·Captain: wurtle

Balanced counterexamples to Ryser's conjecture at prime ordersResearch Paper

Motivation

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

τ(H)≤(r−1) ν(H).\tau(H)\le(r-1)\,\nu(H).

For r=2r=2 this is Kőnig's theorem for bipartite graphs, so the conjecture is a proposed higher-dimensional Kőnig theorem. Its intersecting case (ν=1\nu=1, bound r−1r-1) is equivalent to Gyárfás's conjecture that every rr-edge-coloured complete graph can be covered by r−1r-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=5r=5; Gyárfás had handled r≤4r\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=3r=3 (doi:10.1007/s004930170001).
  • 2012. Haxell and Scott prove τ≤(r−εr)ν\tau\le(r-\varepsilon_r)\nu for r=4,5r=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 τ≥r−4\tau\ge r-4 (doi:10.37236/6460).
  • 2019. Abu-Khazneh, Barát, Pokrovskiy and Szabó construct intersecting (q+2)(q+2)-partite hypergraphs with τ=q+1\tau=q+1, matching the conjectured bound, for prime powers qq (doi:10.1016/j.jcta.2018.07.011).
  • 2025–2026. Clow, Haxell and Mohar disprove Lovász's stronger deletion conjecture at r=3r=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+1r=q+1. A (q+1)(q+1)-partite (q+1)(q+1)-uniform hypergraph on parts V1,…,Vq+1V_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 ν(H)=1\nu(H)=1, so Ryser's conjecture predicts τ(H)≤q\tau(H)\le q.

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

Formalization targets

Goal: Theorem 1.1

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

∣V1∣=⋯=∣Vq+1∣=q+1,τ(H)=q+1,|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 ν(H)=1\nu(H)=1 and τ(H)=q+1>q=r−1\tau(H)=q+1>q=r-1, the theorem would disprove Ryser's conjecture for infinitely many rr, in its intersecting case. The value τ=r\tau=r is the largest possible for an intersecting rr-uniform hypergraph (any edge is a cover), and the part sizes q+1q+1 are the smallest compatible with τ=r\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+1r=q+1 colours. The threshold q0q_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 qq-element cover while keeping the hypergraph intersecting and keeping only q+1q+1 vertices per part; adding a new part, as Abu-Khazneh et al. did, changes rr and only reaches equality. Verifying that no cover of size qq 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 ee contains the vertices (i,e(i))(i,e(i)).
  • Intersecting: edges nonempty and any two edges agree in some coordinate. Nonisolated: every (i,v)(i,v) lies in some edge. HasCoverNumber H k: some cover has exactly kk vertices and every cover has at least kk.
  • 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

2 thms1 active userReviewed
CombinatoricsGraph Theory·Captain: wurtle

A counterexample to Ryser's covering conjectureResearch Paper

Motivation

A vertex cover of a hypergraph HH is a set of vertices meeting every edge; the covering number τ(H)\tau(H) is the minimum size of a cover, and the matching number ν(H)\nu(H) is the maximum number of pairwise disjoint edges. In an rr-partite rr-uniform hypergraph the vertices are split into rr parts and every edge contains exactly one vertex from each part. Ryser's covering conjecture asserts

τ(H)≤(r−1) ν(H).\tau(H)\le(r-1)\,\nu(H).

For r=2r=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 (ν=1\nu=1) it asks for a cover of size r−1r-1, and it is equivalent to Gyárfás's conjecture that r−1r-1 monochromatic trees cover any rr-edge-coloured complete graph.

Background. An equivalent formulation appears in Henderson's 1971 thesis (doi:10.7907/J1Z1-SK19). Aharoni proved the case r=3r=3 in 2001 (doi:10.1007/s004930170001); Gyárfás and Tuza settled the intersecting case through r=5r=5; Haxell and Scott (2012) proved τ≤(r−ϵ)ν\tau\le(r-\epsilon)\nu for r=4,5r=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 tt-intersecting hypergraphs (doi:10.1016/j.jcta.2020.105366). Truncated projective planes give equality whenever r−1r-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=3r=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=sn+1r=s^n+1.

Setting

A finite hypergraph is a finite set of edges, each a finite set of vertices. It is rr-partite rr-uniform if there is a map assigning each vertex one of rr 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 ν(H)=1\nu(H)=1. Every edge of an intersecting hypergraph is itself a cover, so τ(H)≤r\tau(H)\le r always; a counterexample to Ryser's conjecture in the intersecting case needs τ(H)=r\tau(H)=r.

Formalization targets

Milestone: special case of Theorem 1.1

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

Goal: Theorem 1.1

There is s0s_0 such that for every prime s≥s0s\ge s_0 with s≡2(mod3)s\equiv2\pmod 3 there is n0(s)≥3n_0(s)\ge3 such that for every odd n≥n0(s)n\ge n_0(s), with q=snq=s^n, there is a finite intersecting (q+1)(q+1)-partite (q+1)(q+1)-uniform hypergraph HH with

τ(H)=q+1>q=(r−1) ν(H).\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 sn+1s^n+1. The value τ=r\tau=r is the maximum possible. A companion preprint of the same family covers a different range of ranks (prime qq, 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 τ=r−1\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 qq 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 Fsn\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≡2(mod3)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 ν=1\nu=1, τ=r\tau=r and (r−1)ν<τ(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 Fsn\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

2 thms1 active userReviewed
Completed
CombinatoricsDiscrete Geometry·Captain: wurtle

The weak pinned planar distance theoremResearch Paper

Motivation

Erdős's distinct-distance problems ask how few different distances nn 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 nn-point planar set determines at least cn/log⁡ncn/\log n distinct distances (Annals 2015), matching the square lattice up to a log⁡n\sqrt{\log n} factor. The pinned version asks for many distances measured from a single point: given PP, is there a pin x∈Px\in P from which almost nn distinct distances are visible? The weak pinned Erdős conjecture asserts that for every ε>0\varepsilon>0 some pin sees at least n1−ε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 log⁡n\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 n6/7n^{6/7} (DCG 2001).
  • 2003–2004 — Tardos improves the exponent with entropy inequalities (Adv. Math. 2003); Katz and Tardos reach every exponent below 48−14e55−16e=0.8641…\frac{48-14e}{55-16e}=0.8641\ldots (Contemp. Math. 342, 2004).
  • 2015 — Guth and Katz prove the global bound cn/log⁡ncn/\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⊂R2P\subset\mathbb R^2 be a finite set with ∣P∣=n≥2|P|=n\ge2. For distinct x,y∈Px,y\in P, the distance fibre size is

kP(x,y)=#{z∈P∖{x}: ∥z−x∥=∥y−x∥},k_P(x,y)=\#\{z\in P\setminus\{x\}:\ \|z-x\|=\|y-x\|\},

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

Fn(s)=sup⁡P⊂R2, ∣P∣=n #{(x,y)∈P2: x≠y, kP(x,y)≥ns}n(n−1),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 nsn^s.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every fixed s>0s>0,

Fn(s)⟶0(n→∞).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 ε>0\varepsilon>0, the fraction of pins x∈Px\in P with fewer than n1−εn^{1-\varepsilon} distinct distances tends to 00 uniformly in PP, so all but o(n)o(n) points see at least n1−εn^{1-\varepsilon} distances. This settles the weak pinned conjecture, improving the previous best exponent 0.8641…0.8641\ldots to 1−ε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/log⁡nn/\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 11, 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 (Z1(y)−Z1(x))(Z2(y)−Z2(x))(Z_1(y)-Z_1(x))(Z_2(y)-Z_2(x)) with Z1,2=u±ivZ_{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)∈P×P(x,y)\in P\times P with x≠yx\ne y and ns≤kP(x,y)n^s\le k_P(x,y); pairFraction divides by n(n−1)n(n-1) as a real.
  • F n s is the sSup over all nn-point sets of pairFraction for n≥2n\ge2 and is defined as 0 for n<2n<2. For n≥2n\ge2 the set of values is nonempty and contained in [0,1][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 Fn(s)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

7 thms2 active usersReviewed
CombinatoricsDiscrete Geometry·Captain: wurtle

A power saving for planar unit distancesResearch Paper

Motivation

The unit-distance problem of Erdős asks how many pairs among nn 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(n4/3)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β)u(n)=O(n^{\beta}) for some absolute β<4/3\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 n1+c/log⁡log⁡nn^{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(n4/3)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)=n1+o(1)u(n)=n^{1+o(1)} is disproved by an OpenAI construction with n1+εn^{1+\varepsilon} unit distances, simplified by Alon, Bloom, Gowers, Litt et al. (arXiv:2605.20695) and sharpened by Sawin to n1.014114n^{1.014114} (arXiv:2605.20579).
  • September 2026 — The OpenAI preprint claims the upper exponent can be lowered below 4/34/3 (Theorem 1.1, p. 1).

Setting

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

u(X)=#{{x,y}⊂X: ∥x−y∥=1},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⊂R2, ∣X∣=nu(X).u(n)=\max_{X\subset\mathbb R^2,\ |X|=n}u(X).

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

Formalization targets

Goal: Theorem 1.1 (p. 1)

There are absolute constants 0<C<∞0<C<\infty and 1≤β<4/31\le\beta<4/3 such that

u(n)≤C nβfor every integer n≥0.u(n)\le C\,n^{\beta}\qquad\text{for every integer }n\ge0.

Equivalently, u(n)=O(n4/3−δ)u(n)=O(n^{4/3-\delta}) for an absolute δ>0\delta>0. The goal leaves CC 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/34/3 can be lowered by a fixed amount. Combined with the recent lower bounds u(n)≥n1+εu(n)\ge n^{1+\varepsilon} along a sequence, it confines the true exponent to an interval strictly inside (1,4/3)(1,4/3). Because point–line incidences do attain n4/3n^{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(n4/3)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(n4/3)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 n4/3n^{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 t4−o(1)t^{4-o(1)} unit pairs among t3t^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 11) with dist = 1.
  • u n is the natural-number sSup of unitPairCount X over nn-element Finsets; the set is nonempty and bounded by (n2)\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=0n=0 both sides vanish.
  • There is no trivialization: β<4/3\beta<4/3 is strict and the bound must hold for every nn with constants independent of the configuration.

Selected references

2 thms1 active userReviewed
AlgebraCombinatoricsRepresentation Theory·Captain: wurtle

Combinatorial invariance of Kazhdan–Lusztig polynomialsResearch Paper

Motivation

Kazhdan–Lusztig polynomials Pu,b(q)P_{u,b}(q) are integer polynomials attached to pairs u≤bu\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 Pu,bP_{u,b} seemed to depend only on the Bruhat interval [u,b][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][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 qq 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 qq-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)(W,S) is a group WW with a generating set SS of involutions subject only to relations (st)mst=1(st)^{m_{st}}=1. Write ℓ\ell for word length in SS. A reflection is a conjugate of an element of SS. Bruhat order is the partial order generated by x<txx<tx whenever tt is a reflection and ℓ(tx)>ℓ(x)\ell(tx)>\ell(x); the interval [u,b]={x:u≤x≤b}[u,b]=\{x:u\le x\le b\} is finite and graded of rank ℓ(b)−ℓ(u)\ell(b)-\ell(u), even when WW is infinite. The equal-parameter R-polynomials Rx,yR_{x,y} and Kazhdan–Lusztig polynomials Px,yP_{x,y} are the unique families with Rx,x=Px,x=1R_{x,x}=P_{x,x}=1, Rx,y=Px,y=0R_{x,y}=P_{x,y}=0 unless x≤yx\le y, the recursion: for s∈Ss\in S with sy<ysy<y,

Rx,y={Rsx,sy,sx<x,(q−1)Rx,sy+q Rsx,sy,sx>x,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⁡Px,y<(ℓ(y)−ℓ(x))/2\deg P_{x,y}<(\ell(y)-\ell(x))/2 for x<yx<y, and the inversion formula

qℓ(y)−ℓ(x)Px,y(q−1)=∑x≤z≤yRx,z(q) Pz,y(q).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)(W,S) and (W′,S′)(W',S') be arbitrary Coxeter systems, u≤bu\le b in WW and u′≤b′u'\le b' in W′W'. If ι:[u,b]→[u′,b′]\iota:[u,b]\to[u',b'] is an isomorphism of posets (a bijection preserving and reflecting order), then

Pu,bW(q)=Pu′,b′W′(q).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 Px,yP_{x,y} with u≤x≤y≤bu\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 ss with sy<ysy<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→txx\to tx with tt a reflection and ℓ(x)<ℓ(tx)\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, 2deg⁡P<ℓ(y)−ℓ(x)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≤bu\le b, u′≤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

2 thms1 active userReviewed
CombinatoricsGraph TheoryRepresentation Theory·Captain: wurtle

Elementary positivity of chromatic quasisymmetric functionsResearch Paper

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 ("ee-positivity") is a central question in algebraic combinatorics. The Stanley–Stembridge conjecture (1993) predicted ee-positivity for incomparability graphs of (3+1)(3+1)-free posets; it arose from positivity questions for immanants of Jacobi–Trudi matrices. Shareshian and Wachs introduced a qq-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 qq with nonnegative integer coefficients. The qq-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 ee-positivity conjecture for (3+1)(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 N[q]\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 qq-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=1q=1) via a probabilistic formula (arXiv:2410.12758); his weights do not give coefficientwise positivity in N[q]\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 N[q]\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]→[n]h:[n]\to[n] be weakly increasing with i≤h(i)i\le h(i). The natural unit interval graph G=G(h)G=G(h) has vertices [n]={1,…,n}[n]=\{1,\dots,n\} and edges {i,j}\{i,j\} with i<j≤h(i)i<j\le h(i). A proper coloring f:[n]→N>0f:[n]\to\mathbb N_{>0} gives different colors to adjacent vertices, and asc⁡G(f)\operatorname{asc}_G(f) counts edges {a<b}\{a<b\} with f(a)<f(b)f(a)<f(b). The chromatic quasisymmetric function is

χG(X;q)=∑f properqasc⁡G(f)∏a=1nxf(a).\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λ=∏ieλie_\lambda=\prod_i e_{\lambda_i} with ek=∑i1<⋯<ikxi1⋯xike_k=\sum_{i_1<\dots<i_k}x_{i_1}\cdots x_{i_k}. Let DG0D^0_G be the set of permutations σ\sigma (as words σ1⋯σn\sigma_1\cdots\sigma_n) such that every adjacent descent σi>σi+1\sigma_i>\sigma_{i+1} is an edge, and ginv⁡G(σ)\operatorname{ginv}_G(\sigma) the number of inversions i<ji<j, σi>σj\sigma_i>\sigma_j, with {σi,σj}\{\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 χG\chi_G in rr variables as an MvPolynomial (Fin r) (Polynomial ℕ); Nondescent and graphInversions define DG0D^0_G and ginv⁡G\operatorname{ginv}_G; a PermutationWitness is a map θ:DG0→{λ⊢n}\theta:D^0_G\to\{\lambda\vdash n\} together with the identity below in every number rr of variables, using Mathlib's MvPolynomial.esymmPart.

Formalization targets

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

For every nn and every natural unit interval graph GG on [n][n] there is a map θG:DG0→{λ⊢n}\theta_G:D^0_G\to\{\lambda\vdash n\} with

χG(X;q)=∑σ∈DG0qginv⁡G(σ) eθG(σ)(X).\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 χG\chi_G lies in N[q]\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=1q=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 DG0D^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 nn, GG and rr, 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=1q=1, and Hikita's probabilistic formula has rational qq-weights that are only positive at real q>0q>0, not coefficientwise. A proof over N[q]\mathbb N[q] must produce, for each elementary partition and each power of qq, 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≤h(i)i<j\le h(i) in either order.
  • Colorings use rr colors Fin r and the identity is required for every r∈Nr\in\mathbb N, which is equivalent to the identity of symmetric functions since both sides are homogeneous of degree nn.
  • Coefficients live in Polynomial ℕ, so nonnegativity in N[q]\mathbb N[q] is built into the statement; the witness theta is an arbitrary function on the finite set DG0D^0_G. The source's additional assertion that θG\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

2 thms1 active userReviewed
CombinatoricsGraph TheoryProbability·Captain: wurtle

The sharp logarithmic exponent of r(5,t)Research Paper

Motivation: the growth of off-diagonal Ramsey numbers

For integers s,t≥2s,t\ge 2 the Ramsey number r(s,t)r(s,t) is the least nn such that every simple graph on nn vertices contains either a complete subgraph KsK_s or an independent set of tt vertices. Determining how r(s,t)r(s,t) grows when ss is fixed and t→∞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 KsK_s-free graphs with no large independent set, and for decades the two sides did not even agree on the power of tt.

Timeline

  • 1935 — Erdős and Szekeres prove r(s,t)≤(s+t−2s−1)r(s,t)\le\binom{s+t-2}{s-1} (Erdős–Szekeres 1935).
  • 1977 — Spencer's local-lemma method gives r(5,t)≳(t/log⁡t)3r(5,t)\gtrsim (t/\log t)^3 (Spencer 1977).
  • 1980 — Ajtai, Komlós and Szemerédi improve the fixed-ss upper bound to O(ts−1/(log⁡t)s−2)O(t^{s-1}/(\log t)^{s-2}) (AKS 1980).
  • 1995 — Kim shows r(3,t)r(3,t) has order t2/log⁡tt^2/\log t (Kim 1995).
  • 2001 — Li, Rousseau and Zang obtain upper leading constant 1+o(1)1+o(1) for fixed ss (Li–Rousseau–Zang 2001).
  • 2010 — Bohman and Keevash's analysis of the K5K_5-free process gives r(5,t)≳t3/(log⁡t)8/3r(5,t)\gtrsim t^3/(\log t)^{8/3} (Bohman–Keevash 2010, Thm 1.2).
  • 2024 — Mattheus and Verstraëte prove r(4,t)≥c t3/(log⁡t)4r(4,t)\ge c\,t^3/(\log t)^4 via Hermitian unitals, settling the power of tt for s=4s=4 (Mattheus–Verstraëte 2024).
  • 2026 — Bradač's projective construction gives r(s,t)≥cs ts−1/(log⁡t)2s−4r(s,t)\ge c_s\,t^{s-1}/(\log t)^{2s-4} for all s≥3s\ge3; for s=5s=5 the logarithmic exponent is 66 (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)=t4/(log⁡t)3+o(1)r(5,t)=t^4/(\log t)^{3+o(1)}, closing the gap between exponent 66 and the AKS-type exponent 33. The preprint has not been peer reviewed and its main theorem is not formally verified.

Setting

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

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

All logarithms are natural.

Formalization targets

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

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

t4(log⁡t)3+ε ≤ r(5,t) ≤ C t4(log⁡t)3,\frac{t^4}{(\log t)^{3+\varepsilon}}\ \le\ r(5,t)\ \le\ C\,\frac{t^4}{(\log t)^3},

and consequently

lim⁡t→∞4log⁡t−log⁡r(5,t)log⁡log⁡t=3.\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)r(5,t) up to a factor (log⁡t)o(1)(\log t)^{o(1)}, the first case beyond s=4s=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=3s-2=3 is the truth for s=5s=5, and it leaves open only a constant-factor asymptotic for t4/(log⁡t)3t^4/(\log t)^3. The lower-bound construction (random incident point–hyperplane pairs in projective space PG(4,q)\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≥2t\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 K5K_5-free graph on about t4/(log⁡t)3+εt^4/(\log t)^{3+\varepsilon} vertices with no independent set of size tt. Random graph processes lose logarithmic factors and even the power of tt; Bradač's projective graph has the right power but its independent sets were only controlled to logarithmic exponent 66. 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>0C>0 before ε\varepsilon; the threshold t0t_0 may depend on ε\varepsilon. The power (log⁡t)3+ε(\log t)^{3+\varepsilon} is Real.rpow. SharpExponent is a Filter.Tendsto statement over natural tt with real logarithms.
  • Needed infrastructure: finite projective geometry over Fq\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

2 thms1 active userReviewed
CombinatoricsGraph TheoryProbability·Captain: wurtle

Sharp logarithmic exponents for fixed off-diagonal Ramsey numbersResearch Paper

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

For integers s,t≥2s,t\ge2 the Ramsey number r(s,t)r(s,t) is the least NN such that every simple graph on NN vertices contains a clique of order ss or an independent set of order tt. Ramsey's theorem guarantees these numbers are finite. In the off-diagonal regime, ss is fixed and t→∞t\to\infty; the classical upper bounds give r(s,t)=Os ⁣(ts−1/(log⁡t)s−2)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 ts−1t^{s-1}. Once the power was settled, the remaining question was the power of log⁡t\log t.

Timeline

  • 1930 — Ramsey proves finiteness of these numbers (Ramsey 1930, Thm B).
  • 1935 — Erdős and Szekeres: r(s,t)≤(s+t−2s−1)=Os(ts−1)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)=Ωs((t/log⁡t)(s+1)/2)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)=Os(ts−1/(log⁡t)s−2)r(s,t)=O_s\big(t^{s-1}/(\log t)^{s-2}\big) (AKS 1980).
  • 1995 — Kim: r(3,t)=Θ(t2/log⁡t)r(3,t)=\Theta(t^2/\log t) (Kim 1995).
  • 2001 — Li, Rousseau and Zang: upper leading coefficient 1+o(1)1+o(1) (Li–Rousseau–Zang 2001).
  • 2010 — Bohman and Keevash, via the random KsK_s-free process: r(s,t)=Ωs(t(s+1)/2(log⁡t)1/(s−2)−(s+1)/2)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 KsK_s-free graphs would give ts−1/(log⁡t)2s−4t^{s-1}/(\log t)^{2s-4} (Mubayi–Verstraëte 2024); Mattheus and Verstraëte prove r(4,t)=Ω(t3/(log⁡t)4)r(4,t)=\Omega(t^3/(\log t)^4) (Mattheus–Verstraëte 2024).
  • 2026 — Bradač proves r(s,t)≥cs ts−1/(log⁡t)2s−4r(s,t)\ge c_s\,t^{s-1}/(\log t)^{2s-4} for every s≥3s\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)=ts−1/(log⁡t)s−2+o(1)r(s,t)=t^{s-1}/(\log t)^{s-2+o(1)} for every fixed s≥6s\ge6; a companion preprint treats s=5s=5. Neither has been peer reviewed, and the main theorem is not formally verified.

Setting

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

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

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

Formalization targets

Goal: sharp logarithmic exponent for every fixed s≥6s\ge6

For every integer s≥6s\ge6 there is Cs>0C_s>0 such that for every ε>0\varepsilon>0 and every sufficiently large tt (threshold depending on s,εs,\varepsilon)

ts−1(log⁡t)s−2+ε ≤ r(s,t) ≤ Cs ts−1(log⁡t)s−2,andlim⁡t→∞(s−1)log⁡t−log⁡r(s,t)log⁡log⁡t=s−2.\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=5s=5 preprint and the earlier results for s=3,4s=3,4 on the polynomial exponent, the theorem identifies the exact power of log⁡t\log t in r(s,t)r(s,t) up to (log⁡t)o(1)(\log t)^{o(1)} for each fixed ss: 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≥5d\ge5 and large primes qq, a Kd+1K_{d+1}-free graph on ⌊qdlog⁡q⌋\lfloor q^d\log q\rfloor vertices with independence number below q(log⁡q)1+ηq(\log q)^{1+\eta}, built from random incident point–hyperplane flags of PG(d,q)\mathrm{PG}(d,q).

Formalizing it. The upper half is classical (Proposition 7.3 of the source restates the AKS estimate for all fixed ss). 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−42s-4. Improving to s−2+o(1)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)r(s,t) because the defining set is nonempty by Ramsey's theorem.
  • MainBounds s fixes one C>0C>0 (depending on ss) before quantifying over ε\varepsilon; natural subtraction s - 1, s - 2 is harmless because s≥6s\ge6. MainLimit s is a Filter.Tendsto over natural tt.
  • The case s=5s=5 belongs to the companion preprint and is not part of this goal; s=3,4s=3,4 are not covered.
  • Needed infrastructure: projective spaces over Fq\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

2 thms1 active userReviewed
Completed
CombinatoricsGraph TheoryTheoretical Computer Science·Captain: wurtle

The strong thin tree conjectureResearch Paper

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)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/kC/k in a kk-edge-connected graph.

Background. Goddyn recorded the conjecture in a 2004 problem list. The Nash–Williams–Tutte theorem (1961) gives ⌊k/2⌋\lfloor k/2\rfloor edge-disjoint spanning trees in a kk-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/k2/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 poly(log⁡log⁡n)/k\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)G=(V,E) be a finite undirected multigraph without loops; parallel edges are counted separately. For a nonempty proper subset ∅≠S⊊V\varnothing\ne S\subsetneq V, let δG(S)\delta_G(S) be the set of edges with exactly one endpoint in SS. GG is kk-edge-connected if ∣δG(S)∣≥k|\delta_G(S)|\ge k for every such SS. For an edge set T⊆ET\subseteq E, δT(S)=δG(S)∩T\delta_T(S)=\delta_G(S)\cap T. A spanning tree TT is α\alpha-thin if ∣δT(S)∣≤α∣δG(S)∣|\delta_T(S)|\le\alpha|\delta_G(S)| for every nonempty proper SS.

Formalization targets

Goal: Theorem 1.1 (strong thin trees)

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

∣δT(S)∣≤Ck ∣δG(S)∣(∅≠S⊊V).|\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/k1/k is optimal (two vertices joined by kk parallel edges). The theorem would settle both Goddyn's thin tree conjecture and its strong form, removing the poly(log⁡log⁡n)\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 nn. 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\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

5 thms2 active usersReviewed
CombinatoricsGraph TheoryTheoretical Computer Science·Captain: wurtle

A polynomial-time construction of strong thin treesResearch Paper

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)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/kC/k in every kk-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/(klog⁡log⁡n))O(\log n/(k\log\log n))-thin trees. Oveis Gharan and Saberi constructed O(1/k)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 poly(log⁡log⁡n)/k\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 ∅≠S⊊V(G)\varnothing\ne S\subsetneq V(G), δG(S)\delta_G(S) is the multiset of edges with exactly one endpoint in SS, and GG is kk-edge-connected if ∣δG(S)∣≥k|\delta_G(S)|\ge k for every such SS. A spanning tree TT is α\alpha-thin if ∣δT(S)∣≤α∣δG(S)∣|\delta_T(S)|\le\alpha|\delta_G(S)| for all such SS. 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 CC and a deterministic algorithm that, given k≥1k\ge1 and a kk-edge-connected multigraph GG on at least one vertex (in either format), returns in time polynomial in the input length a spanning tree TT with

∣δT(S)∣≤Ck ∣δG(S)∣(∅≠S⊊V(G)),|\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/kC/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/k1/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≥1n\ge1, k≥1k\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=1n=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

2 thms1 active userReviewed
Completed
CombinatoricsGraph TheoryProbability·Captain: wurtle

The second Kahn–Kalai conjectureResearch Paper

Motivation

When does the Erdős–Rényi random graph G(n,p)G(n,p) contain a copy of a prescribed graph HH? A necessary condition is visible from first moments: if some subgraph F⊆HF\subseteq H has expected copy count below a constant, then HH 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 pc=O(qflog⁡ℓ)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 pc=O(pElog⁡3n)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)))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,FG,F let N(G,F)N(G,F) be the number of subgraphs of GG isomorphic to FF (ordinary, non-induced copies). G(n,p)G(n,p) is the random graph on [n][n] with each of the (n2)\binom n2 edges present independently with probability pp. For a graph HH with at least one edge and at most nn vertices,

pc(n,H)=inf⁡{p∈[0,1]: Pr⁡[N(G(n,p),H)>0]≥12},p_c(n,H)=\inf\{p\in[0,1]:\ \Pr[N(G(n,p),H)>0]\ge\tfrac12\}, pE(n,H)=inf⁡{p∈[0,1]: E N(G(n,p),F)≥12 for every subgraph F⊆H}.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 pE≤pcp_E\le p_c. Write h=e(H)h=e(H) for the number of edges.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every n≥2n\ge2 and every finite simple graph HH with h≥1h\ge1 edges and at most nn vertices,

pc(n,H) ≤ min⁡{1, 2048 e50 pE(n,H) (1+log⁡2h)},pc(n,H) ≤ 6144 e50 pE(n,H)log⁡2n.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; HH may vary with nn.

Significance

The result itself. The bound says that, up to a universal constant times log⁡h\log h, the only obstruction to containing HH is a subgraph with too few expected copies. The logarithm cannot be removed: for a perfect matching pE=Θ(1/n)p_E=\Theta(1/n) while pc=Θ(log⁡n/n)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 HH.

Formalizing it. Both thresholds are finite, explicit optimization problems over Bernoulli product measures on the edges of KnK_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 pcp_c with the integral expectation threshold of the family FH\mathcal F_H of edge sets containing a copy of HH, and covers of FH\mathcal F_H may be much cheaper than the copies of a single subgraph, so it does not give a bound in terms of pEp_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)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 pp but used only on [0,1][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∈[0,1]p\in[0,1]; the sets are nonempty (they contain p=1p=1 when HH has at most nn 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.
  • HH 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\log x/\log 2.
  • The constants 2048e502048e^{50} and 6144e506144e^{50} are hard-coded, as in the source.

Selected references

47 thms2 active usersReviewed
Algebraic TopologyCombinatoricsGroup Theory·Captain: wurtle

Bounded-degree coboundary expanders in every dimensionResearch Paper

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 F2\mathbb F_2 is the strongest of the standard notions: the coboundary of any set of ii-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 F2\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 F2\mathbb F_2 coboundary expanders in every dimension d≥3d\ge3. It has not been peer reviewed and its theorem is not formally verified.

Setting

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

wi(σ)=#{τ∈Y(s):σ⊆τ}(s+1i+1)∣Y(s)∣,∥f∥i=∑σ: f(σ)≠0wi(σ),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\|f\|_i is the probability that ff is nonzero on a random ii-face of a uniformly random top face, and dist⁡i(f,A)=min⁡a∈A∥f−a∥i\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 11-skeleton), weight, norm, coboundary, coboundaries and distance follow these definitions, and topDegree X d v counts dd-faces containing vv.

Formalization targets

Goal: bounded-degree coboundary expanders (Theorem 1.1)

For every d≥3d\ge3 there are D<∞D<\infty, ε>0\varepsilon>0 and finite connected pure dd-dimensional complexes XmX_m with ∣Xm(0)∣→∞|X_m(0)|\to\infty, every vertex in at most DD faces of dimension dd, and

∥δif∥Xm,i+1 ≥ ε dist⁡Xm,i(f,Bi(Xm))(f∈Ci(Xm;F2), 0≤i<d),\|\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 mm, ii and ff. 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 F2\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 F2\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 SLN(k[t])\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 Hi(Xm;F2)H^i(X_m;\mathbb F_2) for every i<di<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 dd, uniformly along the tower.

Formalization scope

  • Vertices are Fin vertexCount and every vertex is a face; faces are Finsets, and an ii-face has exactly i+1i+1 vertices.
  • Purity requires at least one dd-face; connectivity is of the 11-skeleton and requires a nonempty vertex set, so empty or disconnected complexes do not satisfy the hypotheses.
  • Cochains are ZMod 2-valued; B0B^0 is the constant cochains (reduced cohomology in degree 00). Distance is a real sInf over the image of a nonempty finite set, hence a minimum.
  • The inequality is required for every i<di<d and every cochain, with DD and ε\varepsilon chosen before the sequence and depending only on dd. Only d≥3d\ge3 is asserted; dimensions 11 and 22 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 F2\mathbb F_2 would be reusable for many high-dimensional-expansion problems.

Selected references

2 thms1 active userReviewed
Completed
AlgebraCombinatoricsNumber Theory·Captain: wurtle

The circulant Hadamard conjectureResearch Paper

Motivation

A Hadamard matrix of order nn is an n×nn\times n matrix with entries ±1\pm1 whose rows are mutually orthogonal, HHT=nInHH^{\mathsf T}=nI_n. Such matrices are extremal for Hadamard's determinant bound and are used throughout coding theory, experimental design and signal processing. Imposing a circulant structure, where every row is a cyclic shift of the first, links the problem to cyclic difference sets and to binary sequences with ideal periodic autocorrelation. The order-4 example with first row (−1,1,1,1)(-1,1,1,1) is easy to find; the circulant Hadamard conjecture, traditionally attributed to Ryser (1963), asserts that apart from the trivial order 1 there are no others.

The question is closely tied to Barker sequences, binary sequences with the smallest possible aperiodic autocorrelations, which are used as radar pulse-compression codes. Only lengths 2,3,4,5,7,11,132,3,4,5,7,11,13 are known, and the long-standing Barker-sequence conjecture says there are no others.

Timeline

Several complete proofs have been claimed (Oh-Hashi 2016, Orozco López 2019, Morris 2023, Gallardo 2024, Manjhi–Kumar 2025). The source of this mission is an OpenAI preprint dated September 23, 2026, which proves the conjecture by an argument with cyclotomic character values over the group ring Z[i][Cu2]\mathbb Z[i][C_{u^2}].

Setting

A real n×nn\times n matrix HH is circulant if there is a function h:Z/nZ→Rh:\mathbb Z/n\mathbb Z\to\mathbb R with Hij=h(j−i)H_{ij}=h(j-i), indices taken modulo nn. It is a sign Hadamard matrix if every entry is 11 or −1-1 and

HHT=n In.HH^{\mathsf T}=n\,I_n.

For a circulant sign matrix with first row hh, the periodic autocorrelations are Ph(t)=∑jhjhj+tP_h(t)=\sum_{j}h_jh_{j+t}; the Hadamard condition says Ph(t)=0P_h(t)=0 for 1≤t<n1\le t<n.

A Barker sequence of length nn is a∈{−1,1}na\in\{-1,1\}^n with aperiodic autocorrelations

Ca(t)=∑j=0n−t−1ajaj+t,∣Ca(t)∣≤1(1≤t<n).C_a(t)=\sum_{j=0}^{n-t-1}a_ja_{j+t},\qquad |C_a(t)|\le1\quad(1\le t<n).

Formalization targets

Goal: Theorem 1.1

For n≥1:∃ a real circulant Hadamard matrix of order n  ⟺  n∈{1,4}.\text{For } n\ge1:\quad \exists\ \text{a real circulant Hadamard matrix of order } n\iff n\in\{1,4\}.

The Lean statement OAI.CirculantHadamard.exists_iff_order_one_or_four is open on the platform.

Milestone: Corollary 1.2, even case

a∈{−1,1}n Barker, n≥1 even ⟹ n∈{2,4}.a\in\{-1,1\}^n\ \text{Barker},\ n\ge1\ \text{even}\ \Longrightarrow\ n\in\{2,4\}.

Combined with the classical odd-length classification, this gives the Barker length list {2,3,4,5,7,11,13}\{2,3,4,5,7,11,13\}.

Significance

Theorem 1.1 closes a problem open since the early 1960s and, through the even-length reduction, completes the classification of Barker-sequence lengths. Equivalently, it shows that cyclic difference sets with parameters (4u2, 2u2−u, u2−u)(4u^2,\,2u^2-u,\,u^2-u) exist only for u=1u=1. It also explains, in a single statement, the computational evidence of Logan and Mossinghoff and the arithmetic restrictions of Turyn and of Leung–Schmidt.

The result is proved in an OpenAI preprint that has not been peer reviewed; given the number of earlier claimed proofs, an independent machine-checked proof would be especially valuable. No formal proof of either statement exists; the formalization would also produce reusable group-ring and cyclotomic machinery.

Difficulty

The orthogonality condition is a norm equation hh∗=nhh^*=n in the group ring Z[Cn]\mathbb Z[C_n], and every character sends hh to a cyclotomic integer of absolute value n\sqrt n. Classical arguments use such character values one at a time, through factorization of ideals in cyclotomic fields, and stop at the case n=4u2n=4u^2 with uu odd and divisible by several primes. The obstruction must combine information from all prime divisors of uu simultaneously and use the fact that the coefficients are signs, not arbitrary integers; norm equations alone do have solutions at these orders.

Formalization scope

  • RealMatrix n := Matrix (Fin n) (Fin n) ℝ; IsCirculant H asks for h : Fin n → ℝ with H i j = h (j - i), where subtraction in Fin n is modular.
  • IsSignHadamard H is entrywise IsSign (equal to 11 or −1-1) together with H * H.transpose = (n : ℝ) • 1.
  • The goal assumes 0 < n, matching the paper's "positive integer nn".
  • The Barker milestone uses integer sequences Fin n → ℤ with IsSign entries and aperiodic h k = Σ_{j<n-k} h_j h_{j+k}, bounded by 11 in absolute value for 0<k<n0<k<n.

A complete development needs group rings of finite cyclic groups, characters and cyclotomic integers, localization at primes above pp, and Kronecker's theorem that an algebraic integer all of whose conjugates have absolute value one is a root of unity. Contributions formalizing Proposition 2.2 (the order restriction n=4u2n=4u^2, uu odd), Lemma 3.1 (character comparison) and Proposition 3.4 (alternating character products are roots of unity of odd order) are welcome.

Selected references

47 thms3 active usersReviewed
Completed
CombinatoricsGraph Theory·Captain: wurtle

A linear cycle-and-edge decomposition of every graphResearch Paper

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 nn vertices already needs n−1n-1 single-edge parts. The Erdős–Gallai cycle decomposition conjecture asserts that this is essentially the only obstruction: every graph on nn vertices can have its edge set partitioned into O(n)O(n) simple cycles and single edges. Equivalently, every graph with all degrees even partitions into O(n)O(n) cycles. The problem is a basic question about edge decompositions, and the partial bounds O(nlog⁡n)O(n\log n), O(nlog⁡log⁡n)O(n\log\log n) and O(nlog⁡∗n)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(nlog⁡n)O(n\log n) bound, distinguishing covers from edge-disjoint partitions (Canad. J. Math. 1966).
  • 1968 — Lovász: every graph on nn vertices partitions into at most ⌊n/2⌋\lfloor n/2\rfloor paths and cycles (On covering of graphs, 1968).
  • 1985 — Pyber shows that n−1n-1 cycles and edges suffice to cover (not partition) every graph (Combinatorica 1985).
  • 2014 — Conlon, Fox and Sudakov prove O(nlog⁡log⁡n)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+δ)n(3/2+\delta)n for dense graphs (Girão–Granet–Kühn–Osthus, J. LMS 2021).
  • 2024 — Bucić and Montgomery prove O(nlog⁡∗n)O(n\log^*n) (Adv. Math. 2024).
  • 2025 — Akbari, Aloni, Beikmohammadi and Clow prove n−1n-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 GG has vertex set of size nn and edge set E(G)E(G) of unordered pairs of distinct vertices. A cycle is a closed walk of length at least 33 with no repeated vertices except the endpoints; its edge set is the set of edges it traverses. A cycle-and-edge decomposition of GG into kk parts is a family E1,…,EkE_1,\dots,E_k of pairwise disjoint subsets of E(G)E(G) with union E(G)E(G), where each EiE_i is either the edge set of a cycle of GG or a single edge of GG. Parts may share vertices; isolated vertices need not be covered; for an edgeless graph k=0k=0 is allowed.

Formalization targets

Goal: Theorem 1.1 (p. 1)

There is an absolute constant C>0C>0 such that for every nn and every simple graph GG on nn vertices,

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

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

Significance

The result itself. The order nn is optimal (trees). The theorem implies that every Eulerian graph (all degrees even) partitions into O(n)O(n) cycles (Corollary 1.2, p. 2), and via known equivalences it gives the sharp Δ(G)/2+δn\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(nlog⁡n)o(n\log n) bound is known.

Difficulty

Covering is easy (Pyber's n−1n-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\log\log n and log⁡∗n\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 ss is p.edgeSet for some p : G.Walk v v with p.IsCycle (Mathlib cycles have length at least 33), or s={e}s=\{e\} for an edge e∈Ge\in G.
  • EdgeDecomposition G k: parts indexed by Fin k, each a cycle or single edge, pairwise disjoint, with union G.edgeSet.
  • MainStatement: ∃C>0, ∀n ∀G, ∃k,\exists C>0,\ \forall n\ \forall G,\ \exists k, EdgeDecomposition G k ∧ k≤Cn\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 kk is a genuine count.

Selected references

8 thms2 active usersReviewed
CombinatoricsHarmonic AnalysisNumber Theory·Captain: wurtle

A power saving for square-difference-free setsResearch Paper

Motivation: how large can a set avoid square differences?

A set A⊆{1,…,N}A\subseteq\{1,\dots,N\} is square-difference-free if no two of its elements differ by a perfect square m2m^2 with m≥1m\ge1. The Furstenberg–Sárközy theorem says such sets have density tending to zero; the question is how fast. Writing s(N)s(N) for the largest size of a square-difference-free subset of {1,…,N}\{1,\dots,N\}, the problem is a prototype for polynomial patterns in dense sets: it is the simplest case of finding differences in the image of a polynomial, and it is the model problem on which Fourier-analytic, ergodic and density-increment methods for polynomial configurations are tested. A long-standing gap separates the upper bounds, which until recently saved only a power of log⁡N\log N (with a slowly growing exponent), from the lower bounds, which are powers N0.73…N^{0.73\ldots} and beyond. Whether a fixed power saving s(N)≤CN1−cs(N)\le CN^{1-c} holds was posed explicitly by Green and Sawhney.

Background and timeline

  • 1977–1978 — Answering a question of Lovász, Furstenberg (J. Analyse Math. 1977, Theorem 1.2) and Sárközy (Acta Math. Hungar. 1978) independently prove s(N)=o(N)s(N)=o(N); Sárközy's bound is N/(log⁡N)1/3+o(1)N/(\log N)^{1/3+o(1)}.
  • 1984 — Ruzsa constructs square-difference-free sets of size ≫N0.7330…\gg N^{0.7330\ldots} (Period. Math. Hungar. 1984).
  • 1988 — Pintz, Steiger and Szemerédi prove s(N)≪N/(log⁡N)clog⁡log⁡log⁡log⁡Ns(N)\ll N/(\log N)^{c\log\log\log\log N} (J. LMS 1988).
  • 2008/2015 — Beigel and Gasarch (arXiv:0804.4892) and Lewko (Electron. J. Combin. 2015) improve the lower exponent to 0.7334…0.7334\ldots.
  • 2022 — Bloom and Maynard prove s(N)≪N/(log⁡N)clog⁡log⁡log⁡Ns(N)\ll N/(\log N)^{c\log\log\log N} (Compos. Math. 2022).
  • 2024/2025 — Green and Sawhney prove s(N)≪Nexp⁡(−clog⁡N)s(N)\ll N\exp(-c\sqrt{\log N}) and ask for a fixed power saving (arXiv:2411.17448, Theorem 1.1 and §1.1).
  • 2026 — Adajar et al. extend the arithmetic level-dd approach to intersective polynomials (arXiv:2605.16216); Krachun pushes the lower exponent past 3/43/4, to 0.7527…0.7527\ldots (arXiv:2608.01325).
  • 2026 — The OpenAI preprint A power saving for square-difference-free sets (OpenAI Math Release, September 24, 2026) claims s(N)≤CN1−cs(N)\le CN^{1-c} with absolute constants. It has not been peer reviewed and its theorem is not formally verified.

Setting

For a positive integer NN write [N]={1,…,N}[N]=\{1,\dots,N\}. A set A⊆[N]A\subseteq[N] is square-difference-free if

(A−A)∩{m2:m∈N, m≥1}=∅,(A-A)\cap\{m^2 : m\in\mathbb N,\ m\ge1\}=\varnothing,

that is, a−b≠m2a-b\neq m^2 for all a,b∈Aa,b\in A and all integers m≥1m\ge1. (Differences are taken in Z\mathbb Z; a−b=0a-b=0 is allowed since 00 is excluded from the squares.)

In Lean (namespace OAI.SquareDifference), sets are Finset ℤ contained in Finset.Icc 1 N, and IsSquareDifferenceFree A states a - b ≠ (m : ℤ)^2 for all a b ∈ A and m : ℕ with 1 ≤ m.

Formalization targets

Goal: a fixed power saving (Theorem 1.1)

There are absolute constants c>0c>0 and C<∞C<\infty such that for every integer N≥1N\ge1 and every square-difference-free A⊆[N]A\subseteq[N],

∣A∣≤C N1−c.|A|\le C\,N^{1-c}.

Equivalently, every subset of [N][N] with more than CN1−cCN^{1-c} elements contains two elements differing by a nonzero perfect square. The Lean goal is published on the platform with status Open. The statement fixes no numerical value of cc, so any improvement of the exponent leaves the goal unchanged.

Significance

The result itself. Every earlier upper bound saved less than any fixed power of NN; the best, due to Green and Sawhney, saved exp⁡(−clog⁡N)\exp(-c\sqrt{\log N}). A fixed power saving changes the nature of the problem: it shows that the extremal exponent lim sup⁡log⁡s(N)/log⁡N\limsup \log s(N)/\log N lies strictly below 11, so both upper and lower bounds are now polynomial and the remaining question is the value of the exponent, now known to lie between 0.7527…0.7527\ldots and 1−c1-c. As an immediate consequence (Remark 1.2 of the source), the graph on [N][N] joining integers differing by a square has chromatic number at least C−1NcC^{-1}N^c, a polynomial bound for the square-difference coloring problem.

Formalizing it. The statement is elementary and self-contained, involving only finite sets of integers. The proof combines a graph/tuple reformulation, reflection-positivity (chessboard) inequalities for a finite-field probability law, and an induction with fixed finite constructions. A formal proof would certify an argument whose constants are explicitly noted to be extremely small and not computed.

Difficulty

Density-increment arguments, starting from Sárközy's circle-method proof, gain a constant factor of density at each step but lose a power of the length of the progression on which they pass, so after the log⁡(1/α)\log(1/\alpha) increments needed the saving is only logarithmic or quasi-logarithmic. The Green–Sawhney level-dd approach controls the relevant rational Fourier coefficients through hypercontractivity but still gives only exp⁡(−clog⁡N)\exp(-c\sqrt{\log N}). A power saving requires an argument whose loss does not compound with the number of iterations — a single estimate that converts square-difference-freeness into a polynomial density loss.

Formalization scope

  • Sets are Finset ℤ inside Finset.Icc 1 N and N≥1N\ge1 is a natural number; the bound is uniform in NN.
  • The constants are existentially quantified before NN and AA; c>0c>0 is required and CC is a real number. The power N1−cN^{1-c} is the real power.
  • Differences a−ba-b are in Z\mathbb Z and the excluded squares are m2m^2 with m≥1m\ge1, so only nonzero squares are forbidden; differences in either order are covered because both a−ba-b and b−ab-a are tested.
  • Needed infrastructure: Fourier analysis on Z/pZ\mathbb Z/p\mathbb Z and on [N][N], reflection-positivity/chessboard estimates, and graph-norm inequalities. Reusable pieces include a chessboard-estimate library and finite-field Fourier tools.

Selected references

2 thms1 active userReviewed

Top contributors

RankContributorAccepted solutionsSubmitted problems
1Eyal199010801520
2Shuze Chen8223136
3dbenbenn350321
4fizzyinc33350
5polylog448
6Ethan Cheung2815
7marwahaha2529
8WillR202
9Yuxuan Xu1834
10SamenHossain1119