All missions

Motivation

This mission develops Chapter 8 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

This is Proposition 8.34 of Nannicini, the end-to-end cost of the quantum mirror-descent solver for the MaxCut SDP relaxation, stated in an explicit hybrid classical–quantum QRAM cost model.

Let $n=2^q$. For a nonzero real symmetric $C\in\mathbb R^{n\times n}$ put $\hat C=C/\|C\|_F$. Call a density matrix $\rho\in\mathbb C^{n\times n}$ an $\epsilon$-solution of (MaxCutSDP) if

$$\sum_{j=1}^n\Big|\rho_{jj}-\frac1n\Big|\le\epsilon\qquad\text{and}\qquad \operatorname{Tr}(\hat C\rho)\ \ge\ \operatorname{Tr}(\hat C\sigma)-\epsilon\ \text{ for every density matrix }\sigma\text{ with }\operatorname{diag}(\sigma)=\tfrac1n\mathbb 1.$$

A hybrid algorithm consists of (i) a classical preprocessing program, a straight-line program of real arithmetic operations ($+,-,\times,\div,\sqrt\cdot,\arccos,\arg$, rational constants), which is the only part that reads the entries of $C$ and which writes the input half of a QRAM ($U_{\mathrm{QRAM}}|j\rangle|y\rangle=|j\rangle|y\oplus M_j\rangle$, Def. 5.39); (ii) $R$ quantum runs, each applying a circuit of two-qubit gates and QRAM calls to $|0\cdots0\rangle$ and measuring all qubits, where the circuit of each run and the contents of the work half of the QRAM are chosen classically from the outcomes of the earlier runs; (iii) an output, computed from all outcomes, in the form of a list of pairs $(y^{(i)},d^{(i)})\in\mathbb R^2\times\mathbb R^n$, which stands for the matrix

$$\bar\rho=\frac1{L}\sum_{i=1}^{L}\frac{\exp\big(y^{(i)}_1\hat C+y^{(i)}_2\operatorname{diag}(d^{(i)})\big)}{\operatorname{Tr}\exp\big(y^{(i)}_1\hat C+y^{(i)}_2\operatorname{diag}(d^{(i)})\big)}.$$

The theorem: there are absolute constants $K>0$ and $c$ such that for all $q$, all $\epsilon\in(0,1]$ and all $\delta\in(0,1)$, with $\Lambda=\log(2+n)+\log(2+1/\epsilon)+\log(2+1/\delta)$, there is a hybrid algorithm, fixed before $C$, such that

1. the QRAM has size at most $K n^2\Lambda^c$, with words of at most $K\Lambda^c$ bits;
2. the preprocessing uses at most $K n^2\Lambda^c$ classical operations;
3. along every measurement record the total number of QRAM accesses and additional gates is at most $K\,\dfrac{n^{1.5}}{\epsilon^5}\Lambda^c$;
4. for every nonzero real symmetric $C$, with probability at least $1-\delta$ the output $\bar\rho$ is an $\epsilon$-solution of (MaxCutSDP).

The proposition is the payoff of the chapter's MaxCut analysis: the subgradient estimation of Prop. 8.28, the iteration count of Thm. 8.30 and the Hamiltonian structure of Lem. 8.33 combine into a quantum solver whose quantum cost is sublinear in the $n^2$ entries of $C$.

Formalization Note The printed proposition has no cost model, no success probability, and no precise meaning for the tolerance over the binary search on $\gamma$; these are fixed as above. The classical bookkeeping between quantum runs (tallying samples, forming the subgradients, updating $y$ and $D$) is not counted, matching the proof, which takes the classical cost from Prop. 7.29 alone; that bookkeeping never sees $C$. The output is the source's own representation of the iterate (Rem. 8.27, Lem. 8.33): with an arbitrary decoder, the optimum could be read off $\hat C$ for free.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Proposition 8.7: Entropic mirror descent iterates are the Gibbs states of the accumulated subgradients.
• Theorem 8.10: Regret bound of the matrix multiplicative weights update.
• Lemma 8.12: Emptiness of the PIC polytope certifies primal feasibility after rescaling.
• Theorem 8.15: Algorithm 7 (MMWU for SDP) returns a primal or a dual certificate.
• Proposition 8.19: The generalized PIC polytope built from θ-accurate traces is sandwiched between P_0 and P_{4Rrθ}.
• Proposition 8.21: Computing the dual vector with Õ(√m) calls to a trace-estimate oracle (corrected statement).
• Proposition 8.28: The estimated MaxCut subgradient is an ϵ/2-subgradient (corrected zero branch).
• Lemma 8.29: A subgradient of the active piece at a nearby point is an approximate subgradient of the max.
• Theorem 8.30: Convergence of inexact entropic mirror descent for the MaxCut SDP feasibility problem.
• Lemma 8.33: The MaxCut mirror-descent Hamiltonians are y₁Ĉ + y₂D with ‖y‖₁ ≤ (4/ϵ) log n.
• Proposition 8.34: End-to-end complexity of the quantum MaxCut SDP solver in the QRAM model (corrected statement).

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Giacomo Nannicini, Quantum algorithms for optimizers, 2025, v5; notes dated 9 July 2025. https://arxiv.org/pdf/2408.07086v5.

Motivation

This mission develops Chapter 2 of An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

An $[[n,k,d]]$ code is a subspace $C$ of $(\mathbb C^2)^{\otimes n}$ of dimension $2^k$ such that every operator $E$ acting on at most $d-1$ qubits satisfies $\langle\psi|E|\psi\rangle=c'(E)$ for all unit vectors $|\psi\rangle\in C$, with $c'(E)$ independent of $|\psi\rangle$ (eq. (34)); that is, $C$ has distance at least $d$. Put $t=\lfloor (d-1)/2\rfloor$. The code is nondegenerate if, for every unit vector $|\psi\rangle\in C$, the Gram matrix $\big(\langle\psi|P_a^\dagger P_b|\psi\rangle\big)_{a,b}$ over the phase-free Pauli operators $P_a$ of weight at most $t$ is nonsingular. Let $H(x)=-x\log_2x-(1-x)\log_2(1-x)$.

1. (Quantum Gilbert–Varshamov bound.) If $d\ge1$ and

$$\Big(\sum_{j=0}^{d-1}3^j\binom nj\Big)2^k\le 2^n,$$

then an $[[n,k,d]]$ code exists. 2. (Quantum Hamming bound.) Every nondegenerate $[[n,k,d]]$ code satisfies

$$\Big(\sum_{j=0}^{t}3^j\binom nj\Big)2^k\le 2^n.$$

3. (Asymptotic rates.) Let $0<p<1/2$ and $\varepsilon>0$. There is $N$ such that for every $n\ge N$:
   • every nondegenerate $[[n,k,d]]$ code with $d\ge 2pn$ has $k/n\le 1-p\log_2 3-H(p)+\varepsilon$;
   • if $1-2p\log_2 3-H(2p)>0$, there is a nondegenerate $[[n,k,d]]$ code with $d\ge 2pn$ and $k/n\ge 1-2p\log_2 3-H(2p)-\varepsilon$.

The first two bounds are counting arguments. The third gives the rate window, eq. (37), between which the best nondegenerate codes lie.

Formalization Note The source's 'distance $d$' is read as distance at least $d$, so existence is meaningful also for $k=0$. The hypothesis $d\ge1$ excludes $d=0$, where (36) is an empty sum and the claim would demand a $2^k$-dimensional code for every $k$. The asymptotic clause is read as an $\varepsilon$–$N$ statement. The lower rate bound is asserted only when it is positive.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Theorem 1: No-Cloning: no quantum operation copies every state.
• Theorem 2: Correctable errors are closed under linear combinations; weight-t Pauli errors give all t-qubit errors.
• Theorem 3: Knill–Laflamme condition for quantum error correction.
• Theorem 4: Quantum Gilbert–Varshamov, quantum Hamming, and asymptotic rate bounds.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1. https://arxiv.org/pdf/0904.2557v1.

Motivation

This mission develops Chapter 7 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

