OAI Math

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 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

In a Maker–Breaker achievement game, two players alternately claim cells of a board; Maker wins by owning every cell of some copy of a fixed shape, and Breaker only tries to prevent this. Polyomino achievement games on the infinite square grid, introduced by Frank Harary, ask which small polyominoes are winners (Maker can force a copy) and which are losers (Breaker can prevent it forever). The six-cell shape Snaky is the long-standing hard case: Maker was known to win with a one-stone handicap or in higher dimensions, but the ordinary planar game without handicap remained undecided.

Timeline

• 2004. Sieben shows that Snaky is a winner in 41 dimensions and records earlier handicap-two strategies of Harary, Harborth and Seemann, as well as the non-existence of a pairing strategy for Breaker (Integers 4, 2004).
• 2007. Halupczok and Schlage-Puchta prove that Snaky wins in three dimensions, loses on an $8\times8$ board, and has planar handicap number at most one (Integers 7, 2007). Ito and Miyagawa give another handicap-one construction.
• 2008. Sieben develops proof trees for weak achievement games and gives a finite proof sequence for the handicap-one win, describing the ordinary planar problem as undecided (Integers 8, 2008).
• 2011. Csernenszky, Martin and Pluhár give a computer-free proof that Breaker has no pairing defense for Snaky (Integers 11, 2011).
• 2023, 2025. Shaik, Mayer-Eichberger, van de Pol and Saffidine study QBF encodings of finite Maker–Breaker games, including Snaky on a $5\times5$ board (arXiv:2301.07345); Boucher and Villemaire treat strong achievement games (doi:10.21428/594757db.6ae0c84a).

The source of this mission, an OpenAI preprint dated September 25, 2026, settles the ordinary planar game: Snaky is a winner, within 21 Maker moves.

Setting

The board is $\mathbb Z^2$, initially empty. Snaky is

$$S=\{(0,0),(1,0),(2,0),(3,0),(3,1),(4,1)\}.$$

An allowed copy is $t+R(S)$ with $t\in\mathbb Z^2$ and $R$ one of the eight $2\times2$ signed permutation matrices (rotations by quarter turns and reflections; no scaling). Maker moves first; then Breaker and Maker alternate, each claiming one previously unclaimed cell. Maker wins when it owns all cells of an allowed copy.

A Maker policy is a rule that, given the current position, returns an unclaimed cell. In the fixed-endpoint formulation, the policy keeps claiming fresh cells even after a win, and one asks that after Maker's $N$-th claim its set of cells contain an allowed copy whenever Breaker's first $N-1$ replies were legal.

Formalization targets

Milestone: Proposition 10 (finite identities of the 35-move certificate)

A pure computation on a printed certificate of 616 cards: card counts, 1,837 placement terms, required-set/envelope/height data of four interface cards, and uniform bounds for all cards.

Milestone: Theorem 11

$$\exists\ \text{Maker policy}\ \sigma:\ \text{every legal play} \Rightarrow \text{an allowed copy of } S \text{ within } 35 \text{ Maker claims}.$$

Goal: Theorem 1

$$\exists\ \text{Maker policy}\ \sigma:\ \text{every legal play} \Rightarrow \text{an allowed copy of } S \text{ within } 21 \text{ Maker claims}.$$

The Lean statement OAI.SnakyPrototype.snaky_winning_strategy_21_with_legal_states is open on the platform.

Significance

Theorem 1 decides the ordinary planar Snaky game, recorded as undecided by Sieben (2008), and gives an explicit bound of 21 Maker moves (a win by the 41st individual turn). It also gives a win on the finite $17\times17$ board (Corollary 6), and removes the handicap from the earlier handicap-one strategies. The paper does not claim the bound 21 is optimal or address the strong game in which both players seek a copy.

The result is proved in an OpenAI preprint that has not been peer reviewed. Its correctness rests on a soundness lemma for a composition rule together with large finite certificates checked by standalone programs. A machine-checked proof would replace this combination of informal soundness argument and external computation by a single certified statement.

Difficulty

The board is infinite and Breaker may play anywhere, so no finite game-tree search applies directly: a proof must cover all Breaker replies, including those far from the action. Pairing strategies, the usual tool for proving shapes are losers, are known to fail for Snaky, but that does not give Maker a strategy. The certificate approach needs a composition rule whose soundness accounts for arbitrary previous ownership on both sides; the move count must be the number of actual Maker claims, including any replacement moves.

Formalization scope

• Cells are ℤ × ℤ; snaky is the six-cell set above and HasSnaky M asks for r : Fin 8, t : Cell with snaky.image (placement r t) ⊆ M, where orient lists all eight signed permutations.
• A Policy is a function of a move counter, the Maker set and the Breaker set; it must never return an owned cell. playState σ N β ∅ ∅ k is the position after $k$ Maker claims and $k$ Breaker replies.
• LegalRepliesBeforeFinal σ N β ∅ ∅ constrains only the first $N-1$ Breaker replies; the theorems conclude a copy of $S$, exactly $N$ Maker cells, and disjointness of the two players' sets throughout.
• The certificate milestone stores the cards as an Array Entry and computes rowAt i (required set, envelope, height) by the composition recursion; it is a decidable statement about explicit finite data.

