All missions

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

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

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

Timeline

• 1961. Turyn and Storer prove that Barker sequences of odd length greater than 13 do not exist, and relate even-length Barker sequences to vanishing periodic autocorrelations (doi:10.1090/S0002-9939-1961-0125026-2).
• 1963. Ryser's monograph Combinatorial Mathematics records the circulant Hadamard problem (doi:10.5948/UPO9781614440147).
• 1965. Turyn, using cyclotomic character sums, shows that any order greater than four must be $4u^2$ with $u$ odd and not a prime power (doi:10.2140/pjm.1965.15.319).
• 1999–2016. B. Schmidt's field descent (doi:10.1090/S0894-0347-99-00298-2) and the work of Leung and Schmidt (2005, 2012, 2016) give much stronger arithmetic restrictions (doi:10.1007/s10623-011-9493-1, doi:10.1016/j.jcta.2015.11.005).
• 2016. Schmidt and Willms give a new proof of the odd-length Barker classification (doi:10.1007/s10623-015-0104-4).
• 2017. Logan and Mossinghoff exclude all but 4,489 candidate orders $4<n\le4\cdot10^{30}$ using double Wieferich prime pairs.
• 2024. Steinerberger shows that approximately orthogonal sign circulants exist in every order (doi:10.1007/s10623-024-01430-w), so the exact equality is essential.

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

Setting

A real $n\times n$ matrix $H$ is circulant if there is a function $h:\mathbb Z/n\mathbb Z\to\mathbb R$ with $H_{ij}=h(j-i)$, indices taken modulo $n$. It is a sign Hadamard matrix if every entry is $1$ or $-1$ and

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

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

A Barker sequence of length $n$ is $a\in\{-1,1\}^n$ with aperiodic autocorrelations

$$C_a(t)=\sum_{j=0}^{n-t-1}a_ja_{j+t},\qquad |C_a(t)|\le1\quad(1\le t<n).$$

Formalization targets

Goal: Theorem 1.1

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

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

Milestone: Corollary 1.2, even case

$$a\in\{-1,1\}^n\ \text{Barker},\ n\ge1\ \text{even}\ \Longrightarrow\ n\in\{2,4\}.$$

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

• OpenAI, The circulant Hadamard conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-circulant-Hadamard-conjecture-September-23-2026/paper.pdf
• H. J. Ryser, Combinatorial Mathematics, Carus Mathematical Monographs, 1963. https://doi.org/10.5948/UPO9781614440147
• R. J. Turyn, Character sums and difference sets, Pacific J. Math., 1965. https://doi.org/10.2140/pjm.1965.15.319
• R. Turyn, J. Storer, On binary sequences, Proc. Amer. Math. Soc., 1961. https://doi.org/10.1090/S0002-9939-1961-0125026-2
• B. Schmidt, Cyclotomic integers and finite geometry, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00298-2
• K. H. Leung, B. Schmidt, New restrictions on possible orders of circulant Hadamard matrices, Des. Codes Cryptogr., 2012. https://doi.org/10.1007/s10623-011-9493-1
• K.-U. Schmidt, J. Willms, Barker sequences of odd length, Des. Codes Cryptogr., 2016. https://doi.org/10.1007/s10623-015-0104-4
• B. Logan, M. J. Mossinghoff, Double Wieferich pairs and circulant Hadamard matrices, J. Combin. Math. Combin. Comput., 2017.
• S. Steinerberger, A note on approximate Hadamard matrices, Des. Codes Cryptogr., 2024. https://doi.org/10.1007/s10623-024-01430-w

Motivation

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

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

Background

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

Setting

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

Formalization targets

Milestone: the upper bound $\chi(\mathbb R^2)\le7$ (Theorem 1.1, p. 2)

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

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

There is no function $c:\mathbb R^2\to\{1,\dots,5\}$ with $c(x)\ne c(y)$ whenever $\|x-y\|=1$. Together with the milestone this gives $6\le\chi(\mathbb R^2)\le7$.

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

• OpenAI, The Euclidean plane is not five-colorable, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Euclidean-plane-is-not-five-colorable-September-23-2026/paper.pdf
• H. Hadwiger, Ungelöste Probleme Nr. 40, Elem. Math. (1961).
• L. Moser, W. Moser, Solution to Problem 10, Canad. Math. Bull. (1961). https://doi.org/10.1017/S0008439500025765
• N. G. de Bruijn, P. Erdős, A colour problem for infinite graphs and a problem in the theory of relations, Indag. Math. (1951). https://users.renyi.hu/~p_erdos/1951-01.pdf
• K. J. Falconer, The realization of distances in measurable subsets covering $\mathbb R^n$, J. Combin. Theory Ser. A (1981). https://doi.org/10.1016/0097-3165(81)90014-5
• D. R. Woodall, Distances realized by sets covering the plane, J. Combin. Theory Ser. A (1973). https://doi.org/10.1016/0097-3165(73)90020-4
• S. P. Townsend, Every 5-coloured map in the plane contains a monochrome unit, J. Combin. Theory Ser. A (1981). https://doi.org/10.1016/0097-3165(81)90046-7
• A. D. N. J. de Grey, The chromatic number of the plane is at least 5, Geombinatorics (2018). https://arxiv.org/abs/1804.02385v3
• M. J. H. Heule, Computing small unit-distance graphs with chromatic number 5, Geombinatorics (2018). https://arxiv.org/abs/1805.12181
• G. Exoo, D. Ismailescu, The chromatic number of the plane is at least 5: a new proof, Discrete Comput. Geom. (2020). https://doi.org/10.1007/s00454-019-00058-1
• G. Sokolov, V. Voronov, On the chromatic number of the plane for map-type colorings, arXiv:2502.01958 (2025). https://arxiv.org/abs/2502.01958v1
• A. Soifer, The 50th anniversary of one problem: the chromatic number of the plane & its relatives, Mathematics Competitions (2003). https://www.wfnmc.org/Journal%202003%201.pdf

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: how short can an Egyptian fraction be?