Fix constants $C_0 \in \mathbb{R}$ and $c_0 \in \mathbb{N}$ (those of the assumption $p = \widetilde{O}(1)$). There are constants $C > 0$ and $c \in \mathbb{N}$ such that the following holds. Let $q, p \in \mathbb{N}$, $d = 2^q$, $\xi > 0$, write $L = \log(2+d) + \log(2+1/\xi)$, and assume $p \le C_0 L^{c_0}$. Then there exist

1. a QRAM (Def. 5.39) with $2^b$ addresses and words of $r$ bits, of size $2^b r \le C d^2 (p+1) L^c$;
2. a straight-line real-arithmetic program of at most $C d^2 L^c$ operations ($+, -, \times, \div, \sqrt{\cdot}, \arccos$, complex argument, rational constants) and an addressing map, which compute the QRAM contents from the entries of the matrix;
3. a quantum circuit $\mathcal{V}$ on $w + q$ qubits with $w \le C (q+1) L^c$, making at most $C L^c$ uncontrolled calls to the QRAM (or its inverse) and using at most $C L^c$ two-qubit gates,

all independent of the matrix, such that for every $A \in \mathbb{C}^{d\times d}$ whose entries satisfy $|\operatorname{Re} a_{ij}|, |\operatorname{Im} a_{ij}| \le 2^p$, the unitary $\mathcal{V}(U_{\mathrm{QRAM}}(A))$ obtained with the QRAM loaded by the program is an $(\|A\|_F, w, \xi)$-block-encoding of $A$:

$$\bigl\| \|A\|_F\,(\langle 0|_w \otimes I)\,\mathcal{V}\,(|0\rangle_w \otimes I) - A \bigr\| \le \xi .$$

This is the data-structure route to block-encodings of classically stored dense matrices, with subnormalization the Frobenius norm and only polylogarithmic quantum cost.

Formalization Note Corrected statement. The source gives no cost model for classical arithmetic, does not say in which parameters $p$ is polylogarithmic, and does not say how the costs depend on $\xi$. Here classical cost is the length of a straight-line real-arithmetic program (the model of the Cor. 5.45 chunk), $p = \widetilde{O}(1)$ means $p \le C_0 L^{c_0}$ for arbitrary $C_0, c_0$, all $\widetilde{O}$ bounds are polylogarithmic in $d$ and $1/\xi$, and the QRAM size is $\widetilde{O}(d^2 p)$ rather than $O(d^2 p)$ because the word size must grow with $\log(1/\xi)$. A $p$-bit entry is modelled by the magnitude bound $2^p$ on its real and imaginary parts.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Proposition 7.9: Iterative refinement reaches residual ϵ in O(log 1/ϵ) iterations.
• Proposition 7.14: Product of block-encodings (error term corrected).
• Proposition 7.18: Linear combination of block-encodings (error term corrected for α < 1).
• Lemma 7.20: Block-encoding of the diagonal matrix of inner products ⟨ϕ_j|ψ_j⟩.
• Proposition 7.21: Block-encoding from sparse-access oracles (rotation cost and entry encoding made explicit).
• Lemma 7.37: A bounded polynomial of degree Õ(β) approximating exp(2βx)/4 on [−1, 0].
• Lemma 7.39: Block-encoding a density matrix from a unitary preparing its purification.
• Proposition 7.41: One-copy trace estimator: a random variable with bias ≤ θ/4 for Tr(Aρ) and constant variance.
• Proposition 7.38: Gibbs-state preparation from a block-encoding of H, for the polynomial of Lemma 7.37 made explicit.
• Proposition 7.29: A (‖A‖_F, Õ(q), ξ)-block-encoding of a classical matrix from QRAM, with an explicit cost model.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Giacomo Nannicini, Quantum algorithms for optimizers, 2025, v5; notes dated 9 July 2025. https://arxiv.org/pdf/2408.07086v5.

Motivation

This mission develops Chapter 5 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

This is a corrected form of the quantum construction of a separation oracle from a membership oracle.

