All missions

Motivation

Shannon's entropy power inequality bounds the entropy of a sum of independent random vectors below by the entropies of the summands; it is a basic tool for classical Gaussian channel capacities. In optical communication, addition is replaced by passive mixing of bosonic modes at a beam splitter. Guha, Erkmen and Shapiro conjectured the sharp bosonic analogue, the entropy photon-number inequality (EPnI), stated in terms of the photon number of the thermal state with the same entropy (ITA 2008). If true, it settles the minimum output entropy of thermal attenuators at fixed input entropy and the capacity regions of bosonic broadcast and wiretap channels, which had been reduced to this inequality (PRA 2007).

This mission asks for a formal proof of the EPnI for finite-energy inputs in any finite number of modes, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1948–1965 — Shannon introduces entropy power; Stam (1959) and Blachman (IEEE IT 1965) prove the entropy power inequality.
• 2004 — Capacity of the pure-loss bosonic channel (PRL 2004) and the minimum-output-entropy conjecture (PRA 2004).
• 2007–2008 — Guha, Shapiro and Erkmen relate broadcast capacity to a minimum-output-entropy conjecture; Guha, Erkmen and Shapiro state the EPnI.
• 2011 — Special cases (one-mode number-diagonal inputs) by Das, Sharma and Muthukrishnan (arXiv:1107.2365).
• 2014 — König and Smith prove a quantum entropy power inequality, including $S(\rho_C)\ge\eta S(\rho_A)+(1-\eta)S(\rho_B)$ (IEEE IT 2014); De Palma, Mari and Giovannetti prove the exponential form $e^{S(\rho_C)/n}\ge\eta e^{S(\rho_A)/n}+(1-\eta)e^{S(\rho_B)/n}$ (Nat. Photonics 2014).
• 2015 — Giovannetti, Holevo and García-Patrón solve the Gaussian optimizer conjecture for unconstrained minimum output entropy (CMP 2015).
• 2016–2018 — De Palma, Trevisan and Giovannetti settle one-mode constrained problems (IEEE IT 2017; PRL 2017); De Palma and Trevisan give a rigorous finite-energy conditional EPI (CMP 2018).
• September 2026 — The OpenAI preprint claims the two-input EPnI for all finite-energy inputs (Theorem 1.1, p. 2).

Setting

An $n$-mode bosonic system has Fock space $\ell^2(\mathbb N^n)$ with number basis $|k\rangle$, $k\in\mathbb N^n$. A state is a positive trace-one operator $\rho$; it has finite energy if $\operatorname{Tr}\rho\sum_ja_j^\dagger a_j=\sum_k(k_1+\dots+k_n)\langle k|\rho|k\rangle<\infty$. The von Neumann entropy is $S(\rho)=-\operatorname{Tr}\rho\log\rho$ (natural log). The thermal entropy per mode is

$$g(t)=(t+1)\log(t+1)-t\log t,\qquad t\ge0,$$

increasing from $0$ to $\infty$, and the entropy photon number of $\rho$ is $N(\rho)=g^{-1}(S(\rho)/n)$, the mean photon number per mode of the product thermal state with the same entropy. For independent inputs $\rho_A,\rho_B$ and transmissivity $0\le\eta\le1$, the beam-splitter output $\rho_C$ is the reduced state of the modes $c_j=\sqrt\eta\,a_j+\sqrt{1-\eta}\,b_j$ after passive mixing of $\rho_A\otimes\rho_B$. No independence among the modes within either input is assumed.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every finite $n\ge1$, every pair of finite-energy $n$-mode states $\rho_A,\rho_B$ and every $0\le\eta\le1$,

$$g^{-1}\!\Bigl(\frac{S(\rho_C)}n\Bigr)\ \ge\ \eta\,g^{-1}\!\Bigl(\frac{S(\rho_A)}n\Bigr)+(1-\eta)\,g^{-1}\!\Bigl(\frac{S(\rho_B)}n\Bigr).$$

Thermal inputs with a common mean photon number within each port give equality.

Significance

