Probability

Motivation

Mixing is the basic notion of asymptotic independence in ergodic theory: a measure-preserving transformation $T$ is mixing if the event $A$ at time $0$ and the event $B$ at time $n$ become independent as $n\to\infty$. Mixing of order $k$ asks the same for $k$ events at times whose gaps all tend to infinity. In 1949 Rokhlin introduced higher-order mixing and asked whether mixing (order $2$) already implies mixing of order $3$, and hence of all orders. The question has been one of the oldest in ergodic theory. It matters because higher-order mixing is the property used to prove multiple recurrence and independence statements, and because for actions of $\mathbb Z^2$ the analogous implication is false.

Timeline

• 1949. Rokhlin introduces higher-order mixing, proves it for ergodic endomorphisms of compact abelian groups, and raises the question for general transformations (mathnet).
• 1967. Furstenberg introduces joinings and disjointness, the language in which failure of higher-order mixing appears as a non-product pairwise-independent joining (doi:10.1007/BF01692494).
• 1978. Ledrappier gives a mixing $\mathbb Z^2$-action that is not mixing of order $3$ (Un champ markovien peut être d'entropie nulle et mélangeant, C. R. Acad. Sci. Paris).
• 1984. Kalikow proves that twofold mixing implies threefold mixing for rank-one transformations (doi:10.1017/S014338570000242X).
• 1991. Host proves mixing of all orders for mixing systems with singular spectrum (doi:10.1007/BF02773866).
• 1993. Ryzhikov proves mixing of all orders for mixing finite-rank actions (doi:10.1007/BF01085983).
• 2006. de la Rue explains why Ledrappier-type "three-dot" counterexamples cannot exist in one dimension (doi:10.1007/s00574-006-0024-z).
• 2008. Janvresse and de la Rue show that certain pairwise-independent joinings force positive entropy (doi:10.1017/S0143385707000958).
• 2024. Bergelson and Zelada show that strongly mixing systems are mixing of all orders along a large set of layouts (doi:10.1017/etds.2023.63); Kanigowski and Ravotti prove multiple mixing for shearing flows (arXiv:2410.13686); Ryzhikov surveys 75 years of the problem (arXiv:2411.07234).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims an affirmative answer for a single invertible transformation.

Setting

Let $(\Omega,\mathcal F,\mu)$ be a probability space and $T:\Omega\to\Omega$ an invertible measurable map with measurable inverse that preserves $\mu$. $T$ is mixing if for all $A,B\in\mathcal F$

$$\mu(A\cap T^{-n}B)\longrightarrow\mu(A)\,\mu(B)\qquad(|n|\to\infty,\ n\in\mathbb Z).$$

For $k\ge2$, $T$ is mixing of order $k$ if for all $A_1,\dots,A_k\in\mathcal F$

$$\mu\Bigl(\bigcap_{i=1}^{k}T^{-t_i}A_i\Bigr)\longrightarrow\prod_{i=1}^{k}\mu(A_i)$$

whenever $t_1<\dots<t_k$ and $\min_i(t_{i+1}-t_i)\to\infty$; by invariance one may take $t_1=0$. The order counts the number of sets (so order $k$ is "multiplicity $k-1$" in Rokhlin's and Ryzhikov's convention).

Formalization targets

Goal: Theorem 1.1

If $T$ is an invertible mixing probability-preserving transformation, then for every $k\ge3$ and all measurable $A_1,\dots,A_k$,

$$\mu\bigl(A_1\cap T^{-n_1}A_2\cap\cdots\cap T^{-(n_1+\cdots+n_{k-1})}A_k\bigr)\longrightarrow\prod_{i=1}^{k}\mu(A_i)\quad\text{as}\ \min(n_1,\dots,n_{k-1})\to\infty,$$

the $n_i$ ranging over positive integers. No standardness or countable-generation assumption is made on $(\Omega,\mathcal F,\mu)$. The Lean statement OAI.Rokhlin.mixing_all_finite_orders is open on the platform.

Significance

The theorem resolves Rokhlin's multiple-mixing problem for one transformation: mixing implies mixing of all orders, with no structural hypothesis (rank, spectrum, algebraic form). It explains the difference between $\mathbb Z$ and $\mathbb Z^2$: Ledrappier's example shows the implication fails for several commuting generators. The paper also derives the conclusion for mixing endomorphisms and for mixing flows with strongly continuous Koopman operators (Corollary 8.1).

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. Given the age and prominence of the problem, an independent formal verification would be valuable.

Difficulty

A failure of threefold mixing produces, in the limit, a joining of three copies of the system that is pairwise independent but not the product. Pairwise independence alone does not force a joining to be a product, so soft joining arguments do not suffice; earlier positive results used rank, spectral or algebraic structure to exclude such joinings. A reduction to zero entropy is available (positive-entropy parts are handled separately), but in zero entropy the non-product joining must be ruled out with no structural information about $T$. In addition, the general (non-standard) probability space prevents direct use of disintegration and Rokhlin–Halmos-type tools without first reducing to a separable factor.

Formalization scope

• $\Omega$ carries an arbitrary MeasurableSpace; $\mu$ has IsProbabilityMeasure; $T$ is a MeasurableEquiv with MeasurePreserving T μ μ.
• timeMap T n is the $n$-th power of $T$ as a permutation, $n\in\mathbb Z$; IsMixing μ T uses the filter comap Int.natAbs atTop on $\mathbb Z$.
• MixingOfOrder μ T k: for every family of measurable sets indexed by Fin k, the measure of $\bigcap_i T^{-\mathrm{layoutTime}(i)}A_i$ tends to $\prod_i\mu(A_i)$ along atTop on Fin (k-1) → ℕ+, where layoutTime gives the partial sums of the gaps.
• The theorem is stated for every $k\ge3$; the case $k=2$ is the hypothesis.

A complete development needs joinings, factor maps and entropy (Pinsker factor), measurable selection or a reduction to standard spaces, and the paper's array and operator machinery. Contributions formalizing the reduction steps (Proposition 2.1, zero-entropy witness) or classical special cases (Kalikow's rank-one theorem) are welcome.