Quantum membership oracle. Points of $\mathbb{R}^d$ are written in an $m$-qubit register through an encoding $p \mapsto \mathrm{enc}(p)$. A quantum oracle implementing $\mathrm{MEM}_{0,\epsilon'}(K)$ is a unitary $O$ acting on the point register, an answer qubit and $k$ workspace qubits. On every basis point it acts as

$$O\,|p\rangle|0\rangle|0^k\rangle = |p\rangle|\varphi_p\rangle ,$$

where measuring the answer qubit of $\varphi_p$ returns the correct membership bit $[\mathrm{enc}(p) \in K]$ with probability at least $1-\epsilon'$.

Separation oracle. $\mathrm{SEP}_{\epsilon,\delta}(x)$ (Definition 5.22) must, with probability at least $1-\delta$, either assert $x \in B_2(K,\epsilon)$ or return a unit vector $g$ with $\langle g, y\rangle \le \langle g, x\rangle + \epsilon$ for all $y \in B_2(K,-\epsilon) = \{y : B_2(y,\epsilon) \subseteq K\}$.

Theorem. There are absolute constants $C > 0$ and $c \in \mathbb{N}$ with the following property. Let $d \in \mathbb{N}$ and $r, R, \epsilon, \delta \in \mathbb{R}$ with $0 < r < R$, $0 < \epsilon < R$ and $0 < \delta < 1/3$. Then there is $\epsilon' > 0$ such that for every $x \in \mathbb{R}^d$ there exist an encoding $\mathrm{enc}$ and, for every workspace size $k$, a quantum circuit with measurement decoding. The circuit makes at most

$$C\,\bigl(\log(2+d) + \log(2+R) + \log(2+1/r) + \log(2+1/\epsilon) + \log(2+1/\delta)\bigr)^{c}$$

uncontrolled calls to the oracle or its inverse. It correctly implements $\mathrm{SEP}_{\epsilon,\delta}(x)$ for every convex $K$ with $B_2(0,r) \subseteq K \subseteq B_2(0,R)$ and $x \notin B_2(K,-\epsilon)$, and for every unitary implementing $\mathrm{MEM}_{0,\epsilon'}(K)$.

Classically, separation from membership needs $\tilde O(d)$ membership calls. This result gives an exponential improvement in the dimension for the query complexity of convex optimization with a membership oracle.

Formalization Note The source leaves several objects open: the unitary implementing $\mathrm{MEM}$, the value of $\epsilon'$, and the parameters hidden in $\tilde O(1)$. The statement makes each of them explicit. The unit-norm requirement on $g$ is added because Definition 5.22 as printed accepts $g = 0$, which would make the separation oracle trivial.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Proposition 5.3: Jordan's gradient circuit recovers the gradient of an exactly representable linear function.
• Proposition 5.6: The gradient algorithm for approximately linear functions.
• Proposition 5.16: A Hadamard-test circuit is a probability oracle for (1 + Re⟨ψ|ϕ_x⟩)/2.
• Corollary 5.18: Pure-state tomography with Euclidean error using Õ(d/ϵ) uses of U.
• Proposition 5.25: Properties of the height function: convexity, Lipschitz continuity, and separation from an ϵ̄-subgradient (corrected).
• Lemma 5.28: The central-difference gradient is within (η/2)Δ^(η)f(x) of every subgradient.
• Lemma 5.30: The Laplace approximation is at most dL/r on average over a cube.
• Lemma 5.32: Deviation from the finite-difference linearization on the ℓ1 ball is at most (η²/2)Δ^(η)f(z).
• Proposition 5.31: Finite differences of an approximate function at a random point give an explicit ϵ′-subgradient at the origin (corrected).
• Proposition 5.36: Algorithm 4 (binary tree of controlled R_Y rotations) prepares the amplitude encoding of a real unit vector.
• Corollary 5.37: Amplitude encoding of a complex vector to error ϵ with Õ(d) gates from {H, T, CX}.
• Corollary 5.45: Amplitude encoding with O(log d) QRAM queries and O(log d (log d + log 1/ϵ)) two-qubit gates after Õ(d) classical preprocessing (corrected).
• Theorem 5.33: Separation oracle from polylogarithmically many calls to a quantum membership oracle (corrected).

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Giacomo Nannicini, Quantum algorithms for optimizers, 2025, v5; notes dated 9 July 2025. https://arxiv.org/pdf/2408.07086v5.

Motivation

This mission develops Chapter 4 of A Survey of Quantum Learning Theory by Srinivasan Arunachalam and Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

This is Aaronson's theorem on "pretty good tomography": an $n$-qubit state can be PAC-learned from linearly many (in $n$) measurement results.

An $n$-qubit state is a density matrix $\rho\in\mathbb C^{2^n\times 2^n}$ (positive semidefinite, trace $1$). A two-outcome measurement is an effect $E$, i.e. $0\preceq E\preceq \mathrm{Id}$; its first outcome has probability $\mathrm{Tr}(E\rho)$. Let $D$ be a probability distribution (Borel) on the set of effects.

There is a polynomial $p$ in three variables with nonnegative coefficients such that for every $n$ and all $\varepsilon,\gamma>0$, $\delta\in(0,1)$ there are a number

$$T\ \le\ n\cdot p\big(1/\varepsilon,\ 1/\gamma,\ \log(1/\delta)\big)$$

and a (measurable) learner $L$, mapping $T$ measurement results to an $n$-qubit density matrix, with the following property: for every $n$-qubit state $\rho$ and every distribution $D$, if $E_1,\dots,E_T$ are drawn i.i.d. from $D$ and, independently given the $E_i$, each $b_i$ is a bit with $\Pr[b_i=1]=\mathrm{Tr}(E_i\rho)$, then with probability at least $1-\delta$ the output $\sigma=L((E_1,b_1),\dots,(E_T,b_T))$ satisfies

$$\Pr_{E\sim D}\big[\,|\mathrm{Tr}(E\sigma)-\mathrm{Tr}(E\rho)|>\gamma\,\big]\ \le\ \varepsilon .$$

The learner knows neither $\rho$ nor $D$. Only the number of measurement results is bounded, not the running time.

Formalization Note "$T=n\cdot\mathrm{poly}$" is read as an upper bound on $T$ (a learner may ignore extra results). The condition $\delta<1$ is added: for $\delta\ge 1$ the claim is empty and $\log(1/\delta)\le 0$. The learner is deterministic and measurable; the probability of success is written out as an integral over $D^{T}$ of the probabilities of the bit strings.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• §4.1.1, Theorem 4.3: Servedio–Gortler: quantum exact learning needs Ω(max{1/√γ(C), log|C|/n}) queries.
• §4.1.1, Corollary 4.4: Servedio–Gortler: D(C) = O(n·Q(C)^3).
• §4.1.2, Theorem 4.5: Classical (N,M)-query complexity of exact learning is Θ(min{M,N}).
• §4.1.2, Theorem 4.6: Kothari: optimal quantum (N,M)-query complexity of exact learning.
• §4.1.2, Theorem 4.8: Kothari: quantum exact learning with O(√((1/γ)/log(1/γ))·log|C|) queries.
• Theorem 4.12: Quantum PAC learning needs Ω(d/ε + log(1/δ)/ε) quantum examples.
• Theorem 4.13: Diagonal of the square root of an XOR-invariant Gram matrix (corrected: with the factor 2^{-k/2}).
• Theorem 4.15: Quantum agnostic learning needs Ω(d/ε² + log(1/δ)/ε²) quantum examples.
• Theorem 4.16: Quantum states are PAC-learnable from n·poly(1/ε, 1/γ, log(1/δ)) measurement results.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Srinivasan Arunachalam and Ronald de Wolf, A Survey of Quantum Learning Theory, 2017, v3. https://arxiv.org/pdf/1701.06806v3.

Motivation

This mission develops Chapter 5 of An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

There exist an $[[n,1,2t+1]]$ code with fault-tolerant gadgets of a common depth (Definitions 2–5) and a threshold $p_T>0$ with the following property. For every $p$ with $0\le p<p_T$ there are constants $K>0$ and $c\in\mathbb N$ such that for every ideal circuit $C$ (Definition 6: preparation, $H$, $R_{\pi/8}$, CNOT, wait and measurement locations, no input) and every $\varepsilon>0$ there is a level $L$ for which the $L$-fold concatenated fault-tolerant simulation $C'=C^{(L)}$ satisfies

1. $\#\mathrm{qubits}(C')\le K\,\big(\log_2(2+|C|/\varepsilon)\big)^{c}\,\#\mathrm{qubits}(C)$ and $\#\mathrm{steps}(C')\le K\,\big(\log_2(2+|C|/\varepsilon)\big)^{c}\,\#\mathrm{steps}(C)$, where $|C|$ is the number of locations of $C$;
2. for every local stochastic error model on $C'$ (Definition 12) with error bounds $p_i\le p$, $p_i<1$,

$$d_{\mathrm{TV}}\big(\text{decoded output of } C',\ \text{output of } C\big)\le\varepsilon.$$

The output of $C'$ is decoded classically level by level. The threshold theorem shows that arbitrarily long quantum computations can be performed reliably with polylogarithmic overhead once the physical error rate is below a constant.

Formalization Note The fault-tolerant circuit is pinned to the concatenated circuit of the proof (p.42); an unconstrained circuit with free classical computation could sample the output of $C$ classically. $\mathrm{polylog}(x)$ is encoded as $K(\log_2(2+x))^c$, which is positive also for $x\le 1$.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• §5.1, Theorem 6: Good implies correct: an extended rectangle with at most t faults is correct.
• §5.2, Theorem 7: A fault-tolerant circuit with only good ExRecs has the ideal output distribution.
• §5.2, Lemma 2: *Correctness for the ideal decoder implies correctness for a -decoder.
• §5.2, Lemma 3: *A good truncated ExRec is correct for ideal decoders and -decoders.
• Theorem 8: A fault-tolerant circuit simulates the ideal circuit with errors at the bad ExRecs.
• Theorem 9: Level reduction: a local stochastic model on C′ induces one on C with bounds Σ_{|R|=t+1} Π p_j.
• Theorem 10: Threshold theorem: below p_T, concatenated circuits simulate C to distance ε with polylog overhead.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1. https://arxiv.org/pdf/0904.2557v1.

Motivation

The invariant subspace problem asks whether every bounded linear operator on an infinite-dimensional separable complex Hilbert space leaves some non-trivial closed subspace invariant. It is listed as a high-importance open problem in analysis in the Open Problem Garden (entry) and is widely regarded as one of the most famous open problems in functional analysis. Invariant subspaces are the infinite-dimensional replacement for eigenvectors: in finite dimensions every complex matrix has an eigenvector, and the structure theory of matrices (triangular and Jordan forms) is built from chains of invariant subspaces. Whether any such structure is available for an arbitrary bounded operator on Hilbert space is exactly what the problem asks.

Timeline

• 1930s (von Neumann, unpublished). Compact operators on Hilbert space have non-trivial closed invariant subspaces.
• 1954 (Aronszajn–Smith). The compact case on arbitrary Banach spaces (doi:10.2307/1969637).
• 1966 (Bernstein–Robinson; Halmos). Polynomially compact operators on Hilbert space.
• 1973 (Lomonosov). Every non-zero compact operator has a non-trivial closed hyperinvariant subspace; consequently every operator commuting with a non-zero compact operator has a non-trivial closed invariant subspace (doi:10.1007/BF01080698).
• 1975 announced / 1987 published (Enflo). A bounded operator on a separable Banach space with no non-trivial closed invariant subspace (doi:10.1007/BF02392260).
• 1985 (Read). Such an operator on the classical space $\ell^1$ (doi:10.1112/blms/17.4.305).
• 2011 (Argyros–Haydon). An infinite-dimensional Banach space on which every operator is a scalar plus a compact operator, so that every operator on it has a non-trivial closed invariant subspace (arXiv:0903.3921).

The Hilbert-space question remains open.

Setting

Let $\mathbb{K}$ be $\mathbb{R}$ or $\mathbb{C}$, let $E$ be a normed space over $\mathbb{K}$, and let $T\colon E\to E$ be a bounded linear operator. A linear subspace $S\subseteq E$ is invariant under $T$ if $T(S)\subseteq S$. It is a non-trivial closed invariant subspace if moreover $S$ is closed in the norm topology and $\{0\}\neq S\neq E$. A closed subspace $S$ with $\{0\}\neq S\neq E$ is a non-trivial closed hyperinvariant subspace of $T$ if $A(S)\subseteq S$ for every bounded operator $A$ with $AT=TA$.

A Hilbert space $H$ is a complete complex inner product space; it is separable if it has a countable dense subset. An operator $K$ is compact if it maps bounded sets to relatively compact sets, and $T$ is normal if $T^*T=TT^*$. In the Lean development these notions are IsInvariantSubspace, IsNontrivialClosedInvariantSubspace, HasNontrivialClosedInvariantSubspace and HasNontrivialClosedHyperinvariantSubspace (namespace InvariantSubspaceProblem), together with Mathlib's IsCompactOperator and IsStarNormal.

Formalization targets

Goal: the invariant subspace problem

$$\forall\, H \text{ separable, } \dim H=\infty,\ \forall\, T\in\mathcal{B}(H):\quad \exists\, S\subseteq H \text{ closed},\ \{0\}\neq S\neq H,\ T(S)\subseteq S .$$

The source poses a yes/no question; the goal states the affirmative answer, and a formal proof of its negation equally settles the problem.

Milestones (known results)

1. Finite-dimensional case: every operator on a complex space of dimension $\ge 2$ has a non-trivial invariant subspace.
2. Non-separable case: every operator on a non-separable complex normed space has a non-trivial closed invariant subspace.
3. Normal operators on a complex Hilbert space of dimension $\ge 2$.
4. Aronszajn–Smith: compact operators on infinite-dimensional real or complex Banach spaces.
5. Lomonosov: non-zero compact operators have non-trivial closed hyperinvariant subspaces.
6. Lomonosov: operators commuting with a non-zero compact operator.
7. Enflo: a separable infinite-dimensional complex Banach space with an operator having no non-trivial closed invariant subspace.
8. Read: such an operator on $\ell^1$.
9. Argyros–Haydon: a separable infinite-dimensional real Banach space on which every operator is $\lambda I+K$ with $K$ compact.
10. Argyros–Haydon: a separable infinite-dimensional real Banach space on which every operator has a non-trivial closed invariant subspace.

Significance

The result itself. A positive answer would give every bounded operator on Hilbert space a non-trivial piece of structure and would be the first step towards triangular-form type theorems for general operators. A negative answer would, after Enflo and Read, show that even the Hilbert-space geometry does not force invariant subspaces. Either answer resolves a question that has organised much of operator theory since the 1930s.

Formalizing it. The goal is open; no proof, formal or informal, is known. The milestones are proved results whose formal proofs would build reusable infrastructure absent from Mathlib: the Aronszajn–Smith and Lomonosov theorems (the latter through Schauder's fixed point theorem), invariant subspaces from the spectral theorem for normal operators, and the large explicit constructions of Enflo, Read and Argyros–Haydon. None of these results is formalized in Mathlib at the time of writing.

Difficulty

The obvious approach, taking the closed linear span of an orbit $\{x, Tx, T^2x,\dots\}$, fails exactly when every non-zero vector is cyclic, which is the situation that has to be ruled out; for separable spaces nothing prevents this a priori. Spectral methods fail because an operator can have a one-point spectrum and no eigenvectors (quasinilpotent operators). Methods that work on Hilbert space must use the inner-product structure in an essential way, since Enflo's and Read's examples show that the statement is false on some Banach spaces. Lomonosov's technique needs a non-zero compact operator in the commutant, which a general operator need not have.

Formalization scope

Hilbert spaces are Mathlib types H with [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is TopologicalSpace.SeparableSpace H and infinite dimension is ¬ FiniteDimensional ℂ H. Operators are continuous linear maps H →L[ℂ] H. Scalars are complex in the goal. Subspaces are Submodules, and closedness is required explicitly: without it the statement is trivially true in infinite dimensions (the algebraic span of an orbit is a proper invariant subspace), and a published platform statement that omits closedness should not be confused with this problem. Existential milestones quantify over spaces in Type.

Useful infrastructure includes: Schauder's fixed point theorem, Riesz theory of compact operators, the spectral theorem for normal operators, and $\ell^1$ machinery for Read's construction. Contributions of reusable lemmas, partial results (for instance further classes of operators known to have invariant subspaces), and proof sketches for the milestones are welcome.

Selected references

• Open Problem Garden, Invariant subspace problem, posted by T. Chow, 2009. http://www.openproblemgarden.org/op/invariant_subspace_problem
• N. Aronszajn, K. T. Smith, Invariant subspaces of completely continuous operators, Ann. of Math. 60 (1954) 345–350. https://doi.org/10.2307/1969637
• V. I. Lomonosov, Invariant subspaces for the family of operators which commute with a completely continuous operator, Funct. Anal. Appl. 7 (1973) 213–214. https://doi.org/10.1007/BF01080698
• P. Enflo, On the invariant subspace problem for Banach spaces, Acta Math. 158 (1987) 213–313. https://doi.org/10.1007/BF02392260
• C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$, Bull. London Math. Soc. 17 (1985) 305–317. https://doi.org/10.1112/blms/17.4.305
• S. A. Argyros, R. G. Haydon, A hereditarily indecomposable $\mathcal{L}_\infty$-space that solves the scalar-plus-compact problem, Acta Math. 206 (2011) 1–54. https://arxiv.org/abs/0903.3921
• H. Radjavi, P. Rosenthal, The invariant subspace problem, Math. Intelligencer 4 (1982) 33–37.
• B. S. Yadav, The present state and heritages of the invariant subspace problem, Milan J. Math. 73 (2005) 289–316.

Motivation

The diffeomorphism group $\mathrm{Diff}(M)$ of a closed smooth manifold $M$, topologized so that two diffeomorphisms are close when they and all their derivatives are uniformly close, is a basic invariant of the smooth structure of $M$. Its set of path components $\pi_0\,\mathrm{Diff}(M)$ is the group of isotopy classes of diffeomorphisms (the smooth mapping class group), and its higher homotopy groups classify smooth fibre bundles with fibre $M$. For spheres, the natural comparison is with the orthogonal group $O(n+1)$ of isometries of the round metric, which sits inside $\mathrm{Diff}(S^n)$.

S. Smale asked how far $\mathrm{Diff}(S^n)$ is from $O(n+1)$. The question was settled positively in dimensions $n \le 3$ and has been studied extensively in dimensions $n \ge 5$, where surgery theory and pseudo-isotopy theory apply. Dimension $4$ is the remaining case, and it is where the least is known. The question is recorded on the Open Problem Garden (problem page) with importance "Outstanding".

Timeline.

• 1959 — S. Smale: $\mathrm{Diff}(S^2) \simeq O(3)$.
• 1963 — M. Kervaire and J. Milnor compute the groups $\Theta_n$ of homotopy spheres; combined with Cerf's pseudo-isotopy theorem this computes $\pi_0\,\mathrm{Diff}(S^n)$ for many $n \ge 5$ (for example $\pi_0\,\mathrm{Diff}^+(S^6) \cong \Theta_7 \cong \mathbb Z/28$).
• 1970s — the Cerf–Morlet comparison theorem $\mathrm{Diff}(D^n) \simeq \Omega^{n+1}(PL_n/O_n)$ (Kirby–Siebenmann, Foundational Essays).
• 1978 — F.T. Farrell and W.C. Hsiang compute $\pi_i\,\mathrm{Diff}(D^n)\otimes\mathbb Q$ in a stable range of degrees for large $n$.
• 1983 — A. Hatcher: $\mathrm{Diff}(S^3) \simeq O(4)$ (the Smale conjecture).
• 2007 — R. Budney: $\mathrm{Diff}(D^4)$ is a $5$-fold loop space, via little cubes acting on spaces of long knots.
• 2018 — T. Watanabe: $\pi_*\,\mathrm{Diff}(D^4)\otimes\mathbb Q \ne 0$; the $4$-dimensional Smale conjecture is false (arXiv:1812.02448).

Whether $\mathrm{Diff}(D^4)$ is connected is still unknown.

Setting

Write $\mathbb R^n$ for Euclidean space with the Euclidean norm, $D^n$ for the closed unit ball and $S^n \subset \mathbb R^{n+1}$ for the round unit sphere.

• $\mathrm{Diff}(D^n)$ is the group of diffeomorphisms of the $n$-ball rel boundary. Concretely it is the group of smooth diffeomorphisms $f\colon \mathbb R^n \to \mathbb R^n$ with $f(x) = x$ whenever $\|x\| \ge 1$. Two such maps are close when their $k$-th derivatives are uniformly close for every $k$ (the $C^\infty$ topology). The base point is the identity.
• $\mathrm{Diff}(S^n)$ is the group of all smooth diffeomorphisms of $S^n$ (orientation-preserving or orientation-reversing), with the $C^\infty$ topology. Derivatives are measured through the degree-one homogeneous extension $x \mapsto \|x\|\, f(x/\|x\|)$, taken on the sphere.
• $O(n)$ is the group of real orthogonal $n\times n$ matrices with the matrix topology.
• $X \simeq Y$ means that $X$ and $Y$ are homotopy equivalent. $\pi_0 X$ is the set of path components, and $\pi_i(X,x)$ is the $i$-th homotopy group. $\Omega^k(Y,y)$ is the $k$-fold loop space, the space of maps $[0,1]^k \to Y$ sending the boundary of the cube to $y$.

The source states that $\mathrm{Diff}(S^4) \simeq O(5) \times \mathrm{Diff}(D^4)$, so the homotopy type of $\mathrm{Diff}(S^4)$ is determined by that of $\mathrm{Diff}(D^4)$.

Formalization targets

Goal: connectivity of $\mathrm{Diff}(D^4)$

$$\pi_0\,\mathrm{Diff}(D^4) = 0, \qquad\text{i.e. } \mathrm{Diff}(D^4) \text{ is path-connected.}$$

The source asks to "determine some (any?) homotopy or homology groups of $\mathrm{Diff}(D^4)$" and singles out connectivity as unknown. The goal is the yes/no question for $\pi_0$. It can be settled either way: a proof shows that every diffeomorphism of $D^4$ rel boundary is isotopic to the identity, and a disproof exhibits one that is not.

Milestones

1. $\mathrm{Diff}(S^4) \simeq O(5)\times\mathrm{Diff}(D^4)$ (problem statement).
2. $\mathrm{Diff}(D^4) \simeq \Omega^5(Y,y)$ for some pointed space $(Y,y)$ (Cerf–Morlet, Budney).
3. $\mathrm{Diff}(D^4)$ is not contractible (Watanabe).
4. $\mathrm{Diff}(S^2) \simeq O(3)$ (Smale).
5. $\mathrm{Diff}(S^3) \simeq O(4)$ (Hatcher).
6. $|\pi_0\,\mathrm{Diff}(S^6)| = 56$ (Kervaire–Milnor and Cerf).
7. For $2 \le i < \min\{\tfrac{n-4}{3}, \tfrac{n-7}{2}\}$: $\pi_i\,\mathrm{Diff}(D^n)\otimes\mathbb Q \cong \mathbb Q$ if $n$ is odd and $4 \mid i+1$, and $0$ otherwise (Farrell–Hsiang).

Significance

The result itself. A positive answer would mean $\pi_0\,\mathrm{Diff}(S^4) \cong \mathbb Z/2$, detected by orientation alone, matching dimensions $1$, $2$ and $3$. A negative answer would give an exotic diffeomorphism of $S^4$: one that is topologically isotopic to the identity (by the Alexander trick) but not smoothly isotopic. By the Cerf–Morlet theorem, $\pi_0\,\mathrm{Diff}(D^4) \cong \pi_5(PL_4/O_4)$, so the question is equivalent to a question about the homotopy of $PL_4/O_4$, the space controlling smoothings of PL $4$-manifolds. The source lists the smooth $4$-dimensional Schoenflies problem as a related problem.

Formalizing it. No part of this theory is currently formalized in Lean or Mathlib: there is no $C^\infty$ topology on diffeomorphism groups and no known homotopy equivalence involving one. The milestones are classical theorems (Smale 1959, Hatcher 1983, Kervaire–Milnor 1963, Farrell–Hsiang 1978, Watanabe 2018). Formalizing any of them is new work, independent of the open goal.

Difficulty

In dimensions $\ge 5$, $\pi_0\,\mathrm{Diff}(D^n)$ is computed by combining Cerf's pseudo-isotopy theorem with the $h$-cobordism theorem. Both rely on the Whitney trick, which fails in dimension $4$. In dimension $4$ one also cannot reduce to a lower-dimensional problem as Smale and Hatcher did. The known invariants that detect non-trivial elements of $\pi_*\,\mathrm{Diff}(D^4)$ (Watanabe's configuration-space integrals) are rational and live in positive degrees, so they say nothing about $\pi_0$. Smale's and Hatcher's arguments for $n = 2, 3$ rely on understanding spaces of embedded spheres in $S^n$ of one lower dimension; the corresponding spaces of $3$-spheres in $S^4$ are not understood, so those arguments do not carry over.

Formalization scope

All statements import the single definition file SmaleDiffS4_Basic and live in the namespace SmaleDiffS4.

• DiffDisk n is the subtype of Mathlib's Diffeomorph 𝓘(ℝ, ℝⁿ) 𝓘(ℝ, ℝⁿ) ℝⁿ ℝⁿ ∞ (smooth = C^∞) of maps fixing every point of norm $\ge 1$. Its topology is induced by the family of iterated derivatives iteratedFDeriv ℝ k f, $k \in \mathbb N$, each with the topology of uniform convergence on $\mathbb R^n$. This "identity outside the open ball" model is the standard model of $\mathrm{Diff}(D^n \text{ rel } \partial)$ and is homotopy equivalent to the "identity on the boundary" and "identity near the boundary" variants.
• DiffSphere n is Mathlib's Diffeomorph (𝓡 n) (𝓡 n) (sphere 0 1) (sphere 0 1) ∞ on the unit sphere of $\mathbb R^{n+1}$. Its topology is induced by the iterated derivatives of the radial extension, restricted to the sphere and uniformly topologized.
• OrthGroup n is Matrix.orthogonalGroup (Fin n) ℝ with the subspace topology.
• Homotopy equivalence is ContinuousMap.HomotopyEquiv. $\Omega^5$ is GenLoop (Fin 5) Y y, $\pi_0$ is ZerothHomotopy, and $\pi_i$ is HomotopyGroup (Fin i). $\pi_i\otimes\mathbb Q$ is TensorProduct ℤ ℚ (Additive π_i), and "$\cong\mathbb Q$" is stated as $\mathbb Q$-rank $1$.
• The Farrell–Hsiang milestone covers only $i \ge 2$, where $\pi_i$ is abelian in Mathlib. It includes the parity hypothesis "$n$ odd" of the original theorem, which is lost in the source page's rendering.

A trivializing formalization is ruled out: the topology is the genuine $C^\infty$ topology rather than the discrete or indiscrete one, and the goal is not vacuous because DiffDisk 4 is nonempty (it contains the identity).

A complete development needs reusable infrastructure: the $C^\infty$ topology and topological-group structure on diffeomorphism groups, isotopy extension and fibration theorems (Cerf–Palais), restriction to a disc, and the Alexander trick. Contributions of this infrastructure as separate theorems are welcome.

Selected references

• Open Problem Garden, What is the homotopy type of the group of diffeomorphisms of the 4-sphere? (posted 2009). http://www.openproblemgarden.org/op/what_is_the_homotopy_type_of_the_group_of_diffeomorphisms_of_the_4_sphere
• S. Smale, Diffeomorphisms of the 2-sphere, Proc. Amer. Math. Soc. 10 (1959), 621–626. https://doi.org/10.1090/S0002-9939-1959-0112149-8
• M. Kervaire, J. Milnor, Groups of homotopy spheres I, Ann. of Math. 77 (1963), 504–537. https://doi.org/10.2307/1970128
• R. Kirby, L. Siebenmann, Foundational Essays on Topological Manifolds, Smoothings, and Triangulations, Princeton University Press, 1977.
• F.T. Farrell, W.C. Hsiang, On the rational homotopy groups of the diffeomorphism groups of discs, spheres and aspherical manifolds, Proc. Sympos. Pure Math. 32 (1978), 403–415.
• A. Hatcher, A proof of a Smale conjecture, $\mathrm{Diff}(S^3)\simeq O(4)$, Ann. of Math. (2) 117 (1983), 553–607. https://doi.org/10.2307/2007035
• R. Budney, Little cubes and long knots, Topology 46 (2007), 1–27. https://arxiv.org/abs/math/0309427
• T. Watanabe, Some exotic nontrivial elements of the rational homotopy groups of $\mathrm{Diff}(S^4)$, 2018. https://arxiv.org/abs/1812.02448

Motivation

Bounded-depth Frege systems are the proof systems of propositional logic in which every formula of a proof has depth bounded by a fixed constant $d$; the resulting system is written $F_d$. They are the proof-theoretic counterpart of the circuit class $\mathrm{AC}^0$ and of the bounded arithmetic theories $I\Delta_0$ and its relatives: short $F_d$-proofs of a family of tautologies correspond to proofs of the corresponding first-order statement in bounded arithmetic. Lower bounds for $F_d$ are among the strongest lower bounds known for any natural proof system.

A basic structural question is whether the depth hierarchy $F_1 \subseteq F_2 \subseteq F_3 \subseteq \dots$ is strict in a strong sense. It is known that one extra level of depth can give an exponential speed-up, but in all known separations the tautologies themselves have depth growing with $d$. J. Krajíček asked whether there is a single fixed depth $k$ at which tautologies witnessing the separation of $F_{d+1}$ from $F_d$ exist for every $d$ (Open Problem Garden, F_d versus F_{d+1}; [Krajíček 1995, p. 243]). The question is closely related to conservativity relations among bounded arithmetic theories.

Timeline.

• 1987 — Buss: the pigeonhole principle $\mathrm{PHP}^{n+1}_n$ has polynomial-size Frege proofs (of unbounded depth).
• 1988 — Ajtai: $\mathrm{PHP}^{n+1}_n$ has no polynomial-size $F_d$-proofs for any fixed $d$.
• 1993/1995 — Pitassi–Beame–Impagliazzo and Krajíček–Pudlák–Woods: $F_d$-proofs of $\mathrm{PHP}^{n+1}_n$ require size $2^{n^{\varepsilon_d}}$.
• 1994 — Krajíček: for each $d$ there are tautologies of depth $d$ with polynomial-size $F_{d+1}$-proofs requiring exponential-size $F_d$-proofs, i.e. the problem is solved when $k$ may depend on $d$ ($k := d$).
• 2002 — Impagliazzo–Krajíček relate the question to conservativity among bounded arithmetic theories.

Setting

Formulas. A formula is in negation normal form over variables $p_0, p_1, \dots$: a literal $p_i$ or $\neg p_i$, a conjunction $\bigwedge(A_1,\dots,A_m)$ or a disjunction $\bigvee(A_1,\dots,A_m)$ of any finite number $m \ge 0$ of formulas. The depth of a literal is $0$, and the depth of $\bigwedge(A_1,\dots,A_m)$ or $\bigvee(A_1,\dots,A_m)$ is $1+\max_j \operatorname{depth}(A_j)$ (so clauses have depth $1$ and CNFs depth $2$). The size $|A|$ is the number of symbols (literals and connectives). A tautology is a formula true under every assignment. The negation $\overline{A}$ of a formula is obtained by De Morgan's laws.

The system $F_d$. Lines of a proof are sequents: finite lists $\Gamma$ of formulas, read as their disjunction. The rules are: (axiom) any $\Gamma$ containing both $p_i$ and $\neg p_i$; ($\wedge$) from $A, \Gamma$ for every $A \in \{A_1,\dots,A_m\}$ infer $\bigwedge(A_1,\dots,A_m), \Gamma$; ($\vee$) from $A_j, \Gamma$ infer $\bigvee(A_1,\dots,A_m), \Gamma$; (weakening) from $\Gamma$ infer any $\Delta$ containing every member of $\Gamma$; (cut) from $A,\Gamma$ and $\overline{A},\Gamma$ infer $\Gamma$. An $F_d$-proof of $A$ is a sequence of sequents, each following from earlier ones by a rule (lines may be reused), in which every formula has depth at most $d$, and which contains the sequent consisting of $A$ alone. Its size is the total size of all formulas in it.

Formalization targets

Write $\tau = (\tau_m)_{m\in\mathbb N}$ for a family of tautologies of depth at most $k$ with $|\tau_m| \ge m$. It requires exponential $F_d$-size if for some $\varepsilon>0$ and all large $m$ every $F_d$-proof of $\tau_m$ has size at least $2^{|\tau_m|^{\varepsilon}}$.

Goal

$$\exists k\ \forall d \ge k\ \exists \tau:\quad \tau_m \text{ has } F_{d+1}\text{-proofs of size } 2^{C(\log_2|\tau_m|)^C} \text{ and } \tau \text{ requires exponential } F_d\text{-size.}$$

The goal takes the weaker of the two upper bounds allowed by the problem (quasi-polynomial); the polynomial version implies it.

Milestones

1. Soundness of $F_d$: every formula with an $F_d$-proof is a tautology.
2. Completeness of $F_d$ for depth-$d$ formulas: every tautology of depth $\le d$ has an $F_d$-proof.
3. Exponential $F_d$ lower bound for $\mathrm{PHP}^{n+1}_n$: size $\ge 2^{n^{\varepsilon_d}}$.
4. The depth-dependent separation: for all large $d$, depth-$d$ tautologies with polynomial-size $F_{d+1}$-proofs requiring exponential $F_d$-size.

Significance

A positive answer would show that the extra power of depth $d+1$ over depth $d$ is visible already on formulas of a fixed, small depth, in particular that the hierarchy of bounded-depth Frege systems does not collapse on (for example) CNF tautologies. Through the correspondence with bounded arithmetic it bears on conservativity of theories of increasing quantifier complexity over a fixed class of low-complexity statements. A negative answer would say that for low-depth tautologies the bounded-depth Frege hierarchy collapses up to quasi-polynomial size.

Status: the goal is open. Milestones 1–2 are standard; milestones 3–4 are published theorems that, to the best of current knowledge, have no machine-checked proofs. Formalizing them requires switching-lemma machinery that would be reusable across proof complexity.

Difficulty

The known lower bounds for $F_d$ go through switching lemmas that simplify depth-$d$ formulas under random restrictions. In the known separations of $F_{d+1}$ from $F_d$ the hard tautologies have depth growing with $d$. Keeping the formulas at one fixed depth $k$ while $d$ ranges over all values requires a lower-bound argument whose strength depends on the depth of the proof lines alone, uniformly in $d$; the switching-lemma arguments used for depth-dependent separations do not directly provide this.

Formalization scope

Formulas are the Lean inductive type FdVersusFdSucc.Formula over variables ℕ, with conjunctions and disjunctions of lists (so and [] is true and or [] is false). Depth counts literals as $0$. $F_d$ is the dag-like one-sided sequent calculus described above; sequents are lists, weakening is by list inclusion. Proof size counts symbols of all formulas in all lines. Exponential lower bounds are asked only for all sufficiently large indices. The goal quantifies over $d \ge k$: for $d+1 < k$ no $F_{d+1}$-proof of a depth-$k$ formula exists, so "every $d$" cannot be meant literally. A family whose formulas have depth $> d$ would satisfy the lower bound vacuously; this is excluded because the formulas must have depth at most $k \le d$. The size condition $|\tau_m| \ge m$ rules out finite families.

Contributions welcome: proofs of soundness and completeness, a formalized switching lemma, and the classical lower bounds.

Selected references

• J. Krajíček, Lower bounds to the size of constant-depth propositional proofs, J. Symbolic Logic 59(1), 1994, 73–86.
• J. Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications 60, Cambridge University Press, 1995 (p. 243).
• Open Problem Garden, F_d versus F_{d+1}, http://www.openproblemgarden.org/op/f_d_versus_f_d_1
• M. Ajtai, The complexity of the pigeonhole principle, FOCS 1988.
• J. Krajíček, P. Pudlák, A. Woods, An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Structures & Algorithms 7(1), 1995.
• T. Pitassi, P. Beame, R. Impagliazzo, Exponential lower bounds for the pigeonhole principle, Computational Complexity 3, 1993.
• S. Buss, Polynomial size proofs of the propositional pigeonhole principle, J. Symbolic Logic 52, 1987.
• R. Impagliazzo, J. Krajíček, A note on conservativity relations among bounded arithmetic theories, Math. Logic Quarterly 48, 2002.

Motivation

Rendezvous search asks how two agents who cannot communicate should move so as to meet as quickly as possible. It was introduced as a mathematical problem by Alpern (The rendezvous search problem, SIAM J. Control Optim. 1995) and developed systematically in Alpern and Gal's monograph The Theory of Search Games and Rendezvous (Kluwer, 2003). Besides its game-theoretic interest, it is a model for coordination without prior agreement: robots or searchers that must find each other with no shared map or orientation.

The simplest non-trivial domain is the line. Even there, the version in which both agents must follow the same strategy remains open, and it is listed on the Open Problem Garden with importance "High".

Timeline:

• 1995. Alpern formulates symmetric rendezvous search problems, in which the players must use the same mixed strategy.
• 1995. Alpern and Gal (Rendezvous search on the line with distinguishable players, SIAM J. Control Optim. 33(4)) solve the asymmetric problem on the line, where the players may use different strategies: the optimal expected meeting time is $3.25$.
• 1995–2008. A series of papers improve upper and lower bounds on the symmetric value.
• 2008. Han, Du, Vera and Zuluaga (Improved bounds for the symmetric rendezvous search problem on the line, Operations Research 56(3)) show that strategies moving at full speed and turning only at integer times dominate, reducing the problem to a discrete one, prove $4.1520 < R < 4.2574$, and conjecture $R = 4.25$.

Setting

Two players are placed on the real line at distance $2$; player I starts at $0$ and player II at $2$. Each player has a private sense of "forward", fixed by an independent fair coin, so neither knows in which direction the other lies. Both move with speed at most $1$.

A feasible path is a function $f$ with $f(0)=0$ and $|f(s)-f(t)|\le |s-t|$ for $s,t\ge 0$, describing a player's position in its own frame. A mixed strategy $S$ is a probability distribution over feasible paths, realised as a probability space $(\Omega,P)$ and a random path $\omega\mapsto f_\omega$ whose position at each fixed time is measurable.

If player I follows $f$ with orientation $\varepsilon_1\in\{\pm1\}$ and player II follows $g$ with orientation $\varepsilon_2$, their positions are $\varepsilon_1 f(t)$ and $2+\varepsilon_2 g(t)$. The meeting time is

$$T=\inf\{t\ge 0:\ \varepsilon_1 f(t) = 2+\varepsilon_2 g(t)\}\in[0,\infty].$$

For strategies $S_1,S_2$ with independent randomisations, the expected meeting time $E(S_1,S_2)$ averages $T$ over $f\sim S_1$, $g\sim S_2$ and the four equally likely orientation pairs. The symmetric rendezvous value and the asymmetric rendezvous value are

$$R=\inf_{S} E(S,S),\qquad R^a=\inf_{S_1,S_2}E(S_1,S_2).$$

An integer zigzag is a path that on each interval $[n,n+1]$, $n\in\mathbb N$, moves with velocity $+1$ or $-1$; $R_{\mathrm{disc}}$ denotes the infimum of $E(S,S)$ over strategies supported on integer zigzags.

Formalization targets

Goal: the conjectured value

$$R=\frac{17}{4}.$$

This is the Han–Du–Vera–Zuluaga conjecture and answers the Open Problem Garden question. A formal disproof is equally valuable.

Milestones from the literature

1. Alpern–Gal: $R^a = \dfrac{13}{4}$.
2. Han–Du–Vera–Zuluaga reduction: $R = R_{\mathrm{disc}}$.
3. Han–Du–Vera–Zuluaga lower bound: $4.1520 < R$.
4. Han–Du–Vera–Zuluaga upper bound: $R < 4.2574$.

Significance

The value $R$ measures the cost of symmetry in the most basic rendezvous problem: $R^a = 3.25$ when roles can be pre-assigned, while the best known symmetric strategies need about $4.25$. Determining $R$ exactly would settle a problem that has been open since 1995 and would calibrate numerical methods (linear and semidefinite relaxations over discretised strategies) used for related search games.

None of these results is formalized. The milestones are proved on paper; formalizing them requires a measure-theoretic treatment of mixed strategies over path space, a rigorous version of the discretisation argument, and certified numerical bounds. The goal itself is open.

Difficulty

The obvious approach is to optimise over finitely many turning times, but a symmetric strategy must be randomised (any deterministic symmetric strategy fails to meet with probability $1/2$, when both players face the same way), so the optimisation is over probability distributions on infinite paths and the objective is a quadratic, non-convex function of the distribution. Truncating to finite horizons gives upper bounds by explicit strategies, but lower bounds require controlling all strategies, including those that delay indefinitely, and the known gap $4.1520$–$4.2574$ has resisted closing.

Formalization scope

All values live in $[0,\infty]$ and expectations are Lebesgue integrals of non-negative functions; a strategy that fails to meet with positive probability has value $\infty$. Sample spaces range over a fixed universe, which loses no generality. Paths are required to be $1$-Lipschitz on $[0,\infty)$ with $f(0)=0$, and positions at fixed times are measurable, so meeting times are random variables. The four orientation pairs are weighted equally. The infimum in $R$ ranges over all such strategies, not only over integer zigzags; the restriction appears only in $R_{\mathrm{disc}}$. A trivializing reading (e.g. a meeting time of $0$ or an unrestricted speed) is excluded: by construction every strategy pair has expected meeting time at least $1$.

Contributions are welcome on: measurability of hitting times for continuous processes, the discretisation argument, explicit strategies with certified expected meeting times, and certified lower-bound certificates.

Selected references

• S. Alpern, The rendezvous search problem, SIAM J. Control Optim. 33(3) (1995), 673–683.
• S. Alpern, S. Gal, Rendezvous search on the line with distinguishable players, SIAM J. Control Optim. 33(4) (1995), 1270–1276.
• S. Alpern, S. Gal, The Theory of Search Games and Rendezvous, International Series in Operations Research & Management Science 55, Kluwer, 2003.
• Q. Han, D. Du, J. C. Vera, L. F. Zuluaga, Improved bounds for the symmetric rendezvous search problem on the line, Operations Research 56(3) (2008).
• Open Problem Garden, Rendezvous on a line. http://www.openproblemgarden.org/op/rendezvous_on_a_line

Motivation

A large family of random growth models, interacting particle systems and directed polymers in one space dimension share a common, non-Gaussian fluctuation theory: observables of size $t$ fluctuate on the scale $t^{1/3}$ (instead of the central-limit scale $t^{1/2}$), with spatial correlations on the scale $t^{2/3}$. This family is the Kardar–Parisi–Zhang (KPZ) universality class, named after the 1986 physics paper of Kardar, Parisi and Zhang. The KPZ universality conjecture (Open Problem Garden, posted 2020, importance "High") asks for a central limit theorem for this class: any one-dimensional growth model with a smoothing mechanism, short-range noise and slope-dependent ("lateral") growth should exhibit KPZ fluctuations.

KPZ fluctuations have been proved only for models with exact algebraic structure, such as the corner growth model / totally asymmetric exclusion process (Johansson, 2000) and the polynuclear growth model (Prähofer–Spohn, 2002). The Open Problem Garden entry describes ballistic deposition (Vold, 1959) as a concrete growth model with the KPZ features. Corwin's survey states the prediction that its column heights fluctuate like $t^{1/3}$ and notes that "this prediction has not been proved" (Corwin 2012, §1.1.1). Ballistic deposition has no known exact solvability, so it tests universality itself rather than one integrable instance of it.

Timeline.

• 1959 — Vold introduces ballistic deposition as a sediment model.
• 1986 — Kardar–Parisi–Zhang predict the exponents $1/3$ and $2/3$.
• 2000 — Seppäläinen proves a strong law of large numbers (hydrodynamic limit) for the ballistic deposition interface (arXiv:math/9906193).
• 2008 — Penrose proves linear growth of the mean height, $L^p$ laws of large numbers, polynomial moment bounds, a duality with a seed-grown process, and the only known lower bound on fluctuations: $\operatorname{Var}\xi_t(0)\gtrsim\log t$ in $d=1$ (arXiv:math/0608540).
• 2021 — Chatterjee proves existence of a stationary measure for the gradient process (arXiv:2110.10294).
• 2026 — Sudijono proves exponential concentration and the upper bound $\operatorname{Var}\xi_t(0)\le Ct$ (arXiv:2609.24056).

The gap between $\log t$ and $t$ is open; the predicted order is $t^{2/3}$.

Setting

Columns are indexed by $x\in\mathbb Z$. Each column carries an independent rate-one Poisson clock: on a probability space $(\Omega,P)$ the inter-arrival times $\tau_{x,k}$, $(x,k)\in\mathbb Z\times\mathbb N$, are independent and $\mathrm{Exp}(1)$-distributed, and the $n$-th ring of column $x$ (counting from $n=0$) is at time $T_{x,n}=\tau_{x,0}+\dots+\tau_{x,n}$.

Random deposition. The height $N_t(x)$ of column $x$ at time $t$ is the number of rings of its clock in $[0,t]$. Columns are independent and $N_t(x)$ is Poisson with mean $t$.

Ballistic deposition (nearest-neighbour model, flat initial surface). Write $\xi_t(x)\in\mathbb N$ for the height of column $x$ at time $t$, with $\xi_0\equiv0$. When the clock of column $x$ rings at time $t$, a unit block falls in column $x$ and sticks at the first point of contact, so

$$\xi_t(x)=\max\{\xi_{t-}(x)+1,\ \xi_{t-}(x-1),\ \xi_{t-}(x+1)\},$$

and all other columns are unchanged. On the finite substrate $Q_L=[-L,L]$ only clocks in $Q_L$ ring and columns outside $Q_L$ stay at height $0$; the finitely many rings in $[0,t]$ are applied in time order. The height on $\mathbb Z$ is the monotone limit $\xi_t(x)=\lim_{L\to\infty}\xi^{Q_L}_t(x)=\sup_L\xi^{Q_L}_t(x)$. The next-arrival height is $\eta_t(x)=\max\{\xi_t(x)+1,\xi_t(x-1),\xi_t(x+1)\}$. This is the model of Penrose (2008) with $d=1$ and the nearest-neighbour displacement function, and the model (1) of Sudijono (2026) with $d=1$.

Formalization targets

Goal: the KPZ fluctuation exponent

$$\exists\,c,C>0,\ T:\qquad c\,t^{2/3}\ \le\ \operatorname{Var}\xi_t(0)\ \le\ C\,t^{2/3}\qquad(t\ge T).$$

This is the statement "the column height fluctuates around its mean like $t^{1/3}$" (Corwin 2012, §1.1.1; Sudijono 2026, §1). The constants are left unspecified because they are model-dependent.

Stronger (not formalized here)

The predicted scaling limit: $(\xi_t(0)-\rho t)/(\sigma t^{1/3})$ converges in law to the Tracy–Widom GOE distribution for some model-dependent $\rho,\sigma>0$.

Milestones (known results)

1. Random deposition CLT: $(N_t(0)-t)/\sqrt t\Rightarrow\mathcal N(0,1)$, the Gaussian class, for contrast.
2. Penrose, Prop. 2.1: $\xi_t(0),\eta_t(0)<\infty$ a.s. and $E[\xi_t(0)^k],E[\eta_t(0)^k]=O(t^k)$.
3. Penrose, Thm. 2.1: $E\xi_t(0)/t\to\rho_1\in(0,\infty)$ and $\xi_t(0)/t\to\rho_1$ in every $L^p$, $p\ge1$.
4. Seppäläinen, Thm. 1 (as noted in Penrose, p. 5): $\xi_t(0)/t\to\rho_1$ almost surely.
5. Penrose, Thm. 2.2: $\liminf_t\operatorname{Var}\xi_t(0)>0$ and $\liminf_t\operatorname{Var}\xi_t(0)/\log t>0$.
6. Sudijono, Thm. 1.1 (2): $P(|\xi_t(0)-E\xi_t(0)|\ge r)\le C\exp(-c\,r^2/(t+r))$ for $t\ge1$, $r\ge0$.
7. Sudijono, Thm. 1.1 (3): $\operatorname{Var}\xi_t(0)\le Ct$ for $t\ge1$.

Significance

A proof of the goal would establish the KPZ exponent for a growth model without exact solvability, which is the content of the universality conjecture as opposed to its integrable special cases. For ballistic deposition only $\log t\lesssim\operatorname{Var}\xi_t(0)\lesssim t$ is currently known.

On the formal side, the milestones are known results with published proofs; formalizing them requires a library for continuous-time interacting particle systems on $\mathbb Z$ (graphical constructions, monotone couplings, finite speed of propagation), subadditive ergodic theory, and concentration inequalities for Poisson-driven processes. These pieces are reusable for first-passage percolation and other growth models. The goal itself is open.

Difficulty

The standard tools give the wrong exponents. Bounded-difference concentration applied to a last-passage representation fails because adding one clock ring can change future heights by an unbounded amount (Sudijono 2026, §1); martingale hitting-time arguments reach only the diffusive bound $O(t)$. Lower bounds of Pemantle–Peres type reach only $\log t$, as in first-passage percolation, where the analogous gap is also open. The exact formulas (determinantal structure, Bethe ansatz) behind the proved instances of KPZ fluctuations are not available for ballistic deposition.

Formalization scope

The model is encoded on a general probability space $(\Omega,P)$ with inter-arrival times τ : ℤ → ℕ → Ω → ℝ satisfying IsPoissonClocks P τ (measurability, mutual independence over ℤ × ℕ, each law expMeasure 1). The finite-substrate process boxHeight τ L t ω sorts the rings in $[-L,L]\times[0,t]$ lexicographically by (time, column) and folds the update rule bdStep; bdHeight τ t x ω : ℕ∞ is the supremum over $L$. Real-valued statements use bdHeightReal, which is bdHeight cast to ℝ with the value $0$ on the event $\{\xi_t(x)=\infty\}$; this event is null (Milestone 2), so the convention does not affect any distributional statement. Ties between rings and non-divergent arrival times are null events and receive junk values. Variances are Mathlib's variance, which returns $0$ for non-square-integrable variables; the lower bound in the goal therefore also forces square-integrability, so the goal cannot hold vacuously. Moments in Milestone 2 are lower Lebesgue integrals in $[0,\infty]$, so they are not trivialised by non-integrability.

Contributions welcome: the graphical construction and its basic properties (monotonicity in $L$ and $t$, a.s. finiteness), the duality with seed-grown deposition, subadditivity of hitting times, and the Poisson CLT.

Selected references

• I. Corwin, The Kardar–Parisi–Zhang equation and universality class, Random Matrices Theory Appl. 1 (2012). https://arxiv.org/abs/1106.1596
• M. Kardar, G. Parisi, Y.-C. Zhang, Dynamic scaling of growing interfaces, Phys. Rev. Lett. 56 (1986). https://doi.org/10.1103/PhysRevLett.56.889
• T. Kojar (poster), KPZ Universality Conjecture, Open Problem Garden (2020). http://www.openproblemgarden.org/op/kpz_universality_conjecture
• M. D. Penrose, Growth and roughness of the interface for ballistic deposition, J. Stat. Phys. 131 (2008). https://arxiv.org/abs/math/0608540
• T. Seppäläinen, Strong law of large numbers for the interface in ballistic deposition, Ann. Inst. H. Poincaré Probab. Statist. 36 (2000). https://arxiv.org/abs/math/9906193
• T. Sudijono, A linear variance bound for ballistic deposition, preprint (2026). https://arxiv.org/abs/2609.24056
• S. Chatterjee, Existence of stationary ballistic deposition on the infinite lattice, preprint (2021). https://arxiv.org/abs/2110.10294
• K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209 (2000).
• M. J. Vold, A numerical approach to the problem of sediment volume, J. Colloid Sci. 14 (1959).