The result itself. The EPnI is sharper than the exponential quantum entropy power inequality when the two input entropies differ, which is exactly the regime needed for constrained minimum output entropy. The preprint derives the exact minimum output entropy at fixed input entropy for every tensor power of an identical thermal attenuator, with inputs entangled across modes (Corollary 1.2, p. 2), and the exact capacity region of the degraded two-receiver pure-loss broadcast channel (Corollary 7.1, p. 26), completing the converse of Guha, Shapiro and Erkmen.

Formalizing it. The statement involves infinite-dimensional Fock space, trace-class positive operators, continuous functional calculus for the entropy, and the partial trace after a passive unitary. The Lean development builds these concretely in the number basis. A formal proof would give machine-checked infrastructure for quantum entropy on infinite-dimensional spaces, which Mathlib currently lacks. No machine-checked version of any quantum entropy power inequality is known.

Difficulty

Heat-flow (quantum Fisher information) proofs give the linear and exponential bounds, but these are attained only for equal entropies and do not recover the thermal comparison at unequal entropy levels. The preprint instead minimizes a regularized functional over pairs of inputs and must show that minimizers are thermal. This requires an interpolation theorem for diagonal form comparisons (Theorem 3.1, p. 8), attainment and Gibbs regularity of minimizers in infinite dimensions (Lemma 4.1, Proposition 4.2, pp. 15–16), a component entropy-Hessian estimate, and a stationarity identity whose cancellation forces convergence to thermal inputs (Section 6). Compactness relies on the finite-energy hypothesis; without it entropies can be infinite.

Formalization scope

• Fock n is lp (fun _ : Fin n → ℕ => ℂ) 2. A State is a positive bounded operator whose diagonal in the number basis sums (HasSum) to $1$.
• FiniteEnergy ρ is summability of $\sum_k|k|\,\langle k|\rho|k\rangle$.
• entropy ρ is the sum of diagonal entries of $\mathrm{cfc}(-t\log t)(\rho)$; for finite-energy states it is finite, so the tsum is the true entropy.
• gInv s = sInf {t ≥ 0 | s ≤ g t}, the inverse of $g$ on $[0,\infty)$.
• IsBeamSplitterOutput η ρA ρB ρC requires every number-basis entry of $\rho_C$ to be the (convergent) partial-trace sum of the explicitly given beam-splitter coefficients applied to $\rho_A\otimes\rho_B$; the inputs are arbitrary density matrices, so internal entanglement is allowed.
• The hypotheses are satisfiable (e.g. vacuum or thermal inputs) and the conclusion is the inequality as stated.

Selected references

• OpenAI, The entropy photon-number inequality, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-entropy-photon-number-inequality-September-24-2026/paper.pdf
• S. Guha, B. I. Erkmen, J. H. Shapiro, The entropy photon-number inequality and its consequences, ITA Workshop 2008, 128–130. https://doi.org/10.1109/ITA.2008.4601037
• S. Guha, J. H. Shapiro, B. I. Erkmen, Classical capacity of bosonic broadcast communication and a minimum output entropy conjecture, Phys. Rev. A 76 (2007), 032303. https://doi.org/10.1103/PhysRevA.76.032303
• R. König, G. Smith, The entropy power inequality for quantum systems, IEEE Trans. Inf. Theory 60 (2014), 1536–1548. https://doi.org/10.1109/TIT.2014.2298436
• G. De Palma, A. Mari, V. Giovannetti, A generalization of the entropy power inequality to bosonic quantum systems, Nat. Photonics 8 (2014), 958–964. https://doi.org/10.1038/nphoton.2014.252
• G. De Palma, D. Trevisan, The conditional entropy power inequality for bosonic quantum systems, Comm. Math. Phys. 360 (2018), 639–662. https://doi.org/10.1007/s00220-017-3082-8
• V. Giovannetti, A. S. Holevo, R. García-Patrón, A solution of Gaussian optimizer conjecture for quantum channels, Comm. Math. Phys. 334 (2015), 1553–1571. https://doi.org/10.1007/s00220-014-2150-6
• V. Giovannetti, S. Guha, S. Lloyd, L. Maccone, J. H. Shapiro, H. P. Yuen, Classical capacity of the lossy bosonic channel: the exact solution, Phys. Rev. Lett. 92 (2004), 027902. https://doi.org/10.1103/PhysRevLett.92.027902
• C. E. Shannon, A mathematical theory of communication, Bell Syst. Tech. J. 27 (1948). https://doi.org/10.1002/j.1538-7305.1948.tb00917.x

