Probability

Motivation

A finite message chosen from data changes the conditional distribution of those data. In memory-constrained inference this matters directly: a learner observing a signal $S$ through exact Gaussian equations keeps a finite state $W$, and after conditioning on $W$ the rows that were used to select it are biased. An independent Gaussian matrix has the same unconditional law as those rows, but once its labels are revealed it need not leave the same information about $S$.

This preprint quantifies the cost of that replacement. For a uniform signal on the sphere and a message of entropy at most $d^2$, replacing the actual rows by fresh independent rows increases the remaining conditional information by at most $O(d)$. As an application, learners with $o(d^2)$ persistent bits need $\Omega(d\log(1/\epsilon))$ exact Gaussian observations to reach angular accuracy $\epsilon$.

Background

• 1975. Mattila's two-point averaging estimate controls projection energies by inverse distances.
• 2015–2017. Steinhardt and Duchi establish memory-dependent minimax bounds for sparse noisy regression; Raz proves branching-program time–space lower bounds for parity learning (2016) and broader discrete problems (2017).
• 2016–2017. Russo and Zou bound the bias of a selected statistic by the information used for selection; Xu and Raginsky give an information-theoretic bound on generalization via a sub-Gaussian test under the product law.
• 2019. Sharan, Sidford and Valiant prove an $\Omega(d\log r)$ sample lower bound for Gaussian regression with small uniform noise and $d^2/4$ bits at Euclidean accuracy $d^{-r}$. Dagan, Kur and Shamir prove quadratic-space lower bounds for related linear-algebra tasks.
• 2026. The OpenAI preprint Replacing Gaussian observations in memory-constrained inference (dated September 27, 2026) proves the replacement comparison and its streaming consequence. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Let $\sigma$ be uniform probability on $S^{d-1}$, $\gamma_k$ the law of a $k \times d$ matrix with i.i.d. $N(0,1)$ entries, $H$ discrete entropy and $I(\cdot\,;\cdot\mid\cdot)$ conditional mutual information, all in nats. Put

$$m = \lfloor d/10\rfloor, \qquad \ell = \lfloor d/2\rfloor, \qquad r = \ell - m.$$

Let $S \sim \sigma$ and $A \sim \gamma_m$ be independent, and let $W$ be a countable message with an arbitrary joint law with $(S, A)$.

• In the aligned experiment, keep $(S, A, W)$ and append an independent $r$-row Gaussian matrix $C$, so the analyst sees $G_1 = (A; C)$ and $G_1 S$.
• In the independent experiment, keep $(S, W)$ and draw a fresh $\ell$-row Gaussian matrix $G_0$ independent of $(S, W)$.

In Lean (OAI.CurrentProjection), the joint law of $((S, W), A)$ is a probability measure P on (Sphere d × W) × Rows (d/10) d whose $(S, A)$ marginal is uniformSphere d ⊗ gaussianRows (d/10) d; alignedExperiment and P.fst.prod (gaussianRows ...) are the two experiments; exposedInformation is $I(S; W \mid G, GS)$ computed as a relative entropy via condKernel; shannonEntropy is $H(W)$.

Formalization targets

Goal: Theorem 4.1 (Critical-radius comparison)

There are an absolute $K$ and $d_0$ such that for $d \ge d_0$ and every such countable $W$ with $H(W) \le d^2$,

$$I_0(S; W \mid G_0, G_0 S) \le I_1(S; W \mid G_1, G_1 S) + K d .$$

Milestones

• Theorem 3.1 (mixed projection moment and exact density version): for $\ell = m + r < d - 1$, $r \ge q$, and a finite measure $\rho$ on the sphere with $\rho(B(z,t)) \le B t^\ell$ and $\rho(B(z,t)) \le D t^{d-1}$,

$$\Big[\mathbb{E}_X\big(\mathbb{E}_Z\, p_{\rho,\delta}((X;Z),(X;Z)s)\big)^q\Big]^{1/q} \le e^{Cd} B\big(1 + \log^+(D/B)\big),$$

with an exact-density version when $\rho \ll \sigma$.

• Proposition 3.2 (actual-row tilt and exact-label limit).
• Propositions 5.3 and 5.4 (one-level and two-label auxiliary-row comparisons).
• Proposition 6.1 (averaged information increase per block, hybrid route).
• Proposition 7.1 (information through a Gaussian block, fiber route) and Lemma 7.2 (two-point Gaussian fiber measure identity).

Significance

The result. Theorem 4.1 converts a statement about the actual, selection-biased rows into one about fresh rows at an additive cost of $O(d)$, which is the step that lets block-by-block information bounds be iterated along a stream. With the residual-sphere endpoint it gives the lower bound $T = \Omega(d\log(1/\epsilon))$ for learners with $o(d^2)$ bits (Theorem 8.4, Corollary 8.7). The mixed projection moment (Theorem 3.1) is a reusable estimate on exact Gaussian projections of measures with local mass control.

Formalizing it. All results are in an unrefereed preprint, with no machine-checked proofs. The streaming theorems themselves (Theorem 8.4, Theorem 8.6, Corollary 8.7) are not among the published Lean targets and remain future work.

Difficulty

Conditioning on $W$ biases $A$ in a way that depends on the unknown signal, so the two experiments have different joint laws even though their $(S, W)$ and $(S, G)$ marginals agree. A direct comparison of densities fails because the exact label density under the actual law can be large on a selection-dependent set; controlling it requires a high moment of the projected density with the row-information charge $I(A; W \mid S) \le H(W)$ entering only with coefficient $1/q$.

Formalization scope

• Signals live on Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1 with normalized surface measure; rows are Fin k → EuclideanSpace ℝ (Fin d) with stdGaussian entries.
• Messages are countable types with measurable singletons (finite types for some milestones); entropies and informations are ℝ≥0∞-valued.
• Row counts are d/10, d/2 - d/10, d/32, d/8, d/4, d/3 as in each source statement.

The goal is not vacuous: it quantifies over all joint laws with the stated marginal and entropy bound, and the right side is finite for many of them.

Needed infrastructure: conditional mutual information for standard Borel variables, chain rules, exact density versions of Gaussian projections, local mass bounds on the sphere. Contributions toward any milestone are welcome.

Selected references

