Combinatorics

Motivation

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

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

Background

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 1.1 (p. 1)

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

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

Background

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every fixed $s>0$,

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

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

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

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

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

Setting

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

Formalization targets

Milestone: special case of Theorem 1.1

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

Goal: Theorem 1.1

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

• OpenAI, A counterexample to Ryser's covering conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Counterexample-to-Rysers-Covering-Conjecture-September-23-2026/paper.pdf
• J. R. Henderson, Permutation decompositions of (0,1)-matrices and decomposition transversals, PhD thesis, 1971. https://doi.org/10.7907/J1Z1-SK19
• R. Aharoni, Ryser's conjecture for tripartite 3-graphs, Combinatorica, 2001. https://doi.org/10.1007/s004930170001
• P. Haxell, A. Scott, On Ryser's conjecture, Electron. J. Combin., 2012. https://doi.org/10.37236/1175
• N. Francetić, S. Herke, B. D. McKay, I. M. Wanless, On Ryser's conjecture for linear intersecting multipartite hypergraphs, European J. Combin., 2017. https://doi.org/10.1016/j.ejc.2016.10.004
• A. Abu-Khazneh, J. Barát, A. Pokrovskiy, T. Szabó, A family of extremal hypergraphs for Ryser's conjecture, J. Combin. Theory Ser. A, 2019. https://doi.org/10.1016/j.jcta.2018.07.011
• J. Bourgain, N. Katz, T. Tao, A sum-product estimate in finite fields, and applications, Geom. Funct. Anal., 2004. https://doi.org/10.1007/s00039-004-0451-1
• A. Clow, P. Haxell, B. Mohar, A counterexample to a conjecture of Lovász, Combinatorica, 2026. https://doi.org/10.1007/s00493-026-00220-3
• OpenAI, Balanced counterexamples to Ryser's conjecture at prime orders, preprint, September 27, 2026.

Motivation

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

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

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

Timeline

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

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

Setting

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

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

Formalization targets

Goal: Theorem 1.1

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

Timeline

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

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

Setting

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

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

Colourings may use fewer than $r$ colours.

Formalization targets

Goal: Theorem 1.1

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

Timeline

• 1933. Borsuk poses the partition question (doi:10.4064/fm-20-1-177-190).
• 1981. Frankl and Wilson prove a forbidden-intersection theorem that later drives the first counterexample (doi:10.1007/BF02579457).
• 1993. Kahn and Kalai disprove Borsuk's conjecture in dimension $1325$ and all large dimensions (doi:10.1090/S0273-0979-1993-00398-7).
• 1994–2000. Reductions to dimension $946$ (Nilli), $561$ (Raigorodskii, doi:10.1070/RM1997v052n06ABEH002184) and $560$ (Weißbach).
• 2002–2003. Spherical codes from the Leech lattice give $323$ (Hinrichs, doi:10.1016/S0012-365X(01)00202-3), $321$ (Pikhurko, arXiv:math/0202112) and $298$ (Hinrichs–Richter, doi:10.1016/S0012-365X(02)00833-6).
• 2014. Strongly regular graphs give $65$ (Bondarenko, doi:10.1007/s00454-014-9579-4) and $64$ (Jenrich–Brouwer, doi:10.37236/4069).
• 2015. Kalai surveys the problem and describes the projector embedding $x\mapsto x\otimes x$ (doi:10.1017/CBO9781316106853.005).
• 2026. Grinsztajn gives a finite counterexample in dimension $63$ (author manuscript).

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

Setting

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

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

Formalization targets

Goal: Theorem 1.1

The set

$$X=\{uu^{\mathsf T}:u\in\mathbb R^4,\ \|u\|=1\}\subset\{A\in\mathrm{Sym}_4(\mathbb R):\operatorname{tr}A=1\}$$

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

• OpenAI, A nine-dimensional counterexample to Borsuk's covering assertion, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-nine-dimensional-counterexample-to-Borsuks-covering-assertion-September-23-2026/paper.pdf
• K. Borsuk, Drei Sätze über die $n$-dimensionale euklidische Sphäre, Fund. Math., 1933. https://doi.org/10.4064/fm-20-1-177-190
• J. Kahn, G. Kalai, A counterexample to Borsuk's conjecture, Bull. Amer. Math. Soc., 1993. https://doi.org/10.1090/S0273-0979-1993-00398-7
• A. Hinrichs, C. Richter, New sets with large Borsuk numbers, Discrete Math., 2003. https://doi.org/10.1016/S0012-365X(02)00833-6
• A. V. Bondarenko, On Borsuk's conjecture for two-distance sets, Discrete Comput. Geom., 2014. https://doi.org/10.1007/s00454-014-9579-4
• T. Jenrich, A. E. Brouwer, A 64-dimensional counterexample to Borsuk's conjecture, Electron. J. Combin., 2014. https://doi.org/10.37236/4069
• G. Kalai, Some old and new problems in combinatorial geometry I: around Borsuk's problem, Surveys in Combinatorics, 2015. https://doi.org/10.1017/CBO9781316106853.005
• D. W. Walkup, The lower bound conjecture for 3- and 4-manifolds, Acta Math., 1970. https://doi.org/10.1007/BF02392331

Motivation

A cell-bounded contingency table is a nonnegative integer matrix with prescribed row sums, column sums and an upper bound on each entry. Bounds of zero forbid entries (structural zeros), and bounds of one give bipartite graphs with prescribed degrees, so the model contains degree-constrained subgraph counting and perfect matchings (the permanent). Counting such tables is central to exact conditional inference in statistics and is equivalent to counting integer flows in bipartite networks. Exact counting is #P-complete even for two-row ordinary tables (Dyer, Kannan and Mount, 1997), so the target is a fully polynomial randomized approximation scheme (FPRAS): a randomized algorithm that, for any $\varepsilon,\delta\in(0,1)$, returns a $(1\pm\varepsilon)$-approximation with probability at least $1-\delta$ in time polynomial in the input length, $1/\varepsilon$ and $\log(1/\delta)$.