An Egyptian-fraction expansion writes a positive rational number as a sum of distinct unit fractions $1/n$. Every fraction $a/b$ with $1\le a<b$ has one, by the greedy algorithm, but greedy expansions can be long. The basic quantitative question is how many terms are needed in the worst case for a fixed denominator $b$. Let $N(a,b)$ be the least length of an expansion of $a/b$ with denominators $\ge2$, and $N(b)=\max_{1\le a<b}N(a,b)$. Erdős proved in 1950 that $N(b)\ll\log b/\log\log b$, showed that $N(b)\gg\log\log b$ (already for $a=b-1$), and conjectured that the double-logarithmic order is correct. The question appears in Erdős–Graham's 1980 problem book and as Erdős Problem 304. The same circle of questions asks how many expansions of $1$ with exactly $k$ terms exist, and which integers can appear as denominators in them (Erdős Problem 293).

Timeline

• 1940 — Nakayama studies $N(a,b)$ through arithmetic criteria for expansions with few terms (Tohoku Math. J. 46).
• 1950 — Erdős reports de Bruijn's bound $N(b)\ll\log b/\log\log\log b$, improves it to $N(b)\ll\log b/\log\log b$, proves the lower bound $N(b)\gg\log\log b$, and conjectures the matching upper bound (Mat. Lapok 1950).
• 1980 — Erdős and Graham restate the problem and ask for estimates of the number of $k$-term expansions of $1$ and for the least missing denominator (Old and New Problems…).
• 1985 — Vose proves $N(b)\ll\sqrt{\log b}$ (Bull. LMS 17).
• 1990 — Tenenbaum and Yokota give length $(1+\varepsilon)\log b/\log\log b$ with denominators $O(b(\log b)^2\log\log b)$ (J. Number Theory).
• 2014–2021 — Konyagin proves a lower bound for the number $F(k)$ of $k$-term expansions of $1$ with $\log\log F(k)\gg k/\log k$ (Mat. Zametki); Elsholtz extends it to restricted denominators (Q. J. Math.); Elsholtz and Planitzer prove $\log\log F(k)=O(k)$ (Bull. LMS).
• 2026 — van Doorn and Tang prove $v(k)\ge\exp(ck^2)$ for the least missing denominator (Math. Proc. Cambridge Philos. Soc.).
• 2026 — An OpenAI preprint, Short Egyptian fractions (OpenAI Math Release, September 25, 2026), claims $N(b)\asymp\log\log b$, settling Erdős's conjecture, together with $\log\log F(k)\asymp k$ and $\log\log v(k)\asymp k$. It has not been peer reviewed, and its proofs are not formally verified.

Setting

For integers $1\le a<b$, an expansion of $a/b$ is a finite list $2\le n_1<\dots<n_k$ of integers with

$$\frac ab=\frac1{n_1}+\dots+\frac1{n_k}.$$

The fraction need not be in lowest terms and the denominators are unbounded. $N(a,b)$ is the least such $k$, and

$$N(b)=\max_{1\le a<b}N(a,b).$$

For $k\ge1$, $F(k)$ is the number of tuples $1\le n_1<\dots<n_k$ with $\sum 1/n_i=1$; $D_k$ is the set of integers $m\ge2$ occurring as some $n_i$ in such a tuple; and $v(k)=\min(\{2,3,\dots\}\setminus D_k)$.

Formalization targets

Goal: the optimal order of the shortest expansions (Theorem 1.1)

Every $a/b$ with $1\le a<b$ has an expansion, and there are absolute constants $c_1,c_2>0$ and $b_0$ such that for every $b\ge b_0$

$$c_1\log\log b\;\le\;N(b)\;\le\;c_2\log\log b .$$

No values of the constants are fixed. The goal statement is published on the platform with status Open.

Milestones

• Theorem 1.1, second formulation, stated with the definitions shared by the corollaries below.
• Corollary 1.2: there are $c,C>0$ and $k_0$ with $ck\le\log\log F(k)\le Ck$ for every $k\ge k_0$.
• Lemma 7.2: for $r\ge3$, any exact $r$-term expansion of $1$ containing the denominator $m$ can be lengthened to an exact $(r+1)$-term expansion still containing $m$; hence $D_r\subseteq D_{r+1}$.
• Proposition 8.1: for every $\varepsilon>0$, every sufficiently large $m$ is a denominator in an expansion of $1$ with at most $(257/\log2+\varepsilon)\log\log m$ terms.
• Corollary 1.3: eventually $\exp(\exp(k/600))\le v(k)\le1+k^{2^{k-1}}$, and $\log2/257\le\liminf_k \log\log v(k)/k\le\limsup_k\log\log v(k)/k\le\log2$.

Significance

The result itself. Theorem 1.1 answers Erdős's 1950 conjecture (Erdős Problem 304) affirmatively. The lower bound is classical; the content is the uniform upper bound for every numerator. As consequences, the paper determines the double-logarithmic order of the number of representations of $1$ (Corollary 1.2) and of the least integer absent from all $k$-term expansions of $1$ (Corollary 1.3), improving van Doorn–Tang's $\exp(ck^2)$ lower bound to a double exponential.