Selected references

• OpenAI, Rokhlin's multiple-mixing problem for one transformation, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Rokhlins-multiple-mixing-problem-for-one-transformation-September-23-2026/paper.pdf
• V. A. Rokhlin, On endomorphisms of compact commutative groups, Izv. Akad. Nauk SSSR Ser. Mat., 1949. https://www.mathnet.ru/eng/im3198
• T. de la Rue, 2-fold and 3-fold mixing: why 3-dot-type counterexamples are impossible in one dimension, Bull. Braz. Math. Soc., 2006. https://doi.org/10.1007/s00574-006-0024-z
• S. A. Kalikow, Twofold mixing implies threefold mixing for rank one transformations, Ergodic Theory Dynam. Systems, 1984. https://doi.org/10.1017/S014338570000242X
• B. Host, Mixing of all orders and pairwise independent joinings of systems with singular spectrum, Israel J. Math., 1991. https://doi.org/10.1007/BF02773866
• V. V. Ryzhikov, Joinings and multiple mixing of finite rank actions, Funct. Anal. Appl., 1993. https://doi.org/10.1007/BF01085983
• V. V. Ryzhikov, Multiple mixing, 75 years of Rokhlin's problem, preprint, 2024. https://arxiv.org/abs/2411.07234
• H. Furstenberg, Disjointness in ergodic theory, minimal sets, and a problem in Diophantine approximation, Math. Systems Theory, 1967. https://doi.org/10.1007/BF01692494

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

Motivation

In the local model of differential privacy, no trusted curator holds the data: each individual randomizes their own record before handing it to the analyst. This is the model of randomized response in survey statistics and of the privacy-preserving telemetry deployed by large software vendors. 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), asked which learning tasks remain possible in this model. Their answer (§5) is that local algorithms are exactly as powerful as statistical query (SQ) algorithms in the sense of Kearns (J. ACM 1998), up to polynomial factors. This mission formalizes one direction of that equivalence: every local algorithm run on i.i.d. data can be simulated by an SQ algorithm.