Timeline

• 1986. Jerrum, Valiant and Vazirani relate approximate counting and sampling through self-reducibility.
• 1995. Diaconis and Gangolli survey fixed-margin arrays (doi:10.1007/978-1-4612-0801-3_3).
• 1997. Dyer, Kannan and Mount prove #P-completeness for two-row tables and give geometric methods for large margins; Morris improves the margin requirements in 2002 (doi:10.1002/rsa.10049).
• 2000–2003. Dyer and Greenhill (two rows), Cryan and Dyer (fixed number of rows), Dyer (dynamic programming) give approximate counting for a bounded number of rows.
• 2004. Jerrum, Sinclair and Vigoda's permanent algorithm yields an FPRAS for all 0/1 caps (doi:10.1145/1008731.1008738).
• 2009–2010. Barvinok bounds weighted table counts within $N^{O(m+n)}$ (doi:10.1093/imrn/rnn133); Barvinok, Luria, Samorodnitsky and Yong give quasipolynomial randomized approximations for smooth margins (doi:10.1002/rsa.20301).
• 2010. Cryan, Dyer and Randall give an FPRAS for integral flows with large tight capacities and for cell-bounded tables with a fixed number of rows, and list unrestricted approximation as open (doi:10.1137/060650544).
• 2023. Brändén, Leake and Pak give capacity lower bounds via Lorentzian polynomials (doi:10.1007/s11856-022-2364-9); Guo and Jerrum count vertices of certain 0/1 polytopes (doi:10.1007/s00454-022-00406-8).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims an FPRAS with no restriction on dimensions, margins or caps.

Setting

For positive integers $m,n$, margins $r\in\mathbb Z_{\ge0}^m$, $c\in\mathbb Z_{\ge0}^n$ with equal totals, and bounds $b\in\mathbb Z_{\ge0}^{m\times n}$,

$$\Omega(r,c,b)=\Bigl\{X\in\mathbb Z_{\ge0}^{m\times n}:\ \textstyle\sum_jX_{ij}=r_i,\ \sum_iX_{ij}=c_j,\ X_{ij}\le b_{ij}\Bigr\},\qquad Z(r,c,b)=|\Omega(r,c,b)|.$$

All numbers are written in binary, so a capacity can be exponentially larger than its description. $L$ denotes the total binary input length including the rational accuracy parameters $\varepsilon,\delta$. The algorithm uses independent unbiased random bits and is charged for every bit operation.

Formalization targets

Goal: Theorem 1.1 (FPRAS)

One randomized algorithm, given $(r,c,b)$ and rational $\varepsilon,\delta\in(0,1)$, outputs a nonnegative rational $\widehat Z$ with

$$\Pr\bigl[(1-\varepsilon)Z(r,c,b)\le\widehat Z\le(1+\varepsilon)Z(r,c,b)\bigr]\ge1-\delta,$$

outputs exactly $0$ on every execution when $\Omega(r,c,b)=\emptyset$, and performs at most $\mathrm{poly}(L,\varepsilon^{-1},\log\delta^{-1})$ bit operations on every execution. Lean: OAI.ContingencyTables.counting, open on the platform.

Significance

The theorem would answer the question left open by Cryan, Dyer and Randall in 2010: approximate counting of cell-bounded tables (equivalently, integral flows in bipartite networks with arbitrary capacities) without any fixed-dimension, large-capacity, density or balance assumption, with polynomial cost on every execution and no oracle. It contains the 0/1 case handled by Jerrum–Sinclair–Vigoda and the fixed-row results as special cases, and via self-reduction it gives approximate samplers for integer flows. A companion preprint of the same family treats exact uniform sampling of uncapped tables. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Two regimes clash. Large capacities cannot be expanded into that many binary choices without exponential blow-up, so geometric (polytope volume) methods are needed for them; but those methods require every cell to be large. Small capacities need combinatorial Markov chains, which in turn must preserve exactly one unit of mass per table despite the multiplicities created by encoding a bounded integer by binary choices. Arbitrary mixtures of tiny and huge caps, zero caps and variable dimensions defeat each approach used alone.

Formalization scope

• Algorithms are MatchingFPRAS.RandomMachines: a single finite transition table on an 8-symbol alphabet, one random bit per tick; time is counted in ticks (polynomially equivalent to bit operations).
• Inputs are delimited binary encodings of $m,n,r,c,b$ and of $\varepsilon,\delta$ as reduced fractions (encodeCountingInput); outputs are encoded rationals.
• count r c b is Fintype.card of bounded tables.
• CountingStatement: one machine and constants $C>0$, $d$; with $t=C(|\text{input}|+\lceil1/\varepsilon\rceil+\lceil\log_2\lceil1/\delta\rceil\rceil+1)^d$, every tape of length $t$ halts with a rational $q\ge0$; if count = 0 every tape outputs $0$; and the fraction of tapes with $(1-\varepsilon)Z\le q\le(1+\varepsilon)Z$ is at least $1-\delta$.
• $m,n\ge1$ and equal margin totals are hypotheses, as in the paper.

Needed infrastructure: randomized Turing machines, Markov chain mixing and Poincaré inequalities, log-concavity (Prékopa–Leindler), and network-flow feasibility. The machine model and encodings are shared with the exact-sampling mission of this family. Contributions formalizing Proposition 2.2 (contamination bound), Lemma 3.3 (log-concave tree marginals), Proposition 6.1 (weight evaluation) or Proposition 7.2 are welcome.

Selected references