• OpenAI, Replacing Gaussian observations in memory-constrained inference, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Replacing-Gaussian-observations-in-memory-constrained-inference-September-27-2026/paper.pdf
• V. Sharan, A. Sidford, G. Valiant, Memory-Sample Tradeoffs for Linear Regression with Small Error, STOC 2019. https://doi.org/10.1145/3313276.3316403
• J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
• R. Raz, Fast Learning Requires Good Memory, 2016. https://arxiv.org/abs/1602.05161
• R. Raz, A Time-Space Lower Bound for a Large Class of Learning Problems, FOCS 2017. https://doi.org/10.1109/FOCS.2017.73
• Y. Dagan, G. Kur, O. Shamir, Space Lower Bounds for Linear Prediction in the Streaming Model, COLT 2019. https://proceedings.mlr.press/v99/dagan19b.html
• D. Russo, J. Zou, Controlling Bias in Adaptive Data Analysis Using Information Theory, AISTATS 2016. https://proceedings.mlr.press/v51/russo16.html
• A. Xu, M. Raginsky, Information-theoretic analysis of generalization capability of learning algorithms, NeurIPS 2017. https://papers.nips.cc/paper_files/paper/2017/hash/ad71c82b22f4f65b9398f76d8be4c615-Abstract.html
• P. Mattila, Hausdorff Dimension, Orthogonal Projections and Intersections with Planes, Ann. Acad. Sci. Fenn. 1 (1975). https://doi.org/10.5186/aasfm.1975.0110

Motivation

An exact linear observation $\langle x, S\rangle$ of a real signal can carry arbitrarily many bits. A finite message computed from a block of such observations cannot, but its information content is not controlled by the number of observations alone: if earlier messages have already concentrated the signal in a small region, the next block can exploit that concentration. Bounds of this kind are the engine of memory–sample lower bounds for noiseless Gaussian regression, where a learner with $M$ bits of memory must recover a unit vector to angular accuracy $\epsilon$ from a stream of exact Gaussian measurements.

This preprint asks how to restore a geometric spread condition on the posterior while paying for the information revealed in doing so, and proves that, for a cube-shaped prior on a spherical patch, $t$ blocks of $\Theta(d)$ exact measurements with messages of at most $\exp(Ad^2)$ values reveal only $O_A(dt)$ nats.

Background

• 2015. Steinhardt and Duchi prove memory–sample trade-offs for noisy sparse regression.
• 2016. Steinhardt, Valiant and Wager formulate a memory/sample conjecture for parity learning; Raz proves a quadratic-memory versus exponential-sample separation for parities, extended to a broad class of finite problems in 2017.
• 2019. Sharan, Sidford and Valiant prove an $\Omega(d\log r)$ sample lower bound for Gaussian regression with small additive noise, memory at most $d^2/4$ bits and Euclidean accuracy $d^{-r}$; their Section 7 expands projection moments into independent signal copies. Dagan, Kur and Shamir prove quadratic-memory lower bounds for approximately solving a consistent linear system in random order.
• 2026. OpenAI preprints on exact observations: Posterior replicas and conditional information in Gaussian regression, Replacing Gaussian observations in memory-constrained inference, and the present Localization costs and information growth for exact Gaussian observations (dated September 27, 2026), which supplies several localization routes to the $\Omega(d\log(1/\epsilon))$ lower bound for $o(d^2)$ memory. None of these preprints is peer reviewed; the Lean goal is open on this platform.

Setting

Let $d$ be large, $n = d - 1$, $k = \lfloor n/16\rfloor$, $m = \lfloor n/8\rfloor$. The cube prior is normalized Lebesgue measure $\mu_0$ on the half-open cube $Q_0 = [-1/(2\sqrt n), 1/(2\sqrt n))^n$, and the chart $\phi(z) = (z, \sqrt{1 - \|z\|^2})$ maps it into $S^{d-1}$. Dyadic cells of level $J$ subdivide $Q_0$ into $2^{nJ}$ half-open subcubes of side $2^{-J}/\sqrt n$.

Draw $Z \sim \mu_0$. In block $i = 1, \dots, t$ an independent standard Gaussian $k \times d$ matrix $X_i$ is drawn, and $(X_i, X_i\phi(Z))$ is observed exactly. A message $W_i \in \{1, \dots, N\}$ is drawn from a Borel probability kernel of the block data, whose choice may depend on the preceding messages $W_1, \dots, W_{i-1}$. Information is measured in nats by mutual information $I(\cdot\,;\cdot)$, defined as a relative entropy.

In Lean (OAI.RepeatedLocalization), Coordinate n = Fin n → ℝ, cubePrior n is Lebesgue measure conditioned on initialCube n, chart is $\phi$, a Cell n is a level $J$ with a multi-index in Fin (2^J), a BlockRule n N is a measurable probability vector on Fin N indexed by block data, Rules n N t chooses a rule for each block from the past history, and experimentLaw rules is the joint law of $(Z, W_1, \dots, W_t)$.

Formalization targets

Goal: Theorem 3.2 (Repeated localization), repeated_localization

There is an absolute $c > 0$ such that for every $C_0 > 0$ there is $C$ with the following property, for $d$ large. If

$$\big(2/m + e^{-ck}\big)\log N \le C_0 d,$$

then one can reveal nested dyadic cells $Q_0 \supset Q_1 \supset \cdots \supset Q_t$ containing $Z$, with $Q_i$ a finite-valued measurable function of $Z$ and $W_1, \dots, W_i$, such that the augmented transcript $\Pi_t = (W_1, Q_1, \dots, W_t, Q_t)$ satisfies

$$I(Z; \Pi_t) \le C d t, \qquad \mathbb{E}\, J_t \le C t,$$

where $J_t$ is the level of $Q_t$. An alphabet of size $N \le \exp(Ad^2)$ satisfies the hypothesis with $C_0$ depending only on $A$.