Formalizing it. All statements are elementary, with no analytic objects beyond logarithms, so a formal proof would give a complete machine-checked account of a problem from Erdős's list. The proof uses residue distribution of divisors, uniform divisor moments and a probabilistic construction, none of which is machine-checked. The elementary pieces — finiteness of $F(k)$, the denominator bound $n_i\le k^{2^{i-1}}$, and the padding lemma — are independently checkable and useful for other unit-fraction problems.

Difficulty

The greedy algorithm and divisor methods (Erdős; Tenenbaum–Yokota) lose a factor $\log b/(\log\log b)^2$ because they treat each numerator individually. The proof instead builds an auxiliary denominator $M$ for which almost every numerator in a large range has a short expansion, and descends through $O(\log\log b)$ ranges. The obstacle is that the exceptional numerators at each level could accumulate during the descent; controlling them requires a uniform moment bound for small divisors in shifted intervals. For Corollary 1.3, an additional difficulty is that the exact term $1/m$ must survive every operation that lengthens the expansion.

Formalization scope

• The goal uses OAI.ShortEgyptian: expansions are List ℕ that are strictly increasing (Pairwise (· < ·)), with entries $\ge2$ and rational sum $a/b$; minLength a b is an sInf and maxMinLength b the maximum over $1\le a<b$. The existence conjunct guarantees that sInf is taken over a nonempty set, so the bounds cannot hold through a junk value.
• The Problem337 milestones use Fin k → ℕ tuples (StrictMono, entries $\ge2$ for $a/b$ and $\ge1$ for expansions of $1$); $F(k)$ is Set.ncard, and $v(k)$ is sInf of the missing denominators. Finiteness of $D_k$ and of the expansion sets, which make these values meaningful, are separate statements in the proposal. In Corollary 1.3 the slopes are real liminf/limsup, accompanied by the explicit eventual bounds.
• Logarithms are Real.log; all constants are existential, apart from the explicit $600$, $257/\log 2$ and $\log2$ of the source.
• Needed infrastructure: divisor-counting and residue-distribution estimates, elementary prime-number bounds (the counting corollary uses the prime number theorem), and finite probabilistic constructions. Contributions proving the elementary pieces are welcome.

Selected references

• M. Nakayama, On the decomposition of a rational number into "Stammbrüche", Tohoku Math. J. 46 (1940). https://www.jstage.jst.go.jp/article/tmj1911/46/0/46_0_1/_article/-char/en
• P. Erdős, Az $1/x_1+1/x_2+\dots+1/x_n=a/b$ egyenlet egész számú megoldásairól, Mat. Lapok (1950). https://users.renyi.hu/~p_erdos/1950-02.pdf
• P. Erdős and R. L. Graham, Old and New Problems and Results in Combinatorial Number Theory, 1980. https://mathweb.ucsd.edu/~ronspubs/80_11_number_theory.pdf
• T. F. Bloom, Erdős Problem 304. https://www.erdosproblems.com/304
• M. D. Vose, Egyptian fractions, Bull. London Math. Soc. 17 (1985). https://doi.org/10.1112/blms/17.1.21
• G. Tenenbaum and H. Yokota, Length and denominators of Egyptian fractions, III, J. Number Theory (1990). https://doi.org/10.1016/0022-314X(90)90109-5
• S. V. Konyagin, Double exponential lower bound for the number of representations of unity by Egyptian fractions, Mat. Zametki (2014). https://doi.org/10.4213/mzm10417
• C. Elsholtz and S. Planitzer, Sums of four and more unit fractions and approximate parametrizations, Bull. London Math. Soc. (2021). https://doi.org/10.1112/blms.12452
• W. van Doorn and Q. Tang, The smallest denominator not contained in a unit fraction decomposition of 1 with fixed length, Math. Proc. Cambridge Philos. Soc. (2026). https://doi.org/10.1017/S0305004126102102
• OpenAI, Short Egyptian fractions, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 2; Corollaries 1.2–1.3, p. 3; Lemma 7.2, p. 26; Proposition 8.1, p. 27). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Short-Egyptian-fractions-September-25-2026/Short-Egyptian-fractions-September-25-2026.pdf

Motivation

In the local model of differential privacy, each individual randomizes their own data before handing it to an untrusted learner. Local protocols are the deployed form of private data collection, and in practice every round of interaction with the population is expensive: the learner must broadcast new instructions and wait for new reports. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith, What Can We Learn Privately? (arXiv:0803.0924v3, published in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are those of arXiv v3) show that local learning is equivalent to learning with statistical queries (SQ) in the sense of Kearns (1998), and that the equivalence maps noninteractive local learners to nonadaptive SQ learners. The question whether interaction is ever necessary in the local model therefore becomes the question whether adaptivity is ever necessary for SQ learning.

This mission formalizes the paper's answer (§5.3, Theorem 5.16): a concept class, MASKED-PARITY, that an adaptive SQ learner learns exactly with $d+1$ queries in two rounds, while every nonadaptive SQ learner with fewer than exponentially many queries fails against a specific valid oracle, under the uniform distribution on examples.

Setting

