Combinatorics

Motivation

A tile may admit a translation tiling while forcing every such tiling to lack a full lattice of periods. The mission asks for this phenomenon in dimension three and its persistence under Euclidean thickening. The source manuscript presents the surrounding research claim.

Setting

A finite nonempty integer tile T⊆ℤᵈ tiles with complement A when addition T×A→ℤᵈ is bijective. Full periodicity means invariance under a finite-index subgroup. The thickening is the union of closed unit cubes based at T; Euclidean tiling means unique covering almost everywhere.

Formalization target

Construct T⊆ℤ³ that tiles but has no fully periodic complement, and whose thickening tiles ℝ³ but has no complement invariant under any full-rank lattice. Also prove

$$\min\{d:\text{an integer tile without a periodic complement exists in }\mathbb Z^d\}=3.$$

The selected formal target is OAI.PeriodicTilingThree.periodic_tiling_counterexample_and_minimality.

Significance and status

The goal includes both discrete and arbitrary-real-translation Euclidean assertions, plus minimality among all natural dimensions. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Excluding periodic integer translation sets does not automatically exclude Euclidean tilings with noninteger shifts. The latter universal quantifier is a separate clause.

Formalization scope

Discrete tilings are exact bijections, whereas Euclidean tilings are almost-everywhere unique representations relative to Lebesgue measure. Euclidean full periodicity uses the integer span of a real basis. Closed-cube overlaps are handled by the almost-everywhere convention.

Selected references

• OpenAI, A translational tile with no fully periodic tiling in dimension three, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Choosing real signs in a polynomial controls how much its values can peak around the unit circle. The target seeks asymptotically optimal maximum modulus at every sufficiently large length. The source manuscript presents the surrounding research claim.

Setting

A real Littlewood polynomial has consecutive coefficients εₖ∈{−1,1}: P_N(z)=Σₖ₌₀ᴺ⁻¹ εₖzᵏ. The coefficient family may depend on both its length and the requested accuracy.

Formalization target

Prove

$$\forall\eta>0\;\exists N_0\ge1\;\forall N\ge N_0\;\exists\varepsilon,\quad\sup_{|z|=1}|P_N(z)|\le(1+\eta)\sqrt N.$$

All sufficiently large integer lengths are required, rather than a subsequence.

The selected formal target is OAI.AsymptoticallyMinimalLittlewood.main.

Significance and status

The selected target is the uniform maximum-modulus assertion. The companion finite-flatness target gives one sign family whose normalized modulus tends to one in every positive finite Lᵖ moment. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Control at finitely many sample points does not directly give a bound on the full circle. Uniformity in the circle variable and coverage of all large lengths are separate obligations.

Formalization scope

Coefficients are real-valued Fin N functions explicitly constrained to ±1 and evaluated as complex polynomials. The companion theorem uses Haar probability on UnitAddCircle and a single family for every p>0. Both independent definition groups are referenced; finite-flatness is a related endpoint rather than a claimed prerequisite.

Selected references

• OpenAI, Asymptotically minimal maxima of real Littlewood polynomials, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