Motivation

Given a group $A$, adjoin one new generator $t$ and impose one relation $w=1$, where $w$ is a word in $t$ and elements of $A$. Can the result collapse to the trivial group when $A$ is nontrivial? The Kervaire conjecture says no. It arose from Kervaire's 1965 characterization of high-dimensional knot groups, which involves groups normally generated by a single element, and it is one of the best-known problems about equations over groups: when does an equation $w(t)=1$ with coefficients in $A$ have a solution in some group containing $A$?

Timeline

• 1962. Gerstenhaber and Rothaus prove that nonsingular systems of equations over finite groups are solvable in finite overgroups, using unitary groups and degree theory (doi:10.1073/pnas.48.9.1531); this gives the result for residually finite groups.
• 1965. Kervaire characterizes high-dimensional knot groups (doi:10.24033/bsmf.1624); the group-theoretic Kervaire problem is traced to this setting.
• 1983. Howie studies equations of length three over groups (doi:10.1017/S0013091500028108).
• 1993. Klyachko proves unimodular injectivity for torsion-free groups (doi:10.1080/00927879308824692).
• 2005. Klyachko records the reduction showing that universal nontriviality is equivalent to unimodular injectivity (doi:10.1007/s10469-005-0023-y).
• 2008. Pestov records the extension to hyperlinear groups (doi:10.2178/bsl/1231081461).
• 2012. Klyachko and Lurye prove injectivity for arbitrary coefficient groups after imposing $w^m=1$, $m\ge2$ (doi:10.1016/j.jpaa.2011.06.020).
• 2017. Klyachko and Thom develop new topological methods for equations over groups (doi:10.2140/agt.2017.17.331).
• 2024–2026. Kawauchi publishes a proposed resolution via ribbon sphere-links; Chen gives a new proof of the torsion-free case via the complexity of surfaces (arXiv:2302.09811).

The source of this mission, an OpenAI preprint dated September 24, 2026, proves unimodular coefficient injectivity for every group by a route through spectral phase and a fixed-space theorem for unitary matrices.

Setting

Let $A$ be a group, $\langle t\rangle\cong\mathbb Z$, and $H=A*\langle t\rangle$ the free product. Let $p:H\to\mathbb Z$ be the homomorphism that kills $A$ and sends $t$ to $1$; $p(w)$ is the exponent sum of $t$ in $w$. A word $w\in H$ is unimodular if $p(w)=\pm1$. Write $\langle\!\langle w\rangle\!\rangle_H$ for the normal closure of $w$ in $H$. The coefficient map is the composite

$$A\hookrightarrow H\twoheadrightarrow H/\langle\!\langle w\rangle\!\rangle_H.$$

Its injectivity is equivalent to solvability of $w(t)=1$ over $A$: there is an overgroup $B\supseteq A$ and $b\in B$ with $w(b)=1$.

Formalization targets

Goal: Theorem 1.1

$$\forall A,\ \forall w\in A*\langle t\rangle\ \text{with}\ p(w)=\pm1:\qquad A\longrightarrow (A*\langle t\rangle)/\langle\!\langle w\rangle\!\rangle_H\ \text{is injective}.$$

The Lean statement OAI.Kervaire.coefficient_injective is open on the platform.

Significance

Theorem 1.1 immediately gives the Kervaire conjecture (Corollary 1.2): if $A\ne1$ then $(A*\langle t\rangle)/\langle\!\langle w\rangle\!\rangle\ne1$ for every $w$, since for $p(w)=d\ne\pm1$ the quotient maps onto $\mathbb Z/d\mathbb Z$. It proves the unimodular case of the stronger Kervaire–Laudenbach conjecture with no hypothesis on $A$: no torsion-freeness, residual finiteness, hyperlinearity or countability. The paper's companion work extends the method to nonsingular systems of equations (Howie's conjecture).

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The statement is short and entirely algebraic, which makes it an attractive formalization target; Mathlib already provides free products and normal closures.