Milestones (results from the paper's other routes)

• Lemma 5.2 (finite expected regularization of a finite-relative-entropy posterior by a terminating dyadic search).
• Lemma 12.1 (convexity and coercivity of the kernel potential $\Phi(\nu) = D(\nu\|\sigma) - \int \log J_\nu\, d\nu$).
• Proposition 12.6 (the potential grows by at most $Cd$ per block).
• Lemma 13.2 (inverse simplex-volume moment under a ball bound, with no support restriction).

Significance

The result. Theorem 3.2 is the first information estimate in the paper and the model for its later routes: it shows that revealing a nested dyadic cell after each block, which restores the spread condition needed by the projection estimate, costs only $O(d)$ nats per block. Since the original message history is a function of $\Pi_t$, the bound also controls the information in the messages alone. Combined with the paper's endpoint arguments this yields the lower bound $T \ge c\,d\log(1/\epsilon)$ for learners with $o(d^2)$ bits.

Formalizing it. These results are proved only in an unrefereed preprint; no machine-checked proofs exist. The milestones are independent analytic statements (an entropy regularization, a convex potential and its drift, an inverse-volume moment) that are reusable in the companion missions on exact Gaussian observations.

Difficulty

The information a block reveals depends on how concentrated the current posterior is, and earlier messages can make it arbitrarily concentrated. Simply conditioning on messages gives no control. Revealing a localizing cell restores spread, but naming a cell itself costs information, and the count of candidate cells at depth $j$ grows like $2^{nj/2}$; the argument must show that confinement to a depth-$j$ cell (worth $nj$ bits relative to the prior) pays for this, uniformly over all message rules.

Formalization scope

• The prior is the image of cube volume under $\phi$, not surface measure; coordinates are Fin n → ℝ, and $d$ appears as n + 1.
• Row counts and parameters are natural-number floors n / 16, n / 8. Gaussian entries are gaussianReal 0 1.
• A disclosure Q : Disclosure n N t is valid when each cell map is measurable with finite range, contains $Z$, lies in $Q_0$, and the cells are nested. The goal asserts existence of a valid disclosure with mutualInformation (augmentedLaw rules Q) ≤ C (n+1) t and expected final level at most $Ct$.
• Mutual information is klDiv of the joint law against the product of marginals, valued in ℝ≥0∞.

The goal is not trivial: the trivial disclosure (always $Q_0$) does not bound the information in arbitrary messages, and the quantifier order (absolute $c$, then $C_0$, then $C$) matches the source.

Needed infrastructure: Gaussian projections of measures on cells, $L^m$ density bounds, dyadic cell combinatorics, and relative-entropy chain rules. Contributions toward any milestone are welcome.

Selected references

• OpenAI, Localization costs and information growth for exact Gaussian observations, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Localization-costs-and-information-growth-for-exact-Gaussian-observations-September-27-2026/paper.pdf
• OpenAI, Posterior replicas and conditional information in Gaussian regression, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/main/preprints/Posterior-replicas-and-conditional-information-in-Gaussian-regression-September-27-2026/paper.pdf
• V. Sharan, A. Sidford, G. Valiant, Memory-Sample Tradeoffs for Linear Regression with Small Error, STOC 2019. https://doi.org/10.1145/3313276.3316403
• R. Raz, Fast Learning Requires Good Memory, 2016. https://arxiv.org/abs/1602.05161
• R. Raz, A Time-Space Lower Bound for a Large Class of Learning Problems, FOCS 2017. https://doi.org/10.1109/FOCS.2017.73
• J. Steinhardt, G. Valiant, S. Wager, Memory, Communication, and Statistical Queries, COLT 2016. https://proceedings.mlr.press/v49/steinhardt16.html
• J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
• Y. Dagan, G. Kur, O. Shamir, Space Lower Bounds for Linear Prediction in the Streaming Model, COLT 2019. https://proceedings.mlr.press/v99/dagan19b.html
• T. Austin, Multi-variate correlation and mixtures of product measures, Kybernetika, 2020.

Motivation: how many deletion traces does it take to recover a word?

In the trace reconstruction problem an unknown binary word $x\in\{0,1\}^n$ is passed repeatedly through a deletion channel: each bit is deleted independently with known probability $q\in(0,1)$ and the surviving bits are concatenated in order. Each output, called a trace, reveals its length and its bits but not which positions survived. The question is how many independent traces are needed to recover every word $x$ exactly with a fixed success probability. The problem arises in DNA storage and sequencing, in multiple sequence alignment, and as a basic test of how much information a channel with synchronization errors destroys. Its central open question has been whether a polynomial number of traces suffices at a fixed deletion probability.

Timeline

• 2001 — Levenshtein studies efficient reconstruction of sequences from corrupted copies, in combinatorial and memoryless-channel versions (IEEE Trans. Inf. Theory 2001).
• 2004 — Batu, Kannan, Khanna and McGregor introduce the independent-deletion trace problem in connection with multiple sequence alignment and outline a linear lower bound at fixed deletion probability (SODA 2004).
• 2008 — Holenstein, Mitzenmacher, Panigrahy and Wieder give the first worst-case upper bound $\exp(\widetilde O(\sqrt n))$ at constant deletion probability (SODA 2008).
• 2014 — McGregor, Price and Vorotnikova analyze lower bounds via a single displaced one among zeros (ESA 2014).
• 2017 — De, O'Donnell and Servedio (STOC 2017) and, independently, Nazarov and Peres (STOC 2017) improve the upper bound to $\exp(O(n^{1/3}))$.
• 2020 — Holden and Lyons prove the lower bound $\Omega(n^{5/4}/\sqrt{\log n})$ (Ann. Appl. Probab. 2020; erratum 2022).
• 2021 — Chase improves the lower bound to $\Omega(n^{3/2}/\log^7 n)$ (Ann. Inst. Henri Poincaré Probab. Stat. 2021) and the upper bound to $\exp(O(n^{1/5}\log^5 n))$ (STOC 2021).
• 2026 — Burudgunte, Valiant and Wang give a quasipolynomial sample upper bound $\exp(p^{-7/3}(\log_2 n)^{C_0})$ with $p=1-q$ (arXiv:2607.04073).
• 2026 — An OpenAI preprint, Quantitative lower bounds for trace reconstruction (OpenAI Math Release, September 24, 2026), claims that $n^{\Omega(\log\log n)}$ traces are necessary at every fixed $q$, answering the polynomial-sample question negatively. The preprint has not been peer reviewed and its theorems are not formally verified.

Setting

Fix $n$ and $q\in(0,1)$. A deletion mask $a\in\{0,1\}^n$ keeps bit $i$ when $a_i=1$; it has probability $\prod_i (1-q)^{a_i} q^{1-a_i}$. The trace of $x$ under $a$ is the list of the bits $x_i$ with $a_i=1$, in order. Write $\mathcal D_q(x)$ for the law of the trace of $x$ under a random mask.

An estimator with budget $m$ receives $m$ independent traces of $x$ and returns a random word; it may be randomized and its computation is unrestricted. For $s\in(0,1]$, the sample complexity $T_{q,s}(n)$ is the least $m$ such that some estimator recovers every $x\in\{0,1\}^n$ with probability at least $s$; it is $+\infty$ if no finite $m$ works. The one-trace distance is

$$\operatorname{TV}\bigl(\mathcal D_q(x),\mathcal D_q(y)\bigr)=\tfrac12\sum_{w}\bigl|\mathcal D_q(x)(w)-\mathcal D_q(y)(w)\bigr|,$$

the sum running over all finite binary words.

In Lean (namespace OAI.TraceReconstruction), words are Fin n → Bool, traceMass q x w is the probability of output w, an estimator is a function A : (Fin m → Trace) → Word n → ℝ giving a probability vector for each sample, sampleComplexity n q s : ℝ≥0∞ is the infimum of sufficient budgets, and minTraceTV n q is the minimum of traceTV q x y over $x\neq y$.

Formalization targets

Goal: quantitative sample lower bound (Theorem 1.1)

Fix $s\in(0,1]$ and $0<c<1/(4\log 2)$. For every sequence of instances $(n_k,q_k)$ with $n_k\to\infty$, $q_k\in(0,1)$ and $q_k^3\log n_k\to\infty$,

$$T_{q_k,s}(n_k)\;\ge\; n_k^{\,c\log(q_k^3\log n_k)}\qquad\text{for all sufficiently large }k.$$

At fixed $q$ this gives $T_{q,s}(n)\ge n^{\Omega(\log\log n)}$, so no polynomial number of traces suffices. The goal is published on the platform with status Open.

Milestones: superpolynomial indistinguishability (Theorem 1.2)

For every fixed $q\in(0,1)$ and every $A>0$,

$$\lim_{n\to\infty} n^{A}\min_{x\neq y\in\{0,1\}^n}\operatorname{TV}\bigl(\mathcal D_q(x),\mathcal D_q(y)\bigr)=0, \qquad \lim_{n\to\infty}\frac{T_{q,s}(n)}{n^{A}}=\infty\quad (s\in(0,1]).$$

Significance

The result itself. Theorem 1.1 is the first superpolynomial lower bound for exact worst-case trace reconstruction at a fixed deletion probability; previous lower bounds were of order $n^{3/2}$ up to logarithms. It holds against unrestricted computation and any fixed positive success probability, and it settles in the negative the question of whether polynomially many traces suffice. Combined with the 2026 quasipolynomial upper bound of Burudgunte, Valiant and Wang, the sample complexity at fixed $q$ is now known to lie between $\exp(\Theta(\log n\log\log n))$ and $\exp((\log n)^{O(1)})$. Theorem 1.2 isolates the underlying phenomenon: some pairs of distinct words have single-trace laws closer than every inverse polynomial.

Formalizing it. The definitions fix exactly what an estimator may see (only the complete traces, no positions or boundaries) and what "sample complexity" means, including the value $+\infty$. A formal proof would certify a lower bound whose argument is a long multi-scale construction with many quantitative error budgets, the kind of argument where an overlooked loss would invalidate the conclusion.

Difficulty

Earlier lower bounds compare two words that differ by a single local defect and compute their trace distance directly; such pairs are distinguishable from polynomially many traces, so no single-defect construction can give a superpolynomial bound. A superpolynomial bound needs pairs of words whose trace laws agree to every polynomial order, while the argument must remain uniform in the deletion probability (which may tend to $0$ slowly), keep all constants below scale margins that shrink as the number of construction stages grows with $n$, and transfer a bound for one trace to a bound for $m$ independent traces and for arbitrary randomized estimators.

Formalization scope

• Traces are List Bool; traceTV sums over the finite set of all lists of length at most $n$, which contains the support of every trace law, so it agrees with the source's total variation over all finite words.
• sampleComplexity is an sInf in ℝ≥0∞; the infimum of the empty set is $\top$, matching $T_{q,s}(n)=+\infty$. The lower bound is compared after ENNReal.ofReal, and the right-hand side $n^{c\log(q^3\log n)}$ uses the real power.
• Theorem 1.1 is encoded with sequences n q : ℕ → …, Tendsto n atTop atTop, and Tendsto (q k ^ 3 * log (n k)) atTop atTop; the conclusion is ∀ᶠ k in atTop. Logarithms are natural.
• Estimators are arbitrary real-valued probability kernels from samples to words; success is the exact probability of returning the true word, required to be at least $s$ for every input.
• minTraceTV n q is a real sInf, attained for $n\ge1$; at $n=0$ the set is empty and the junk value $0$ does not affect the limit.
• Needed infrastructure: the deletion channel and its trace law, total variation and Hellinger distance for finite laws and their tensorization, and the reduction from sample complexity to pairwise distinguishability. These are reusable for other deletion-channel problems.

Selected references

• V. I. Levenshtein, Efficient reconstruction of sequences, IEEE Trans. Inform. Theory, 2001. https://doi.org/10.1109/18.904499
• T. Batu, S. Kannan, S. Khanna and A. McGregor, Reconstructing strings from random traces, SODA 2004. https://people.cs.umass.edu/~mcgregor/papers/04-soda.pdf
• T. Holenstein, M. Mitzenmacher, R. Panigrahy and U. Wieder, Trace reconstruction with constant deletion probability and related results, SODA 2008. https://www.eecs.harvard.edu/~michaelm/postscripts/soda2008c.pdf
• A. McGregor, E. Price and S. Vorotnikova, Trace reconstruction revisited, ESA 2014. https://doi.org/10.1007/978-3-662-44777-2_57
• A. De, R. O'Donnell and R. A. Servedio, Optimal mean-based algorithms for trace reconstruction, STOC 2017. https://doi.org/10.1145/3055399.3055450
• F. Nazarov and Y. Peres, Trace reconstruction with $\exp(O(n^{1/3}))$ samples, STOC 2017. https://doi.org/10.1145/3055399.3055494
• N. Holden and R. Lyons, Lower bounds for trace reconstruction, Ann. Appl. Probab., 2020. https://doi.org/10.1214/19-AAP1506
• Z. Chase, New lower bounds for trace reconstruction, Ann. Inst. Henri Poincaré Probab. Stat. 57 (2021), 627–643. https://doi.org/10.1214/20-AIHP1089
• Z. Chase, Separating words and trace reconstruction, STOC 2021. https://doi.org/10.1145/3406325.3451118
• A. Burudgunte, P. Valiant and H. Wang, Quasipolynomial trace reconstruction, preprint, 2026. https://arxiv.org/abs/2607.04073
• OpenAI, Quantitative lower bounds for trace reconstruction, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1; Theorem 1.2, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/quantitative-lower-bounds-for-trace-reconstruction-September-24-2026/paper.pdf

Motivation

Split Euclidean space into finitely many measurable cells and record, for each cell, its Gaussian first moment, the integral of $x$ against the standard Gaussian measure over that cell. How large can the sum of the squared lengths of these vectors be? The propeller conjecture predicts that, with at least three cells in dimension at least two, the answer is $9/(8\pi)$, attained by three planar sectors of angle $2\pi/3$ (a "propeller") times the orthogonal complement. The question arose in Khot and Naor's work on approximate kernel clustering (Mathematika 2009), where this Gaussian partition parameter determines both the approximation ratio of Gaussian rounding and the matching Unique-Games hardness threshold. The surprise is that more cells or more dimensions do not help: the optimum uses only three cells in a plane.

This mission asks for a formal proof of the propeller bound in every dimension, 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

• 1983–2003 — The Gaussian Minkowski (Ehrhard) inequality: Ehrhard for convex sets (Math. Scand. 1983), Latała when one set is convex (Studia Math. 1996), Borell for Borel sets (C. R. Acad. Sci. 2003); later van Handel's game proof (PTRF 2018).
• 2009 — Khot and Naor introduce the problem, reduce maximizers to conical partitions in the span of their centroids, and compute the three-cell value (Mathematika 2009); see also their sharp kernel-clustering paper (RSA 2013).
• 2013 — Heilman, Jagannath and Naor prove the conjecture in $\mathbb R^3$ with a computer-assisted argument (DCG 2013).
• 2022 — Heilman gives a conditional route for three or four cells in any dimension, under a stability hypothesis on noise-stability maximizers (arXiv:2209.11216).
• September 2026 — The OpenAI preprint claims the bound for every dimension and every number of cells (Theorem 1.1, p. 1).

Setting

Let $\gamma_d$ be the standard Gaussian probability measure on $\mathbb R^d$, with density $(2\pi)^{-d/2}e^{-\|x\|^2/2}$. For a measurable set $A\subseteq\mathbb R^d$, its centroid is the unnormalized vector

$$z(A)=\int_A x\,d\gamma_d(x)\in\mathbb R^d .$$

A measurable partition $(A_1,\dots,A_k)$ of $\mathbb R^d$ consists of measurable sets such that almost every point (for $\gamma_d$) lies in exactly one of them; empty cells and arbitrary cell probabilities are allowed. Its value is $F(A)=\sum_{i=1}^k\|z(A_i)\|^2$. The propeller is the partition of $\mathbb R^d$, $d\ge2$, into the three sets $S_j\times\mathbb R^{d-2}$, where $S_1,S_2,S_3$ are the planar sectors of opening $2\pi/3$ bounded by the rays at angles $\pm\pi/3$ and $\pi$, with any further cells empty.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For all positive integers $d,k$ and every measurable partition $(A_1,\dots,A_k)$ of $\mathbb R^d$,

$$\sum_{i=1}^k\Bigl\|\int_{A_i}x\,d\gamma_d(x)\Bigr\|^2\ \le\ \frac{9}{8\pi},$$

and for $d\ge2$, $k\ge3$ the propeller is a measurable partition attaining equality.

Significance

The result itself. It settles the propeller conjecture in all dimensions and for all numbers of cells, without constraints on cell masses. Through Khot and Naor's analysis, the constant $9/(8\pi)$ fixes the loss factor $\alpha_k=\frac{8\pi}{9}(1-\frac1k)$ of Gaussian rounding for identity-target kernel clustering; combined with the companion Unique Games preprint, the preprint deduces NP-hardness of any better fixed loss factor (Theorem 6.1, p. 18). The bound also gives a sharp inequality for expected Gaussian maxima (Corollary 5.1, p. 17).

Formalizing it. A formal proof needs Gaussian measures on Euclidean space (available in Mathlib as stdGaussian), a compactness argument for extremal partitions, the convex case of the Ehrhard inequality, and the three-dimensional theorem of Heilman, Jagannath and Naor, which the preprint uses as an established input and which itself relies on a finite computer verification. Each of these is a reusable component; the three-dimensional case alone would be a substantial formalization.

Difficulty

The optimization runs over all measurable partitions, with both shapes and probabilities free. Khot and Naor's reduction gives conical extremizers whose $m$ nonzero centroids span an $(m-1)$-dimensional space, so the three-dimensional theorem disposes of $m\le4$ active cells. The remaining cases $m\ge5$ cannot be handled by any fixed finite computation. The preprint constrains them in two ways: deleting one score costs a definite amount of expected maximum, via concavity from the Ehrhard inequality (Section 3), and competition against two residual scores constrains a covariance determinant (Section 4, Lemma 4.1 and Corollary 4.2, pp. 11–12). Combining these must rule out every configuration with five or more cells.

Formalization scope

• Space d is EuclideanSpace ℝ (Fin d) and the measure is stdGaussian. IsPartition A asks each cell to be measurable and almost every point to lie in exactly one cell, matching the paper's convention that partitions are taken up to null sets.
• centroid A is the Bochner integral of the identity over A; value sums squared Euclidean norms. Integrability holds because Gaussian measures have finite first moments.
• The goal is a conjunction: the bound for all $d,k\ge1$, and, for $d\ge2$, $k\ge3$, that the explicit three-sector propeller d k (cells $\ge3$ empty) is a partition with value exactly $9/(8\pi)$. The sectors are written with closed inequalities, so they overlap only on null rays.
• No hypothesis is vacuous: the case $k=1$ is included (value $0$), and the equality clause pins the constant.

Selected references

• OpenAI, The Gaussian propeller bound in every dimension, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Gaussian-Propeller-Bound-in-Every-Dimension-September-24-2026/main.pdf
• S. Khot, A. Naor, Approximate kernel clustering, Mathematika 55 (2009), 129–165. https://doi.org/10.1112/S002557930000098X
• S. Khot, A. Naor, Sharp kernel clustering algorithms and their associated Grothendieck inequalities, Random Struct. Algorithms 42 (2013), 269–300. https://doi.org/10.1002/rsa.20398
• S. Heilman, A. Jagannath, A. Naor, Solution of the Propeller Conjecture in $\mathbb R^3$, Discrete Comput. Geom. 50 (2013), 263–305. https://doi.org/10.1007/s00454-013-9530-0
• S. Heilman, Hyperstable sets with voting and algorithmic hardness applications, arXiv:2209.11216 (2022). https://arxiv.org/abs/2209.11216v1
• A. Ehrhard, Symétrisation dans l'espace de Gauss, Math. Scand. 53 (1983), 281–301. https://doi.org/10.7146/math.scand.a-12035
• R. Latała, A note on the Ehrhard inequality, Studia Math. 118 (1996), 169–174. https://doi.org/10.4064/sm-118-2-169-174
• C. Borell, The Ehrhard inequality, C. R. Acad. Sci. Paris 337 (2003), 663–666. https://doi.org/10.1016/j.crma.2003.09.031
• R. van Handel, The Borell–Ehrhard game, Probab. Theory Relat. Fields 170 (2018), 555–585. https://doi.org/10.1007/s00440-017-0762-4
• E. Mossel, R. O'Donnell, K. Oleszkiewicz, Noise stability of functions with low influences: invariance and optimality, Ann. of Math. 171 (2010), 295–341. https://doi.org/10.4007/annals.2010.171.295

Motivation: largest prime factors of neighbouring integers

Let $P^+(n)$ be the largest prime factor of an integer $n\ge2$. The classical theory of smooth numbers (Dickman 1930, Ramaswami 1949, de Bruijn 1951) shows that $\log P^+(n)/\log n$ has a limiting distribution: the proportion of $n\le X$ with $P^+(n)\le X^a$ tends to $\rho(1/a)$, where $\rho$ is the Dickman function. Multiplicative structure of $n$ and of $n+1$ is expected to be independent, since consecutive integers share no prime factor, but proving independence of such "additive shifts" of multiplicative data is the core difficulty of the Chowla/Elliott circle of problems. Erdős and Pomerance (1978) asked whether $P^+(n)$ and $P^+(n+1)$ are asymptotically independent with Dickman marginals, and, as a consequence, whether $P^+(n)<P^+(n+1)$ holds for exactly half of all $n$ (a comparison question usually attributed to Erdős and Turán).

Timeline

• 1930–1951 — Dickman, Ramaswami and de Bruijn establish the one-variable law $\#\{n\le X: P^+(n)\le X^a\}/X\to\rho(1/a)$.
• 1978 — Erdős and Pomerance formulate the joint independence problem, prove that each ordering of $P^+(n),P^+(n+1)$ has lower natural density at least $0.0099$, and show that $P^+(n)/P^+(n+1)$ rarely lies in $(X^{-\delta},X^{\delta})$ (Aequationes Math. 17 (1978)).
• 2005 — de la Bretèche, Pomerance and Tenenbaum raise the lower density to $0.05544$ (and $0.05866$ via an observation of Fouvry).
• 2017–2018 — Wang obtains $0.1063$ and $0.1356$.
• 2018 — Teräväinen proves the joint Dickman law in logarithmic density, and logarithmic density $1/2$ for the ordering (Forum Math. Sigma 6 (2018)).
• 2019 — Tao and Teräväinen obtain the joint law for ordinary averages outside an exceptional set of scales of logarithmic density zero (Algebra Number Theory 13 (2019)).
• 2021 — Wang proves the ordinary joint law conditionally on the Elliott–Halberstam conjecture for friable integers (J. Number Theory 223).
• 2022 — Jiang, Lü and Wang prove averaged-over-shift versions (Adv. Math. 409).
• 2025–2026 — Lü and Wang reach lower density $0.2017$; Yang reaches $0.280$ (arXiv:2607.16032); Tao and Teräväinen give a quantitative joint law outside exceptional scales (arXiv:2512.01739).
• 2026 — An OpenAI preprint, The joint Dickman law for consecutive integers (OpenAI Math Release, September 24, 2026), claims the unconditional joint law in ordinary natural density at every scale. It has not been peer reviewed, and its proof is not formally verified.

Setting

For $n\ge2$, $P^+(n)$ is the largest prime dividing $n$. The Dickman function $\rho:[0,\infty)\to\mathbb R$ is the continuous function with

$$\rho(u)=1\ (0\le u\le1),\qquad u\rho'(u)=-\rho(u-1)\ (u>1),$$

equivalently $\rho(u)=1-\int_1^u \rho(t-1)\,\frac{dt}{t}$ for $u\ge1$. For a property $P$ of integers and real $X>0$, the natural density at scale $X$ is

$$\mathrm{realDensity}(P,X)=\frac1X\,\#\{2\le n\le X:\ P(n)\}.$$

Formalization targets

Goal: the joint Dickman law (Theorem 1.1)

For every fixed $a,b\in(0,1)$,

$$\lim_{X\to\infty}\frac1X\#\{2\le n\le X:\ P^+(n)\le n^a,\ P^+(n+1)\le n^b\}=\rho(1/a)\,\rho(1/b),$$

with $X$ running over all reals and ordinary, unweighted counting. The goal statement is published on the platform with status Open.

Milestones: equal ordering densities (Corollary 1.2)

$$\lim_{X\to\infty}\frac1X\#\{2\le n\le X:\ P^+(n)<P^+(n+1)\}=\tfrac12, \qquad \lim_{X\to\infty}\frac1X\#\{2\le n\le X:\ P^+(n+1)<P^+(n)\}=\tfrac12 .$$

Significance

The result itself. Theorem 1.1 says that, in natural density, $\log P^+(n)/\log n$ and $\log P^+(n+1)/\log n$ are independent with Dickman marginals. It settles the Erdős–Pomerance independence question positively, removes the logarithmic weighting of Teräväinen's theorem and the exceptional scales of Tao–Teräväinen, and implies the Erdős–Turán comparison: because the limiting marginal is continuous, the product law gives no mass to the diagonal, so each strict ordering has density $1/2$ (Corollary 1.2). Previous unconditional work only gave lower natural densities, never the existence of the density.

Formalizing it. The goal is a clean density statement about elementary objects, but its proof combines Matomäki–Radziwiłł short-interval estimates, sieve bounds, a divisor amplifier, graph comparison and cut-norm sampling. No part of this argument is machine-checked. Even the one-variable Dickman law (the marginal case) is not in Mathlib, and would be a reusable milestone in its own right.

Difficulty

Independence of $n$ and $n+1$ is a binary correlation problem for multiplicative data, of the same nature as the two-point Chowla conjecture. Tao's entropy-decrement and logarithmic-averaging method handles such correlations only with weight $1/n$, or at almost all scales; the step that fails for ordinary density is ruling out a positive correlation along a sparse sequence of scales. The indicator $\mathbf 1_{P^+(n)\le n^a}$ is also not multiplicative, so short-interval theorems for multiplicative functions do not apply to it directly.

Formalization scope

• Nat.maxPrimeFac n (largest element of the prime factor list, a faithful backport of the Mathlib definition) represents $P^+(n)$; its junk values at $0,1$ are irrelevant since counting starts at $n=2$.
• realDensity P X is #{n ∈ [2, ⌊X⌋] : P n} / X as a real number, and limits are Tendsto … atTop over real $X$, matching "the limit over all real $X$".
• The thresholds are $P^+(n)\le n^a$ with real powers (n:ℝ)^a, and the hypotheses $0<a<1$, $0<b<1$ are explicit.
• $\rho$ is constructed by iterating the delay integral equation stepApprox and evaluating the $\lceil u\rceil$-th iterate at $u$; this agrees with the Dickman function on $[0,\infty)$, which is the only range used ($1/a,1/b>1$). A wrong $\rho$ would make the goal false, so this definition is part of what solvers should check.
• Needed infrastructure: the one-variable Dickman law, Selberg–Delange and sieve estimates, short-interval mean values of multiplicative functions, and profinite/Haar-measure compactness arguments. Contributions formalizing the smooth-number marginal or the deduction of Corollary 1.2 from Theorem 1.1 are welcome.

Selected references

• K. Dickman, On the frequency of numbers containing prime factors of a certain relative magnitude, Ark. Mat. Astr. Fys. 22A (1930).
• N. G. de Bruijn, On the number of positive integers $\le x$ and free of prime factors $>y$, Proc. KNAW Ser. A 54 (1951). https://research.tue.nl/en/publications/on-the-number-of-positive-integers-leq-x-and-free-of-prime-factor/
• P. Erdős and C. Pomerance, On the largest prime factors of $n$ and $n+1$, Aequationes Math. 17 (1978), 311–321. https://www.renyi.hu/~p_erdos/1978-29.pdf
• J. Teräväinen, On binary correlations of multiplicative functions, Forum Math. Sigma 6 (2018), e10. https://doi.org/10.1017/fms.2018.10
• T. Tao and J. Teräväinen, The structure of correlations of multiplicative functions at almost all scales, with applications to the Chowla and Elliott conjectures, Algebra Number Theory 13 (2019). https://doi.org/10.2140/ant.2019.13.2103
• K. Matomäki and M. Radziwiłł, Multiplicative functions in short intervals, Ann. of Math. 183 (2016). https://doi.org/10.4007/annals.2016.183.3.6
• T. Tao and J. Teräväinen, Quantitative correlations and some problems on prime factors of consecutive integers, preprint (2026). https://arxiv.org/abs/2512.01739
• OpenAI, The joint Dickman law for consecutive integers, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1 and Corollary 1.2, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-joint-Dickman-law-for-consecutive-integers-September-24-2026/paper.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

Matrix-valued affine processes on the cone of positive semidefinite matrices are used in finance as models of stochastic covariance: multi-asset option pricing with stochastic volatility and correlation, and fixed-income models with stochastically correlated risk factors and default intensities. The best-known example is the Wishart process of Bru (1991). What makes these models tractable is that the Laplace transform of the state is exponential-affine in the initial state, with exponents that solve ordinary differential equations of Riccati type.

Cuchiero, Filipović, Mayerhofer and Teichmann (2011) give the mathematical foundation: a complete characterization of stochastically continuous affine processes on $S_d^+$ through an admissible parameter set. Their Theorem 2.4 has two halves. This mission formalizes the first, necessity, half: every affine process on $S_d^+$ is regular and Feller, and its generator and Riccati equations are given by an admissible parameter set.

Timeline. Duffie, Filipović and Schachermayer (2003) characterized regular affine processes on the canonical state space $\mathbb R_+^m \times \mathbb R^n$, assuming regularity. Keller-Ressel, Schachermayer and Teichmann showed that on that state space stochastic continuity already implies regularity. The 2011 paper carries both the characterization and the regularity result over to $S_d^+$, a non-polyhedral cone with a curved boundary, on which the drift must satisfy the new condition $b \succeq (d-1)\alpha$.

Setting

Let $S_d$ be the space of real symmetric $d\times d$ matrices with scalar product $\langle x,y\rangle = \mathrm{Tr}(xy)$ and norm $\|x\| = \langle x,x\rangle^{1/2}$. Let $S_d^+$ be the cone of positive semidefinite matrices and $S_d^{++}$ its interior, and write $x \preceq y$ when $y - x \in S_d^+$.

A time-homogeneous Markov process $X$ on $S_d^+$ is described by sub-stochastic transition kernels $p_t(x,d\xi)$, $t\ge 0$. Mass that is lost goes to a cemetery state $\Delta$. The kernels satisfy the Chapman–Kolmogorov equations, and the semigroup is $P_tf(x) = \int f(\xi)\,p_t(x,d\xi)$. The process is affine (Definition 2.1) if it is stochastically continuous, i.e. $p_s(x,\cdot) \to p_t(x,\cdot)$ weakly as $s \to t$, and if there are $\varphi : \mathbb R_+ \times S_d^+ \to \mathbb R_+$ and $\psi : \mathbb R_+\times S_d^+ \to S_d^+$ with

$$\int_{S_d^+} e^{-\langle u,\xi\rangle}\,p_t(x,d\xi) = e^{-\varphi(t,u) - \langle\psi(t,u),x\rangle}, \qquad t\ge0,\ u,x\in S_d^+.$$

It is regular (Definition 2.2) if $F(u) = \partial_t\varphi(t,u)|_{t=0+}$ and $R(u) = \partial_t\psi(t,u)|_{t=0+}$ exist and are continuous at $u=0$.

An admissible parameter set $(\alpha, b, \beta^{ij}, c, \gamma, m, \mu)$, associated with a bounded continuous truncation function $\chi$ (equal to the identity near $0$), consists of:

• a diffusion coefficient $\alpha \in S_d^+$ and a constant drift $b \succeq (d-1)\alpha$;
• killing rates $c \ge 0$ and $\gamma \in S_d^+$;
• a jump measure $m$ with $\int(\|\xi\|\wedge1)\,m(d\xi)<\infty$;
• a matrix $\mu$ of finite signed measures with $\mu(E) \in S_d^+$, defining $M(x,d\xi) = \langle x,\mu(d\xi)\rangle/(\|\xi\|^2\wedge1)$;
• a linear drift $B(x) = \sum_{i,j}\beta^{ij}x_{ij}$.

These are subject to the boundary conditions (2.9) and (2.11) for $x,u \in S_d^+$ with $\langle x,u\rangle = 0$. The space $\mathcal S_+$ consists of restrictions to $S_d^+$ of rapidly decreasing smooth functions on $S_d$.

Formalization targets

Goal: Theorem 2.4, first part

If $X$ is affine on $S_d^+$, then $X$ is regular and Feller, $\mathcal S_+$ lies in the domain of its generator $\mathcal A$ on $C_0(S_d^+)$, and there is an admissible parameter set such that for $f \in \mathcal S_+$

$$\mathcal Af(x) = \tfrac12\sum A_{ijkl}(x)\,\partial_{ij}\partial_{kl}f(x) + \sum (b_{ij}+B_{ij}(x))\,\partial_{ij}f(x) - (c+\langle\gamma,x\rangle)f(x) + \int (f(x+\xi)-f(x))\,m(d\xi) + \int \big(f(x+\xi)-f(x)-\langle\chi(\xi),\nabla f(x)\rangle\big)\,M(x,d\xi),$$

with $A_{ijkl}(x) = x_{ik}\alpha_{jl}+x_{il}\alpha_{jk}+x_{jk}\alpha_{il}+x_{jl}\alpha_{ik}$. In addition, $\varphi,\psi$ solve $\partial_t\varphi = F(\psi)$, $\varphi(0,u)=0$, $\partial_t\psi = R(\psi)$, $\psi(0,u) = u$, with

$$F(u) = \langle b,u\rangle + c - \int (e^{-\langle u,\xi\rangle}-1)\,m(d\xi),\qquad R(u) = -2u\alpha u + B^\top(u) + \gamma - \int \frac{e^{-\langle u,\xi\rangle}-1+\langle\chi(\xi),u\rangle}{\|\xi\|^2\wedge1}\,\mu(d\xi).$$

Milestones, in attack order

1. Lemma 3.1 and Lemma 3.3: order-preserving, continuous, analytic semiflows map $S_d^{++}$ into $S_d^{++}$.
2. Lemma 3.2: semiflow identities, monotonicity, continuity and analyticity of $\varphi,\psi$.
3. Proposition 3.4: Feller and regular.
4. Lemmas 4.1 and 4.4: zero divisors in the cone, and linear extension of additive maps.
5. Proposition 4.9: $F,R$ have the form (2.16)–(2.17) with $b\in S_d^+$.
6. Lemma B.2 and Theorem B.3: exponentials lie in $\mathcal S_+$ and span a dense subspace.
7. Proposition 4.12: the generator formula (2.12) on $\mathcal S_+$.
8. Lemma 4.17 and Proposition 4.18: derivatives of $\det$ at diagonal matrices, and the drift condition $b\succeq(d-1)\alpha$.

Significance

The result. Theorem 2.4 reduces the study of affine processes on $S_d^+$ to finitely many parameters. Any such process, a priori specified only through its Laplace transform, has the Lévy–Khintchine-type generator (2.12), its Laplace exponents solve the Riccati system, and its parameters obey the admissibility conditions. The drift condition $b\succeq(d-1)\alpha$ is the matrix analogue of the Feller condition, and for $d\ge2$ it excludes affine diffusions on $S_d^+$ with zero constant drift. The Feller property yields càdlàg versions, and the generator formula is the starting point for the semimartingale description and for the converse existence result.

Formalizing it. The theorem is proved in the paper, and this mission produces a machine-checked version of the necessity direction. Along the way it builds reusable infrastructure: a Lean model of Markov transition families on a cone, Feller semigroups on $C_0$ of a closed cone, generators on Schwartz-type test spaces with the symmetric-matrix derivative convention, and the positive semidefinite cone's order and boundary facts. No machine-checked proof of this theorem, or of its $\mathbb R_+^m\times\mathbb R^n$ predecessor, is known to exist.

Difficulty

The definition assumes only stochastic continuity and the exponential-affine form of the Laplace transform; differentiability in time is not given. Obtaining regularity, and hence the Riccati equations, needs the positivity statement of Lemma 3.3. Its proof uses analyticity in $u$ and the boundary geometry of $S_d^+$. Identifying $F$ and $R$ requires Lévy–Khintchine representations on cones and on $S_d$, and a convergence theorem for Laplace transforms. The admissibility conditions on the boundary come from support considerations at each boundary point. The drift condition (2.4) is not captured by the conditions read off from Laplace exponents at boundary points along single directions; it is a genuinely matrix-valued constraint coupling $b$ and $\alpha$. Extending the generator formula from exponentials to all of $\mathcal S_+$ needs a density result in a Fréchet topology and the closedness of the generator.

Formalization scope

• Matrices are Fin d → Fin d → ℝ, with $\langle x,y\rangle=\sum x_{ij}y_{ji}$ and $\|x\|=\langle x,x\rangle^{1/2}$. Mathlib's positive semidefiniteness, which includes symmetry over $\mathbb R$, defines $S_d^+$. The state space is the subtype $S_d^+$ with its subspace topology and Borel $\sigma$-algebra.
• Transition families are Mathlib kernels indexed by $t\in\mathbb R$ and constrained only for $t\ge0$. Sub-stochasticity encodes the cemetery. Stochastic continuity is convergence of integrals of bounded continuous functions as $s\to t$ within $[0,\infty)$.
• The exponents $\varphi,\psi$ are functions on $\mathbb R\times M_d$, used at $t\ge0$ and positive semidefinite arguments. Analyticity on $S_d^{++}$ is analyticity of $y\mapsto\psi(t,(y+y^\top)/2)$ on an open subset of $M_d$.
• The matrix measure $\mu$ is encoded as $H\,d\nu$ with $\nu$ finite and $H$ positive semidefinite and integrable. This loses nothing, since $\nu = \sum_i\mu_{ii}$ dominates every $\mu_{ij}$.
• $\mathcal S_+$ is the set of restrictions of Schwartz functions on $M_d$. Partial derivatives $\partial/\partial x_{ij}$ of functions on $S_d$ are taken in the direction $\tfrac12(E^{ij}+E^{ji})$, per §1.2 of the paper. Lemma 4.17 alone uses raw entry derivatives of $\det$ on $M_d$, as its proof does.
• The Feller property uses the platform definition EthierKurtz.IsStronglyContinuousContractionSemigroup on $C_0(S_d^+)$. "$f\in D(\mathcal A)$ and $\mathcal Af=g$" is uniform convergence of $(P_tf-f)/t$ to $g$ on $S_d^+$.
• Lean assigns the value $0$ to the integral of a non-integrable function. Wherever a statement concludes a formula containing an integral, it therefore also concludes integrability of the integrand, so the formula cannot hold through this default value. Regularity and the Feller property are conclusions, never hypotheses, of the goal. The drift condition (2.4) is part of admissibility in the goal; Propositions 4.9, 4.12 and 4.18 use admissibility without (2.4) and $b\in S_d^+$, as in the paper.
• Contributions are welcome on any milestone. The matrix lemmas (3.1, 3.3, 4.1, 4.4, 4.17) are self-contained, and Lemma B.2 and Theorem B.3 concern only Schwartz functions.

Selected references

• C. Cuchiero, D. Filipović, E. Mayerhofer, J. Teichmann, Affine processes on positive semidefinite matrices, Ann. Appl. Probab. 21 (2011) 397–463; cited as arXiv:0910.0137v3. https://arxiv.org/abs/0910.0137
• D. Duffie, D. Filipović, W. Schachermayer, Affine processes and applications in finance, Ann. Appl. Probab. 13 (2003) 984–1053. https://doi.org/10.1214/aoap/1060202833
• M. Keller-Ressel, W. Schachermayer, J. Teichmann, Affine processes are regular, Probab. Theory Related Fields 151 (2011) 591–611. https://arxiv.org/abs/0906.3392
• M.-F. Bru, Wishart processes, J. Theoret. Probab. 4 (1991) 725–751. https://doi.org/10.1007/BF01259552