At its critical weight, a self-avoiding path on the honeycomb lattice can make long excursions without paying an exponential cost. A basic quantitative question is how much of its total weight reaches the far side of a strip of height $N$. Physics heuristics (Nienhuis's Coulomb gas and the conjectured $\mathrm{SLE}_{8/3}$ scaling limit with boundary exponent $5/8$) predict that this crossing mass decays like $N^{-1/4}$. Rigorous results so far showed only that it tends to zero, with a polynomial upper bound with a tiny exponent.

The OpenAI preprint behind this mission, dated September 26, 2026 (source), claims the predicted power with bounded-factor constants: the crossing mass is comparable to $N^{-1/4}$, and the first horizontal-displacement moment of paths returning to the starting side is comparable to $N^{3/4}$ (Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1982 — Nienhuis's Coulomb-gas analysis of the dilute $O(n)$ model predicts the honeycomb critical point $\sqrt{2+\sqrt2}$ and the planar self-avoiding-walk exponents, including $\nu=3/4$ (PRL 1982).
• 2004 — Lawler, Schramm and Werner describe the conjectural $\mathrm{SLE}_{8/3}$ scaling limit; the boundary exponent $5/8$ predicts a crossing power $-1/4$ for strips.
• 2012 — Duminil-Copin and Smirnov prove that the connective constant of the honeycomb lattice is $\sqrt{2+\sqrt2}$ using a parafermionic observable and a boundary identity (Annals 2012); their strip argument bounds the crossing mass between orders $1/N$ and $1$.
• 2014 — Beaton, Bousquet-Mélou, de Gier, Duminil-Copin and Guttmann prove that the critical bridge mass tends to zero (CMP 2014).
• 2020 — Glazman and Manolescu give a shorter proof and a quantitative bound along a subsequence of heights (AIHP 2020).
• 2026 — Krachun and Panagiotis prove a polynomial upper bound on the bridge mass and quantitative sub-ballisticity (Ann. Probab. 2026).
• September 2026 — A group of OpenAI preprints claims the strip crossing power $-1/4$ with bounded-factor constants (source), the bridge mean-length exponent $4/3$ (source), and spatial exponent $3/4$ for several laws of critical walks (source).

Setting

Use the honeycomb lattice dual to the equilateral triangular tiling of side one, with one edge direction horizontal; its vertices are the triangles up i j and down i j, where $j\ge0$ indexes the horizontal band. Let $S_N$ be the strip of $N$ bands. A path starts in the triangle up 0 0 (just above bottom port $0$), visits distinct triangles, moves between adjacent ones, and stays in bands $0,\dots,N-1$. Its length $|\gamma|$ is the number of visited triangles and its critical weight is $\rho^{|\gamma|}$ with $\rho=(2+\sqrt2)^{-1/2}$. An arch ends at up k 0 with $k\neq0$ (bottom port $k$); a bridge ends at a down triangle of the top band. Put $c=\cos(3\pi/8)$ and

$$K_N(k)=\sum_{\text{arches to }k}\rho^{|\gamma|},\quad A_N=\sum_{k\ne0}K_N(k),\quad B_N=\sum_{\text{bridges}}\rho^{|\gamma|},\quad m_N=\sum_{k\ge1}k\,K_N(k).$$

Write $f_N\asymp g_N$ if $\ell g_N\le f_N\le u g_N$ for all $N\ge1$ with fixed constants $\ell,u>0$.

Formalization targets

Goal: Theorem 1.1 (Critical strip mass, p. 2)

For every $N\ge1$ all sums above are finite, and with constants independent of $N$,

$$cA_N+B_N=1,\qquad m_{N+1}-m_N\asymp B_N,\qquad m_N\asymp N^{3/4},\qquad B_N\asymp N^{-1/4},$$

and $B_N$ is nonincreasing in $N$.

Significance

The result itself. It establishes the predicted crossing power $-1/4$ with uniform multiplicative constants, not just a logarithmic exponent, improving the qualitative decay of Beaton et al. and the polynomial upper bound of Krachun and Panagiotis. It is an input for the bridge-length and spatial-exponent results of companion preprints. The exponent of $m_N$ concerns an unnormalized displacement moment summed over all lengths; the fixed-length displacement conjecture and the scaling limit are different questions.

Formalizing it. The proof combines an exact boundary identity of Duminil-Copin–Smirnov type, finite-strip transfer matrices with integrable local relations, a Pfaffian that makes the stationary vector polynomial, and a comparison of the resulting positive integral with Bures–Laguerre ensembles. A formal proof would include the honeycomb boundary identity, the core of the connective-constant proof, which is itself a natural formalization target. No machine-checked honeycomb walk result of this kind is known.

Difficulty

The boundary identity $cA_N+B_N=1$ (Lemma 4.2, p. 15) does not determine the power: it only gives $B_N$ between orders $1/N$ and $1$. The preprint's route computes the arch moment $m_N$ first, as one coefficient of a ratio $p_{N+1}/p_N$ of Pfaffians (Proposition 4.1, p. 13), converts it into a positive $N$-fold integral with Bures-type interaction (Section 5), and estimates that integral uniformly in $N$ by comparison with Laguerre laws (Section 6). The crossing power then follows from monotonicity and $m_{N+1}-m_N\asymp B_N$. A degree bound on the polynomial vacuum (Lemma 3.2, p. 10) is essential, because it turns interpolation into an identity argument.

Formalization scope

• Triangles are ℤ × ℕ × Bool (column, band, up/down); adjacency joins an up triangle to the down triangles sharing an edge. Paths are Lists with Nodup, IsChain adjacent, head up 0 0, a prescribed last triangle, and all bands < N.
• Weights are rho ^ p.length on paths satisfying IsPath, and 0 otherwise; all masses are tsums over lists. The goal includes summability of each family, so the tsums are genuine sums.
• moment N = ∑' k : ℕ, (k+1) * K N (k+1), i.e. $\sum_{k\ge1}kK_N(k)$.
• Comparable f g asks for constants $0<\ell,u$ with $\ell g(N)\le f(N)\le ug(N)$ for every $N\ge1$; powers are real rpow.
• Monotonicity is $B_{N+1}\le B_N$ for $N\ge1$.

Reusable contributions: the honeycomb boundary (parafermionic) identity in finite domains, and summability of critical walk weights in strips.

Selected references

• OpenAI, Critical strip-crossing mass on the honeycomb lattice, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Critical-strip-crossing-mass-on-the-honeycomb-lattice-September-26-2026/main.pdf
• G. F. Lawler, O. Schramm, W. Werner, On the scaling limit of planar self-avoiding walk, Proc. Sympos. Pure Math. 72, Part 2 (2004), 339–364.
• Y. Ikhlef, J. Cardy, Discretely holomorphic parafermions and integrable loop models, J. Phys. A 42 (2009), 102001. https://doi.org/10.1088/1751-8113/42/10/102001
• A. Glazman, Connective constant for a weighted self-avoiding walk on $\mathbb Z^2$, Electron. Commun. Probab. 20 (2015), paper 86. https://doi.org/10.1214/ECP.v20-3844
• B. Nienhuis, Exact critical point and critical exponents of O(n) models in two dimensions, Phys. Rev. Lett. 49 (1982), 1062–1065. https://doi.org/10.1103/PhysRevLett.49.1062
• H. Duminil-Copin, S. Smirnov, The connective constant of the honeycomb lattice equals $\sqrt{2+\sqrt2}$, Ann. of Math. 175 (2012), 1653–1665. https://doi.org/10.4007/annals.2012.175.3.14
• N. R. Beaton, M. Bousquet-Mélou, J. de Gier, H. Duminil-Copin, A. J. Guttmann, The critical fugacity for surface adsorption of self-avoiding walks on the honeycomb lattice is $1+\sqrt2$, Comm. Math. Phys. 326 (2014). https://doi.org/10.1007/s00220-014-1896-1
• A. Glazman, I. Manolescu, Self-avoiding walk on $\mathbb Z^2$ with Yang–Baxter weights: universality of critical fugacity and 2-point function, Ann. Inst. H. Poincaré Probab. Statist. 56 (2020). https://doi.org/10.1214/19-AIHP1024
• D. Krachun, C. Panagiotis, Quantitative sub-ballisticity of self-avoiding walk on the hexagonal lattice, Ann. Probab. 54 (2026), 1109–1125. https://doi.org/10.1214/24-AOP1730

Motivation

Random 3-SAT, a conjunction of random three-literal clauses on $n$ variables, is the classic test case for the typical behavior of satisfiability. Experiments placed the hardest instances near the density where half the formulas are satisfiable, and statistical physics predicts a sharp satisfiability threshold near $4.267$. Once a limiting threshold $\alpha_3$ is known to exist, a natural question is whether it is a computable real: is there an algorithm that, given $r$, outputs a rational within $2^{-r}$ of $\alpha_3$? Existence alone does not imply this, since limits of computable sequences need not be computable (Specker 1949). This mission asks for such an algorithm.

Timeline

• 1949. Specker constructs a bounded monotone computable sequence of rationals with a noncomputable limit.
• 1999. Friedgut, with an appendix by Bourgain, proves a sharp transition about a size-dependent location (doi:10.1090/S0894-0347-99-00305-7).
• 2003, 2006. Hajiaghayi and Sorkin, and Kaporis, Kirousis and Lalas, prove the lower bound $3.52$ (arXiv:math/0310193).
• 2002–2006. Mézard, Parisi and Zecchina develop the cavity/survey-propagation picture; Mertens, Mézard and Zecchina predict $\alpha_3\approx4.267$.
• 2009. Díaz, Kirousis, Mitsche and Pérez-Giménez prove the upper bound $4.4898$.
• 2013. Bayati, Gamarnik and Tetali prove limits for normalized optimization values via sparse interpolation (doi:10.1214/12-AOP816).
• 2022. Ding, Sly and Sun prove the satisfiability conjecture with the predicted value for all large $k$ (doi:10.4007/annals.2022.196.1.1).
• 2026. Carenini proves a polynomial scaling window and the existence of limiting thresholds for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026); priority for the satisfiability conjecture belongs to Carenini.

The source of this mission is an OpenAI preprint dated September 27, 2026. Its contribution is computability of $\alpha_3$, beyond existence.

Setting

For $n\ge3$, a proper random 3-clause chooses three distinct variables uniformly from $x_1,\dots,x_n$ and gives each an independent fair sign. Let $\Phi(n,m)$ be the conjunction of $m\ge0$ independent such clauses (sampled with replacement from the $8\binom n3$ possibilities; the empty formula is satisfiable) and

$$p(n,m)=\mathbb P\{\Phi(n,m)\ \text{is satisfiable}\}.$$

A real $\alpha$ is computable if a single algorithm, on input $r$, halts with a rational $q_r$ satisfying $|q_r-\alpha|\le2^{-r}$.

Formalization targets

Goal: Theorem 1.1

There is $\alpha_3\in(0,\infty)$ such that for every fixed real $a\ge0$

$$\lim_{n\to\infty}p(n,\lfloor an\rfloor)=\begin{cases}1,&a<\alpha_3,\\0,&a>\alpha_3,\end{cases}$$

and one finite deterministic Turing machine, on input $1^r$, halts with a rational $q_r$ with $|q_r-\alpha_3|\le2^{-r}$, using no oracle, advice, or noncomputable constant. Lean: OAI.FixedClauseThreshold.Computability.main, open on the platform.

Significance

The theorem makes the random 3-SAT threshold an effectively approximable constant: in principle its digits can be certified, although no efficiency bound is obtained. The method produces two families of finite certificates, rational lower bounds from a deletion estimate and rational upper bounds from finite hierarchical approximations of a soft pressure, and a fair search over them halts without any computable rate of finite-size convergence. The paper also gives a self-contained existence proof of $\alpha_3$ (Theorem 4.4) for the same proper-clause model.

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

Difficulty

Finite-size satisfiability probabilities are computable, but their convergence rate is unknown, so truncating at a finite $n$ certifies nothing. Lower certificates need an explicit bound on how far the finite-size centers can lie above the limit. Upper certificates are harder: one must show that above $\alpha_3$ some finite, checkable object witnesses unsatisfiability in the limit. This requires a variational (Parisi-type) description of the limiting pressure of the soft constraint model, approximated by finitely many rational parameters with a proof that the approximation is complete at every rational density above the threshold.

Formalization scope

• ProperClause n k is Fin n → Option Bool with exactly $k$ defined entries; Formula n k m := Fin m → ProperClause n k; properSATProbability n 3 m is the exact counting ratio, equal to $p(n,m)$.
• MainStatement asserts $\exists\,\alpha>0$ with the two strict-side limits at $m=\lfloor an\rfloor$, a sequence q : ℕ → ℚ with Computable (fun r => encode (q r)), a Nat.Partrec.Code c with c.eval r = some (encode (q r)), and $|q_r-\alpha|\le2^{-r}$ for all $r$.
• The input is a natural number rather than a unary string, which is equivalent for computability; the $r=0$ case is a harmless extra requirement.
• Nothing is asserted at $a=\alpha_3$.

Infrastructure: Mathlib's Computable/Nat.Partrec.Code, finite counting for random formulas, Poisson clause processes, interpolation bounds, and Ruelle cascades for the upper certificates. Formalizations of Lemma 2.1 (finite-certificate search, purely computability-theoretic and reusable), Theorem 4.4 and Theorem 8.4 are welcome.

Selected references

• OpenAI, Computing the Random 3-SAT Threshold, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Computing-the-Random-3-SAT-Threshold-September-27-2026/article.pdf
• OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
• G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
• E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
• J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
• M. Bayati, D. Gamarnik, P. Tetali, Combinatorial approach to the interpolation method and scaling limits in sparse random graphs, Ann. Probab., 2013. https://doi.org/10.1214/12-AOP816
• M. Hajiaghayi, G. B. Sorkin, The satisfiability threshold of random 3-SAT is at least 3.52, preprint, 2003. https://arxiv.org/abs/math/0310193
• D. Panchenko, The Parisi ultrametricity conjecture, Ann. of Math., 2013. https://doi.org/10.4007/annals.2013.177.1.8
• E. Specker, Nicht konstruktiv beweisbare Sätze der Analysis, J. Symbolic Logic, 1949.

Motivation

Random planar maps are graphs embedded in the sphere, chosen at random; they are the discrete models of two-dimensional quantum gravity. Decorating a map with a Fortuin–Kasteleyn (FK) random-cluster configuration with parameter $q$ couples the geometry of the map to a statistical-mechanics model (percolation, Ising, Potts), and the coupling changes the large-scale shape of the map. For $0<q<4$ the maps are expected to converge to Liouville quantum gravity surfaces; for $q>4$ the cluster weight is so strong that the map is predicted to become tree-like at large scales. This mission concerns that tree-like regime.

Timeline

• 1963. Tutte decomposes planar maps into nonseparable blocks (doi:10.4153/CJM-1963-029-x).
• 1967. Mullin enumerates tree-rooted maps (doi:10.4153/CJM-1967-010-x).
• 1972. Fortuin and Kasteleyn introduce the random-cluster model (doi:10.1016/0031-8914(72)90045-6).
• 1993. Aldous introduces the Brownian continuum random tree (CRT) as the limit of finite-variance conditioned Galton–Watson trees (doi:10.1214/aop/1176989404).
• 2007–2008. Bernardi gives bijective encodings of tree-rooted maps and connects them to the Tutte polynomial (doi:10.37236/928).
• 2016. Sheffield's inventory-accumulation (hamburger–cheeseburger) bijection encodes FK-decorated maps and identifies the transition at $q=4$; his appendix predicts a CRT limit for $q>4$ (doi:10.1214/15-AOP1061). Panagiotou, Stufler and Weller prove CRT limits for subcritical graph classes (doi:10.1214/15-AOP1048).
• 2026. Feng proves an infinite-volume counterpart: an infinite FK map with $q>4$ converges to an infinite CRT in the local Gromov–Hausdorff–Prokhorov topology (doi:10.1007/s00440-025-01424-2); Stufler proves degree-measure CRT limits for maps whose block weights depend only on block size (arXiv:2608.21063).

The source of this mission, an OpenAI preprint dated September 24, 2026, proves the finite-volume CRT prediction for every $q>4$.

Setting

A rooted planar map is a connected graph embedded in the oriented sphere, up to orientation-preserving homeomorphism, with a distinguished dart (oriented edge); loops and multiple edges are allowed. For an edge subset $A\subseteq E(M)$, $k_M(A)$ is the number of connected components of $(V(M),A)$, isolated vertices included. For $q>4$ and $n\ge1$, sample $(M_n,A_n)$ with $|E(M_n)|=n$ according to

$$\mathbb P\bigl((M_n,A_n)=(M,A)\bigr)=\frac{1}{Z_{n,q}}\,q^{\,k_M(A)+(|A|-|V(M)|)/2}.$$

Let $d_n$ be graph distance on $V(M_n)$ using all edges and $\mu_n(\{v\})=\deg(v)/(2n)$.

For a standard normalized Brownian excursion $e$ on $[0,1]$, $d_e(s,t)=e(s)+e(t)-2\min_{[s\wedge t,\,s\vee t]}e$; the quotient by $d_e=0$ with the pushforward $\mu_e$ of Lebesgue measure is the Brownian CRT $(\mathcal T_e,d_e,\mu_e)$.

The Gromov–Hausdorff–Prokhorov (GHP) distance between compact metric probability spaces is the infimum, over isometric embeddings into a common space, of the maximum of the Hausdorff distance of the images and the Lévy–Prokhorov distance of the pushed-forward measures.

Formalization targets

Goal: Theorem 1.1

$$\forall q>4\ \exists c(q)\in(0,\infty):\qquad \bigl(V(M_n),\ c(q)\,n^{-1/2}d_n,\ \mu_n\bigr)\ \Longrightarrow\ (\mathcal T_e,d_e,\mu_e)$$

in distribution for the GHP topology, as $n\to\infty$ through all positive integers. The Lean statement OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt is open on the platform.

Significance

The theorem establishes the tree side of the geometric phase transition of FK planar maps at $q=4$ in the natural finite-volume setting: the law is conditioned on the total size, the metric uses every edge, and the measure is the degree measure. Feng's infinite-volume result does not imply it, and a limit of an unconditioned encoding walk gives neither conditioning nor metric control. Together with companion results for $0<q\le4$, it completes the picture surface versus tree.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would also build reusable infrastructure: combinatorial maps as rotation systems, the GHP topology, and the Brownian CRT, none of which is in Mathlib.

Difficulty

The FK weight of a nonseparable block depends on its shape, not only on its size, so the block-weighted map results with uniform blocks do not apply, and exponential moments of block sizes are not available. The proof must show that the block tree is a critical Galton–Watson tree with finite offspring variance, and that graph distance along every ancestral path is asymptotically a constant times the depth, uniformly over all paths, using only a second moment.

Formalization scope

• A map with $n+1$ edges is a pair of permutations of Fin (2*(n+1)) (edge involution without fixed points, vertex rotation), connected, with $|V|+|F|=n+3$ (genus zero), modulo isomorphisms fixing dart 0. The Lean index $n$ corresponds to $n+1$ edges, and the scale is $c/\sqrt{n+1}$.
• The FK law sums over all Finsets of edge orbits; clusterCount counts components including isolated vertices; loops are omitted from adjacency only.
• MetricMeasureData packages a carrier, a distance and a measure; Valid means a compact metric probability space with Borel σ-algebra. ghpEDist is the infimum over pseudometrics on the disjoint union extending both distances.
• Convergence in distribution is expressed by expectations of bounded tests F continuous for ghpEDist at valid objects.
• The normalized excursion is realized as $\lvert B(t)-tB(1)\rvert$ for a three-dimensional Brownian motion $B$, and the statement holds for every such realization. The limit expectation is a Bochner integral, so measurability of the integrand is part of what must be proved.

A complete development needs Sheffield's inventory bijection or an equivalent finite word identity, Tutte's block decomposition, conditioned Galton–Watson tree limits with finite variance (Aldous; Broutin–Marckert), and GHP comparison lemmas. Contributions formalizing Proposition 2.2 (finite word identity), Proposition 4.3 (exact finite representation), Theorem 5.5 (uniform marked path sums) and Lemma 6.3 (metric and mass comparison) are welcome.

Selected references

• OpenAI, Brownian continuum random tree limits of finite Fortuin–Kasteleyn maps above four, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Brownian-continuum-random-tree-limits-of-finite-Fortuin-Kasteleyn-maps-above-four-September-24-2026/main.pdf
• S. Sheffield, Quantum gravity and inventory accumulation, Ann. Probab., 2016. https://doi.org/10.1214/15-AOP1061
• Y. Feng, Triviality of critical Fortuin–Kasteleyn decorated planar maps for $q>4$, Probab. Theory Related Fields, 2026. https://doi.org/10.1007/s00440-025-01424-2
• D. Aldous, The continuum random tree III, Ann. Probab., 1993. https://doi.org/10.1214/aop/1176989404
• C. M. Fortuin, P. W. Kasteleyn, On the random-cluster model I, Physica, 1972. https://doi.org/10.1016/0031-8914(72)90045-6
• W. T. Tutte, A census of planar maps, Canad. J. Math., 1963. https://doi.org/10.4153/CJM-1963-029-x
• N. Broutin, J.-F. Marckert, Asymptotics of trees with a prescribed degree sequence and applications, Random Structures Algorithms, 2014. https://doi.org/10.1002/rsa.20463
• K. Panagiotou, B. Stufler, K. Weller, Scaling limits of random graphs from subcritical classes, Ann. Probab., 2016. https://doi.org/10.1214/15-AOP1048
• B. Stufler, Non-bijective scaling limits and phase transitions of planar maps, preprint, 2026. https://arxiv.org/abs/2608.21063

Motivation: Saxl's conjecture on the staircase tensor square

The irreducible complex representations of the symmetric group $S_n$ are the Specht modules $S^\lambda$, indexed by partitions $\lambda\vdash n$. How a tensor product $S^\alpha\otimes S^\beta$ (with diagonal action) decomposes is recorded by the Kronecker coefficients

$$g(\alpha,\beta,\lambda)=\dim\operatorname{Hom}_{S_n}\!\big(S^\lambda,\,S^\alpha\otimes S^\beta\big),$$

for which no positive combinatorial rule is known; even deciding positivity is hard, and the question is studied in algebraic combinatorics and geometric complexity theory. In 2012 Jan Saxl proposed that the staircase $\rho_m=(m,m-1,\dots,1)$, a partition of $N_m=m(m+1)/2$, has a tensor square containing every irreducible representation of $S_{N_m}$.

Timeline

• 2012 — Saxl proposes the conjecture at the UCLA Combinatorics Seminar (20 March 2012), as recorded by Pak, Panova and Vallejo.
• 2010 — Brown, van Willigenburg and Zabrocki show that $S^{(m,m-1)}\otimes S^{(m,m-1)}$ is the multiplicity-free sum of all irreducibles with at most four rows (BWZ 2010, Cor. 4.1).
• 2013 — Heide, Saxl, Tiep and Zalesski prove that the Steinberg square of most finite simple groups of Lie type contains every irreducible, a motivating precedent (HSTZ 2013, Thm 1.2).
• 2015 — Ikenmeyer proves positivity for all $\lambda$ comparable with $\rho_m$ in dominance order, and all hooks (Ikenmeyer 2015).
• 2016 — Pak, Panova and Vallejo formulate the conjecture in print, give a character-nonvanishing criterion, and handle hooks and two-row shapes for large $m$ (PPV 2016).
• 2017 — Luo and Sellke: almost every partition occurs (uniform and Plancherel measures) (Luo–Sellke 2017).
• 2018–2021 — Bessenrodt: double hooks (2018); Bessenrodt, Bowman and Sutton: all 2-height-zero constituents and framed staircases (2021); Li: triple hooks (2021).
• 2023 — Harman and Ryba: the staircase tensor cube contains everything (Harman–Ryba 2023).
• 2025 — Letellier and Nam prove the staircase-square statement for unipotent characters of $\mathrm{GL}_n(q)$, a different character theory (Letellier–Nam 2025).
• 2026 — An OpenAI preprint, A Cyclic Polytabloid Proof of Saxl's Conjecture (OpenAI Math Release, September 24, 2026), claims a proof of the full conjecture. It has not been peer reviewed and the theorem is not formally verified.

Setting

A partition is a Mathlib YoungDiagram. The Lean development builds $S^\lambda$ concretely: for a tableau $t$ (a bijection between $\{0,\dots,n-1\}$ and the cells), the polytabloid $e_t$ is the signed sum over the column group of $t$ of the permuted indicator of the row word of $t$, inside the space of functions on words $\mathrm{Fin}\,n\to\mathrm{Fin}\,d$; Specht t is the $\mathbb C$-span of the $S_n$-orbit of $e_t$. The coefficient kronecker a b t is the complex dimension of the space of $S_n$-intertwining maps from spechtRep t into spechtRep a ⊗ spechtRep b. The staircase staircase m is the diagram of cells $(i,j)$ with $i+j<m$, i.e. $\rho_m$.

Formalization targets

Goal: Saxl's conjecture

For every integer $m\ge1$ and every partition $\lambda\vdash N_m$,

$$g(\rho_m,\rho_m,\lambda)>0 ,$$

equivalently $S^{\rho_m}\otimes S^{\rho_m}$ contains every irreducible representation of $S_{N_m}$. This is Theorem 1.1 of the source, formalized as SaxlConjecture (positivity of kronecker for every Young diagram $\mu$ with as many cells as staircase m). The goal is published on the platform with status Open.

Significance

The result itself. Saxl's conjecture is the best-known instance of the tensor-square covering problem for symmetric groups. The source proves a stronger cyclic form (its Theorem 3.1): every $S^\lambda$ already occurs in the submodule $W_m$ generated by one explicit tensor $v_{R_m}\otimes v_{C_m}$ of row and column polytabloids. A companion preprint uses this cyclic form to construct, for every $n\notin\{2,4,9\}$, an irreducible representation of $S_n$ whose tensor square contains every irreducible (the tensor square conjecture of Pak–Panova–Vallejo).

Formalizing it. The Lean statement is the classical, non-cyclic conclusion, the form in which the conjecture is usually quoted. A formal proof would require Specht-module theory (irreducibility, Young's rule, branching, induced modules), none of which is presently in Mathlib in usable form; that layer would be reusable across representation theory of $S_n$.

Difficulty

Positivity of a Kronecker coefficient cannot be read off from characters in general: character sums cancel, and the families handled earlier (hooks, two rows, double and triple hooks, dominance-comparable shapes, 2-height-zero shapes) each relied on a special structure. Asymptotic statements (almost all $\lambda$) or higher powers (cube, fourth power) leave exceptional constituents. An induction on $m$ must retain an explicit vector at every step, because knowing that a constituent appears somewhere in a smaller square does not propagate through the projections needed to grow the staircase.

Formalization scope

• staircase m has cells $\{(i,j): i+j<m\}$, with $m(m+1)/2$ cells; canonicalTableau fixes one enumeration of cells (any enumeration gives an isomorphic module). The target diagram ranges over all YoungDiagrams of the same cardinality.
• kronecker is Module.finrank ℂ of Representation.IntertwiningMap, the genuine multiplicity; positivity means a nonzero equivariant map $S^\lambda\to S^{\rho_m}\otimes S^{\rho_m}$ exists.
• The case $m\ge1$ matches the source; $m=0$ is excluded.
• Needed infrastructure: Specht modules and polytabloid bases, Young's rule and dominance, sign twists, induction and restriction, Littlewood–Richardson branching. The definitions are shared verbatim with the companion universal-tensor-square mission.

Selected references

• I. Pak, G. Panova and E. Vallejo, Kronecker products, characters, partitions, and the tensor square conjectures, Adv. Math. 288 (2016), 702–731. https://doi.org/10.1016/j.aim.2015.11.002
• G. Heide, J. Saxl, P. H. Tiep and A. E. Zalesski, Conjugacy action, induced representations and the Steinberg square for simple groups of Lie type, Proc. London Math. Soc. 106 (2013), 908–930. https://doi.org/10.1112/plms/pds062
• A. A. H. Brown, S. van Willigenburg and M. Zabrocki, Expressions for Catalan Kronecker products, Pacific J. Math. 248 (2010), 31–48. https://doi.org/10.2140/pjm.2010.248.31
• C. Ikenmeyer, The Saxl conjecture and the dominance order, Discrete Math. 338 (2015), 1970–1975. https://doi.org/10.1016/j.disc.2015.04.027
• S. Luo and M. Sellke, The Saxl conjecture for fourth powers via the semigroup property, J. Algebraic Combin. 45 (2017), 33–80. https://arxiv.org/abs/1511.02387v2
• C. Bessenrodt, Critical classes, Kronecker products of spin characters, and the Saxl conjecture, Algebr. Comb. 1 (2018), 353–369. https://doi.org/10.5802/alco.18
• C. Bessenrodt, C. Bowman and L. Sutton, Kronecker positivity and 2-modular representation theory, Trans. Amer. Math. Soc. Ser. B 8 (2021), 1024–1055. https://doi.org/10.1090/btran/70
• X. Li, Saxl Conjecture for triple hooks, Discrete Math. 344 (2021), 112340. https://doi.org/10.1016/j.disc.2021.112340
• N. Harman and C. Ryba, A tensor-cube version of the Saxl conjecture, Algebr. Comb. 6 (2023), 507–511. https://doi.org/10.5802/alco.267
• E. Letellier and G. Nam, The Saxl conjecture and the tensor square of unipotent characters of GL_n(q), Algebr. Comb. 8 (2025), 1119–1140. https://doi.org/10.5802/alco.434
• OpenAI, A Cyclic Polytabloid Proof of Saxl's Conjecture, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf

Motivation: tensor squares that contain everything

The irreducible complex representations of the symmetric group $S_n$ are indexed by partitions $\lambda\vdash n$ and written $S^\lambda$ (Specht modules). Decomposing a tensor product $S^\lambda\otimes S^\mu$ (with the diagonal action) into irreducibles is governed by the Kronecker coefficients

$$g(\lambda,\mu,\nu)=\dim\operatorname{Hom}_{S_n}\!\big(S^\nu,\,S^\lambda\otimes S^\mu\big),$$

which have no known positive combinatorial formula and are a central open topic in algebraic combinatorics and geometric complexity theory. A basic test of how far tensor products spread is the tensor square conjecture: in every degree (with a few exceptions) some single irreducible representation has a tensor square containing every irreducible representation.

Timeline

• 2012 — Saxl proposes (UCLA Combinatorics Seminar, 20 March 2012) that the staircase $\rho_m=(m,m-1,\dots,1)$ at triangular degree $n=m(m+1)/2$ has this property; recorded by Pak, Panova and Vallejo.
• 2013 — Heide, Saxl, Tiep and Zalesski conjecture an analogous covering property for alternating simple groups (HSTZ 2013, Rem. 1.3(3)).
• 2013/2016 — Pak, Panova and Vallejo state the tensor square conjecture for $n\ge3$, $n\ne4,9$, and the Saxl conjecture, and give a character-nonvanishing criterion (PPV 2016, Conj. 1.1–1.2, Lemma 1.3).
• 2015 — Ikenmeyer proves the staircase assertion for all $\nu$ comparable with the staircase in dominance order (Ikenmeyer 2015, Thm 2.1).
• 2017 — Luo and Sellke: staircase squares contain almost all partitions, and fourth powers cover everything in large degree (Luo–Sellke 2017).
• 2018 — Bessenrodt: all double-hook constituents (Bessenrodt 2018, Thm 4.10).
• 2021 — Li: the triple-hook case, and a conjectured family for nontriangular degrees (Li 2021).
• 2023 — Harman and Ryba: staircase tensor cubes contain everything (Harman–Ryba 2023, Thm 1.1).
• 2026 — An OpenAI preprint, Universal Tensor Squares for Symmetric Groups (OpenAI Math Release, September 24, 2026), claims the tensor square conjecture for every $n\notin\{2,4,9\}$, building on a companion preprint that proves Saxl's conjecture in a cyclic form. Neither preprint is peer reviewed and the main theorem is not formally verified; its proof uses exact computer calculations for degrees up to $64$.

Setting

For a Young diagram $\lambda$ with $n$ cells, fix a bijection $t$ between $\{0,\dots,n-1\}$ and the cells (a tableau). The Lean development realizes $S^\lambda$ inside the space of functions on words $\mathrm{Fin}\,n\to\mathrm{Fin}\,d$ ($d$ = number of rows), with $S_n$ acting by permuting letters: the polytabloid $e_t$ is the signed sum, over the column group of $t$, of the permuted indicator of the row word of $t$, and Specht t is the $\mathbb C$-span of the $S_n$-orbit of $e_t$. The Kronecker coefficient kronecker a b t is finrank of the space of $S_n$-intertwining maps from spechtRep t to the tensor product spechtRep a ⊗ spechtRep b. canonicalTableau λ is a fixed tableau of shape $\lambda$.

Formalization targets

Goal: a universal tensor square in every degree $n\notin\{2,4,9\}$

For every positive integer $n$ with $n\ne2,4,9$ there is a partition $\lambda\vdash n$ such that

$$g(\lambda,\lambda,\nu)>0\qquad\text{for every }\nu\vdash n ,$$

so the tensor square $S^\lambda\otimes S^\lambda$ contains every irreducible representation of $S_n$. The Lean statement asserts, for one Young diagram $\lambda$ with $n$ cells: positivity of kronecker for every target diagram $\nu$ with $n$ cells; irreducibility of spechtRep for $\lambda$; and that every finite-dimensional irreducible complex representation of $S_n$ admits an injective intertwining map into $S^\lambda\otimes S^\lambda$. This is Theorem 1.1 of the source together with its "thus" sentence. The goal is published on the platform with status Open.

Significance

The result itself. The theorem settles the tensor square conjecture of Pak, Panova and Vallejo, including all nontriangular degrees. Since the sign representation occurs, the chosen $\lambda$ must be self-conjugate. Via Letellier's results it also gives tensor squares of unipotent characters of $\mathrm{GL}_n(\mathbb F_q)$ that contain every unipotent character (Corollary 1.2 of the source). The companion cyclic Saxl theorem is used as input at staircase degrees.

Formalizing it. The proof combines representation-theoretic constructions with exact finite computations (Murnaghan–Nakayama recursion for all eligible $n\le64$, and capacity calculations), which the source certifies by included programs. A formal proof would replace these with checked computation and would require building Specht modules, Kronecker coefficients and branching rules in Lean, infrastructure Mathlib currently lacks.

Difficulty

Knowing that a smaller staircase square contains every constituent does not transfer to an enlarged diagram: constituents must survive a map from the actual enlarged tensor square, and the attached cells introduce alternating terms that can cancel. Almost-all or higher-power results (Luo–Sellke, Harman–Ryba) do not give a universal square. Small degrees cannot be handled by asymptotic estimates and require exact Kronecker computations, and $n=2,4,9$ are genuine exceptions.

Formalization scope

• Partitions are Mathlib YoungDiagrams with card = n; the representation space is (Fin n → Fin d) → ℂ, and Specht t is the cyclic span of one polytabloid. kronecker is Module.finrank ℂ of Representation.IntertwiningMap, so it is the genuine multiplicity of $S^\nu$ in the tensor square.
• The third conjunct quantifies over all finite-dimensional complex irreducible representations in a fixed universe; proving it requires that every irreducible of $S_n$ is isomorphic to some Specht module. The second conjunct (irreducibility of $S^\lambda$) is a standard fact the source uses implicitly.
• $n>0$ and $n\ne2,4,9$ match the source; $n=1$ is trivial.
• Needed infrastructure: Specht module theory (irreducibility, completeness), characters and Murnaghan–Nakayama, Littlewood–Richardson branching, verified computation for $n\le 64$. The Specht and Kronecker layer is shared with the companion Saxl mission.

Selected references

• I. Pak, G. Panova and E. Vallejo, Kronecker products, characters, partitions, and the tensor square conjectures, Adv. Math. 288 (2016), 702–731. https://doi.org/10.1016/j.aim.2015.11.002
• G. Heide, J. Saxl, P. H. Tiep and A. E. Zalesski, Conjugacy action, induced representations and the Steinberg square for simple groups of Lie type, Proc. London Math. Soc. 106 (2013), 908–930. https://doi.org/10.1112/plms/pds062
• C. Ikenmeyer, The Saxl conjecture and the dominance order, Discrete Math. 338 (2015), 1970–1975. https://doi.org/10.1016/j.disc.2015.04.027
• S. Luo and M. Sellke, The Saxl conjecture for fourth powers via the semigroup property, J. Algebraic Combin. 45 (2017), 33–80. https://arxiv.org/abs/1511.02387v2
• C. Bessenrodt, Critical classes, Kronecker products of spin characters, and the Saxl conjecture, Algebr. Comb. 1 (2018), 353–369. https://doi.org/10.5802/alco.18
• X. Li, Saxl Conjecture for triple hooks, Discrete Math. 344 (2021), 112340. https://doi.org/10.1016/j.disc.2021.112340
• N. Harman and C. Ryba, A tensor-cube version of the Saxl conjecture, Algebr. Comb. 6 (2023), 507–511. https://doi.org/10.5802/alco.267
• E. Letellier, Tensor products of unipotent characters of general linear groups over finite fields, Transform. Groups 18 (2013), 233–262. https://doi.org/10.1007/s00031-013-9211-3
• OpenAI, A Cyclic Polytabloid Proof of Saxl's Conjecture, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf
• OpenAI, Universal Tensor Squares for Symmetric Groups, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026/main.pdf

Motivation: removal lemmas and property testing for ordered matrices

A removal lemma says that an object far from having a forbidden substructure must contain many copies of it. Such statements are the combinatorial backbone of property testing: if every matrix that is $\epsilon$-far from avoiding a pattern $H$ contains at least $c_H\epsilon^{C_H}n^{2k}$ copies of $H$, then sampling a number of rows and columns polynomial in $1/\epsilon$ detects the pattern with constant probability. Whether removal bounds are polynomial determines whether testers are efficient. For binary matrices whose rows and columns carry a fixed order, qualitative removal is known, and the polynomial version was conjectured.

Timeline

• 2007 — Alon, Fischer and Newman prove polynomial-query testing for fixed finite forbidden families of binary matrices when row and column order is ignored, and raise the ordered question (SIAM J. Comput. 2007, §7).
• 2007 — Fischer and Rozenberg obtain nonpolynomial lower bounds for a fixed $2\times2$ pattern in ternary host matrices, order ignored (APPROX–RANDOM 2007).
• 2017 — Alon, Ben-Eliezer and Fischer establish qualitative removal for ordered graphs and matrices: a positive copy density exists for each fixed positive distance (FOCS 2017).
• 2020 — Alon and Ben-Eliezer prove polynomial removal for families closed under row (or column) permutations and polynomial bounds for many entry-disjoint copies, and pose the polynomial removal question for finite families of ordered binary matrices (Problem 1.4) (Order 2020).
• 2022 — Gishboliner and Tomon classify polynomial induced removal for ordered graphs, a different single-order symmetric model (Combinatorial Theory 2022).
• 2025 — The singleton version appears as Conjecture 4.5 in the survey of Gishboliner and Shapira (Comput. Sci. Rev. 2025).
• 2026 — An OpenAI preprint, Polynomial removal fails for ordered binary matrices (OpenAI Math Release, September 25, 2026), claims a fixed $66\times66$ binary pattern for which no polynomial removal bound holds. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A binary matrix of order $n$ is a map $A:[n]\times[n]\to\{0,1\}$ (in Lean BinaryMatrix n := Fin n → Fin n → Bool). For a $k\times k$ binary pattern $H$, an ordered copy of $H$ in $A$ is a pair of strictly increasing maps $r,c:[k]\to[n]$ with $A(r_i,c_j)=H(i,j)$ for all $i,j$: zeros must match as well as ones, and rows and columns are chosen independently. $N_H(A)$ is the number of ordered copies, and $A$ is $H$-free if $N_H(A)=0$. The normalized distance to $H$-freeness is

$$\operatorname{dist}_H(A)=\frac1{n^2}\min_{B\ H\text{-free}}\bigl|\{(r,c):A(r,c)\neq B(r,c)\}\bigr|,$$

where every cell may be changed in either direction.

The polynomial ordered binary matrix-removal conjecture asserts that for each fixed $H$ there are $c_H,C_H>0$ such that $N_H(A)\ge c_H\epsilon^{C_H}n^{2k}$ whenever $\operatorname{dist}_H(A)\ge\epsilon$, for all $n\ge1$ and $0<\epsilon<1$.

The pattern $H$ is explicit: with $s=64$ and $\eta_b(a)=\lfloor a/2^{5-b}\rfloor\bmod 2$, the $64\times64$ anchor $S$ has $S(u,v)=\eta_{v-59}(u-33)$ for $33\le u\le 64$, $60\le v\le 64$, and $S(u,v)=\mathbf 1[u\neq v]$ otherwise, and

$$H=\begin{pmatrix} S & e_1 & e_2\\ e_1^{\mathsf T} & 1 & 0\\ e_2^{\mathsf T} & 1 & 1\end{pmatrix}\in\{0,1\}^{66\times66}.$$

Formalization targets

Goal: no polynomial removal bound for $H$

For every $c,C>0$ there exist $n\ge1$, $\epsilon\in(0,1)$ and a binary $n\times n$ matrix $A$ with

$$\operatorname{dist}_H(A)\ge\epsilon\qquad\text{and}\qquad N_H(A)<c\,\epsilon^{C}\,n^{132}.$$

This is the "consequently" clause of Theorem 1.1 of the source, i.e. the negation of the conjecture for this fixed $H$ (here $2k=132$). The source proves more: for every $h\ge1$, with $n_h=(386h+2)2^h$ and $\epsilon_h=(386h+2)^{-2}$, an explicit $A_h$ has $\operatorname{dist}_H(A_h)\ge\epsilon_h$ and $N_H(A_h)\le\epsilon_h2^{-h}n_h^{132}$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. A single explicit pattern shows that ordered binary matrix removal can be super-polynomial, answering the finite-family question of Alon and Ben-Eliezer negatively and disproving the singleton conjecture recorded by Gishboliner and Shapira. It also gives a testing lower bound (Corollary 5.1): a canonical row–column sampler needs $q\ge\exp(\Omega(\epsilon_h^{-1/2}))$ sampled positions per axis on these examples. Earlier non-polynomial examples needed a third symbol in the host; here the host is binary. The example separates hitting all existing copies (a set of $2^h$ cells meets them) from repairing the matrix (at least $4^h$ edits are needed).

Formalizing it. The statement is fully finite and explicit, so a formal proof would certify both the construction and the two counting estimates. The construction is intricate (tree-indexed blocks with interleaved orders, a 66-cell pattern), which is exactly where a machine check adds confidence.

Difficulty

Two estimates pull in opposite directions. The distance bound must hold against every binary repair, including repairs that create new copies elsewhere; the obvious argument — delete one cell per copy — fails because changing cells can create copies, and the source must show any repair needs at least $m^2$ edits. The copy bound requires locating every ordered copy of the 66-cell pattern in the unedited host, not only the designated anchors, which forces a rigidity analysis of how the anchor $S$ can embed.

Formalization scope

• Matrices are Fin n → Fin n → Bool; ordered copies are pairs of StrictMono maps Fin k → Fin n, counted by copyCount. fixedH : BinaryMatrix 66 encodes $H$ with 0-based indices (the anchor rule becomes etaBit (u-32) (v-58) for $32\le u$, $59\le v$).
• fixedMinEdits A is the minimum Hamming distance from $A$ to an $H$-free matrix (the all-zero matrix is $H$-free, so the minimum is attained by a genuine matrix, and the sentinel $n^2+1$ is never selected); fixedDistance divides by $n^2$.
• The bound $c\,\epsilon^C n^{132}$ uses Real.rpow; $c,C$ are arbitrary positive reals, and $n,\epsilon,A$ are existentially chosen, so the statement is exactly the failure of the conjectured inequality for this $H$. It is weaker than the explicit quantitative family of Theorem 1.1; a stronger milestone recording $n_h,\epsilon_h$ and the bound $\epsilon_h2^{-h}$ would be welcome.
• Needed infrastructure: the explicit tree matrices $A_h$, counting of ordered copies, and a lower bound for Hamming distance to $H$-freeness.

Selected references

• N. Alon, E. Fischer and I. Newman, Efficient testing of bipartite graphs for forbidden induced subgraphs, SIAM J. Comput. (2007). https://doi.org/10.1137/050627915
• E. Fischer and E. Rozenberg, Lower bounds for testing forbidden induced substructures in bipartite-graph-like combinatorial objects, APPROX–RANDOM 2007. https://doi.org/10.1007/978-3-540-74208-1_34
• N. Alon, O. Ben-Eliezer and E. Fischer, Testing hereditary properties of ordered graphs and matrices, FOCS 2017. https://doi.org/10.1109/FOCS.2017.83
• N. Alon and O. Ben-Eliezer, Efficient removal lemmas for matrices, Order (2020). https://doi.org/10.1007/s11083-019-09494-3
• L. Gishboliner and I. Tomon, Polynomial removal lemmas for ordered graphs, Combinatorial Theory (2022). https://doi.org/10.5070/C62359151
• L. Gishboliner and A. Shapira, Polynomial property testing, Computer Science Review (2025). https://doi.org/10.1016/j.cosrev.2025.100806
• OpenAI, Polynomial removal fails for ordered binary matrices, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Polynomial-removal-fails-for-ordered-binary-matrices-September-25-2026/paper.pdf

Motivation

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

This mission asks for a formal proof of the full conjecture as stated in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open. Part of the proof is a finite case analysis of 3,099 parameter-pattern instances carried out by two exact programs that accompany the paper.

Background

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

Setting

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

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

Formalization targets

Goal: Theorem 1.1 (p. 2)

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation: how sharp is the threshold of a graph property?

Many questions about random graphs ask when a property — connectivity, containing a triangle, having a perfect matching — appears in the Erdős–Rényi random graph $G(n,p)$, where each of the $\binom n2$ possible edges is present independently with probability $p$. For an increasing property the probability $\mu_p(\mathcal P)$ rises from $0$ to $1$ as $p$ grows, and the threshold width measures how quickly: the length of the interval of $p$ over which $\mu_p(\mathcal P)$ climbs from $\varepsilon$ to $1-\varepsilon$. Friedgut and Kalai showed in 1996 that symmetry alone forces every such transition to be narrow, and conjectured the optimal universal width. This question links probabilistic combinatorics with the Fourier analysis of Boolean functions, and the influence inequalities developed for it are now standard tools in theoretical computer science and statistical physics.

Timeline

• 1981 — Russo's formula (the Margulis–Russo identity) expresses $\frac{d}{dp}\mu_p(\mathcal P)$ as a total influence (Russo 1981).
• 1988 — Kahn, Kalai and Linial prove that every balanced Boolean function has a coordinate of influence $\Omega(\log N/N)$ (KKL, FOCS 1988).
• 1992 — Bourgain, Kahn, Kalai, Katznelson and Linial extend the influence theorem to product measures (BKKKL, Israel J. Math. 1992).
• 1996 — Friedgut and Kalai prove that every monotone graph property on $n$ vertices has threshold width at most $C\log(1/(2\varepsilon))/\log n$ (Theorem 1.1) and conjecture the bound with $(\log n)^2$ in the denominator (Conjecture 1.2) (Friedgut–Kalai, Proc. AMS 1996). The property of containing a clique of order proportional to $\log n$ shows $(\log n)^{-2}$ would be optimal.
• 1997 — Bourgain and Kalai, using the action of the symmetry group on sets of coordinates, obtain width $C_{\eta,\varepsilon}(\log n)^{-2+\eta}$ for every $\eta>0$ (Bourgain–Kalai, GAFA 1997).
• 2020 — Kelman, Kindler, Lifshitz, Minzer and Safra prove, at $p=1/2$, the graph-symmetric influence bound $I_{1/2}(f)\ge c\,(\log n)^2(\log\log n)^{-2}\operatorname{Var}_{1/2}(f)$ (KKLMS, GAFA 2020).
• 2022 — Friedgut surveys the influence method (ICM 2022).
• 2026 — An OpenAI preprint, A Sharp Threshold Bound for Monotone Graph Properties (OpenAI Math Release, September 25, 2026), claims the conjectured bound with explicit constant $2^{19}$. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Fix an integer $n\ge2$ and let $E_n=\binom{[n]}{2}$ be the set of unordered pairs of vertices. A graph configuration is a map $x:E_n\to\{0,1\}$ (in Lean GraphConfig n := GraphEdge n → Bool, where GraphEdge n is the type of 2-element subsets of Fin n). A Boolean function $f$ on configurations is

• vertex invariant if $f(\pi\cdot x)=f(x)$ for every permutation $\pi$ of the vertices, where $\pi$ acts on edges by relabelling endpoints;
• increasing if $x\le y$ edgewise and $f(x)=1$ imply $f(y)=1$;
• nontrivial if it takes both values.

For $p\in\mathbb R$ the graph mean is $\mu_p(f)=\sum_x \prod_{e} p^{x_e}(1-p)^{1-x_e}\, f(x)$, the probability that $G(n,p)$ has the property when $p\in[0,1]$. For $0<a<1$ the quantile is

$$p_a(f)=\inf\{p\in[0,1]:\ \mu_p(f)\ge a\}.$$

Formalization targets

Goal: the Friedgut–Kalai sharp-threshold conjecture (Theorem 1.1)

For every $n\ge2$, every vertex-invariant, increasing, nontrivial $f$, and every $0<\varepsilon<1/2$,

$$p_{1-\varepsilon}(f)-p_\varepsilon(f)\ \le\ \frac{2^{19}}{(\log n)^2}\,\log\frac{1}{2\varepsilon}.$$

The constant $2^{19}$ is the source's explicit choice and is not claimed to be sharp; the content is the order $(\log n)^{-2}$ with linear dependence on $\log(1/(2\varepsilon))$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The bound is uniform over all monotone graph properties and is of optimal order in $n$ for fixed $\varepsilon$, as the clique example of Friedgut and Kalai shows. It settles the exponent question left open between the $(\log n)^{-1}$ bound of 1996 and the $(\log n)^{-2+\eta}$ bound of 1997. The driving estimate in the source, Theorem 1.2 (variance is at most $2^{17}(\log n)^{-2}$ times total influence, for every $0<p<1$ and without monotonicity), is a graph-symmetric influence inequality of independent interest; it removes the $(\log\log n)^2$ loss of the 2020 bound and holds at every bias.

Formalizing it. A formal proof would certify a universal statement over all graph properties with an explicit constant. The supporting library — Fourier–Walsh analysis on biased product spaces, pivotal influences, the Margulis–Russo derivative formula, and random restrictions — is reusable for other threshold and influence results, none of which are currently formalized in Mathlib in this form.

Difficulty

The classical route bounds the derivative $\frac{d}{dp}\mu_p$ from below through the largest influence, using only that the symmetry group acts transitively on edges; transitivity alone cannot give better than $(\log n)^{-1}$, because there are transitive families (on non-graph coordinate sets) whose thresholds are that wide. Reaching $(\log n)^{-2}$ requires using the vertex structure of the symmetry group, and the bound must hold uniformly for every bias $p\in(0,1)$, including very small $p$ where hypercontractive estimates degrade. Influence estimates at $p=1/2$ alone do not suffice, since a width bound requires control throughout the transition interval.

Formalization scope

• Configurations are GraphEdge n → Bool; the measure is the explicit finite sum graphMean p f with product weights $p$ or $1-p$; logarithms are natural (Real.log).
• graphQuantile a f is sInf of $\{p\in[0,1]:\mu_p(f)\ge a\}$. For a nontrivial increasing $f$, $\mu_1(f)=1$, so this set is nonempty and the infimum is not a junk value; the hypotheses NontrivialGraphProperty and $0<\varepsilon<1/2$ exclude the degenerate cases.
• The theorem quantifies over all $n\ge 2$, all such $f$, and all real $\varepsilon\in(0,1/2)$; no asymptotic or "sufficiently large $n$" assumption is used.
• Needed infrastructure: biased Fourier expansion on $\{0,1\}^{E_n}$, influences and the Russo derivative formula, the action of $S_n$ on edges, and integration of a differential inequality for the quantile. Contributions formalizing Theorem 1.2 (variance–influence) or Russo's formula separately are welcome as stepping stones.

Selected references

• E. Friedgut and G. Kalai, Every monotone graph property has a sharp threshold, Proc. Amer. Math. Soc. 124 (1996), 2993–3002. https://doi.org/10.1090/S0002-9939-96-03732-X
• J. Bourgain and G. Kalai, Influences of variables and threshold intervals under group symmetries, Geom. Funct. Anal. 7 (1997), 438–461. https://doi.org/10.1007/s000390050015
• J. Kahn, G. Kalai and N. Linial, The influence of variables on Boolean functions, FOCS 1988, 68–80. https://doi.org/10.1109/SFCS.1988.21923
• J. Bourgain, J. Kahn, G. Kalai, Y. Katznelson and N. Linial, The influence of variables in product spaces, Israel J. Math. 77 (1992), 55–64. https://doi.org/10.1007/BF02808010
• L. Russo, On the critical percolation probabilities, Z. Wahrsch. Verw. Gebiete 56 (1981), 229–237. https://doi.org/10.1007/BF00535742
• E. Kelman, G. Kindler, N. Lifshitz, D. Minzer and M. Safra, Towards a proof of the Fourier–entropy conjecture?, Geom. Funct. Anal. 30 (2020), 1097–1138. https://doi.org/10.1007/s00039-020-00544-2
• E. Friedgut, KKL's influence on me, Proc. ICM 2022, Vol. 6, 4568–4581. https://doi.org/10.4171/ICM2022/78
• OpenAI, A Sharp Threshold Bound for Monotone Graph Properties, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Sharp-Threshold-Bound-for-Monotone-Graph-Properties-September-25-2026/paper.pdf

Motivation

Given $n$ points in the plane with no three on a line, a halving line is a line through two of the points that leaves exactly half of the remaining points on each side. How many halving lines can an $n$-point set have? The question is the middle case of the $k$-set problem: count the $k$-element subsets that a line can cut off. It controls the complexity of levels in line arrangements, and through them the running time of many algorithms in computational geometry (levels, ham-sandwich cuts, $k$-th order Voronoi diagrams).

The gap between the bounds is one of the best known in discrete geometry: the upper bound has been $O(n^{4/3})$ since 1998, while the best constructions give only $n\,e^{\Omega(\sqrt{\log n})}$.

Timeline

• 1971, 1973. Lovász, and Erdős–Lovász–Simmons–Straus, prove the $O(n^{3/2})$ upper bound and construct sets with $\Omega(n\log n)$ halving lines.
• 1992. Pach, Steiger and Szemerédi improve the upper bound by an iterated-logarithm factor (doi:10.1007/BF02187829).
• 1998. Dey proves that the number of $k$-sets is $O(n(k+1)^{1/3})$, hence $O(n^{4/3})$ halving lines, using convex chains and the crossing lemma (doi:10.1007/PL00009354).
• 2001, 2008. Tóth constructs sets with $n\,e^{\Omega(\sqrt{\log n})}$ halving lines (doi:10.1007/s004540010022); Nivasch simplifies the construction and improves the constant (doi:10.1090/conm/453/08804).
• 2009. Pinchasi relates changes between balanced cuts to measure concentration in the plane (doi:10.1145/1542362.1542393).
• 2024. Alonso, López and Rodrigo improve a lower-order term while keeping the exponent $4/3$ (doi:10.3390/sym16070936).

The source of this mission is an OpenAI preprint dated September 25, 2026, which claims the first power saving below $4/3$.

Setting

Let $P=(P_1,\dots,P_n)$ be distinct points of $\mathbb R^2$ with no three collinear. For $i\ne j$, the orientation $\operatorname{orient}(P_i,P_j,P_l)$ is the usual $2\times2$ determinant; its sign says on which side of the line $P_iP_j$ the point $P_l$ lies. For even $n$, an unordered pair $\{i,j\}$ is a halving pair if exactly $(n-2)/2$ points lie strictly on each side of the line $P_iP_j$; $h(P)$ is the number of halving pairs.

A configuration is generic if moreover its $x$-coordinates are distinct, the slopes of the $\binom n2$ segments $P_iP_j$ are distinct, and no point where two of these segments properly cross lies on a third segment. Fix a rank $0\le k\le n$. For a slope $s$, mark the $k$ points with smallest value of $y-sx$. As $s$ increases from $-\infty$ to $+\infty$, the marked set changes by exchanging one point for another; each change is a switch, and $S_k(P)$ is the total number of switches. A switch at rank $k$ happens at the slope of $P_iP_j$ exactly when $k-1$ points lie strictly below the line $P_iP_j$. At the middle rank, switches are halving pairs.

Formalization targets

Goal: Theorems 1.1 and 1.2

$$\exists\,\varepsilon>0,\ C,\ n_0:\quad h(P)\le C\,n^{4/3-\varepsilon}\quad\text{for all even } n\ge n_0 \text{ and all } P \text{ with no three collinear};$$ $$\exists\,\varepsilon>0,\ C:\quad S_k(P)\le C\,n^{4/3-\varepsilon}\quad\text{for all } n\ge1,\ \text{generic } P,\ 0\le k\le n.$$

The Lean statement OAI.PlanarHalving.power_bounds is the conjunction of these two clauses and is open on the platform. Neither $\varepsilon$ nor $C$ is specified, so the goal asserts only the shape of the improvement and survives any later numerical sharpening.

Significance

A power saving $n^{4/3-\varepsilon}$ is the first improvement of the exponent in Dey's bound since 1998. The uniform version over all ranks gives, through shallow cuttings, a $k$-sensitive bound $O(n(k+1)^{1/3-\varepsilon_0})$ for planar $k$-sets and for the complexity of the $k$-level in an arrangement of lines (Corollary 1.3). The saving is non-quantitative: the paper's compactness argument gives no numerical $\varepsilon$.

The result is proved in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. Formalizing it would certify a long compactness argument (limiting measures, rank coordinates, differentiation of monotone functions) whose ineffective nature makes informal checking hard.

Difficulty

Dey's argument decomposes the halving graph into convex chains and applies the crossing lemma; both ingredients are tight on their own, so a power saving must show that configurations nearly attaining the crossing-lemma bound cannot exist. The bound must also hold uniformly over all ranks $k$, because restricting a block of switches to the points that take part in it changes the rank. Since the lower-bound constructions are far below $n^{4/3}$, there is no extremal example to guide the argument.

Formalization scope

• Points are ℝ × ℝ, configurations are P : Fin n → Point; GeneralPosition P is injectivity plus nonvanishing orient for every triple of distinct indices.
• halvingCount P counts pairs i < j with sideCount P i j = (n-2)/2 and sideCount P j i = (n-2)/2, where sideCount counts points with strictly positive orientation. Natural-number division is harmless because $n$ is even.
• Generic P adds distinct first coordinates, distinct slopes of index pairs, and the condition that no proper crossing of two determined open segments lies on a third closed segment.
• switchCount P k counts pairs i < j with 0 < k < n and exactly k - 1 points strictly below the line through P i, P j in the order $y-sx$. Ranks $0$ and $n$ therefore contribute zero, as in the paper.
• slope divides by the $x$-difference; the generic hypothesis makes it nonzero.

A complete development needs the crossing lemma, convex-chain decompositions of the rotating-line process, weak compactness of finite Borel measures, the Radon–Nikodym and Lebesgue differentiation theorems, Rademacher-type differentiability of monotone functions, and planar Jordan-curve separation. Contributions formalizing Dey's $O(n^{4/3})$ bound, Theorem 2.1 (uniform activity packing) and Proposition 8.1 (the fixed-scale recurrence) are welcome.

Selected references

• OpenAI, A power saving for planar halving lines, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-power-saving-for-planar-halving-lines-September-25-2026/main.pdf
• T. K. Dey, Improved bounds for planar $k$-sets and related problems, Discrete Comput. Geom., 1998. https://doi.org/10.1007/PL00009354
• J. Pach, W. Steiger, E. Szemerédi, An upper bound on the number of planar $k$-sets, Discrete Comput. Geom., 1992. https://doi.org/10.1007/BF02187829
• P. Erdős, L. Lovász, A. Simmons, E. G. Straus, Dissection graphs of planar point sets, in A Survey of Combinatorial Theory, 1973.
• L. Lovász, On the number of halving lines, Ann. Univ. Sci. Budapest. Eötvös Sect. Math., 1971.
• G. Tóth, Point sets with many $k$-sets, Discrete Comput. Geom., 2001. https://doi.org/10.1007/s004540010022
• G. Nivasch, An improved, simple construction of many halving edges, Contemp. Math. 453, 2008. https://doi.org/10.1090/conm/453/08804
• R. Pinchasi, Halving lines and measure concentration in the plane, SoCG 2009. https://doi.org/10.1145/1542362.1542393
• E. Alonso, M. López, J. Rodrigo, An improvement of the upper bound for the number of halving lines of planar sets, Symmetry, 2024. https://doi.org/10.3390/sym16070936

Motivation: how large can a set avoid square differences?

A set $A\subseteq\{1,\dots,N\}$ is square-difference-free if no two of its elements differ by a perfect square $m^2$ with $m\ge1$. The Furstenberg–Sárközy theorem says such sets have density tending to zero; the question is how fast. Writing $s(N)$ for the largest size of a square-difference-free subset of $\{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$ (with a slowly growing exponent), from the lower bounds, which are powers $N^{0.73\ldots}$ and beyond. Whether a fixed power saving $s(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árközy's bound is $N/(\log N)^{1/3+o(1)}$.
• 1984 — Ruzsa constructs square-difference-free sets of size $\gg N^{0.7330\ldots}$ (Period. Math. Hungar. 1984).
• 1988 — Pintz, Steiger and Szemerédi prove $s(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\ldots$.
• 2022 — Bloom and Maynard prove $s(N)\ll N/(\log N)^{c\log\log\log N}$ (Compos. Math. 2022).
• 2024/2025 — Green and Sawhney prove $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-$d$ approach to intersective polynomials (arXiv:2605.16216); Krachun pushes the lower exponent past $3/4$, to $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)\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 $N$ write $[N]=\{1,\dots,N\}$. A set $A\subseteq[N]$ is square-difference-free if

$$(A-A)\cap\{m^2 : m\in\mathbb N,\ m\ge1\}=\varnothing,$$

that is, $a-b\neq m^2$ for all $a,b\in A$ and all integers $m\ge1$. (Differences are taken in $\mathbb Z$; $a-b=0$ is allowed since $0$ 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>0$ and $C<\infty$ such that for every integer $N\ge1$ and every square-difference-free $A\subseteq[N]$,

$$|A|\le C\,N^{1-c}.$$

Equivalently, every subset of $[N]$ with more than $CN^{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 $c$, 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 $N$; the best, due to Green and Sawhney, saved $\exp(-c\sqrt{\log N})$. A fixed power saving changes the nature of the problem: it shows that the extremal exponent $\limsup \log s(N)/\log N$ lies strictly below $1$, 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\ldots$ and $1-c$. As an immediate consequence (Remark 1.2 of the source), the graph on $[N]$ joining integers differing by a square has chromatic number at least $C^{-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/\alpha)$ increments needed the saving is only logarithmic or quasi-logarithmic. The Green–Sawhney level-$d$ approach controls the relevant rational Fourier coefficients through hypercontractivity but still gives only $\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\ge1$ is a natural number; the bound is uniform in $N$.
• The constants are existentially quantified before $N$ and $A$; $c>0$ is required and $C$ is a real number. The power $N^{1-c}$ is the real power.
• Differences $a-b$ are in $\mathbb Z$ and the excluded squares are $m^2$ with $m\ge1$, so only nonzero squares are forbidden; differences in either order are covered because both $a-b$ and $b-a$ are tested.
• Needed infrastructure: Fourier analysis on $\mathbb Z/p\mathbb Z$ and on $[N]$, reflection-positivity/chessboard estimates, and graph-norm inequalities. Reusable pieces include a chessboard-estimate library and finite-field Fourier tools.

Selected references

• H. Furstenberg, Ergodic behavior of diagonal measures and a theorem of Szemerédi on arithmetic progressions, J. Analyse Math. 31 (1977). https://doi.org/10.1007/BF02813304
• A. Sárközy, On difference sets of sequences of integers. I, Acta Math. Acad. Sci. Hungar. 31 (1978). https://doi.org/10.1007/BF01896079
• I. Z. Ruzsa, Difference sets without squares, Period. Math. Hungar. 15 (1984). https://doi.org/10.1007/BF02454169
• J. Pintz, W. L. Steiger and E. Szemerédi, On sets of natural numbers whose difference set contains no squares, J. London Math. Soc. 37 (1988). https://doi.org/10.1112/jlms/s2-37.2.219
• R. Beigel and W. Gasarch, Square-difference-free sets of size $\Omega(n^{0.7334\ldots})$, arXiv:0804.4892 (2008). https://arxiv.org/abs/0804.4892v3
• M. Lewko, An improved lower bound related to the Furstenberg–Sárközy theorem, Electron. J. Combin. 22 (2015). https://doi.org/10.37236/4656
• T. F. Bloom and J. Maynard, A new upper bound for sets with no square differences, Compos. Math. 158 (2022). https://doi.org/10.1112/S0010437X22007679
• B. Green and M. Sawhney, New bounds for the Furstenberg–Sárközy theorem, arXiv:2411.17448 (2025). https://arxiv.org/abs/2411.17448v2
• D. Krachun, Square-difference-free sets beyond the three-quarter barrier, arXiv:2608.01325 (2026). https://arxiv.org/abs/2608.01325v1
• OpenAI, A power saving for square-difference-free sets, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-power-saving-for-square-difference-free-sets-September-24-2026/paper.pdf