Difficulty

The classical Gerstenhaber–Rothaus argument solves the equation in a unitary group and needs $A$ to embed in (an ultraproduct of) unitary groups, which is not known for arbitrary groups. Torsion in $A$ blocks the diagrammatic and topological arguments that work in the torsion-free case. A proof for every group therefore needs a representation available for all groups (the left regular representation, with its faithful finite trace) together with an argument that does not rely on finite-dimensional approximation of $A$.

Formalization scope

• The free product is Monoid.Coprod A (Multiplicative ℤ); the exponent sum is Multiplicative.toAdd (Monoid.Coprod.snd w).
• Unimodular w is exponentSum w = 1 ∨ exponentSum w = -1.
• The quotient is by Subgroup.normalClosure {w}, and coefficientMap w is the quotient map composed with Monoid.Coprod.inl.
• No hypothesis is placed on $A$; the group may live in any universe.

A complete development needs the group von Neumann algebra of $A$ (or at least its trace), the spectral phase of unitaries and its subadditivity, a degree computation on a compact manifold of unitaries with fixed $k$-planes, and corner-labelled planar diagrams with Euler-characteristic estimates. Contributions formalizing Corollary 1.2 from Theorem 1.1, Lemma 2.1 (subadditivity of spectral phase) and Lemma 3.1 (fixed-space lemma) are welcome.

Selected references

• OpenAI, The Kervaire theorem for groups, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Kervaire-Theorem-for-Groups-September-24-2026/The-Kervaire-Theorem-for-Groups-September-24-2026.pdf
• M. A. Kervaire, Les nœuds de dimensions supérieures, Bull. Soc. Math. France, 1965. https://doi.org/10.24033/bsmf.1624
• M. Gerstenhaber, O. S. Rothaus, The solution of sets of equations in groups, Proc. Natl. Acad. Sci. USA, 1962. https://doi.org/10.1073/pnas.48.9.1531
• A. A. Klyachko, A funny property of sphere and equations over groups, Comm. Algebra, 1993. https://doi.org/10.1080/00927879308824692
• A. A. Klyachko, The Kervaire–Laudenbach conjecture and presentations of simple groups, Algebra and Logic, 2005. https://doi.org/10.1007/s10469-005-0023-y
• A. A. Klyachko, D. E. Lurye, Relative hyperbolicity and similar properties of one-generator one-relator relative presentations with powered unimodular relator, J. Pure Appl. Algebra, 2012. https://doi.org/10.1016/j.jpaa.2011.06.020
• V. G. Pestov, Hyperlinear and sofic groups: a brief guide, Bull. Symb. Log., 2008. https://doi.org/10.2178/bsl/1231081461
• A. Klyachko, A. Thom, New topological methods to solve equations over groups, Algebr. Geom. Topol., 2017. https://doi.org/10.2140/agt.2017.17.331
• L. Chen, The Kervaire conjecture and the minimal complexity of surfaces, Trans. Amer. Math. Soc., 2026. https://arxiv.org/abs/2302.09811

Motivation: categoricity transfer beyond first-order logic

A class of structures is categorical in a cardinal $\lambda$ if it has exactly one model of size $\lambda$ up to isomorphism. Morley's theorem (1965) says that a complete first-order theory in a countable language categorical in one uncountable cardinal is categorical in all of them. Abstract elementary classes (AECs), introduced by Shelah in the 1970s, axiomatize classes of structures with a well-behaved notion of strong substructure (closure under isomorphism, coherence, unions of chains, a Löwenheim–Skolem number) without requiring first-order axiomatizability; they cover classes defined in infinitary logics and many classes of modules. Shelah's categoricity conjecture for AECs, in its eventual form, asks whether categoricity in one sufficiently large cardinal transfers to all sufficiently large cardinals. A sharper, prescribed-threshold form names the threshold explicitly: with $H(K)=\beth_{(2^{\mathrm{LS}(K)})^+}$ (the Hanf number for existence of arbitrarily large models), categoricity in some $\lambda\ge H(K)$ should imply categoricity in every $\mu\ge H(K)$. Deciding which form holds is a central question in non-elementary model theory.