Fix $d$, a power of two. The domain is $D=\{0,1\}^d\times\{0,1\}^{\log d}\times\{0,1\}$, with points $u=(x,i,b)$, and examples are drawn from the uniform distribution $\mathcal D$ on $D$. For $r\in\{0,1\}^d$ and $a\in\{0,1\}$, the concept $c_{r,a}:D\to\{+1,-1\}$ is

$$c_{r,a}(x,i,b)=\begin{cases}(-1)^{r\odot x+a}&b=0,\\(-1)^{r_i}&b=1,\end{cases}$$

where $r\odot x$ is the inner product modulo 2. MASKED-PARITY is the class $\{c_{r,a}\}$: on the half $b=0$ it is the parity $r$ or its negation, according to the mask $a$; on the half $b=1$ it reveals the bit $r_i$.

A statistical query is a function $g(u,y)$ of an example and a label together with a tolerance $\tau$. The SQ oracle for the target $c$ answers with any real $v$ such that $|v-\mathbb E_{u\sim\mathcal D}[g(u,c(u))]|\le\tau$; the learner must succeed for every such answer. An SQ learner is nonadaptive if it fixes all its queries before receiving any answer, and adaptive otherwise. Write $\langle f,h\rangle=\mathbb E_{u\sim\mathcal D}[f(u)h(u)]$ and $\mathrm{err}(f,h)=\Pr_{u\sim\mathcal D}[f(u)\ne h(u)]$.

The lower bound uses the decomposition of a query into $f_g(u)=\frac{g(u,1)-g(u,-1)}2$ and $C_g=\frac12\mathbb E[g(u,1)+g(u,-1)]$, the restrictions $c^s_{r,a}$, $f^s_g$ of $c_{r,a}$ and $f_g$ to the half $b=s$ (equation (6)), and the oracle

$$\mathcal O_{c_{r,a},\mathcal D}(g,\tau)=\begin{cases}C_g+\langle f^1_g,c^1_{r,a}\rangle&\text{if }|\langle f^0_g,c^0_{r,a}\rangle|<\tau,\\ \mathbb E[g(u,c_{r,a}(u))]&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 5.16 (p. 27)

1. There is a two-round SQ learner ($d$ queries, then one), with $\{0,1\}$-valued queries of tolerance at least $\frac1{4d+1}$, that outputs $c_{r,a}$ for every target and every valid answers.
2. $\mathcal O$ is a valid SQ oracle, and every nonadaptive learner making $t$ queries with values $\pm1$ and tolerance at least $2^{-d/3}$, run against $\mathcal O$ on a uniformly random target, satisfies

$$\Pr_{c_{\bar r,\bar a}}\Bigl[\mathrm{err}(c_{\bar r,\bar a},h)\ge\tfrac14\Bigr]\ge\frac12-\frac t{2^{d/3+2}}.$$

Milestones