• OpenAI, An FPRAS for Cell-Bounded Contingency Tables, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-FPRAS-for-Cell-Bounded-Contingency-Tables-September-24-2026/main.pdf
• M. Cryan, M. Dyer, D. Randall, Approximately counting integral flows and cell-bounded contingency tables, SIAM J. Comput., 2010. https://doi.org/10.1137/060650544
• M. Jerrum, A. Sinclair, E. Vigoda, A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries, J. ACM, 2004. https://doi.org/10.1145/1008731.1008738
• B. Morris, Improved bounds for sampling contingency tables, Random Structures Algorithms, 2002. https://doi.org/10.1002/rsa.10049
• A. Barvinok, Asymptotic estimates for the number of contingency tables, integer flows, and volumes of transportation polytopes, IMRN, 2009. https://doi.org/10.1093/imrn/rnn133
• A. Barvinok, Z. Luria, A. Samorodnitsky, A. Yong, An approximation algorithm for counting contingency tables, Random Structures Algorithms, 2010. https://doi.org/10.1002/rsa.20301
• P. Brändén, J. Leake, I. Pak, Lower bounds for contingency tables via Lorentzian polynomials, Israel J. Math., 2023. https://doi.org/10.1007/s11856-022-2364-9
• H. Guo, M. Jerrum, Counting vertices of integral polytopes defined by facets, Discrete Comput. Geom., 2023. https://doi.org/10.1007/s00454-022-00406-8

Motivation