Timeline

• 1965 — Morley proves the categoricity theorem for countable first-order theories (Trans. AMS 1965).
• 1970s — Shelah introduces abstract elementary classes (see the survey of Boney–Vasey 2017, §2).
• 1990 — Hart and Shelah show categoricity in $L_{\omega_1,\omega}$ can stop at $\aleph_k$ while holding for $\aleph_0,\dots,\aleph_{k-1}$, using finite-support group constructions (Israel J. Math. 1990).
• 1999 — Shelah proves categoricity transfer for AECs with amalgamation and records $H(K)$ as the existence bound (APAL 1999).
• 2016 — Kolesnikov and Lambie-Hanson study Hanf numbers for amalgamation of coloring classes (JSL 2016).
• 2017 — Vasey proves downward transfer from a successor cardinal $\ge H(K)$ under amalgamation and tameness (APAL 2017).
• 2021 — Grossberg distinguishes the prescribed-bound and eventual forms of the conjecture (A Course in Model Theory I, draft, Ch. 2 §4).
• 2022–2023 — Espíndola announces a proof of eventual categoricity and, for arbitrary AECs, a transfer at the prescribed bound via accessible categories (arXiv:1906.09169, arXiv:2301.13167).
• 2024 — Šaroch and Trlifaj state the prescribed-threshold formulation with both endpoints included (Bull. LMS 2024, §2.3).
• 2026 — An OpenAI preprint, A CH obstruction to a prescribed categoricity threshold (OpenAI Math Release, September 24, 2026), claims that under CH there is an AEC with $\mathrm{LS}(K)=\aleph_0$, categorical on a tail but with two nonisomorphic models at $H(K)=\beth_{\omega_2}$; this conflicts with the transfer claimed in Espíndola 2023 (Theorem 4.1). The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Work with relational structures in a finitary relational language $L$ (a set of relation symbols, each with a finite arity). An abstract elementary class is a class $K$ of $L$-structures with a relation $M\preceq_K N$ ("strong substructure") such that: $\preceq_K$ is a partial order on $K$ refining substructure; $K$ and $\preceq_K$ are closed under isomorphism; coherence holds ($M_0\subseteq M_1$, $M_0\preceq_K M_2$, $M_1\preceq_K M_2$ imply $M_0\preceq_K M_1$); unions of $\preceq_K$-chains are in $K$, are $\preceq_K$-extensions of each member, and are $\preceq_K$-below any common strong extension (Tarski–Vaught chain axioms); and there is a Löwenheim–Skolem number $\mathrm{LS}(K)\ge\aleph_0+|L|$, the least $\theta$ such that every subset $A$ of a model $M$ lies in some $N\preceq_K M$ with $|N|\le|A|+\theta$.

$K$ is categorical in $\mu$ if it has a model of size $\mu$ and any two models of size $\mu$ are isomorphic. The beth numbers are $\beth_0=\aleph_0$, $\beth_{\alpha+1}=2^{\beth_\alpha}$ and suprema at limits. CH is $2^{\aleph_0}=\aleph_1$.

Formalization targets

Goal: the CH counterexample (Theorem 1.1)

Assume CH. There is a countable finitary relational language $L$ and an AEC $K$ in $L$ such that

$$\mathrm{LS}(K)=\aleph_0,\qquad \beth_{\omega_2}=H(K)=\beth_{(2^{\aleph_0})^+},$$

$K$ has two nonisomorphic models of cardinality $\beth_{\omega_2}$, and, with $\Lambda=\beth_{(2^{\aleph_1})^+}$,

$$K\ \text{is categorical in every cardinal } \mu\ge\Lambda .$$

Hence $\Lambda^+>H(K)$ is a categoricity cardinal from which downward transfer to $H(K)$ fails, while eventual categoricity holds for this $K$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Combined with Gödel's relative consistency of CH, the theorem shows that, if ZFC is consistent, the prescribed-threshold form of Shelah's categoricity conjecture is not provable in ZFC (Corollary 6.1 of the source). The example has no amalgamation or joint embedding, which explains why transfer theorems that assume these properties are unaffected, and it is compatible with qualitative eventual categoricity. It also bears directly on a published claim of transfer at the prescribed bound for arbitrary AECs.