• Proposition 5.18 (p. 28): the learner $\mathcal A_{\mathrm{MP}}$ recovers $\hat r=r$ and $\hat a=a$ from every valid answers.
• Equation (7) (p. 29): $\mathbb E[g(u,c_{r,a}(u))]=C_g+\langle f^0_g,c^0_{r,a}\rangle+\langle f^1_g,c^1_{r,a}\rangle$.
• The oracle (p. 30): $\mathcal O$ is valid and answers identically on $c_{r,0}$ and $c_{r,1}$ when $|\langle f^0_g,c^0_{r,0}\rangle|<\tau$.
• Orthogonality (p. 30): $\langle c^0_{r,a},c^0_{r',a}\rangle$ is $1/2$ if $r=r'$ and $0$ otherwise.
• Bessel bound (p. 30): $\sum_{(r,a)}2\langle f^0_g,c^0_{r,a}\rangle^2\le1$ for $\pm1$-valued $g$.
• Counting (p. 30): at most $2^{2d/3-1}$ pairs $(r,a)$ have $|\langle f^0_g,c^0_{r,a}\rangle|\ge2^{-d/3}$.
• $\Pr[\mathit{Good}]\ge1-t/2^{d/3+2}$ (p. 30).

Significance

The result. Combined with the paper's equivalence between local and SQ learning (Theorem 5.14), Theorem 5.16 shows that interaction is sometimes necessary in local differential privacy: there is a class learnable by an interactive local protocol with polynomially many examples, but not by any noninteractive one with fewer than exponentially many (Corollary 5.17). The separation concerns strong learning under a fixed distribution; the paper notes that adaptive and nonadaptive SQ learning coincide for weak learning, and that a distribution-free separation was left open.

Formalizing it. The result is proved in the paper and has, to our knowledge, no machine-checked proof. The mission produces a self-contained Lean model of statistical query learning with labelled queries and adversarial oracles, a finite Fourier calculus for parities on $\{0,1\}^d$ (orthogonality and a Bessel inequality for $\pm1$-valued functions), and the counting and union-bound argument of SQ lower bounds. The proof of part (2) contains several printed slips (listed below); a formal proof settles the corrected argument.

Difficulty

The upper bound is a direct computation. The difficulty is in part (2): the learner's hypothesis may be any function, not a concept of the class, and the lower bound must hold for every nonadaptive strategy at once. A naive argument that each query "reveals little about $a$" fails, because the true answer to a query does depend on $a$; the argument needs an oracle that is valid (within tolerance of the truth) and yet independent of $a$ on most targets, and a quantitative bound on how many targets any single $\pm1$-valued query can correlate with on the half $b=0$. That bound is an $L^2$ statement over all $2^{d+1}$ concepts, not a pointwise one.

Formalization scope

• Domain and distribution. The index $i\in\{0,1\}^{\log d}$ is encoded as Fin d, and every theorem assumes $d=2^m$ (implicit in the paper). Vectors are Fin d → ZMod 2, with 0-based bits. Expectations are averages over the finite domain; probabilities over the target are counts of pairs $(r,a)$ divided by $2^{d+1}$.
• Values. Concepts, hypotheses and queries are real-valued; labels $\pm1$ are reals. Queries in part (1) take values in $\{0,1\}$, as $\mathcal A_{\mathrm{MP}}$'s do; queries in part (2) take values $\pm1$ on labels $\pm1$, as in the paper's proof. The paper allows non-Boolean queries (p. 19); a version of part (2) for real queries with values in $[-1,1]$ is a true strengthening that the same argument supports, and is not stated.
• Oracles. An SQ oracle is adversarial within the tolerance: the upper bound holds for every valid answer. Part (2) exhibits the paper's oracle $\mathcal O$ and asserts its validity for every $\tau>0$. Without that conjunct an "oracle" that ignores the tolerance would make part (2) trivial; the statement rules this out.
• Learners. Learners are deterministic structures (a nonadaptive learner is a list of queries and tolerances plus an output map; a two-round learner's second-round queries are functions of the first-round answers). A randomized learner is a mixture over its coins and the bounds hold coin by coin. "Efficient" is not modelled. The informal "with a polynomial number of queries" is formalized through its quantitative "Specifically" sentence.
• Real powers. $2^{d/3}$, $2^{2d/3-1}$ and $2^{d/3+2}$ are real powers; no natural-number division is used.
• Corrections of the proof (not of the theorem). The event $\mathit{Good}$ on p. 30 is printed with $c_{\bar r,\bar a}$ and $\le$; the milestone uses $c^0_{\bar r,\bar a}$ and the strict $<$, which is what the counting display and the oracle's test require. The quotient $2^{2d/3-1}/2^{d+1}$ is printed as $2^{-d/3}$ and equals $2^{-d/3-2}$; "$c^0_{r,0}=-c^0_{r,0}$" should read $c^0_{r,1}=-c^0_{r,0}$. The final display of the proof gives $\frac12(1-t/2^{d/3+2})$, which is at least the theorem's bound.

Contributions welcome: the Fourier facts for $\{0,1\}^d$ (reusable for any parity-based SQ lower bound), the general decomposition (7), and the probability bound of part (2) from the milestones.

Selected references

• S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826. arXiv:0803.0924v3, DOI 10.1137/090756090.
• M. Kearns, Efficient noise-tolerant learning from statistical queries, J. ACM 45(6) (1998) 983–1006. DOI 10.1145/293347.293351.
• A. Blum, M. Furst, J. Jackson, M. Kearns, Y. Mansour, S. Rudich, Weakly learning DNF and characterizing statistical query learning using Fourier analysis, STOC 1994. DOI 10.1145/195058.195147.
• N. Bshouty, V. Feldman, On using extended statistical queries to avoid membership queries, J. Mach. Learn. Res. 2 (2002) 359–395. JMLR.

Motivation

A finite strategic game can be changed in ways that no player can detect strategically. Adding to player $m$'s utility any function that does not depend on player $m$'s own strategy leaves every unilateral comparison "is strategy $a$ better for me than strategy $b$, given what the others do?" unchanged, so it leaves every best response and every pure Nash equilibrium unchanged. Such changes are not irrelevant, however: they move the payoff levels, and therefore change which outcomes are efficient.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Math. Oper. Res. 36(3), 2011, DOI 10.1287/moor.1110.0500) make this precise. They decompose every finite game uniquely into a potential component, a harmonic component and a nonstrategic component (their Theorem 4.1). The first two determine all pairwise comparisons; the third determines nothing about equilibria. Section 5.3 of the paper asks what the third component can do to efficiency, and answers with Theorem 5.9: by changing only the nonstrategic component, the pure Nash equilibria of a game can be made to coincide exactly with its Pareto optimal profiles. This mission formalizes that result.

The question matters wherever a designer can transfer payoffs without altering incentives (for instance side payments to a player that depend only on the other players' actions): the theorem says such transfers can always align equilibrium with efficiency, provided an equilibrium exists.

Setting

There is a finite set $\mathcal M$ of players. Player $m$ has a finite nonempty set $E^m$ of strategies; a strategy profile is $p = (p^m)_{m\in\mathcal M} \in E = \prod_m E^m$, and $(q^m, p^{-m})$ denotes $p$ with player $m$'s strategy replaced by $q^m$. A game is a family of utilities $u = (u^m)_m$, $u^m : E \to \mathbb R$.

Two profiles are $m$-comparable if they differ, and differ only in player $m$'s strategy. The game graph has node set $E$ and an edge between every pair of profiles that are $m$-comparable for some $m$. On this graph:

• $C_0$ is the space of functions $E \to \mathbb R$ with $\langle \varphi, \psi\rangle_0 = \sum_p \varphi(p)\psi(p)$;
• $C_1$ is the space of edge flows $X$ ($X(p,q) = -X(q,p)$ on edges, $0$ off edges) with $\langle X, Y\rangle_1 = \tfrac12\sum_{(p,q)} X(p,q)Y(p,q)$, summed over ordered adjacent pairs;
• $\delta_0 : C_0 \to C_1$, $(\delta_0\varphi)(p,q) = \varphi(q) - \varphi(p)$ on edges, is the combinatorial gradient;
• $D_m : C_0 \to C_1$ is the same difference restricted to $m$-comparable pairs, and $D u = \sum_m D_m u^m$. For $m$-comparable $p,q$, $(Du)(p,q) = u^m(q) - u^m(p)$: $D$ records the game's pairwise comparisons.

Games form the space $C_0^M$ with the inner product $\sum_m\langle u^m, v^m\rangle_0$. With $\dagger$ the Moore–Penrose pseudoinverse for these inner products, the potential and harmonic components of a game are

$$u_{\mathcal P} = D^\dagger\delta_0\delta_0^\dagger D u, \qquad u_{\mathcal H} = D^\dagger(I - \delta_0\delta_0^\dagger) D u ,$$

and the nonstrategic component is what remains. A profile $p$ is a pure Nash equilibrium of $u$ if $u^m(q^m, p^{-m}) \le u^m(p)$ for all $m$ and $q^m$, and it is Pareto optimal (Definition 5.3) if no profile $q$ has $u^m(q) \ge u^m(p)$ for all $m$ and $u^k(q) > u^k(p)$ for some $k$.

Formalization targets

Goal: Theorem 5.9

For every game $u$ that has a pure Nash equilibrium there is a game $\bar u$ with

$$\bar u_{\mathcal P} = u_{\mathcal P},\qquad \bar u_{\mathcal H} = u_{\mathcal H},\qquad \{p : p \text{ pure NE of } \bar u\} = \{p : p \text{ Pareto optimal in } \bar u\}.$$

The statement is existential and fixes nothing about $\bar u$ beyond its potential and harmonic components; it asserts the full equality of the two sets, not one inclusion.

Milestones

1. §5.3, p. 32. Games with the same potential and harmonic components have the same pure Nash equilibria.
2. Lemma 5.4. For every game $u$ there is a game $\hat u$ with $\hat u_{\mathcal P} = u_{\mathcal P}$, $\hat u_{\mathcal H} = u_{\mathcal H}$, and $\hat u^m(p) = 0$ for every player $m$ at every pure Nash equilibrium $p$ of $u$.

Significance

The result. The nonstrategic component has no influence on the pairwise comparisons, and hence on equilibria, yet Theorem 5.9 shows that it controls efficiency completely: whenever a pure equilibrium exists, some choice of it makes every equilibrium Pareto optimal and every Pareto optimal profile an equilibrium. Read the other way, two games that are strategically indistinguishable can have opposite efficiency properties, so any efficiency statement about a class of games (a price-of-anarchy bound, for instance) must depend on more than the strategic structure. The paper also uses Lemma 5.4 as a normalisation: the payoff levels at equilibria are a free parameter of the nonstrategic component.

Formalizing it. The theorem has a short proof on paper, but the proof works with the pairwise comparisons, whereas the statement is about the components $u_{\mathcal P}$, $u_{\mathcal H}$ defined through pseudoinverses. Connecting the two requires the identities of the decomposition: that $u_{\mathcal P} + u_{\mathcal H} = D^\dagger D u$ and that $D D^\dagger D = D$. The mission therefore produces a machine-checked link between the linear-algebraic decomposition of games and their equilibrium sets, which other results of the paper (and of the literature on near-potential games) also need. To the best of our knowledge, none of these statements has been formalized before; the result itself is proved in the paper.

Difficulty

The construction on pp. 31–33 is explicit, so the difficulty is not finding $\bar u$ but keeping two descriptions of "differ only in the nonstrategic component" consistent. The statement uses the component maps; the proof checks pointwise that $u^m(p) - u^m(q) = \bar u^m(p) - \bar u^m(q)$ for $m$-comparable $p, q$. Passing from the second to the first needs the pseudoinverse identities for $D$ and $\delta_0$ with respect to the specific inner products of $C_0^M$ and $C_1$; a naive argument that treats $D^\dagger$ as an inverse fails because $D$ has a large kernel. A second point is the case analysis in the definition of $\bar u$: whether a profile is $m$-comparable to an equilibrium must be shown independent of which of two $m$-comparable profiles is examined, and the case where a non-equilibrium profile is $m$-comparable to an equilibrium for every player $m$ needs the separate argument of p. 33.

Formalization scope

Players form a finite type ι with decidable equality; strategy sets E m are finite, nonempty and have decidable equality. A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)), i.e. $C_0^M$ with the unweighted sum inner product of Section 4; the weighted inner product of Section 6 is not used. $C_1$ carries the inner product with the factor $\tfrac12$. The pseudoinverse is defined directly (Mathlib has none) as the inverse of $L$ on $(\ker L)^\perp$ composed with the orthogonal projection onto the range. Pure Nash equilibrium is AGT.IsPureNash from the published agt_games bundle; Pareto optimality is Definition 5.3, stated for a plain utility function.