A contingency table with margins $r=(r_1,\dots,r_m)$ and $c=(c_1,\dots,c_n)$ is a nonnegative integer matrix whose row sums are $r$ and column sums are $c$. Such tables are the basic objects of categorical data analysis: conditional tests of independence (Fisher's exact test and its generalizations) compare an observed table with the uniform distribution on all tables with the same margins, and in practice this requires sampling uniformly from that set. The set is finite but can be exponentially large in the input size when margins are written in binary. Whether one can sample it (approximately or exactly) in time polynomial in both dimensions and in the bit length of the margins has been open since the 1990s.

Timeline

• 1995. Diaconis and Gangolli survey enumeration and random generation of rectangular arrays with fixed margins (doi:10.1007/978-1-4612-0801-3_3).
• 1997–2002. Dyer, Kannan and Mount sample dense tables via the transportation polytope; Morris improves the dense bounds (doi:10.1002/rsa.10049).
• 2000. Dyer and Greenhill give polynomial-time approximate counting and sampling for two-rowed tables.
• 2003. Kijima and Matsui give exact sampling for two rows by coupling from the past; Cryan and Dyer approximately count for a fixed number of rows (doi:10.1016/S0022-0000(03)00014-X); Dyer gives an exact dynamic-programming sampler for fixed row count.
• 2006. Cryan, Dyer, Goldberg, Jerrum and Martin prove rapid mixing of the heat-bath chain for every fixed number of rows (doi:10.1137/S0097539703434243).
• 2016. DeSalvo and Zhao give an exact divide-and-conquer sampler whose polynomial runtime is conditional on a conjecture (arXiv:1507.00070).
• 2021. Arman, Gao and Wormald give linear-time exact generation for sparse margins with $5\Delta^4<N$, and report that no polynomial-time approximately uniform sampler for arbitrary margins was known (arXiv:2104.09413).
• 2024. Göbel, Liu, Manurangsi and Pappik turn sufficiently accurate samplers into perfect samplers (arXiv:2410.00882).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims both an almost-uniform and an exactly uniform sampler for arbitrary margins.

Setting

For nonnegative integer vectors $r\in\mathbb Z_{\ge0}^m$, $c\in\mathbb Z_{\ge0}^n$ with common total $N=\sum_ir_i=\sum_jc_j$, let

$$\Omega(r,c)=\Bigl\{X\in\mathbb Z_{\ge0}^{m\times n}:\ \textstyle\sum_jX_{ij}=r_i,\ \sum_iX_{ij}=c_j\Bigr\}.$$

The input is $(m,n,r,c)$ with margins in binary, so its length is polynomial in $m$, $n$ and $\log(N+1)$. An algorithm uses unbiased random bits. For laws on a finite set, $\mathrm{TV}(\mu,\nu)=\tfrac12\sum_x|\mu(x)-\nu(x)|$.

Formalization targets

Milestone: Theorem 1.1(i) (almost-uniform, bounded time)

For each $k\ge1$, an algorithm halts on every execution in time $\mathrm{poly}(m,n,\log(N+1),k)$ and outputs $X\in\Omega(r,c)$ with

$$\mathrm{TV}\bigl(\mathrm{law}(X),\ \mathrm{Unif}\,\Omega(r,c)\bigr)\le2^{-k}.$$

Goal: Theorem 1.1(ii) (exact uniform sampling)

An algorithm outputs $X\in\Omega(r,c)$ with

$$\Pr[X=Y]=\frac1{|\Omega(r,c)|}\quad(Y\in\Omega(r,c)),$$

terminates almost surely, and has expected running time $\mathrm{poly}(m,n,\log(N+1))$, with polynomials uniform over all margins. Lean: OAI.ContingencyTables.exactSampling, open on the platform.

Significance

The theorem would give the first unconditional polynomial-time exact uniform sampler for contingency tables with arbitrary dimensions and binary margins, with no positivity, sparsity, balance or fixed-dimension restriction, and with all random bits and integer arithmetic counted. It removes the fixed-row restriction of the Dyer–Greenhill and Cryan–Dyer line and the sparsity condition of Arman–Gao–Wormald. The exponents are deliberately large; the contribution is the existence of a polynomial algorithm. Exact time is polynomial in expectation, not on every run. A companion preprint of the same family gives an FPRAS for counting tables with cell bounds. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Markov-chain approaches mix rapidly for a fixed number of rows, but the bounds degrade with the row count. Geometric (polytope) methods need all margins to be large, and fail when some margins are tiny while others are huge, which is exactly the mixed regime that arbitrary binary margins allow. Making the sampler exact rather than approximate adds a separate difficulty: the residual-mixture correction requires that the actual output law of the approximate sampler can be computed, with cost polynomial in the accuracy bits.

Formalization scope

• Algorithms are MatchingFPRAS.RandomMachines: a single finite transition table over an 8-symbol tape alphabet; each tick reads one random bit and either moves, writes or halts. Time is counted in ticks, polynomially equivalent to bit operations.
• Inputs are binary encodings with delimiters (encodeNat, encodeMargins); outputs are row-major matrix encodings left on the tape (OutputsTable).
• tableMass A input t X and haltMass A input t are the fractions of the $2^t$ random tapes of length $t$ that halt with output $X$, respectively halt at all, within $t$ ticks.
• ExactSamplingStatement: one machine and constants $C>0$, $d$ such that for all $m,n,r,c$ with equal totals: every halted output is in $\Omega(r,c)$; tableMass → 1/|Ω| for each table; haltMass → 1; and $\sum_t(1-\text{haltMass}_t)$, the expected running time, is at most $C(m+n+\lceil\log_2(N+1)\rceil+1)^d$.
• BoundedSamplingStatement: every tape of length $t=C(m+n+\lceil\log_2(N+1)\rceil+k+1)^d$ halts with a feasible table, and the TV distance to uniform is at most $2^{-k}$.
• Dimensions $m,n$ vary freely (zero allowed); the machine is uniform, not one per size.

Needed infrastructure: randomized Turing machines and their output laws, Markov chain mixing (conductance, Poincaré inequalities), and log-concave sampling. Contributions formalizing Theorem 4.3 (graph Poincaré inequality), Theorem 5.1 (dense completion draw), Proposition 6.3 (law tabulation) or the Göbel–Liu–Manurangsi–Pappik correction are welcome.

Selected references

• OpenAI, Exact Uniform Sampling of Contingency Tables with Arbitrary Margins, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Exact-Uniform-Sampling-of-Contingency-Tables-with-Arbitrary-Margins-September-24-2026/main.pdf
• P. Diaconis, A. Gangolli, Rectangular arrays with fixed margins, Discrete Probability and Algorithms, 1995. https://doi.org/10.1007/978-1-4612-0801-3_3
• B. Morris, Improved bounds for sampling contingency tables, Random Structures Algorithms, 2002. https://doi.org/10.1002/rsa.10049
• M. Cryan, M. Dyer, A polynomial-time algorithm to approximately count contingency tables when the number of rows is constant, J. Comput. System Sci., 2003. https://doi.org/10.1016/S0022-0000(03)00014-X
• M. Cryan, M. Dyer, L. A. Goldberg, M. Jerrum, R. Martin, Rapidly mixing Markov chains for sampling contingency tables with a constant number of rows, SIAM J. Comput., 2006. https://doi.org/10.1137/S0097539703434243
• S. DeSalvo, J. Y. Zhao, Random sampling of contingency tables via probabilistic divide-and-conquer, preprint, 2016. https://arxiv.org/abs/1507.00070
• A. Arman, P. Gao, N. Wormald, Linear-time uniform generation of random sparse contingency tables with specified marginals, preprint, 2021. https://arxiv.org/abs/2104.09413
• A. Göbel, J. Liu, P. Manurangsi, M. Pappik, Perfect sampling from rapidly mixing Markov chains, preprint, 2024. https://arxiv.org/abs/2410.00882

Motivation: counting common bases of two matroids

A matroid abstracts linear independence: a finite ground set with a family of "independent" subsets that is closed under subsets and satisfies the augmentation axiom. Its maximal independent sets, the bases, all have the same size, the rank. Matroid intersection, finding a common basis of two matroids, is one of the central polynomially solvable problems of combinatorial optimization (Edmonds, 1979). Counting common bases is much harder. It contains counting bases of a single matroid (take both matroids equal) and counting perfect matchings of a bipartite graph (take two partition matroids), and exact counting is #P-hard. The natural goal is therefore a fully polynomial randomized approximation scheme (FPRAS): an algorithm whose output is within relative error $\epsilon$ with probability at least $1-\delta$, in time polynomial in the input size, $\epsilon^{-1}$ and $\log\delta^{-1}$. The matroids should be accessible only through independence oracles.

Background and timeline

• 1979 — Edmonds gives a polynomial-time algorithm for matroid intersection (Ann. Discrete Math. 4).
• 1992 — Feder and Mihail give sampling and approximate counting for balanced matroids (STOC 1992).
• 2004 — Jerrum, Sinclair and Vigoda give an FPRAS for the permanent of nonnegative matrices, covering bipartite perfect matchings (J. ACM 51).
• 2007 — Barvinok and Samorodnitsky obtain coarse logarithmic estimates via random weighting (Israel J. Math. 158).
• 2016–2017 — Anari, Oveis Gharan and Rezaei prove rapid mixing for strongly Rayleigh distributions (COLT 2016); Anari and Oveis Gharan obtain exponential-factor approximations from real-stable polynomials (arXiv:1702.02937).
• 2020 — Brändén and Huh develop Lorentzian polynomials (Ann. of Math. 192).
• 2021 — Anari, Oveis Gharan and Vinzant give a deterministic $2^{O(r)}$-factor approximation for common bases of rank-$r$ matroids (Duke Math. J. 170); Cryan, Guo and Mousa ask for a rapidly mixing chain for common bases (Ann. Probab. 49).
• 2023–2024 — Liu's dissertation records the FPRAS question for two arbitrary oracle matroids (Section 13.2, Problem 1, thesis); Anari, Liu, Oveis Gharan and Vinzant give an FPRAS for bases of a single matroid (Ann. of Math. 199).
• 2026 — An OpenAI preprint, Approximate counting of common bases of two matroids (OpenAI Math Release, September 23, 2026), claims an independence-oracle FPRAS for common bases of two arbitrary matroids of equal rank. It has not been peer reviewed, and its proof is not formally verified.

Setting

Let $M_1,M_2$ be matroids of the same rank $r$ on the ground set $[n]$, supplied by exact independence oracles: a query is an $n$-bit indicator of a subset, and the answer says whether it is independent. The quantity to estimate is

$$Z(M_1,M_2)=\bigl|\mathcal B(M_1)\cap\mathcal B(M_2)\bigr|,$$

the number of common bases. The input also contains rationals $\epsilon,\delta\in(0,1)$; $\ell$ denotes the binary encoding length of $n,r,\epsilon,\delta$. Oracle calls are counted separately from the bit operations used to build queries and process answers.

Formalization targets

Goal: an FPRAS for common bases in the independence-oracle model (Theorem 1.1)

There is a single randomized oracle algorithm and a fixed polynomial $p$ such that, for all rank-$r$ matroids $M_1,M_2$ on $[n]$ and rational $\epsilon,\delta\in(0,1)$, it outputs a nonnegative rational $\widehat Z$ with

$$\Pr\bigl[(1-\epsilon)Z\le\widehat Z\le(1+\epsilon)Z\bigr]\ \ge\ 1-\delta,$$

the output is always $0$ when $Z=0$, and on every execution the numbers of oracle calls and bit operations are at most $p(n,\ell,\epsilon^{-1},\log\delta^{-1})$. The algorithm uses only independent fair random bits. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.1 answers the question recorded by Liu (2023) and extends both the single-matroid FPRAS of Anari–Liu–Oveis Gharan–Vinzant and, in the bipartite-matching case, the permanent FPRAS of Jerrum–Sinclair–Vigoda. It needs no representation of either matroid and holds for unrestricted rank, whereas the previous oracle-model scheme was fully polynomial only for $r=O(\log n)$. The source derives FPRASs and almost-uniform samplers for common independent sets of prescribed, unrestricted or maximum size, even for matroids of different ranks (Corollary 9.1).

Formalizing it. The Lean goal fixes a concrete machine model, so it states a complete complexity-theoretic claim with no informal "polynomial-time" left. A proof would combine Lorentzian-polynomial inequalities (Brändén–Huh), a transport inequality, a Markov-chain Poincaré bound, and simulated annealing with explicit bit accounting. Each layer is reusable: Mathlib has matroids, but no Lorentzian polynomials, no mixing-time theory of this kind and no randomized-algorithm framework.

Difficulty

For one matroid, the bases-exchange walk mixes rapidly because the basis generating polynomial is log-concave. The intersection of two matroids has no such structure: its common bases need not be connected by short exchanges, and the natural chain on transversals of the paired construction passes through states of exponentially small weight, so positivity and connectivity alone give no polynomial bound. Earlier approaches either lost exponential factors or needed real-stable polynomials that an independence oracle does not provide. The proof must balance defect classes, as in Jerrum–Sinclair–Vigoda, and establish a Poincaré inequality for observables from matroid-theoretic inequalities alone.

Formalization scope

• Matroids are Mathlib Matroid (Fin n) with ground set univ and eRank = r for both. Oracles are functions Bool → (Fin n → Bool) → Bool, required to answer independence queries exactly.
• The algorithm is one fixed Program k s for a register machine with $k+8$ binary stacks: push/pop, fair coin, oracle query on an $n$-bit register, and halt with output (register 6)/(register 7) as a rational. Inputs $n,r,\epsilon,\delta$ are loaded in binary.
• The resource bound is $B=C(1+n+\ell+\lceil\epsilon^{-1}\rceil+\lceil\log_2\lceil\delta^{-1}\rceil\rceil)^d$ with constants $C>0,d$ fixed before the instance. For every infinite bit stream, the run halts within $B$ steps with at most $B$ oracle calls and $B$ bit operations, outputs a nonnegative rational, and outputs $0$ when $Z=0$.
• The success probability is expressed by counting: at least $(1-\delta)2^B$ of the $2^B$ bit strings of length $B$ lead to an output within relative error $\epsilon$ of $Z$.
• A trivializing reading is excluded: the program and constants come first and must work for every $n,r$, matroid pair, oracle and $\epsilon,\delta$.
• Needed infrastructure: Lorentzian polynomials and the homogeneous Tutte inequalities, Markov chains on finite state spaces with Poincaré/variance bounds, annealing estimators, and correctness proofs for the register machine. Contributions on any layer are welcome.

Selected references

• J. Edmonds, Matroid intersection, Ann. Discrete Math. 4 (1979), 39–49. https://doi.org/10.1016/S0167-5060(08)70817-3
• T. Feder and M. Mihail, Balanced matroids, STOC 1992. https://doi.org/10.1145/129712.129716
• M. Jerrum, A. Sinclair and E. Vigoda, A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries, J. ACM 51 (2004), 671–697. https://doi.org/10.1145/1008731.1008738
• A. Barvinok and A. Samorodnitsky, Random weighting, asymptotic counting, and inverse isoperimetry, Israel J. Math. 158 (2007). https://doi.org/10.1007/s11856-007-0008-8
• P. Brändén and J. Huh, Lorentzian polynomials, Ann. of Math. 192 (2020), 821–891. https://doi.org/10.4007/annals.2020.192.3.4
• N. Anari, S. Oveis Gharan and C. Vinzant, Log-concave polynomials I, Duke Math. J. 170 (2021). https://doi.org/10.1215/00127094-2020-0091
• M. Cryan, H. Guo and G. Mousa, Modified log-Sobolev inequalities for strongly log-concave distributions, Ann. Probab. 49 (2021). https://doi.org/10.1214/20-AOP1453
• N. Anari, K. Liu, S. Oveis Gharan and C. Vinzant, Log-concave polynomials II: high-dimensional walks and an FPRAS for counting bases of a matroid, Ann. of Math. 199 (2024). https://doi.org/10.4007/annals.2024.199.1.4
• K. Liu, Spectral Independence: A New Tool to Analyze Markov Chains, PhD thesis, University of Washington, 2023. https://kuikuiliu.github.io/files/dissertation.pdf
• OpenAI, Approximate counting of common bases of two matroids, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Approximate-counting-of-common-bases-of-two-matroids-September-23-2026/main.pdf

Motivation: approximately counting perfect matchings

A perfect matching of a graph is a set of edges covering every vertex exactly once. Finding one is easy — Edmonds (1965) gave a polynomial-time algorithm for general graphs — but counting them is hard: Valiant (1979) proved exact counting #P-complete already for bipartite graphs, where the count is the permanent of a 0–1 matrix. Exact counting is tractable only in special classes, such as planar graphs via Pfaffians (Kasteleyn 1963). The natural relaxation is a fully polynomial randomized approximation scheme (FPRAS): an algorithm that, with probability at least $1-\delta$, returns the count within relative error $\varepsilon$, in time polynomial in the input size, $1/\varepsilon$ and $\log(1/\delta)$. Whether perfect matchings in general (nonbipartite) graphs admit an FPRAS was explicitly raised by Jerrum and Sinclair in 1989 and has been a benchmark question in approximate counting since. Perfect-matching counts are partition functions of the monomer–dimer model, so the question also connects to statistical physics.

Timeline

• 1963 — Kasteleyn: exact counting of perfect matchings in planar graphs (J. Math. Phys. 1963).
• 1965 — Edmonds: polynomial-time maximum matching in general graphs (Canad. J. Math. 1965).
• 1979 — Valiant: computing the permanent is #P-complete (TCS 1979).
• 1986 — Jerrum, Valiant and Vazirani: equivalence of approximate counting and almost-uniform sampling for self-reducible problems (TCS 1986).
• 1989 — Jerrum and Sinclair: FPRAS for the number of all matchings in any graph, and for perfect matchings when the near-perfect/perfect ratio is polynomially bounded; they raise the general question (SIAM J. Comput. 1989, Section 7(i)).
• 2004 — Jerrum, Sinclair and Vigoda: FPRAS for the permanent of every nonnegative matrix, i.e. bipartite perfect matchings (J. ACM 2004); accelerated by Bezáková, Štefankovič, Vazirani and Vigoda (SIAM J. Comput. 2008).
• 2018 — Štefankovič, Vigoda and Wilmes: graphs on which every chain of Jerrum–Sinclair–Vigoda type either gives perfect matchings exponentially small mass or mixes exponentially slowly (LATIN 2018).
• 2020–2025 — Cai and Liu relate the problem to the eight-vertex model (ICALP 2020); Fei, Goldberg and Lu locate it among two-state spin systems (Inf. Comput. 2025).
• 2026 — Further permanent speedups by Chen, Vigoda and Yang (arXiv:2608.26599) and Chen, Guo, Vigoda and Yang (arXiv:2609.20717); deterministic hafnian approximation for dense graphs by Yi (arXiv:2609.04079). An OpenAI preprint, A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs (OpenAI Math Release, September 23, 2026), claims an FPRAS for every finite simple graph. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

A finite simple undirected graph $G$ on vertices $\{0,\dots,n-1\}$ is given by a set of edges, each written once as a pair $(u,v)$ with $u<v$. A set $M\subseteq E$ is a perfect matching if every vertex lies in exactly one edge of $M$, and

$$Z(G)=\#\{M\subseteq E: M\text{ is a perfect matching of }G\}.$$

(The graph with no vertices has $Z=1$; any graph with an odd number of vertices has $Z=0$.)

A randomized algorithm is modelled as a single fixed machine with a finite transition table over a finite tape alphabet, which at each step reads the current tape symbol and one fresh fair random bit, then writes, moves, or halts. The input is the graph in binary (number of vertices, number of edges, the sorted edge list) followed by the rationals $\varepsilon$ and $\delta$ in reduced form; the output is a rational number written on the tape when the machine halts.

Formalization targets

Goal: Theorem 1.1 (FPRAS for perfect matchings)

There are a machine $A$ and constants $C>0$, $d$ such that for every graph $G$ and rationals $0<\varepsilon<1$, $0<\delta<1/2$, with $t=C\,(|\mathrm{input}|+\lceil\varepsilon^{-1}\rceil+\lceil\log_2\lceil\delta^{-1}\rceil\rceil+1)^d$:

• on every random string of length $t$, $A$ halts within $t$ steps with a nonnegative rational output $\widehat Z$;
• if $Z(G)=0$, the output is $0$ on every random string;

$$\Pr_{\text{bits}}\big[(1-\varepsilon)Z(G)\le\widehat Z\le(1+\varepsilon)Z(G)\big]\;\ge\;1-\delta.$$

The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem answers the Jerrum–Sinclair question affirmatively: perfect matchings in arbitrary graphs can be approximately counted as efficiently, up to polynomial factors, as in the bipartite case. The worst-case time bound holds for every execution, not just in expectation. Via standard reductions, the source also derives counting schemes for edge subsets with prescribed vertex degrees and for matchings of a fixed size (Corollary 10.1). The accompanying samplers for those families always return a feasible object and approximate the uniform law in total variation.

Formalizing it. The statement fixes a concrete machine model, input encoding and time bound, so a formal proof would certify both correctness of the estimator and the polynomial running time of an explicit algorithm — a level of rigor rarely reached for Markov-chain Monte Carlo results, whose analyses involve many interacting constants.

Difficulty

The natural approach extends the Jerrum–Sinclair–Vigoda Markov chain on perfect and near-perfect matchings, with weights learned while edge activities are gradually lowered. In general graphs this approach provably fails: Štefankovič, Vigoda and Wilmes constructed graphs on which every chain of that type, for any hole-dependent weights, has either exponentially small stationary mass on perfect matchings or exponentially slow mixing. Odd cycles (blossoms) are the reason the bipartite canonical-path arguments do not carry over. A solution needs a different state space and a different mixing analysis.

Formalization scope

• GraphInput is a vertex count n and a Finset (Fin n × Fin n) of edges with strictly increasing endpoints, so loops and duplicate edges are excluded. Perfect G M requires M ⊆ edges and that each vertex is incident to exactly one edge of M; Z G is the number of such M.
• The machine model is RandomMachine: a finite transition table on Fin 8 symbols, whose step consumes one random bit and performs a Turing.TM0 write or move, or halts. run folds tick over a list of t bits; halted configurations are absorbing.
• encodeInput writes the vertex count, edge count and lexicographically sorted edges in binary, then encodeRat ε and encodeRat δ (reduced numerator with sign, denominator). Outputs requires that the machine has halted and the tape to the right of the head is exactly the encoding of the output rational.
• The time bound is a fixed polynomial with natural ceilings; the success probability is the fraction of good tapes among all $2^t$ tapes.
• The scheme must be uniform: one machine for all inputs, quantified before the graph. A trivializing reading is excluded because every tape must halt within the bound with a nonnegative output, and zero must be returned exactly when $Z(G)=0$.
• Infrastructure needed: a compiler-style layer turning structured randomized algorithms into RandomMachine transitions, Markov-chain spectral-gap bounds, and sampling-to-counting reductions. The machine model and encodings are reusable for other approximate-counting missions.

Selected references

• P. W. Kasteleyn, Dimer statistics and phase transitions, J. Math. Phys. 4 (1963), 287–293. https://doi.org/10.1063/1.1703953
• J. Edmonds, Paths, trees, and flowers, Canad. J. Math. 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
• L. G. Valiant, The complexity of computing the permanent, Theoret. Comput. Sci. 8 (1979), 189–201. https://doi.org/10.1016/0304-3975(79)90044-6
• M. R. Jerrum, L. G. Valiant, V. V. Vazirani, Random generation of combinatorial structures from a uniform distribution, Theoret. Comput. Sci. 43 (1986), 169–188. https://doi.org/10.1016/0304-3975(86)90174-X
• M. Jerrum, A. Sinclair, Approximating the permanent, SIAM J. Comput. 18 (1989), 1149–1178. https://doi.org/10.1137/0218077
• M. Jerrum, A. Sinclair, E. Vigoda, A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries, J. ACM 51 (2004), 671–697. https://doi.org/10.1145/1008731.1008738
• I. Bezáková, D. Štefankovič, V. V. Vazirani, E. Vigoda, Accelerating simulated annealing for the permanent and combinatorial counting problems, SIAM J. Comput. 37 (2008), 1429–1454. https://doi.org/10.1137/050644033
• D. Štefankovič, E. Vigoda, J. Wilmes, On counting perfect matchings in general graphs, LATIN 2018, LNCS 10807, 873–885. https://doi.org/10.1007/978-3-319-77404-6_63
• J.-Y. Cai, T. Liu, Counting perfect matchings and the eight-vertex model, ICALP 2020, LIPIcs 168, 23:1–23:18. https://doi.org/10.4230/LIPIcs.ICALP.2020.23
• Y. Fei, L. A. Goldberg, P. Lu, Two-state spin systems with negative interactions, Inf. Comput. 307 (2025), 105340. https://doi.org/10.1016/j.ic.2025.105340
• OpenAI, A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Fully-Polynomial-Randomized-Approximation-Scheme-for-Perfect-Matchings-in-General-Graphs-September-23-2026/main.pdf

Motivation

Edit distance $\mathrm{ED}(x,y)$, the least number of single-symbol insertions, deletions and substitutions turning $x$ into $y$, is the standard distance on strings. Embedding strings into $\ell_1$ with small distortion would make edit distance amenable to the fast nearest-neighbour and sketching tools available for $\ell_1$, so the least achievable distortion is a central quantity in metric embedding theory. A single insertion shifts every later symbol, yet cyclically shifting a word costs only two edits; this tension between position and alignment is what makes edit distance hard to embed.

This preprint gives two independent constructions of binary word sets whose least $\ell_1$ distortion is $\exp(\Omega(\sqrt{\log d\log\log d}))$, two binary coding arguments that transfer large-alphabet constructions to binary, and a complete histogram embedding attaining the matching upper scale. Together they determine the exponential scale of the distortion.

Background

• 1966, 1974. Levenshtein introduces insertion/deletion codes; Wagner and Fischer describe alignments by increasing traces.
• 1995. Linial, London and Rabinovich develop finite metric embeddings into $\ell_1$.
• 1999. Schulman and Zuckerman construct asymptotically good codes for insertions and deletions.
• 2003. Andoni, Deza, Gupta, Indyk and Raskhodnikova give binary sets with $\ell_1$ distortion approaching $3/2$.
• 2006. Khot and Naor prove a $(\log d)^{1/2 - o(1)}$ lower bound by Fourier analysis of cuts.
• 2007. Ostrovsky and Rabani prove the upper bound $\exp(O(\sqrt{\log d\log\log d}))$ for fixed-length binary strings.
• 2009. Krauthgamer and Rabani prove an $\Omega(\log d)$ lower bound.
• 2026. The OpenAI preprint Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance (dated September 27, 2026), a companion to Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent, proves the results below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

For a finite alphabet $\Sigma$ with $|\Sigma| \ge 2$ and an integer $d \ge 1$, let $\Sigma^{\le d}$ be the words of length at most $d$, including the empty word. For an injective $f : \Sigma^{\le d} \to \ell_1$,

$$\mathrm{dist}(f) = \Big(\max_{x\ne y}\frac{\|f(x)-f(y)\|_1}{\mathrm{ED}(x,y)}\Big)\Big(\max_{x\ne y}\frac{\mathrm{ED}(x,y)}{\|f(x)-f(y)\|_1}\Big), \qquad E_\Sigma(d) = \inf_f \mathrm{dist}(f).$$

The longest common subsequence $\mathrm{LCS}(x,y)$ and the deficit $r_L(x,y) = L - \mathrm{LCS}(x,y)$ for words of length $L$ are used in the coding results. A binary substitution $c : \Sigma \to \{0,1\}^w$ replaces each letter by a codeword.

In Lean (OAI.FiniteCircle), editDistance is the least script length, lcs and deficit are as above, optimalDistortion is the infimum of distortion over injective maps into lp (fun _ : ℕ => ℝ) 1, E α d is the least distortion of words of length at most $d$, and maskWord, excludedWord are the two finite-circle constructions with prime-period parameters.

Formalization targets

Goal: finiteCircle_fullMain

The conjunction of the paper's main statements, with common absolute constants:

• Theorem 1.1. For $d \ge d_0$ and every finite $\Sigma$ with $|\Sigma| \ge 2$,

$$\exp\big(c\sqrt{\log d\log\log d}\big) \le E_\Sigma(d) \le \exp\big(C\sqrt{\log d\log\log d}\big),$$

and the same bounds for $\sup_{|\Sigma| \ge 2} E_\Sigma(d)$.

• Lower constructions (Sections 5–7): for each $d \ge d_0$, both the mask construction and the excluded-prime construction, encoded in binary, give a set of words of one common length $n \le d$ with least distortion at least $\exp(c\sqrt{\log d\log\log d})$.
• Theorem 4.1 (two binary substitutions): for every alphabet of $A \ge 2$ letters there are codes $c : \Sigma \to \{0,1\}^w$ with $w = O(\log 2A)$ and $a\,w\,r_L(x,y) \le r_{wL}(c(x),c(y)) \le w\,r_L(x,y)$ for equal-length words, $\mathrm{ED}(c(x),c(y)) \le w\,\mathrm{ED}(x,y)$, plus the local separation property each construction needs.
• Theorem 8.1 (uniform upper bound): a deterministic finite-dimensional map $F$ with $\mathrm{ED}(x,y) \le \|F(x)-F(y)\|_1 \le \exp(C\sqrt{\log d\log\log d})\,\mathrm{ED}(x,y)$.

Significance

The result. The lower bounds reach the Ostrovsky–Rabani scale, so the order of $\log E_\Sigma(d)$ is $\sqrt{\log d\log\log d}$; this improves the previous $\Omega(\log d)$ lower bound to $\exp(\Omega(\sqrt{\log d\log\log d}))$. The histogram embedding gives an explicit, alphabet-uniform upper bound including all shorter words.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Unlike the companion paper, the upper bound here is proved in full (Section 8) rather than imported, so the goal is self-contained relative to the preprint. The edit-distance and distortion definitions are reusable across the edit-distance missions.

Difficulty

Lower bounds for edit distance must control every increasing matching of the two words, including matchings crossing the row boundaries used to construct them. A cheap translation of phases moves row lists at low edit cost, while a simultaneous half-turn at every leaf must be expensive; proving the latter for arbitrary alignments, and then showing that every $\ell_1$ image must distort one of these comparisons, requires combining a combinatorial separation estimate with a Fourier argument on the finite phase space that forces large total frequency.

Formalization scope

• Words are List α with Fintype α; the domain $\Sigma^{\le d}$ is a subtype by length; the empty word is included.
• distortion uses sSup over finite sets of ratios; optimalDistortion is sInf over injective maps into $\ell_1(\mathbb N)$; exponentScale d = sqrt(log d · log log d) with natural logarithms.
• The lower witnesses fix the paper's constructions (prime assignments MaskPrimes, ExcludedPrimes, depth parameters) and require a common positive length $n \le d$.
• UniformUpper asks for a map into Fin M → ℝ with the $\ell_1$ norm written as a finite sum.

The goal is not vacuous: a set with one element would have least distortion $0$, so witnesses must be nontrivial, and both bounds are required uniformly.

Needed infrastructure: LCS and alignment combinatorics, cut decompositions of finite $\ell_1$ metrics, Fourier analysis on finite cyclic groups, prime counting estimates, and random partition arguments for the upper bound. Contributions toward any component are welcome.

Selected references

• OpenAI, Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Finite-Circle-Obstructions-Binary-Codes-and-Histogram-Embeddings-for-Edit-Distance-September-27-2026/paper.pdf
• OpenAI, Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/main/preprints/Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026/paper.pdf
• R. Ostrovsky, Y. Rabani, Low distortion embeddings for edit distance, J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284322
• R. Krauthgamer, Y. Rabani, Improved lower bounds for embeddings into $L_1$, SIAM J. Comput. 38(6), 2009.
• S. Khot, A. Naor, Nonembeddability theorems via Fourier analysis, Math. Ann. 334(4), 2006. https://doi.org/10.1007/s00208-005-0745-0
• A. Andoni, M. Deza, A. Gupta, P. Indyk, S. Raskhodnikova, Lower bounds for embedding edit distance into normed spaces, SODA 2003.
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 1995. https://doi.org/10.1007/BF01200757
• L. J. Schulman, D. Zuckerman, Asymptotically good codes correcting insertions, deletions, and transpositions, IEEE Trans. Inform. Theory 45(7), 1999. https://doi.org/10.1109/18.796406
• V. I. Levenshtein, Binary codes capable of correcting deletions, insertions, and reversals, Soviet Physics Doklady 10(8), 1966.
• R. A. Wagner, M. J. Fischer, The string-to-string correction problem, J. ACM 21(1), 1974. https://doi.org/10.1145/321796.321811