Formalizing it. Because the result contradicts a claimed theorem in the literature, an independent machine check is especially valuable. The formal statement verifies every AEC axiom explicitly, not just the two cardinal-arithmetic conclusions. Mathlib has cardinal and ordinal arithmetic, beth numbers and ZFC sets; the AEC framework built here would be reusable for further formal work in non-elementary model theory.

Difficulty

Most known non-transfer examples (Hart–Shelah) fail categoricity at small cardinals; here the failure must happen exactly at the Hanf-type bound $\beth_{\omega_2}$ while categoricity holds on a tail, with $\mathrm{LS}(K)=\aleph_0$. One must build two nonisomorphic models at $\beth_{\omega_2}$ and simultaneously rule out any two nonisomorphic models above $\Lambda$, without appealing to a general eventual-categoricity theorem. All AEC axioms — in particular coherence and smoothness of unions of arbitrary directed chains — must survive the exceptional sets used to separate models, which is where naive constructions break.

Formalization scope

• Structures are RelModel L with carrier a ZFSet (so cardinalities are cardinals of genuine sets in universe u) and relations indexed by arity; $L:\mathbb N\to$ Type with $\Sigma_n L_n$ countable.
• ClassData packages a predicate of objects and a strong-substructure relation; IsAEC lists the axioms above, including invariance under isomorphisms compatible with inclusion, coherence, and the union axioms for chains indexed by any nonzero ordinal.
• HasLSNumber ℵ₀ asserts both that $\aleph_0$ is a Löwenheim–Skolem bound and that it is the least one.
• hanf κ = beth (succ (2^κ)).ord, endpoint = beth (ω_2), tailThreshold = beth (succ (2^{ℵ₁})).ord. The equality endpoint = hanf ℵ₀ is part of the goal (it follows from CH).
• Categorical μ includes existence of a model of size $\mu$; TwoModels asks for two nonisomorphic models of the given size.
• CH is a hypothesis of the theorem, in the same universe; the consistency corollary is not part of the goal.

Selected references

• M. Morley, Categoricity in power, Trans. Amer. Math. Soc. (1965). https://doi.org/10.1090/S0002-9947-1965-0175782-0
• K. Gödel, The consistency of the axiom of choice and of the generalized continuum-hypothesis, Proc. Nat. Acad. Sci. USA (1938). https://doi.org/10.1073/pnas.24.12.556
• B. Hart and S. Shelah, Categoricity over P for first order T or categoricity for φ∈L_{ω1ω} can stop at ℵ_k while holding for ℵ_0,…,ℵ_{k−1}, Israel J. Math. (1990). https://doi.org/10.1007/BF02807869
• S. Shelah, Categoricity for abstract classes with amalgamation, Ann. Pure Appl. Logic (1999). https://doi.org/10.1016/S0168-0072(98)00016-5
• S. Vasey, Downward categoricity from a successor inside a good frame, Ann. Pure Appl. Logic (2017). https://doi.org/10.1016/j.apal.2016.10.003
• W. Boney and S. Vasey, A survey on tame abstract elementary classes, 2017. https://arxiv.org/abs/1512.00060
• A. Kolesnikov and C. Lambie-Hanson, The Hanf number for amalgamation of coloring classes, J. Symb. Logic (2016). https://doi.org/10.1017/jsl.2015.48
• J. Šaroch and J. Trlifaj, Deconstructible abstract elementary classes of modules and categoricity, Bull. London Math. Soc. (2024). https://doi.org/10.1112/blms.13172
• C. Espíndola, A complete classification of categoricity spectra of accessible categories with directed colimits, preprint, 2023. https://arxiv.org/abs/2301.13167
• OpenAI, A CH obstruction to a prescribed categoricity threshold, OpenAI Math Release preprint, September 24, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-CH-Obstruction-to-a-Prescribed-Categoricity-Threshold-September-24-2026/paper.pdf

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.