A trivializing reading is ruled out: the policy is required to be legal on all inputs, and Breaker's replies are arbitrary legal cells of the infinite board. A complete development needs a soundness proof for the composition rule (Lemma 3) and verified evaluation of the certificates; the policy, game and certificate infrastructure is shared between the 21- and 35-move statements. Contributions formalizing Lemma 3, Proposition 5 (the 21-move certificate identities) and Corollary 6 are welcome.

Selected references

• OpenAI, Snaky in 21 Maker moves, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Snaky-in-21-Maker-moves-September-25-2026/article.pdf
• N. Sieben, Snaky is a 41-dimensional winner, Integers 4, 2004. https://math.colgate.edu/~integers/eg5/eg5.pdf
• I. Halupczok, J.-C. Schlage-Puchta, Achieving Snaky, Integers 7, 2007. https://math.colgate.edu/~integers/hg2/hg2.pdf
• N. Sieben, Proof trees for weak achievement games, Integers 8, 2008. https://math.colgate.edu/~integers/ig7/ig7.pdf
• H. Ito, H. Miyagawa, Snaky is a winner with one handicap, 8th Hellenic European Conference on Computer Mathematics and its Applications, 2007.
• A. Csernenszky, R. R. Martin, A. Pluhár, On the complexity of Chooser–Picker positional games, Integers 11, 2011. https://math.colgate.edu/~integers/lg2/lg2.pdf
• I. Shaik, V. Mayer-Eichberger, J. van de Pol, A. Saffidine, Implicit state and goals in QBF encodings for positional games, preprint, 2023. https://arxiv.org/abs/2301.07345
• S. Boucher, R. Villemaire, The QBF Cover encoding for Harary's Tic-Tac-Toe, Canadian Conference on AI, 2025. https://doi.org/10.21428/594757db.6ae0c84a

Motivation: 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: Kaplansky's zero-divisor conjecture

For a field $K$ and a group $G$, the group algebra $K[G]$ consists of finite formal sums $\sum_g a_g g$ with $a_g\in K$, multiplied by extending the group law bilinearly. If $g\in G$ has finite order $m>1$, then $(1-g)(1+g+\dots+g^{m-1})=0$, so $K[G]$ has zero divisors. Kaplansky's zero-divisor conjecture asserts that this is the only source: if $G$ is torsion-free, $K[G]$ has no nonzero zero divisors. Together with the unit and idempotent conjectures it is one of the central problems connecting ring theory, group theory and topology, and positive answers are known for large classes of groups (elementary amenable groups, groups with the unique-product property, torsion-free 3-manifold groups).

Timeline

• 1940 — Higman's thesis raises the question and proves the domain property for groups in which every nontrivial subgroup maps onto $\mathbb Z$ (Higman, Proc. LMS 1940); the thesis formulation is reproduced by Sandling (1981).
• 1956/1957 — Kaplansky poses the problem (Problem 6 in Problems in the theory of rings, National Research Council, 1957).
• 1987 — Rips and Segev construct torsion-free groups without the unique-product property, removing the standard route to the conjecture (J. Algebra 1987); Steenbock gives a graphical small-cancellation treatment (J. Algebra 2015).
• 1988 — Kropholler, Linnell and Moody prove the conjecture for torsion-free elementary amenable groups (Proc. AMS 1988).
• 2021 — Gardam disproves the related unit conjecture over $\mathbb F_2$ (Ann. of Math. 2021), and later over $\mathbb C$ (arXiv:2312.05240, 2024). A nontrivial unit is not a zero divisor, so the zero-divisor conjecture remained open.
• 2026 — Fisher and Sánchez-Peralta prove the domain conclusion for torsion-free 3-manifold groups and division-ring embeddings for virtually compact special groups (J. Comb. Algebra 2026).
• 2026 — An OpenAI preprint, A Torsion-Free Group Algebra with Zero Divisors (OpenAI Math Release, September 23, 2026), claims a finitely presented torsion-free group $G$ with a finite 2-dimensional classifying space such that $\mathbb F_2[G]$ has nonzero zero divisors. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A group $G$ is torsion-free if $g^n=1$ with $n\ge1$ implies $g=1$. It is finitely presented if it has a presentation with finitely many generators and relations. A classifying space (or $K(G,1)$) for $G$ is a path-connected space $X$ with $\pi_1(X)\cong G$ whose universal cover is contractible; it is finite two-dimensional if it is a finite CW complex with cells only in dimensions $\le 2$. A group with a finite-dimensional classifying space is automatically torsion-free, but the formal goal asks for both properties explicitly.