This is the fourth of five missions on the paper. Mission III formalizes the converse direction (Theorem 5.7). All theorem numbers refer to arXiv:0803.0924v3.

Setting

A database is $z=(z_1,\dots,z_n)\in D^n$. Here its entries are drawn i.i.d. from a probability distribution $P$ on $D$.

• An $\varepsilon$-local randomizer (Definition 5.1) is a randomized map $R:D\to W$ to a discrete set $W$ such that $\Pr[R(u)=w]\le e^{\varepsilon}\Pr[R(u')=w]$ for all $u,u'\in D$ and $w\in W$.
• An $\varepsilon$-local algorithm $A$ making $t$ queries (Definitions 5.2, 5.3) sees the database only through an LR oracle. At its $k$-th call it names an index $i_k$ and an $\varepsilon_k$-local randomizer $R_k$, both possibly depending on its earlier answers, and receives a fresh sample of $R_k(z_{i_k})$. For each index $i$ the budgets of the calls on $i$ sum to at most $\varepsilon$. $A$ is noninteractive if its calls do not depend on earlier answers. Its output is a function of the $t$ answers. Its output distribution is taken over $z\sim P^n$ and the randomizers' coins.
• An SQ oracle for $P$ (Definition 5.4) answers a query $(g,\tau)$, with $g:D\to[-1,1]$ and tolerance $\tau$, with any number $v$ such that $|v-\mathbb E_{u\sim P}[g(u)]|\le\tau$. It may choose its answers adversarially and adaptively.
• An SQ algorithm $B$ (Definition 5.5) accesses $P$ only through such an oracle. It may use its own coins, and the number of queries it makes may be random and unbounded.
• The statistical difference of two distributions on a discrete space (p. 8) is $\max_S|\mu(S)-\nu(S)|$.

Formalization targets

Goal: Lemma 5.8 (p. 21)

There is an absolute constant $C$ such that for every $\varepsilon$-local algorithm $A$ making $t$ queries there is an SQ algorithm $B$ with the following properties against every distribution $P$ and every valid oracle:

$$\tau=\frac{\beta}{3e^{2\varepsilon}t},\qquad \mathbb E[\#\text{queries of }B]\le C\,t\,e^{\varepsilon},\qquad \mathrm{SD}\bigl(B,\ A(z),\ z\sim P^n\bigr)\le\beta .$$

The constant $C$ is the paper's $O(\cdot)$. The tolerance is the proof's own choice.

Milestones

1. Display (5) (p. 22): a single query estimates $p(w)=\Pr_{z_i\sim P}[R(z_i)=w]$ within a factor $1\pm\beta/(3t)$, whatever valid answer the oracle gives.
2. One rejection-sampling iteration (p. 23): every iteration terminates with probability at least $\frac{1-\varphi}{1+\varphi}e^{-\varepsilon}$. Conditioned on terminating, it outputs $w$ with probability in $(1\pm3\varphi)p(w)$.
3. The interactive estimate (p. 24): two queries estimate the conditional probability of the next answer given earlier answers on the same entry, within a factor $1\pm3e^{2\varepsilon}\tau$.
4. Claim 5.9 (p. 22): the noninteractive case, with the explicit bound $2t\,e^{\varepsilon}$ on the expected number of queries.

Significance

The result. Lemma 5.8, combined with Theorem 5.7, shows that a concept class is learnable by a locally private algorithm if and only if it is learnable with statistical queries (Theorem 5.14). Every SQ lower bound therefore becomes a lower bound for local privacy. For instance, parity functions are privately learnable by a centralized algorithm (Theorem 4.4) but not by a local one, because parities need exponentially many statistical queries (Corollary 5.15, which also uses the SQ lower bound of Blum et al., STOC 1994).

Formalizing it. The result is proved on paper. As far as we know it has no machine-checked proof. The paper's proof is a few paragraphs and leaves the model implicit: what an SQ algorithm with a random number of queries is, how an adversarial oracle interacts with it, and in what sense the per-randomizer errors add up over $t$ adaptively chosen randomizers. The formal statement makes each of these explicit. The milestones isolate the estimates the proof uses, so they can be proved independently of the composition argument.

Difficulty

The estimates in the milestones are elementary inequalities. The difficulty is in the goal. First, the oracle's answers, and therefore the estimates $\tilde p(w)$, change from iteration to iteration, so the simulated distribution is not a fixed rejection sampler: the output law must be controlled iteration by iteration against an adversary. Second, the SQ algorithm has no bound on its number of steps. Its output law is a limit over an unbounded run, and its query count is an expectation that is finite only because every iteration terminates with probability bounded away from zero. Third, in the interactive case the randomizers applied to one entry are correlated through the entry. The simulation must sample from the conditional law given earlier answers on that entry, while the errors of all $t$ steps combine along adaptively chosen histories.

Formalization scope

• Local randomizers have discrete output: R u : PMF W. The simulation uses the point probabilities $\Pr[R(z_i)=w]$. Every map $u\mapsto\Pr[R(u)=w]$ is required to be measurable.
• A local algorithm makes exactly $t$ calls. Its index, randomizer and budget at call $k$ are functions of the earlier answers. The budget is required along every answer sequence. Its own coins are calls to $0$-local randomizers.
• An SQ algorithm is a state machine with a random start, random transitions depending on the answer, and an output on stopping. Its output law is a sub-probability mass function. Its expected query count lies in $[0,\infty]$ and counts every query, including those in rejected iterations.
• The oracle is an arbitrary deterministic function of the whole state trajectory, constrained only by Definition 5.4. The conclusions must hold for every valid oracle, not for the exact-mean oracle alone.
• $B$ is quantified before $P$ and sees $P$ only through answers, and every query of $B$ is a measurable $[-1,1]$-valued function with tolerance exactly $\beta/(3e^{2\varepsilon}t)$. Without these two constraints the statement would be trivial: $B$ could hard-code $P$, or rescale a query to shrink its effective tolerance.
• The constant $C$ is quantified outside every other object.
• The implicit hypotheses $\varepsilon>0$ (the queries divide by $e^{\varepsilon}-e^{-\varepsilon}$), $0<\beta\le1$ and $t\ge1$ (so that $\varphi=\beta/(3t)\le1/3$ and $\tau$ is defined) are stated. The paper's reference input $\mathbf 0$ is an arbitrary point $u_0\in D$.
• Claim 5.9 states "$t\cdot e^{\varepsilon}$ queries". Its proof gives at most $2t\,e^{\varepsilon}$, which is the bound stated.
• The paper's refinement "noninteractive $A$ yields nonadaptive $B$" is not formalized. The simulation decides from each answer whether to stop, and so which randomizer the next query belongs to. It therefore does not prepare its queries before receiving answers in the sense of Definition 5.5. The goal is the adaptive statement for all local algorithms, which contains the noninteractive case. Claim 5.10, whose statement coincides with this goal, is represented by its estimate (milestone 3) rather than restated.
• The statistical difference is valued in $[0,\infty]$, which avoids junk values of a real supremum.

Reusable beyond this mission: the SQ-algorithm state machine with expected query count, the statistical difference of sub-probability mass functions, and the model of interactive local algorithms. Welcome contributions include proofs of the estimate milestones, a general lemma bounding the statistical difference of sequentially composed approximate samplers, and the termination and expected-runtime analysis of rejection sampling with varying acceptance probabilities.

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; cited from arXiv:0803.0924v3. https://arxiv.org/abs/0803.0924 · https://doi.org/10.1137/090756090
• M. Kearns, Efficient noise-tolerant learning from statistical queries, J. ACM 45(6) (1998) 983–1006. https://doi.org/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, 253–262. https://doi.org/10.1145/195058.195147
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating noise to sensitivity in private data analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• S. L. Warner, Randomized response: a survey technique for eliminating evasive answer bias, J. Amer. Statist. Assoc. 60 (1965) 63–69. https://doi.org/10.1080/01621459.1965.10480775