Added hypothesis. The paper leaves implicit that $G$ has a pure Nash equilibrium, and the goal carries it as a hypothesis. It is necessary: every finite game has a Pareto optimal profile (a maximizer of $\sum_m u^m$), while a game without pure equilibria, such as matching pennies, has none in any game with the same potential and harmonic components, so the set equality would fail. The paper's proof uses an equilibrium in the step "deviation to a NE increases the payoff of at least one player". Lemma 5.4 needs no such hypothesis.

"Same potential and harmonic components" is stated as equality of the two component maps of Theorem 4.1, never as membership of $u - \bar u$ in $\ker D$; the two are equivalent only through the decomposition theorem. Without condition (i) the goal would be trivial (take $\bar u$ constant, so that every profile is both an equilibrium and Pareto optimal), so condition (i) is what makes the statement nontrivial.

Needed infrastructure: the Penrose identities for the pseudoinverse; $D D^\dagger D = D$; the fact that $Du$ determines each $D_m u^m$ (the $m$-comparable edge sets for different $m$ are disjoint); and the explicit constructions of $\hat u$ and $\bar u$. The pseudoinverse lemmas and the "same comparisons, same equilibria" bridge are reusable throughout the series. Proofs of the milestones, of the bridge in either direction, and of the Penrose identities are welcome as separate contributions.

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010. https://arxiv.org/abs/1005.2405 — journal version: Mathematics of Operations Research 36(3):474–503, 2011. https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
• R. Penrose, A generalized inverse for matrices, Mathematical Proceedings of the Cambridge Philosophical Society 51(3):406–413, 1955. https://doi.org/10.1017/S0305004100030401