The coefficient field is $\mathbb F_2=\mathbb Z/2$, and $\mathbb F_2[G]$ is Mathlib's MonoidAlgebra (ZMod 2) G.

Formalization targets

Goal: a counterexample to the zero-divisor conjecture (Theorem 1.1)

There exist a group $G$ and $\alpha,\beta\in\mathbb F_2[G]$ such that

$$G\ \text{finitely presented},\quad G\ \text{torsion-free},\quad G\ \text{has a finite 2-dimensional } K(G,1),\quad \alpha\neq0,\ \beta\neq0,\ \alpha\beta=0.$$

This is the full Theorem 1.1 of the source, including its "Moreover" clause. The source proves existence probabilistically; it does not exhibit a concrete presentation. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If correct, the theorem disproves Kaplansky's zero-divisor conjecture over $\mathbb F_2$, a problem open since the 1940s, and shows that torsion-freeness — even together with finite presentability and a 2-dimensional classifying space — does not force $K[G]$ to be a domain. It implies that $G$ fails the unique-product property, and it bears on the implications among the Kaplansky conjectures (zero divisors, units, idempotents) and on approaches through the Atiyah conjecture and division-ring embeddings.

Formalizing it. The claim refutes a long-standing conjecture by an intricate probabilistic and topological construction, which is a strong case for machine verification. A full formal proof needs the probabilistic existence argument, planar separation, and asphericity of a 2-complex — none of which is a routine Mathlib application. Partial contributions (e.g. the characteristic-2 cancellation argument once asphericity and root separation are assumed, or the torsion-freeness of groups with finite-dimensional $K(G,1)$) are welcome. A related machine-checked result exists only for the weaker non-unique-product property of Gardam's $\widetilde A_2$ lattice (Mian–Siddique 2026).

Difficulty

Writing down $\alpha,\beta$ whose product cancels in characteristic two is the easy part; the source does this by a parity argument on a graph of simultaneous steps. The hard part is two safeguards in the quotient group: both factors must remain nonzero (no vertex label other than the root can collapse to the identity), and the group must be torsion-free, which the source obtains by proving the 2-complex is aspherical. Standard tools — small-cancellation or CAT(0) criteria — are not applied; instead the source must exclude spherical arrangements of arbitrarily many paths of arbitrary length, which a union bound over sizes cannot handle.

Formalization scope

• TorsionFree G is the plain group-theoretic notion ($g^n=1$, $n>0$ implies $g=1$); finite presentability is Group.IsFinitelyPresented.
• HasFiniteTwoDimensionalClassifyingSpace G asks for a Hausdorff, path-connected space $X$ with a finite CW structure on all of $X$, no cells above dimension $2$, at least one $2$-cell, a group isomorphism $G\simeq\pi_1(X,x)$, and a surjective covering map from a contractible space onto $X$ (so $X$ is aspherical). Requiring a $2$-cell excludes only the case of free groups, whose group algebras are domains.
• The witnessing group lives in Type and is existentially quantified together with its group structure; the zero divisors are elements of MonoidAlgebra (ZMod 2) G.
• A trivializing reading is excluded because all three group properties and both nonvanishing conditions are required simultaneously.
• Infrastructure needed: CW complexes and covering spaces (partially in Mathlib), the fundamental group of a 2-complex built by attaching cones, Hurewicz/Whitehead-type asphericity arguments, and random graph constructions.

Selected references

• G. Higman, The units of group-rings, Proc. London Math. Soc. (2) 46 (1940). https://doi.org/10.1112/plms/s2-46.1.231
• I. Kaplansky, Problems in the theory of rings, Report of a Conference on Linear Algebras (1956), National Research Council, 1957.
• E. Rips and Y. Segev, Torsion-free group without unique product property, J. Algebra (1987). https://doi.org/10.1016/0021-8693(87)90125-6
• P. H. Kropholler, P. A. Linnell and J. A. Moody, Applications of a new K-theoretic theorem to soluble group rings, Proc. Amer. Math. Soc. (1988). https://doi.org/10.2307/2046771
• M. Steenbock, Rips–Segev torsion-free groups without the unique product property, J. Algebra (2015). https://doi.org/10.1016/j.jalgebra.2015.05.004
• G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021). https://doi.org/10.4007/annals.2021.194.3.9
• G. Gardam, Non-trivial units of complex group rings, preprint, 2024. https://arxiv.org/abs/2312.05240v2
• S. P. Fisher and P. Sánchez-Peralta, Division rings for group algebras of virtually compact special groups and 3-manifold groups, J. Comb. Algebra (2026). https://doi.org/10.4171/JCA/89
• I. Mian and S. Siddique, A machine-checked proof that Gardam's $\widetilde A_2$ lattice does not have unique products, preprint, 2026. https://arxiv.org/abs/2609.22380v1
• OpenAI, A Torsion-Free Group Algebra with Zero Divisors, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Torsion-Free-Group-Algebra-with-Zero-Divisors-September-23-2026/paper.pdf

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