Motivation

Robust dynamic programming replaces the single transition law of a Markov decision process by a set of laws, and values a policy by its worst-case expected reward over that set. Iyengar (Robust dynamic programming, CORC Tech Report TR-2002-07, 2004; Math. Oper. Res. 30(2), 2005) and Nilim and El Ghaoui (Robust control of Markov decision processes with uncertain transition matrices, Oper. Res. 53(5), 2005) showed that under a rectangularity assumption the robust value satisfies a robust Bellman equation. Each step of that equation solves, for every state–action pair, an inner problem

$$\inf_{p\in\mathcal P}\ \mathbf E^p[v],$$

the worst-case expectation of a value vector $v$ over the ambiguity set $\mathcal P$. Robust value iteration is only as practical as this inner problem is cheap.

The ambiguity sets of interest come from statistics: when transition probabilities are estimated from data, natural sets are confidence regions around the empirical distribution. Section 4 of Iyengar's report studies three such families: relative-entropy balls (Lemma 4), a χ² approximation of them (Lemma 5), and an $L_1$ outer approximation (Lemma 6). This mission formalizes the χ² case. The relative-entropy case is already posed on the platform as RobustMDP.EntropyInner.kl_ball_inner_problem_dual (Nilim–El Ghaoui series), up to the sign change $v\to -v$.

Setting

Let $\mathcal S$ be a finite set of states and let $\mathcal M(\mathcal S)=\{p:\mathcal S\to\mathbb R:\ p\ge 0,\ \sum_s p(s)=1\}$ be the probability measures on $\mathcal S$. For $p\in\mathcal M(\mathcal S)$ and $x:\mathcal S\to\mathbb R$ write

$$\mathbf E^p[x]=\sum_{s}p(s)x(s),\qquad \mathbf{Var}^q[x]=\sum_s q(s)\big(x(s)-\mathbf E^q[x]\big)^2 .$$

Fix a centre $q\in\mathcal M(\mathcal S)$ with $q(s)>0$ for every $s$ (in the paper $q$ is the empirical next-state distribution of one state–action pair) and a radius $t\ge 0$. The χ² set (46) is

$$\mathcal P=\Big\{p\in\mathcal M(\mathcal S):\ \sum_{s\in\mathcal S}\frac{(p(s)-q(s))^2}{q(s)}\le t\Big\}.$$

Since $\log(1+x)\le x$, the relative entropy $D(p\|q)=\sum_s p(s)\log(p(s)/q(s))$ is at most the χ² distance, so $\mathcal P$ lies inside the relative-entropy ball of radius $t$: it is a conservative approximation of it. The Lean development names these objects expect, variance, chiSqDist, chiSqSet, relEntropy and the dual objective dualObj q t v μ $=\mathbf E^q[v-\mu]-\sqrt{t\,\mathbf{Var}^q[v-\mu]}$, all in the namespace RobustDP.ChiSquare.

Formalization targets

Goal: Lemma 5 (p. 18)

For every value vector $v:\mathcal S\to\mathbb R$,

$$\min_{p\in\mathcal P}\ \mathbf E^p[v]\;=\;\max_{\mu\ge 0}\Big\{\mathbf E^q[v-\mu]-\sqrt{t\,\mathbf{Var}^q[v-\mu]}\Big\},$$

where $\mu$ ranges over vectors $\mu:\mathcal S\to\mathbb R$ with $\mu\ge 0$ componentwise. Both extrema are attained. The lemma's complexity claim, $\mathcal O(|\mathcal S|\log|\mathcal S|)$ for (48), is a statement about an algorithm and is not part of the mission.

Milestones (the steps of the paper's proof)

1. (49) With $y=p-q$, the value of the primal problem is $\mathbf E^q[v]$ plus the minimum of $\sum_s y(s)v(s)$ over $\sum_s y(s)^2/q(s)\le t$, $\sum_s y(s)=0$, $y\ge -q$.
2. (50) For fixed multipliers $\mu$ and $\gamma\in\mathbb R$, the minimum of the Lagrangian over the ellipsoid $\{y:\sum_s y(s)^2/q(s)\le t\}$ is $\mathbf E^q[v-\mu]-\sqrt{t\sum_s q(s)(v(s)-\mu(s)-\gamma)^2}$, attained at an explicit $y^*$.
3. (51) Maximizing over $\gamma$ replaces the sum of squares by $\mathbf{Var}^q[v-\mu]$, attained at $\gamma=\mathbf E^q[v-\mu]$.
4. (52)–(53) Some optimal multiplier has the form $\mu^*(s)=(v(s)-\alpha)^+$ with $\alpha\ge\min_s v(s)$, so the dual is a one-dimensional problem.

Two further results stand on the same definitions: the inequality $D(p\|q)\le\sum_s(p(s)-q(s))^2/q(s)$ of Section 4.2, and the $L_1$ analogue of Lemma 5 established in the proof of Lemma 6 (p. 20):

$$\min_{\substack{p\in\mathcal M(\mathcal S)\\ \|p-q\|_1\le c}}\mathbf E^p[v]=\max_{\mu\ge0}\Big\{\mathbf E^q[v-\mu]-\tfrac12 c\big(\max_s(v-\mu)(s)-\min_s(v-\mu)(s)\big)\Big\},\qquad c=\sqrt{2\ln(2)\,t}.$$

Significance

The result. Lemma 5 reduces a worst-case expectation over a curved convex set of probability vectors to a concave problem in one scalar, which the paper solves by sorting. This makes robust value iteration with χ² ambiguity sets about as expensive as nominal value iteration, up to a logarithmic factor. The identity also explains the shape of the answer: a mean minus a standard-deviation penalty, applied to a value vector truncated from above at the level $\alpha$. The truncation comes from the constraint $p\ge 0$.

Formalizing it. The result is proved in the paper; no machine-checked proof is known. A complete formalization gives a verified finite-dimensional duality theorem for a quadratic constraint combined with polyhedral constraints, which is the computational core of χ²-ambiguity robust MDPs and of χ²-divergence distributionally robust optimization in general. Lemma 6's printed formula (57) is false (see below); the mission poses the corrected identity that the paper's proof establishes.

Difficulty

The obvious argument drops the constraint $p\ge 0$. Without it, the minimum of the linear function $\mathbf E^p[v]$ over the ellipsoid $\{\sum_s p(s)=1,\ \chi^2(p,q)\le t\}$ follows from Cauchy–Schwarz and equals $\mathbf E^q[v]-\sqrt{t\,\mathbf{Var}^q[v]}$. The page notes (p. 19) that earlier work solved only this relaxed problem. With $p\ge 0$ the minimizer of the relaxation can leave the simplex, so the problem has an ellipsoidal constraint, a polyhedral constraint and an equality at once. The multiplier $\mu$ of $p\ge 0$ is what Lemma 5 has to handle. Equality of the primal minimum with the dual supremum needs a duality theorem that is not in Mathlib in this form. Attainment of the dual maximum over the unbounded cone $\mu\ge 0$ needs an additional argument, namely that an optimal multiplier has the truncation form (53).

Formalization scope

• $\mathcal S$ is a Fintype; vectors are functions S → ℝ; $\mathcal M(\mathcal S)$ is Mathlib's stdSimplex ℝ S. Nonemptiness of $\mathcal S$ follows from $\sum_s q(s)=1$. Finiteness is the standing restriction of Section 4 (p. 15).
• $q(s)>0$ for every $s$ is a hypothesis of every χ² statement. The page divides by $q(s)$; in Lean $x/0=0$ would silently drop a coordinate from the constraint.
• $t\ge 0$ is assumed. The page puts no sign condition on $t$. At $t=0$ the set is $\{q\}$ and both sides equal $\mathbf E^q[v]$.
• Minimum and maximum are IsLeast and IsGreatest of image sets, so the goal asserts attainment on both sides, as the page's "minimize" and "max" do.
• $\mu\ge 0$ is a vector inequality (0 ≤ μ). The multiplier $\gamma$ of the equality $\sum_s y(s)=0$ ranges over $\mathbb R$. The page's "$\gamma\ge 0$" in (50) is a misprint: the proof of Lemma 6 writes $\gamma\in\mathbb R$, and the optimal $\gamma=\mathbf E^q[v-\mu]$ may be negative.
• The relative entropy uses the natural logarithm, as in (35), with $0\log 0=0$.
• Lemma 6 is posed only as established in its proof. The printed (57) is false: taking $\mu=v-\min_s v(s)$ makes the bracket vanish, so (57) always equals $\mathbf E^q[v]$. For $q=(\frac12,\frac12)$, $v=(0,1)$ and $c=\frac12$ the true minimum is $\frac14$. The set (55) is also restricted to $p\in\mathcal M(\mathcal S)$, which its proof uses.
• Ruled out: a formalization of Lemma 5 whose feasible set omits $p\ge 0$ (or that takes $\mu=0$) states the easier relaxed identity above and is not this mission's goal. Likewise a χ² set whose centre may vanish, or a dual written as ⨆ over an unbounded set, would make the statement junk.
• All complexity claims (Lemmas 5 and 6, the sorting argument, (54)) are excluded. So are the Pinsker step of Section 4.3, whose constant $1/(2\ln 2)$ is wrong for the natural logarithm, and the asymptotic confidence statements (33)–(39).
• Reusable infrastructure: Lagrangian duality for a linear objective over an ellipsoid intersected with a polyhedron, and Cauchy–Schwarz minimization of a linear function over a weighted ellipsoid. Proofs of the milestones, alternative proofs of the goal, and a formalization of the paper's sorting algorithm on top of (52)–(53) are welcome.

Selected references

• G. Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07, IEOR Department, Columbia University, revised May 4, 2004; published in Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• J. K. Satia and R. E. Lave, Markovian decision processes with uncertain transition probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• T. M. Cover and J. A. Thomas, Elements of Information Theory, Wiley, 1991. https://doi.org/10.1002/0471200611