Motivation

Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.

This mission turns CUHK-Shenzhen AI Math Problem 16, Existence of complete sets of mutually unbiased bases, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

Construct seven 6 by 6 unitary-column matrices whose every distinct pair has all transition amplitudes of squared modulus 1/6. The baseline milestone constructs three pairwise mutually unbiased bases, a known lower bound that tests all matrix conventions.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in quantum information theory, mutually unbiased bases, finite fields, Hilbert spaces. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.

Difficulty

The equations are a large coupled system of polynomial equalities over complex phases, modulo substantial gauge symmetry. Numerical near-solutions do not certify exact existence, while nonexistence would require a global obstruction beyond currently known bounds. Dimension six lacks the finite-field structure that supplies complete prime-power constructions.

Suggested attack route

Formalize standard gauge reductions: fix the first basis to the identity and dephase transition Hadamard matrices. Verify a three-basis tensor-product construction. Then encode additional bases through complex Hadamard matrices and study algebraic constraints, Gröbner-style eliminations, semidefinite bounds, or exact certificates. Computational searches may guide conjectures, but uploaded proofs must convert numerical evidence to exact algebraic identities or certified inequalities.

Formalization scope

The Lean target is exact: column orthonormality is U-adjoint times U equals identity, and mutual unbiasedness uses Mathlib complex norm squared. Seven bases are indexed by Fin 7. No quotient by phase, permutation, or global unitary is built into the statement, since these symmetries preserve the predicate and can be used within proofs.

The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.

Milestones

Publish an exact three-basis construction in dimension six, then formalize dephasing and obstruction lemmas for extending a partial family.

The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.

Timeline and literature status

The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

• Original problem
• Durt et al., review of MUBs

Motivation

Quantum circuits built from Clifford gates alone are classically simulable in polynomial time. Universality is recovered by adding copies of a magic state, and the fastest known classical simulators of such circuits work by writing the magic-state input as a short linear combination of stabilizer states. The length of the shortest such combination -- the stabilizer rank -- is therefore the exponent governing classical simulation of quantum computation in this model, and lower bounds on it are among the very few unconditional obstructions to classical simulation available at all.

A timeline of what is established for the standard magic state $|H\rangle$:

• 2016. Bravyi, Smith and Smolin exhibit a decomposition giving $\chi(|H^{\otimes 6}\rangle)\le 7$, hence $\chi(|H^{\otimes n}\rangle)\le 7^{\,n/6}\le 2^{\,0.468n}$, and prove a lower bound of order $\sqrt{n}$.
• 2020. Huang, Newman and Szegedy show that hardness assumptions stronger than $\mathrm{P}\neq\mathrm{NP}$, such as the exponential time hypothesis, imply $\chi(|H^{\otimes n}\rangle)=2^{\Omega(n)}$ (arXiv link).
• 2022. Peleg, Shpilka and Volk improve the unconditional lower bound to $\Omega(n)$ and give the first non-trivial bound for the approximate rank (arXiv:2106.03214).
• 2024. A quadratic lower bound is obtained for the approximate stabilizer rank (arXiv:2305.10277).

Between the linear unconditional lower bound and the $2^{0.468n}$ upper bound lies the open problem this mission targets.

Setting

Index the computational basis of an $n$-qubit system by bit strings $x\in\{0,1\}^n$, so a state is a vector $\psi\in\mathbb{C}^{2^n}$ with coordinates $\psi(x)$.

The Pauli operators are $X^aZ^b$ for $a,b\in\{0,1\}^n$, acting by $X^aZ^b|x\rangle=(-1)^{\,b\cdot x}|x\oplus a\rangle$, where $b\cdot x$ counts the coordinates on which both are $1$ and $\oplus$ is bitwise addition; the Pauli group is the set of $4\cdot 4^n$ operators $i^cX^aZ^b$. A unitary $U$ is a Clifford unitary when $UPU^\dagger$ lies in the Pauli group for every Pauli group element $P$, and a stabilizer state is a vector $U|0\cdots0\rangle$ for some Clifford $U$. There are $2^n\prod_{k=1}^{n}(2^k+1)$ of them up to phase -- six for a single qubit.

The stabilizer rank $\chi(\psi)$ is the least $r$ admitting coefficients $c_1,\dots,c_r\in\mathbb{C}$ and stabilizer states $\varphi_1,\dots,\varphi_r$ with $\psi=\sum_{j\le r}c_j\varphi_j$.

The magic state is $|H\rangle=\cos(\pi/8)|0\rangle+\sin(\pi/8)|1\rangle$, and $|H^{\otimes n}\rangle$ its $n$-fold tensor power, with coordinates $\cos(\pi/8)^{\,n-|x|}\sin(\pi/8)^{\,|x|}$ where $|x|$ is the Hamming weight of $x$.

Target

The goal is a super-polynomial lower bound: for every exponent $d$ and constant $C$ there exists $n$ with

$$\chi\bigl(|H^{\otimes n}\rangle\bigr)\;>\;C\,n^{d},$$

equivalently, $\chi(|H^{\otimes n}\rangle)$ is not $O(n^d)$ for any fixed $d$.

Stronger statements are expected but are deliberately not the goal. An exponential bound $\chi=2^{\Omega(n)}$ is believed and follows from hardness assumptions, but a goal naming a specific growth rate would be superseded by the next improvement; super-polynomiality is the weakest statement that settles the question of principle.

Significance

The result itself. A super-polynomial lower bound would unconditionally rule out efficient classical simulation of Clifford-plus-magic-state circuits by stabilizer decomposition, currently the leading such technique. The converse direction shows how much is at stake: a polynomial upper bound on $\chi(|H^{\otimes n}\rangle)$ would imply $\mathrm{BPP}=\mathrm{BQP}$, and via postselection $\mathrm{P}=\mathrm{NP}$. There is also a purely classical payoff -- improving the known bound even to super-linear would produce a Boolean function computable in polynomial time requiring a super-linear number of summands in any decomposition into exponentials of quadratic forms over $\mathbb{F}_2$, resolving a separate open question.

Formalizing it. The goal is open, so no known proof is being transcribed. What the mission produces is a machine-checked statement of the problem together with formalizations of the established bounds, none of which has a machine-checked proof anywhere. It also produces the first Pauli/Clifford/stabilizer layer in Lean: no existing Lean library contains the $n$-qubit Pauli group, the Clifford group, or stabilizer states, and that layer is reusable for stabilizer error correction, magic monotones, and Clifford simulation generally.

Difficulty

Counting settles the problem for random states: the stabilizer states are too few for short combinations to cover a generic state, so almost every state has exponential stabilizer rank. This says nothing about $|H^{\otimes n}\rangle$, which is a single explicit, highly structured vector, and the entire difficulty is that lower bounds must be proved for that specific state rather than for a typical one. Every newcomer proposes the counting argument; it does not apply.

The known techniques reduce the question to statements about decompositions of explicit Boolean functions into quadratic-form exponentials, and the barrier is quantitative: the available arguments lose a factor that caps them at linear bounds. The source of the current record documents explicitly why its method cannot pass super-linear, and the fact that going beyond linear would resolve an independent open problem in Boolean function complexity indicates the obstruction is not merely technical.

Formalization scope

State vectors are functions $\{0,1\}^n\to\mathbb{C}$ and are not required to be normalised; normalisation does not affect the rank, and stabilizer states are unit vectors automatically as Clifford images of $|0\cdots0\rangle$. The Pauli group is given by the explicit parametrisation $i^cX^aZ^b$ rather than an abstract presentation, and the Clifford group is characterised as its unitary normaliser, equivalent to the usual generated-by-$H,S,\mathrm{CNOT}$ description. Because $e^{i\theta}U$ normalises the Pauli group whenever $U$ does, the stabilizer states are closed under global phase; this is harmless, as the coefficients are arbitrary complex numbers.

One trivialising reading must be excluded. The rank is defined as an infimum over a set of natural numbers, and Lean gives the empty infimum the value $0$; if no decomposition existed the rank would be $0$ for every state and the goal would be false rather than merely unproved. The milestone $\chi(\psi)\le 2^n$ is what certifies the set is nonempty, making the rank a genuine minimum, and it should be proved first. Separately, the goal quantifies $C$ over all reals including negative values, for which the inequality is trivially satisfiable; the content lies in large positive $C$.

A complete development needs, beyond the published definitions, the correspondence between stabilizer states and affine subspaces carrying quadratic phase functions, on which all known lower-bound arguments rest. Contributions of any milestone are welcome, as are function-level reformulations of the rank and the equivalent characterisation of stabilizer states via maximal abelian Pauli subgroups.

Selected references

• S. Peleg, A. Shpilka, B. L. Volk, Lower Bounds on Stabilizer Rank, Quantum 6 (2022) 652; arXiv:2106.03214.
• S. Bravyi, G. Smith, J. Smolin, Trading Classical and Quantum Computational Resources, Phys. Rev. X 6 (2016) 021043; arXiv:1506.01396.
• C. Huang, M. Newman, M. Szegedy, Explicit Lower Bounds on Strong Quantum Simulation, IEEE Trans. Inf. Theory 66(9) (2020) 5585--5600.
• Quadratic Lower Bounds on the Approximate Stabilizer Rank: A Probabilistic Approach, STOC 2024; arXiv:2305.10277.

Motivation

Quantum communication and computation often require a receiver to infer which preparation was sent after it has passed through a noisy quantum process. When possible preparations are mixed states, their overlap makes exact identification impossible. A measurement is then judged by its average probability of a correct label. The pretty good measurement gives a concrete measurement from the ensemble itself, without first solving the optimization over all measurements. Barnum and Knill related it to a general reversal operation for noisy dynamics and bounded its error through pairwise state fidelities in their preprint, §V–VI. The bound is useful when the overlaps are easier to estimate than the measurement's success probability.

The present mission addresses the preprint's second main result. The source is arXiv:quant-ph/0004088v2, not the later journal pagination. The preprint also strengthens its Theorem 3 relative to the published text, as its acknowledgment explains; this mission concerns Theorem 5 and the calculation around it.

Setting

An ensemble is a finite family of output density matrices $\hat\rho_j$ with probabilities $p_j\geq0$ satisfying $\sum_jp_j=1$. A density matrix is a positive semidefinite complex matrix with trace one. For each label $j$, fix an orthonormal eigenbasis $v_{ij}$ and nonnegative eigenvalues $\lambda_{ij}$ such that

$$\hat\rho_j=\sum_i\lambda_{ij}|v_{ij}\rangle\langle v_{ij}|, \qquad \sum_i\lambda_{ij}=1.$$

The eigenpair index $i$ runs over a finite output basis $O$; zero eigenvalues are allowed. The input labels form a finite basis $J$. A label distribution is represented by $\rho=\sum_jp_j|j\rangle\langle j|$.

The paper's classicizing channel $A$ has Kraus operators $A_{ij}=\sqrt{\lambda_{ij}}|v_{ij}\rangle\langle j|$. Acting on an input matrix $X$, its value is $A(X)=\sum_{i,j}A_{ij}X A_{ij}^{\dagger}$. In particular, its output on $\rho$ is $\rho_{\mathrm{out}}=\sum_jp_j\hat\rho_j$. The paper assumes $\rho_{\mathrm{out}}$ has full support when it writes its reversal operation. For a general Kraus family $A_a$, that operation has operators

$$(R_{A,\rho})_a=\rho^{1/2}A_a^\dagger A(\rho)^{-1/2}.$$

The inverse square root is spectral: invert nonzero eigenvalues and leave zero eigenvalues at zero. With full support, it is the usual inverse square root.

For an input label $j$, classical fidelity is the chance that the composite operation returns the same label. Averaging gives

$$F_{\mathrm{cl}}(\rho,K)= \sum_jp_j\langle j|K(|j\rangle\langle j|)|j\rangle.$$

The Bures–Uhlmann fidelity used here is the unsquared quantity $F_{\mathrm{BU}}(\sigma,\tau)=\operatorname{tr}\sqrt{\sqrt\sigma\,\tau\,\sqrt\sigma}$. For the classicizing channel, the reversal operation realizes the pretty good measurement, as shown by equation (36) and the discussion after equation (37) in the preprint, p. 10.

Formalization targets

Recovery error

The goal, in the reading established by the paper's proof, is

$$F_{\mathrm{cl}}(\rho,R_{A,\rho}A) \geq 1-\sum_{\substack{i,j\in J\\i\ne j}} \sqrt{p_ip_j}\,F_{\mathrm{BU}}(\hat\rho_i,\hat\rho_j).$$

The sum is over ordered pairs; each unordered pair of distinct labels is counted twice. The coefficient is exactly one. The goal applies to every finite ensemble with the spectral data above and a full-support output. It does not fix the number of labels or the dimension of the output.

The milestones are the reversal formula (36), the classical-fidelity identities in (38), the unit squared Frobenius norm (40), the diagonal-block expression (41), the off-diagonal trace-norm identity following (42), and the two-block estimate of Lemma 6. They record the paper's mathematical statements and keep the attack path tied to the authors' displayed results.

Significance

The result bounds a measurement's probability of error using only pairwise similarities of the possible output states and their prior probabilities. For nearly distinguishable states, the weighted fidelity sum is small, so this particular measurement succeeds with high probability. The theorem therefore gives a usable guarantee for a specified recovery procedure, rather than only asserting that some procedure exists. In the preprint, §VII, Barnum and Knill describe quantum-information applications of such recovery bounds.

The mathematical result is already proved in the paper, subject to the correction explained below. The formalization work is to make the mixed-state channel, its recovery, the finite-dimensional spectral conventions, and the block-matrix norm estimate precise in Lean. The published Prove2Me definitions for Kraus updates and trace norm supply reusable starting points. A complete proof of this mission would add a checked mixed-state pretty-good-measurement bound; the local statements here compile as open theorems, and no proof is claimed.

Difficulty

The obvious pairwise-overlap estimate does not by itself express the error of the recovery channel. The recovery's classical fidelity is initially a channel evaluation on basis states, while the bound uses trace norms of blocks of a Gram matrix. The key obstacle is controlling the off-diagonal Frobenius mass of the positive square root of that Gram matrix by the trace norms of the corresponding blocks of the Gram matrix itself. Lemma 6 states the needed two-block comparison, including rectangular blocks. The matrix dimension and block labels must remain consistent when it is applied across a larger array.

Formalization scope

All systems and index sets are finite, with matrices over $\mathbb C$ and real probabilities. A general completely positive map is represented by an unbundled finite family of Kraus matrices. The classicizing family has rectangular matrices from the input-label space to the output space; the reversal has matrices in the opposite direction. Composite Kraus families are indexed by pairs. The classical fidelity is defined from the channel action in equation (10); the goal does not define it using the desired overlap bound. The reversal is defined by equation (12) for a general family, so its specialized formula remains a theorem.

The spectral hypotheses include nonnegative probabilities and eigenvalues, unit sums, and orthonormal eigenvectors. Full support of $\rho_{\mathrm{out}}$ is an explicit hypothesis wherever the reversal appears, following page 7. Empty input or output types cannot satisfy the normalized data together with these hypotheses. The Bures–Uhlmann expression is the unsquared trace of a positive square root; using the squared fidelity would change the constant and is outside this mission. Lemma 6 is independent of the ensemble and can be reused for finite block-matrix estimates. Contributions to the spectral identities, the array equalities, and the block-norm argument are welcome.

Equation (39) prints the square of the optimal success probability on its left. The first line of (38) compares that quantity with the recovery fidelity in the opposite direction to Corollary 4. The proof on pages 12–13 concludes the displayed bound for $F_{\mathrm{cl}}(\rho,R_{A,\rho}A)$. This mission states that proved conclusion and records the printed discrepancy in its item and audit notes.

Selected references

• Howard Barnum and Emanuel Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2, 2000/2026 version. arXiv
• Howard Barnum and Emanuel Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, Journal of Mathematical Physics 43 (2002), 2097–2106. DOI

Motivation

Many quantum algorithms end in a measurement that succeeds only with some probability $a$. Two questions follow: how to raise that probability, and how to learn its value. G. Brassard, P. Høyer, M. Mosca and A. Tapp answered both in Quantum Amplitude Amplification and Estimation (arXiv:quant-ph/0005055, 2000; Contemporary Mathematics 305, 2002). Amplitude amplification generalizes Grover's search (Grover 1996) to an arbitrary algorithm $\mathcal A$ and an arbitrary notion of success. Amplitude estimation combines amplification with the quantum Fourier transform to estimate $a$ with error of order $1/M$ after $M$ applications of $\mathcal A$, where classical sampling needs order $1/M^2$ samples. Quantum counting, quantum Monte Carlo integration (Montanaro 2015) and many quantum speedups for statistics and finance rest on this estimation step.

Timeline:

• 1996: Grover's search algorithm.
• 1997: Brassard and Høyer (arXiv:quant-ph/9704027) introduce the amplification operator $\mathbf Q$ for a general algorithm.
• 1998: Brassard, Høyer and Tapp (arXiv:quant-ph/9805082) give quantum counting.
• 2000: the paper formalized here presents amplification, estimation and counting in a unified form with explicit constants.

Setting

Let $\mathcal H = \mathbb C^\iota$ be a finite-dimensional Hilbert space with computational basis $\{|x\rangle : x\in\iota\}$ and a distinguished zero state $|0\rangle$. A quantum algorithm without measurements is a unitary matrix $\mathcal A$ on $\mathcal H$, and a Boolean function $\chi:\iota\to\{0,1\}$ calls a basis state good when $\chi(x)=1$. Write $|\Psi\rangle=\mathcal A|0\rangle=|\Psi_1\rangle+|\Psi_0\rangle$ for the splitting into the projections onto the good and the bad subspaces. The initial success probability is $a=\langle\Psi_1|\Psi_1\rangle$, the probability that measuring $|\Psi\rangle$ gives a good state, and $\theta_a\in[0,\pi/2]$ is the angle with $\sin^2\theta_a=a$.

The operator $\mathbf S_\chi$ flips the sign of the amplitudes of good states, $\mathbf S_0$ flips the sign of the amplitude of $|0\rangle$, and the amplification operator is

$$\mathbf Q=-\mathcal A\,\mathbf S_0\,\mathcal A^{-1}\,\mathbf S_\chi .$$

For an integer $M\ge1$, the quantum Fourier transform is $F_M:|x\rangle\mapsto\frac1{\sqrt M}\sum_{y=0}^{M-1}e^{2\pi\imath xy/M}|y\rangle$, and the controlled power is $\Lambda_M(U):|j\rangle|y\rangle\mapsto|j\rangle U^j|y\rangle$. The phase state is $|S_M(\omega)\rangle=\frac1{\sqrt M}\sum_y e^{2\pi\imath\omega y}|y\rangle$, and $d(\omega_0,\omega_1)=\min_{z\in\mathbb Z}|z+\omega_1-\omega_0|$ is the circular distance. The algorithm $\mathbf{Est\_Amp}(\mathcal A,\chi,M)$ applies $(F_M^{-1}\otimes I)\,\Lambda_M(\mathbf Q)\,(F_M\otimes I)$ to $|0\rangle\mathcal A|0\rangle$, measures the first register to obtain $y\in\{0,\dots,M-1\}$, and outputs $\tilde a=\sin^2(\pi y/M)$.

Formalization targets

Goal: Theorem 12 (Amplitude Estimation)

For every positive integer $k$, the event

$$|\tilde a-a|\le 2\pi k\frac{\sqrt{a(1-a)}}{M}+k^2\frac{\pi^2}{M^2}$$

has probability at least $8/\pi^2$ when $k=1$, and greater than $1-\frac1{2(k-1)}$ when $k\ge2$. If $a=0$ then $\tilde a=0$ with certainty. If $a=1$ and $M$ is even, then $\tilde a=1$ with certainty.

Milestones, in attack order

1. Lemma 1: $\mathbf Q$ acts on $|\Psi_1\rangle$ and $|\Psi_0\rangle$ by an explicit $2\times2$ matrix.
2. Equations (3)–(5): for $0<a<1$, $|\Psi_\pm\rangle$ are orthonormal eigenvectors of $\mathbf Q$ with eigenvalues $e^{\pm\imath2\theta_a}$.
3. Equation (6): $|\Psi\rangle$ in that eigenbasis.
4. Lemma 7: the error in the angle controls the error in $\sin^2$.
5. Lemma 10: the overlap $|\langle S_M(\omega_0)|S_M(\omega_1)\rangle|^2$.
6. Theorem 11: the exact law of phase estimation and its two tail bounds.
7. Two steps of the proof of Theorem 12 (p. 20): the state after $\Lambda_M(\mathbf Q)$, and the outcome law as an even mixture of two phase-estimation laws.

Further statements from the same development are included as companion targets: the success probability $\sin^2((2m+1)\theta_a)$ after $m$ rounds, Theorem 2 (quadratic speedup), Lemma 5 (the phase-generalized $\mathbf Q$), Theorem 13 (counting) and Corollary 14.

Significance

Theorem 12 is the quantitative core of quantum estimation algorithms. Its error bound scales as $1/M$ in the number of applications of $\mathbf Q$, and that scaling is the quadratic speedup behind quantum counting (Theorem 13), quantum mean estimation, and quantum Monte Carlo methods for option pricing and risk analysis. The exact clauses for $a\in\{0,1\}$ make the estimator usable as a zero-error test for the existence of a good state.

All results here are proved in the paper and widely reproduced in textbooks; none is open. What the mission adds is a machine-checked account with the paper's constants: $8/\pi^2$, the strict tail bound $1-1/(2(k-1))$, and the additive term $k^2\pi^2/M^2$. It also covers every modulus $M\ge1$, not only powers of two, and arbitrary $\mathcal A$ and $\chi$, not only uniform search. Related statements are posed on the platform but unproved:

• QAlgorithms.Nannicini.amplitudeEstimation_error is the special case $k=1$, $M=2^m$, with a bit-string presentation of the algorithm.
• QAlgorithms.Nannicini.groverOperator_eigenstates states (3)–(4) for an abstract reflection.
• QAlgorithms.DeWolf.amplitudeAmplification covers (8) and the $1-a$ half of Theorem 2.

The Grover theorems already proved on the platform treat a single marked item with a uniform start.

Difficulty

The obvious argument has two parts: $\mathbf Q$ rotates a plane by $2\theta_a$, and phase estimation reads off $\theta_a$. Neither part settles the measurement law. The outcome probability is a sum over the second register of the squared amplitudes of an entangled state. Reducing it to two independent phase-estimation laws requires orthonormality of $|\Psi_\pm\rangle$, and that holds only for $0<a<1$. The goal does not assume this: the degenerate cases $a\in\{0,1\}$, where $|\Psi_\pm\rangle$ do not exist, must be handled separately.

On the phase-estimation side, the tail bound for $k\ge2$ must be strict and must hold for every $M\ge1$. The bound $8/\pi^2$ for $k=1$ relies on a minimization over $\Delta\in[0,1/M]$ that needs $M>2$, while the goal has no such hypothesis, so the small cases $M\le2$ need their own argument. Finally, the second eigenphase appears as $1-\theta_a/\pi$, and the matching outcome $M-y$ wraps to $0$ at $y=0$.

Formalization scope

States are vectors $\iota\to\mathbb C$ over a finite type $\iota$ (the paper writes $\chi:\mathbb Z\to\{0,1\}$), operators are matrices, and $\{0,1\}$ is Bool. $\mathcal A$ is assumed unitary and $\mathcal A^{-1}$ is written $\mathcal A^\dagger$. The second register is Fin M with $M\ge1$; $F_M$ is the platform's published Fourier matrix ShorAlgorithms.Shared.fourierMatrix (same sign and normalization as (13)), $F_M^{-1}$ is its conjugate transpose, and $\Lambda_M$ is an explicit matrix on Fin M × ι. The outcome law is the sum over the second register of squared moduli of the final state, and an event's probability is the sum of the outcome probabilities over it. $a$ is computed from $\mathcal A$, $\chi$ and $|0\rangle$, and $\theta_a=\arcsin\sqrt a$. The goal assumes neither $0<a<1$ nor $M>2$, and it keeps the strict inequality for $k\ge2$. The step "after step 2, ignoring global phase" is stated with its phase $-\imath$ written out.

A formalization that takes $a$ or $\theta_a$ as a free parameter, assumes the mixture form of the outcome law, or reasons about $|\Psi_\pm\rangle$ without deriving them from $\mathcal A$ and $\chi$ would make the goal trivial. The statements here do none of these: every quantity is computed from $\mathcal A$, $\chi$, $|0\rangle$ and $M$. The clauses "uses exactly $M$ evaluations of $f$" (Theorem 12) and "requires exactly $\lceil\sqrt N\rceil$ evaluations" (Corollary 14) are not formalized, because the matrix model has no oracle whose calls could be counted. Theorem 13 is stated for any unitary sending $|0\rangle$ to the uniform superposition, which includes $F_N$, as the paper allows on p. 20.

A complete development needs:

• geometric sums of roots of unity;
• the Fejér-kernel identity of Lemma 10;
• the inequality $\sin x\ge 2x/\pi$ on $[0,\pi/2]$;
• a bound on $\sum_{j\ge k}1/j^2$;
• Kronecker-product bookkeeping for two-register states.

The phase-estimation part (Lemma 10, Theorem 11) does not depend on amplification and can be reused by any later formalization of Fourier-based phase estimation. Proofs of individual milestones, and lemmas on Fin M Fourier sums, are welcome.

Selected references

• G. Brassard, P. Høyer, M. Mosca, A. Tapp, Quantum Amplitude Amplification and Estimation, in Quantum Computation and Information, Contemporary Mathematics 305, AMS, 2002, pp. 53–74. arXiv:quant-ph/0005055
• G. Brassard, P. Høyer, An exact quantum polynomial-time algorithm for Simon's problem, ISTCS 1997. arXiv:quant-ph/9704027
• G. Brassard, P. Høyer, A. Tapp, Quantum counting, ICALP 1998. arXiv:quant-ph/9805082
• L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
• A. Montanaro, Quantum speedup of Monte Carlo methods, Proc. R. Soc. A 471, 2015. arXiv:1504.06987

Motivation

Grover's algorithm (Grover 1996) finds a marked item among $N$ with $O(\sqrt N)$ queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701001, SIAM J. Comput. 26(5), 1997): relative to a random oracle, a quantum algorithm needs $\Omega(2^{n/2})$ queries to decide whether a string has a preimage. The bound matches Grover's algorithm up to a constant factor, and its hybrid argument is one of the two standard lower-bound methods of the field, together with the polynomial method (Beals et al. 1998) and the adversary method (Ambainis 2000).

Timeline:

• 1996: Grover's algorithm searches $N$ items with $O(\sqrt N)$ queries.
• 1997: the paper proves $\mathbf{BQTime}(o(2^{n/2})) \not\supseteq \mathbf{NP}$ relative to a random oracle with probability 1 (Theorem 3.5), and the $\Omega(2^{n/3})$ bound for random permutations (Theorem 3.6).
• 1998: Boyer, Brassard, Høyer and Tapp give tight bounds for quantum searching.
• 1999: Zalka shows Grover's algorithm is exactly optimal.

Setting

A $T$-query algorithm acts on vectors $\varphi \in \mathbb{C}^{(X \cup \{\bot\}) \times R \times W}$, where $X$ is the set of query strings, $R$ the set of answers (an additive group) and $W$ a finite workspace. A basis configuration $(x, z, w)$ with $x \in X$ is querying $x$; $(\bot, z, w)$ is not querying. For an oracle $f : X \to R$ the oracle operator is

$$O_f\,|x, z, w\rangle = |x, z + f(x), w\rangle, \qquad O_f\,|\bot, z, w\rangle = |\bot, z, w\rangle .$$

The algorithm consists of a unit vector $\varphi_0$, unitaries $U_0, \dots, U_{T-1}$ that do not depend on the oracle, and a set of accepting configurations. With oracle $A$ its states are $\varphi_{i+1} = U_i O_A \varphi_i$; the acceptance probability is the squared norm of the accepting part of $\varphi_T$. The query magnitude of $y$ in $\varphi$ is $q_y(\varphi) = \sum_{z, w} |\varphi(y, z, w)|^2$ (Definition 3.2). The algorithm decides a property if it accepts with probability at least $2/3$ when the property holds and at most $1/3$ when it fails.

In the main theorem $X = R = \{0,1\}^n$ with bitwise addition, and the oracle is a uniformly random function $A : \{0,1\}^n \to \{0,1\}^n$. The question is whether $1^n$ belongs to $\mathcal{L}_A = \{y : \exists x\ A(x) = y\}$.

Formalization targets

Goal: Theorem 3.5 (finite form)

$$\exists\, c > 0\ \exists N\ \forall n \ge N\ \forall M \text{ with } T \le c\, 2^{n/2} \text{ queries}: \quad \Pr_A\bigl[M^A \text{ fails to decide } \exists x\ A(x) = 1^n\bigr] \ge \tfrac18 .$$

The constant is existential, matching the theorem's hypothesis $T(n) = o(2^{n/2})$; $c$ and $N$ do not depend on the workspace or the algorithm.

Milestones

1. Theorem 3.1: unit vectors at distance $\varepsilon$ have measurement distributions within total variation $4\varepsilon$.
2. Theorem 3.3 (corrected): changing oracle answers on time–string pairs of total query magnitude $\le \varepsilon^2/T$ moves the final state by at most $2\varepsilon$.
3. Corollary 3.4 (corrected): outside a set of at most $4T^2/\varepsilon^2$ strings, changing the oracle at one string moves the final state by at most $\varepsilon$.
4. $\Pr[1^n \text{ has no preimage}] = ((2^n-1)/2^n)^{2^n} \ge 1/4$.
5. $\Pr[1^n \text{ has a unique preimage}] = ((2^n-1)/2^n)^{2^n-1} \ge 1/e$.
6. Final states within $1/13$ for $A$ and $A_y$ force failure on one of them.
7. The double counting: failing oracles with a unique preimage are at least half the successful oracles with none.

Significance

The theorem shows that the quadratic speed-up of Grover's algorithm cannot be improved for unstructured search, and that relative to a random oracle $\mathbf{NP} \not\subseteq \mathbf{BQP}$; any quantum algorithm for NP-complete problems must use the structure of the problem. Theorem 3.3 and Corollary 3.4 isolate the constraint unitary evolution places on "quantum parallelism" and are reused across quantum lower bounds, including the permutation bound of the companion mission (Theorem 3.6).

The results are proved on paper and, to our knowledge, have no machine-checked proof. The mission produces a formal query model with an XOR oracle, a formal hybrid argument, and the lower bound with its constants checked. Two printed bounds are wrong by constant factors (below); the formal statements carry the corrected constants, and a formal proof settles them. Grover's matching upper bound is on the platform as Grover.search_succeeds_bounded, for a phase oracle and one fixed algorithm.

Difficulty

The obvious argument — each query reveals one bit about where the preimage is, so $\Omega(2^n)$ queries are needed — fails for quantum algorithms, which query all strings in superposition at once. The difficulty is to bound how much a superposition of queries can learn, which requires controlling the accumulated effect of small changes across $T$ unitary steps, and then converting a bound on states into a statement about the probability of failure over random oracles, where the set of sensitive strings depends on the oracle.

Formalization scope

The paper's oracle quantum Turing machines are replaced by the query model above, the model its proofs use. Every oracle QTM running $T$ steps is a $T$-query algorithm: oracle answers on lengths other than $n$ are fixed and absorbed into the unitaries, as the proof fixes them, and the input $1^n$ is absorbed into $\varphi_0$. Queries return the full value $A(x) \in \{0,1\}^n$; one Boolean query is two full-value queries, so the goal implies the Boolean-oracle bound with $c$ halved. Strings are Fin n → ZMod 2; states are EuclideanSpace ℂ (Option X × R × W); probabilities over oracles are counting fractions over all $(2^n)^{2^n}$ functions; total variation distance is the paper's $\sum_x |\mathcal D(x) - \mathcal D'(x)|$ without the factor $1/2$.

Corrections: Theorem 3.3 is printed with conclusion $\le \varepsilon$, which fails (one query string, $T = 1$, distance $2$ at $\varepsilon = 1$; machine-checked); the true bound is $2\varepsilon$. Corollary 3.4 is printed with $|S| \le 2T^2/\varepsilon^2$, which fails (16 strings, $T = 1$, $\varepsilon = 0.45$); the true bound is $4T^2/\varepsilon^2$. The printed constant $T(n) \le 2^{n/2}/20$ in the proof of Theorem 3.5 does not support the step $2^n - \mathrm{card}(S) \ge 2^{n-1}$ even with the paper's own count; the goal states an existential constant, and $c = 1/37$ works with the corrected Corollary 3.4. The closing probability-$1$ argument over countably many machines and the class statement about $\mathbf{BQTime}$ are not formalized.

A formalization in which algorithms query at every step on every branch (no $\bot$ sector), only one side of the bounded-error condition is tested, or the probability is taken over a set of oracles that excludes the hard instances, proves a weaker theorem and is ruled out by these definitions.

Needed infrastructure: norms of finite-dimensional complex vectors, unitaries as linear isometry equivalences, finite counting of functions. The query model and the hybrid argument are reusable for any quantum query lower bound.

Selected references

• C. H. Bennett, E. Bernstein, G. Brassard, U. Vazirani, Strengths and weaknesses of quantum computing, SIAM J. Comput. 26(5):1510–1523, 1997. arXiv:quant-ph/9701001
• L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
• M. Boyer, G. Brassard, P. Høyer, A. Tapp, Tight bounds on quantum searching, Fortschr. Phys. 46, 1998. arXiv:quant-ph/9605034
• C. Zalka, Grover's quantum searching algorithm is optimal, Phys. Rev. A 60, 1999. arXiv:quant-ph/9711070
• R. Beals, H. Buhrman, R. Cleve, M. Mosca, R. de Wolf, Quantum lower bounds by polynomials, J. ACM 48, 2001. arXiv:quant-ph/9802049
• A. Ambainis, Quantum lower bounds by quantum arguments, J. Comput. Syst. Sci. 64, 2002. arXiv:quant-ph/0002066

Why count copies of a quantum state

A mixed state of a $D$-dimensional quantum system is a $D\times D$ positive semidefinite matrix $\rho$ of trace $1$. Writing $\rho$ down takes about $D^2$ real numbers, and $D$ is exponential in the number of qubits, so learning $\rho$ in full is expensive. Holevo's theorem and the random access code bounds of Ambainis, Nayak, Ta-Shma and Vazirani say that an $n$-qubit state carries far fewer usable classical bits than its $2^n$ amplitudes suggest. Shadow tomography, introduced by S. Aaronson (arXiv:1711.01053), makes this quantitative: given $M$ known two-outcome measurements $E_1,\dots,E_M$, how many copies of an unknown $\rho$ are needed to estimate every acceptance probability $\operatorname{Tr}(E_i\rho)$ to within $\varepsilon$?

Aaronson shows that $\widetilde O(\log^4 M\cdot\log D/\varepsilon^4)$ copies suffice, polylogarithmic in $M$ and $D$. The question this mission addresses is the converse: how many copies are necessary. Section 6 of the paper proves two lower bounds. Theorem 16 gives $\Omega(\min\{D,\log M\}/\varepsilon^2)$ even when $\rho$ and the $E_i$ are diagonal (a classical distribution). Theorem 19, the goal here, strengthens the dimension term to $D^2$ for genuinely quantum states.

Timeline:

• 2016: full tomography of a $D$-dimensional state to trace-distance accuracy $\varepsilon$ needs $\Theta(D^2/\varepsilon^2)$ copies up to logarithmic factors, with upper and lower bounds by O'Donnell and Wright (arXiv:1508.01907) and Haah, Harrow, Ji, Wu and Yu (arXiv:1508.01797).
• 2017–2018: Aaronson poses shadow tomography (Problem 1), proves the polylogarithmic upper bound (Theorem 2), and proves the lower bounds of Theorems 16 and 19.
• 2020 onward: classical shadows (Huang, Kueng and Preskill, arXiv:2002.08953) and later shadow-tomography algorithms study the same estimation task with other measurement models and improved upper bounds.

Setting

Fix a dimension $D$. A two-outcome measurement is a $D\times D$ Hermitian matrix $E$ with $0\preceq E\preceq I$; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$. The tensor power $\rho^{\otimes k}$ is the $D^k\times D^k$ matrix of $k$ independent copies. A strategy using $k$ copies is a measurement of $\rho^{\otimes k}$ with finitely many outcomes $\omega\in\Omega$, given by positive semidefinite matrices $\Pi_\omega$ with $\sum_\omega\Pi_\omega = I$, together with outputs $b(\omega)=(b_1(\omega),\dots,b_M(\omega))$. It succeeds on $\rho$ when, with probability at least $2/3$ over $\omega$, $|b_i(\omega)-\operatorname{Tr}(E_i\rho)|\le\varepsilon$ for every $i\in[M]$.

The proof works with these further objects, all defined in the mission:

• an orthogonal projection $\mathbb P$ onto an $N/2$-dimensional subspace of $\mathbb C^N$ (Hermitian, idempotent, trace $N/2$);
• $\rho_{\mathbb P} := \tfrac2N\mathbb P$, the maximally mixed state on that subspace;
• $\sigma_{\mathbb P,\varepsilon} := (1-6\varepsilon)\,\mathbb I/N + 6\varepsilon\,\rho_{\mathbb P}$;
• the von Neumann entropy in bits, $S(\rho) = -\sum_x\lambda_x\log_2\lambda_x$ over the eigenvalues of $\rho$;
• for states $\sigma_1,\dots,\sigma_K$ and $\zeta := \tfrac1K\sum_i\sigma_i^{\otimes T}$, the quantum mutual information with the classical index, $I(\zeta;i) := S(\zeta) - \tfrac1K\sum_i S(\sigma_i^{\otimes T})$.

Formalization targets

Goal: Theorem 19 (p. 23)

There are a universal constant $c>0$ and a threshold $N_0$ such that for all $D\ge N_0$, all $M$ with $\log_2 M\ge N_0^2$ and all $0<\varepsilon\le\tfrac16$, some measurements $E_1,\dots,E_M$ on $\mathbb C^D$ force every strategy that succeeds on every mixed state to use

$$k \;\ge\; c\,\frac{\min\{D^2,\ \log_2 M\}}{\varepsilon^2}$$

copies. The goal fixes only the shape $\Omega(\min\{D^2,\log M\}/\varepsilon^2)$, not a constant, so a sharper constant does not invalidate it.

Milestones (pp. 23–24)

The milestones follow the proof, which sets $N:=\lfloor\min\{D,\sqrt{\log_2 M}\}\rfloor$ and $K:=\lfloor c^{N^2}\rfloor$:

1. Eq. (2): for some $c\in(1,2)$ and all large even $N$ there are $K$ projections $\mathbb P_i$ of rank $N/2$ with $|\operatorname{Tr}(\mathbb P_i\rho_j)-\tfrac12|\le\tfrac1{12}$ for all $i\ne j$.
2. $\operatorname{Tr}(\mathbb P_i\sigma_i) = \tfrac12+3\varepsilon$.
3. $|\operatorname{Tr}(\mathbb P_j\sigma_i)-\tfrac12| = 6\varepsilon|\operatorname{Tr}(\mathbb P_j\rho_i)-\tfrac12|\le\tfrac\varepsilon2$ for $i\neq j$.
4. The exact entropy $S(\sigma_i) = \log_2 N - [1-h(\tfrac12+3\varepsilon)]$, with $h$ the binary entropy, and the bound $S(\sigma_i)\ge\log_2 N - C\varepsilon^2$.
5. $I(\zeta;i)\le T(\log_2 N - S(\sigma_i))$ when all $\sigma_i$ have equal entropy.

Significance

Theorem 19 shows that the $\log M$ dependence of shadow tomography cannot be removed, and that for $M\ge 2^{D^2}$ shadow tomography is as hard as full tomography: as $M$ grows the bound becomes the $\Omega(D^2/\varepsilon^2)$ tomography lower bound, which it therefore contains. Compared with the classical Theorem 16, it shows that quantum states need quadratically more copies in the dimension term. The $1/\varepsilon^2$ factor matches the upper bound of Proposition 20 for the decision version, so the $\varepsilon$-dependence of the lower bound is tight in that setting.

The results are proved in the paper; none of them has a machine-checked proof that we know of. Formalizing the argument requires von Neumann entropy and its additivity on tensor products, the bound $S\le\log_2(\text{dimension})$, a Holevo-plus-Fano step that turns successful estimation into mutual information, and the existence of many nearly orthogonal half-dimensional subspaces. Each is reusable well beyond this mission.

Difficulty

The obvious attempt adapts the classical argument of Theorem 16, which hides $K$ subsets of $[N]$ in a biased distribution. Quantum states allow $\exp(\Omega(N^2))$ hidden subspaces instead of $\exp(\Omega(N))$ subsets, which is where $D^2$ comes from, but two steps change character. First, the hiding family must be shown to exist: Eq. (2) is a concentration statement for random subspaces, and the lemma the paper cites for it (Lemma 18) is misstated, as explained below. Second, the information bound must be carried out for quantum states: the step "learning $i$ from $\zeta$ requires $I(\zeta;i)\ge\log_2 K$" needs Holevo's bound and Fano's inequality, adjusted for success probability $2/3$ rather than certainty.

Formalization scope

Matrices are Matrix n n ℂ over a finite index type; the goal uses $n=\texttt{Fin } D$. Conventions committed to:

• A mixed state is the published WildeQIT.IsDensityOperator (positive semidefinite, trace $1$), reused as a reference item.
• A strategy is a finite-outcome POVM on $\rho^{\otimes k}$, indexed by Fin k → Fin D, with deterministic outputs $b(\omega)\in\mathbb R^M$; classical randomness can be absorbed into the outcome set.
• Probabilities and traces are real parts of complex traces. Entropies use $\log_2$; Lean's $\log_2 0 = 0$ gives $0\log 0=0$, and vnEntropy returns $0$ on non-Hermitian matrices, which no statement uses.
• Added to the goal: the threshold $N_0$ on $D$ and $\sqrt{\log_2 M}$ (for $D=1$, $k=0$ succeeds) and $\varepsilon\le\tfrac16$ (for $\varepsilon\ge\tfrac12$, the output $b_i=\tfrac12$ succeeds with $k=0$). Problem 1's $b_i\in[0,1]$ is dropped, an equivalent statement under clipping.
• The measurements are chosen before the strategy (for every strategy, the same $E$), which is the meaning of a lower bound.

A trivializing formalization is ruled out: the goal does not mention $N$, $K$, $\mathbb P_i$, $\sigma_i$ or $\zeta$, the success condition quantifies over all mixed states rather than a vacuous class, and the measurements are fixed before the strategy.

Not drafted:

• Lemma 18 (pp. 22–23) is false as printed. Since $\mathbb E_S[\rho_S] = \mathbb I/N$, $\operatorname{Tr}(\mathbb P_T\rho_S)$ concentrates at $1/2$, not $1/4$. The proof needs only Eq. (2), which is centred correctly and is a milestone.
• Eq. (2) is stated as existence, not as "probability $1-o(1)$ over Haar-random subspaces", because Mathlib has no Haar measure on the unitary group or the Grassmannian; existence is what the proof uses.
• "$I(\zeta;i)$ must be at least $\log_2 K$" is not drafted: as stated it is imprecise for success probability $2/3$, and the correct Holevo–Fano form is left to the solver.
• The final combination $I(\zeta;i)=O(T\varepsilon^2)$, $T=\Omega(N^2/\varepsilon^2)$ is the goal's last step.

Contributions welcome: proofs of the milestones; a Haar-measure version of Eq. (2); von Neumann entropy infrastructure (additivity, the dimension bound, concavity); Holevo's bound and Fano's inequality for finite-dimensional states.

Selected references

• S. Aaronson, Shadow Tomography of Quantum States, arXiv:1711.01053v2, 2018; STOC 2018. https://arxiv.org/abs/1711.01053
• P. Hayden, D. Leung, A. Winter, Aspects of generic entanglement, Comm. Math. Phys. 265, 2006. https://arxiv.org/abs/quant-ph/0407049
• R. O'Donnell, J. Wright, Efficient quantum tomography, STOC 2016. https://arxiv.org/abs/1508.01907
• J. Haah, A. W. Harrow, Z. Ji, X. Wu, N. Yu, Sample-optimal tomography of quantum states, IEEE Trans. Inf. Theory 63, 2017. https://arxiv.org/abs/1508.01797
• A. Ambainis, A. Nayak, A. Ta-Shma, U. Vazirani, Dense quantum coding and quantum finite automata, J. ACM 49, 2002. https://arxiv.org/abs/quant-ph/9804043
• H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics 16, 2020. https://arxiv.org/abs/2002.08953

Why quantum Tanner codes matter

An error-correcting code protects information by adding redundancy. A quantum code must also account for two kinds of errors, commonly called $X$ and $Z$ errors. Quantum low-density parity-check codes use checks that each touch only a bounded number of qubits, while each qubit participates in only a bounded number of checks. Such locality matters when the number of qubits grows. For years it was difficult to make both the number of encoded qubits and the minimum distance proportional to the block length while retaining bounded-weight checks. Leverrier and Zémor's quantum Tanner construction gives a route through local codes placed on an expanding square complex; its main distance theorem is the target of this mission Leverrier and Zémor, 2022.

The construction combines two earlier ingredients. Left-right Cayley complexes provide the squares and expansion properties used by the code Dinur, Evra, Livne, Lubotzky, and Mozes, 2021. Robustness of a dual tensor code, including after puncturing coordinates, controls local words Panteleev and Kalachev, 2021. The paper states the local reduction property as Theorem 1 and derives the rate and distance bounds as Theorem 17. This mission formalizes that implication under the paper's stated component-code and expansion conditions; the separate random-code result that supplies robust examples belongs to the second mission of this series.

The square complex and its codes

Let $G$ be a finite group and let $A,B\subseteq G$ be inverse-closed sets, each of size $\Delta$. The total no-conjugacy condition says $ag\ne gb$ for every $a\in A$, $b\in B$, and $g\in G$. Vertices are two copies of the group, $V=G\times\{0,1\}$. A square associated with $v=(g,i)$ and $(a,b)\in A\times B$ has vertices $v$, $(ag,1-i)$, $(gb,1-i)$, and $(agb,i)$. The set of squares is $Q$, and a binary word on $Q$ has length $n=|Q|$. At a vertex $v$, the incident squares are indexed by $A\times B$; this indexing makes the local view $x_v$ of a word $x\in\mathbb F_2^Q$ an $A\times B$ matrix Leverrier and Zémor, §§3.2 and 4.1.

A binary linear code $C_A$ has coordinates indexed by $A$, and $C_B$ has coordinates indexed by $B$. Their tensor code $C_A\otimes C_B$ consists of matrices whose columns lie in $C_A$ and whose rows lie in $C_B$. The dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$ is the sum of the column and row codes. In Definition 5, it is $w$-robust when every member of weight at most $w$ is supported on a union of few rows and columns, with the bounds determined by the two component minimum distances. Definition 8 requires this property after deleting up to $p$ coordinates from each side. These are conditions on all relevant codewords and all permitted puncturings, including the unpunctured pair Leverrier and Zémor, pp. 15–16.

The two Tanner codes are $\mathcal C_0=T(\mathcal G^\square_0,(C_A\otimes C_B)^\perp)$ and $\mathcal C_1=T(\mathcal G^\square_1,(C_A^\perp\otimes C_B^\perp)^\perp)$. Here $\mathcal G^\square_i$ is the square-adjacency graph on the vertices in copy $i$. Together they define the quantum CSS code $\mathcal Q=(\mathcal C_0,\mathcal C_1)$. Its dimension counts encoded qubits. Its distance is the smaller of the minimum weights in $\mathcal C_0\setminus\mathcal C_1^\perp$ and $\mathcal C_1\setminus\mathcal C_0^\perp$ Leverrier and Zémor, pp. 14, 18.

Formalization targets

The goal is Theorem 17. Fix $0<\rho<1/2$, $0<\varepsilon<1/2$, $1/2+\varepsilon<\gamma<1$, and $\delta>0$. For sufficiently large $\Delta$, take a left-right Cayley complex satisfying total no-conjugacy and the paper's Ramanujan conditions. Require $0<\dim C_A\le\rho\Delta$, $\dim C_B=\Delta-\dim C_A$, minimum distance at least $\delta\Delta$ for $C_A,C_B$ and both duals, and $\Delta^{3/2-\varepsilon/2}$ robustness with $\Delta^\gamma$ resistance to puncturing for both relevant dual tensor codes. The target is

$$k\ge (1-2\rho)^2 n,\qquad d\ge \frac{\delta n}{4\Delta^{3/2+\varepsilon}}.$$

The milestones mirror the paper's route to this result. Lemma 4 bounds the nontrivial eigenvalues of the union and square graphs. Propositions 6 and 7 turn dual-tensor robustness into a decomposition and a $3/2$ closeness bound. Theorem 1 supplies a weight-reducing local codeword for every sufficiently light nonzero Tanner-code word. Display (5) supplies the dimension lower bound. Theorem 17 combines the two distance directions with that rate estimate Leverrier and Zémor, pp. 12, 15–16, 18–23.

What the result supplies

The lower bound on $k$ ensures a positive fraction of qubits can carry logical information when $\rho<1/2$. The lower bound on $d$ rules out small undetectable logical errors. For a fixed allowable degree $\Delta$, both bounds scale linearly with $n$. The paper also shows that random component codes can satisfy the robustness assumptions; that probabilistic result is a separate formalization target Leverrier and Zémor, Theorems 9 and 17.

A checked development would make explicit how the square indexing, duals, punctured codes, and CSS quotient fit together. The source proves the mathematical result; the statements here remain open Lean theorems. Reusable contributions include the tensor-code interface, spectral bounds for the graph construction, and lemmas connecting local views to the global Tanner codes. A proof of the existence of infinite Ramanujan complex families is outside this mission's stated target.

Where the proof is difficult

A light global codeword need not have a local view that is itself close to a tensor-code word. Some square-graph vertices have unusually large local weight, and puncturing is needed to isolate coordinates shared with those exceptional vertices. The paper's small-set expansion estimates and robustness conditions control those interactions. Simply averaging local weights does not yield the weight-reducing local codeword asserted by Theorem 1 Leverrier and Zémor, §4.2.

Formalization scope

Words are functions into ZMod 2, codes are submodules, and a matrix is a function on $A\times B$ with $A$ indexing rows. The square coordinates are four-element vertex sets. The construction uses $V=G\times\operatorname{Fin}(2)$ and counts $n$ as the number of squares rather than building $n=\Delta^2|G|/2$ into a definition. The minimum distance of the zero code is infinity, and robustness uses inequalities involving that extended value. Powers of $\Delta$ and the parameters $w,p$ are real; the paper uses integer $w,p$ in Definition 8, while the theorem's power thresholds need real comparisons. The formal robustness predicate includes Definition 5's range $0\le w\le\Delta^2$; the theorem thresholds satisfy it for sufficiently large $\Delta$. These conventions are recorded with each item.

The goal quantifies over every finite complex satisfying inverse closure, total no-conjugacy, and Ramanujan conditions, with a uniform threshold $\Delta_0$ chosen before the group and codes. This pins the complexes in the cited infinite family without formalizing their existence. In particular, the goal contains no auxiliary set or local reduction assumption that could make the distance bound immediate. The published CodingTheory and TillichZemor.HGP.Setting definitions supply dual codes and CSS dimension; the paper-specific setting supplies the square complex, local views, Tanner codes, and robustness. Contributions that keep these conventions and close any milestone theorem are welcome.

Selected references

• A. Leverrier and G. Zémor, Quantum Tanner codes, arXiv preprint, 2022. arXiv:2202.13641v3.
• I. Dinur, S. Evra, R. Livne, A. Lubotzky, and S. Mozes, Locally Testable Codes with constant rate, distance, and locality, arXiv preprint, 2021. arXiv:2111.04808.
• P. Panteleev and G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, arXiv preprint, 2021. arXiv:2111.03654.

Motivation

A max-XORSAT instance asks for a binary assignment that satisfies as many parity constraints as possible. A matrix specifies the parity check in each constraint, while a second binary vector specifies the desired parity. The objective can be written as the number of satisfied constraints minus the number violated, so an assignment with a high objective value is also a good approximate solution. Jordan and coauthors study decoded quantum interferometry (DQI), a way to sample candidate assignments by encoding a weighted superposition of error patterns and then decoding their syndromes. Their ideal-state analysis assumes that low-weight errors have distinct syndromes. Real decoders can succeed on many errors even when this uniqueness condition fails, which makes the theorem in this mission relevant to the algorithmic regime beyond the guaranteed decoding radius. Jordan et al., §§8.1 and 10.

The paper's 2024 preprint introduced DQI for linear constraint satisfaction and related optimization problems. Its revised 2025 version studies the effect of decoder failures on the measured objective in Theorem 10.1. This mission uses that revision, arXiv:2408.08292v5, and isolates the first inequality of equation (172). The same section supplies explicit identities for the norm of the postselected state and for its objective matrix, making the theorem a bounded campaign of finite combinatorics and linear algebra. Jordan et al., §10, pp. 35–43.

Setting

Fix integers $m,n\ge0$ and a binary matrix $B\in\mathbb F_2^{m\times n}$. Its $i$th row defines a parity $b_i\cdot x$ of an assignment $x\in\mathbb F_2^n$. For a binary vector $v\in\mathbb F_2^m$, the objective is

$$f_v(x)=\sum_{i=1}^{m}(-1)^{b_i\cdot x+v_i}.$$

An error pattern $y\in\mathbb F_2^m$ has syndrome $B^\top y$ and Hamming weight $|y|$. The weight-$k$ shell $E_k$ contains all errors with $|y|=k$. Choose $0\le\ell\le m$ and real weights $w_0,\ldots,w_\ell$. The ideal syndrome-space state in equation (140) sums $(-1)^{v\cdot y}|B^\top y\rangle$ over each $E_k$, multiplied by $w_k/\sqrt{\binom m k}$. Jordan et al., equations (140) and (171).

A deterministic decoder $\mathrm{dec}:\mathbb F_2^n\to\mathbb F_2^m$ guesses an error from its syndrome. It correctly identifies $y$ when $\mathrm{dec}(B^\top y)=y$. Write $D_k\subseteq E_k$ for the correctly identified errors and $F_k=E_k\setminus D_k$ for the failures. The shell failure rate is $\varepsilon_k=|F_k|/\binom m k$, and $\varepsilon=\max_{0\le k\le\ell}\varepsilon_k$. Postselecting successful decoding leaves the unnormalized state $\widetilde P_D(f)$ formed by replacing each $E_k$ in the ideal state with $D_k$. Apply the binary Hadamard transform, divide by the resulting norm, measure $x$, and evaluate $f_v(x)$. Denote this measured expectation by $\langle f_v\rangle$. Jordan et al., §10.3, pp. 39–40.

Formalization targets

Theorem 10.1: the averaged objective

Let $N=\sum_{k=0}^{\ell}w_k^2(1-\varepsilon_k)$ be the squared norm of the postselected state. The goal, for $N>0$ and uniform $v\in\mathbb F_2^m$, is

$$\mathbb E_v\langle f_v\rangle\ge \frac{w^\top A^{(m,\ell,0)}w-2\varepsilon(m+1)w^\top w}{N}.$$

The matrix $A^{(m,\ell,0)}$ is the symmetric tridiagonal matrix in equation (70): its diagonal is zero and its entries adjacent to the diagonal are $a_k=\sqrt{k(m-k+1)}$. This is the first inequality of (172), with the decoder's actual failure fractions in $N$ and the worst shell failure rate in the correction. It has no minimum-distance hypothesis. Jordan et al., Theorem 10.1, pp. 39–40.

Supporting targets

The milestone list includes the norm identity of Lemma 10.4, the ideal and postselected objective matrices of Lemmas 10.2 and 10.5, the normalized expectation identity in (179), the averaged matrix identities of Lemmas 10.3 and 10.6, and the error-matrix bound of Lemma 10.7. A separate companion item records the second comparison printed in (172) under an explicit sign condition; without that condition, the printed comparison can fail. Jordan et al., §10, pp. 36–43.

Significance

The result assigns a quantitative cost to decoding errors. It says how the measured max-XORSAT objective changes when some error patterns are lost during postselection, while permitting a code whose low-weight errors share syndromes. Consequently the theorem addresses the setting in which practical decoding succeeds often but exact distance-based uniqueness is unavailable. The denominator also records the survival probability of the weighted state, so the bound keeps the actual normalization visible. Jordan et al., §10, pp. 35 and 39–43.

A complete formalization would provide reusable definitions for binary syndrome decoding, shellwise failure rates, real-amplitude states, normalized measurement expectations, and finite objective matrices. The paper proves the result on paper; this mission asks for machine-checked proofs of the stated goal and its milestones. The formal development would also document exactly which part of equation (172) requires an additional sign assumption. No proof is claimed by the draft statements themselves.

Difficulty

When two errors have the same syndrome, the ideal syndrome state can combine their amplitudes, so its norm need not equal $w^\top w$. Postselection changes which errors remain, and the measured objective depends on the normalized state for each $v$. Replacing that normalized expectation with the objective of an average state would change the claim. The proof must keep the decoder fixed while $v$ varies and must control the error matrix uniformly over every real weight vector. The printed second inequality of (172) adds a separate sign issue: a smaller positive denominator reverses the expected comparison when the numerator is negative. Jordan et al., equations (161), (171)–(172), (179)–(182).

Formalization scope

Lean uses ZMod 2 for bits, Fin m and Fin n for zero-based coordinates, functions for binary vectors, and Matrix for $B$. The decoder is one function of the syndrome, independent of $v$. Hamming shells, correct and failed decoding sets, and $\varepsilon_k$ are computed from that function. Weights and amplitudes are real. The postselected state uses the factor $1/\sqrt{\binom m k}$; the Hadamard transform uses $1/\sqrt{2^n}$. The average over $v$ is the sum over all $2^m$ vectors divided by $2^m$. The tridiagonal entries compute $m-k$ in the reals, preserving the square-root formula at the boundary.

Two domain conditions are made explicit. The bound $\ell\le m$ rules out absent weight shells, for which Lean would otherwise assign zero to division by $\binom m k=0$. The condition $N>0$ rules out a zero postselected state, whose normalized expectation would likewise be assigned a meaningless zero by total real division. The goal ranges over every binary matrix, every fixed deterministic decoder, and every real weight vector satisfying those conditions. It states the expectation of the explicit postselected state after a Hadamard transform, rather than an unconstrained expectation variable.

The supporting development needs finite character sums, Hamming-shell cardinalities, matrix quadratic forms, and an operator bound for a symmetric real matrix. These components can serve other finite decoding and quantum-state calculations. Contributions proving the seven cited milestones or the goal are within scope. The circuit's resource accounting, asymptotic equation (173), and numerical decoder studies are outside this mission.

Selected references

• S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, and R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025 revision of the 2024 preprint. arXiv

Motivation

The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028) prepares a parametrized quantum state whose measurement yields a candidate solution of a combinatorial optimization problem. Its level-one version alternates a single phase operator and a single mixing operator and is simple enough to analyse by hand. In arXiv:1412.6062 the same authors applied it to Max E3LIN2 with bounded occurrence: given linear equations mod 2, each on exactly three bits, with every bit in at most $D+1$ equations, satisfy as many equations as possible. A uniformly random string satisfies half of them in expectation; the question is by how much an algorithm can beat $\tfrac12$.

Without the occurrence bound no efficient algorithm achieves $\tfrac12+\epsilon$ unless P = NP (Håstad, J. ACM 2001). With every bit in at most $D+1$ equations the history, as recounted on pp. 2–3 of the paper, is:

• 2000: Håstad gave a classical algorithm with approximation ratio $\tfrac12+\Omega(1/D)$ (Inf. Process. Lett. 74).
• 2001: Trevisan showed that an efficient algorithm achieving $\tfrac12+c/D^{1/2}$ for a sufficiently large constant $c$ would imply P = NP (STOC).
• 2014: the first version of this paper showed that the level-one QAOA satisfies at least $\big(\tfrac12+\tfrac1{22D^{3/4}}\big)m$ equations.
• 2015: Barak et al. gave an efficient classical algorithm reaching $\big(\tfrac12+\Omega(D^{-1/2})\big)m$ on every instance (arXiv:1505.03424); the second version of this paper improved the QAOA worst-case bound to $\big(\tfrac12+\tfrac1{101D^{1/2}\ln D}\big)m$ (Section II).

Section III, formalized here, studies the typical case: it fixes the triples and draws the right-hand sides at random, and shows that the QAOA then reaches an advantage of order $D^{-1/2}$, the order of the classical algorithm, on all but a vanishing fraction of the instances.

Setting

An instance on $n$ bits with $m$ equations is a list of triples $(a_i,b_i,c_i)$ with $a_i<b_i<c_i$, no triple repeated, together with right-hand sides $r_i\in\{0,1\}$; equation $i$ is $x_{a_i}+x_{b_i}+x_{c_i}\equiv r_i\pmod 2$. The instance has occurrence at most $D+1$ if every bit lies in at most $D+1$ triples. Write $z_v=(-1)^{x_v}$ and $d_i=(-1)^{r_i}$; equation $i$ is satisfied by $x$ exactly when $z_{a_i}z_{b_i}z_{c_i}=d_i$.

Let $C(x)$ be the number of equations satisfied by $x$, viewed as a diagonal operator on the $2^n$-dimensional space spanned by $|x\rangle$, let $B=\sum_v X_v$, and let $|s\rangle$ be the uniform superposition. For angles $\gamma,\beta$ the level-one QAOA state is

$$|\gamma,\beta\rangle=e^{-i\beta B}e^{-i\gamma C}|s\rangle .$$

Measuring it in the computational basis gives a string; $N(\gamma,\beta)=\sum_x|\langle x|\gamma,\beta\rangle|^2C(x)$ is the expected number of satisfied equations.

In Section III the triples are fixed and the instance is drawn uniformly from the $2^m$ choices of right-hand sides; $\mathbb E_d$ and $\mathrm{Var}_d$ denote the mean and variance over this choice. The mixing angle is $\beta=\pi/4$ and the state analysed is $|-\gamma,\pi/4\rangle$, following the paper's sign convention.

For an equation with bits $1,2,3$, the polynomial $c_\rho(z)=\sum d_{\rho ab}z_az_b$ collects the equations that share exactly the bit $\rho$ with it, and $D_\rho$ is its number of terms.

Formalization targets

Goal: concentration above the mean bound

For every E3LIN2 family of $m$ triples with occurrence at most $D+1$, every $\gamma\in[0,\pi/2]$ and every $t>0$,

$$\Pr_d\Big[N(-\gamma,\pi/4)\le\frac m2+\frac m2\sin\gamma\cos^{3D}\gamma-t\Big]\le\frac{m(6D+3)(D+1)}{4t^2}.$$

With $t=c\sqrt m$ and $D$ fixed, all but a fraction $(6D+3)(D+1)/(4c^2)$ of the instances reach $\big(\tfrac12+\tfrac12\sin\gamma\cos^{3D}\gamma\big)m-c\sqrt m$. This is the paper's closing sentence of Section III with an explicit failure probability.

Milestones

1. (55): $N(-\gamma,\pi/4)=\tfrac m2+\sum_i\tfrac12d_i\langle Z_{a_i}Z_{b_i}Z_{c_i}\rangle$.
2. (25): the single-clause term equals $\tfrac18d\,\mathbb E_z\big[\sum_{\pm}\sin(\gamma(d\pm c_1\pm c_2\pm c_3))\big]$ over four sign patterns.
3. (47): averaging over the clause's own sign gives $\tfrac12\sin\gamma\,\mathbb E_z[\cos\gamma c_1\cos\gamma c_2\cos\gamma c_3]$.
4. (48): $\mathbb E_d[\cos\gamma c_\rho(z)]=(\cos\gamma)^{D_\rho}$ for every $z$.
5. (49): $\mathbb E_d$ of the clause term is $\tfrac12\sin\gamma(\cos\gamma)^{D_1+D_2+D_3}$, with $D_1+D_2+D_3\le3D$.
6. (50): for $\gamma\in[0,\pi/2]$, $\tfrac m2\sin\gamma\cos^{3D}\gamma\le\mathbb E_d[N-\tfrac m2]\le\tfrac m2\sin\gamma$.
7. (57): clause terms whose (25) expressions share no sign are uncorrelated.
8. Linked count: each equation is linked to at most $(6D+3)(D+1)$ equations.
9. Variance: $\mathrm{Var}_d\,N(-\gamma,\pi/4)\le\tfrac14m(6D+3)(D+1)$.
10. (51)–(53): $D^{1/2}\sin\gamma_D\cos^{3D}\gamma_D\to1/\sqrt{3e}$ at $\gamma_D=1/\sqrt{3D}$.

Significance

The result shows that on random-sign instances with any fixed bounded-occurrence structure, a single layer of QAOA beats a random assignment by $\Theta(D^{-1/2})m$, the same order as the best known classical guarantee and better than the paper's own worst-case bound by a logarithmic factor. It was one of the first concrete performance statements for the QAOA on a problem where its advantage over random guessing could be compared with the best classical guarantee. The average-case technique, an exact single-clause formula followed by an average over independent signs and a dependency count, applies to other local constraint problems.

The statements are proved in the paper by hand; none of them, and no QAOA performance bound, has a machine-checked proof on the platform. The mission produces a verified link from the quantum state to a classical average (25), a finite second-moment method over sign vectors, and an explicit Chebyshev form of the concentration claim.

Difficulty

The central step is (25): turning the expectation of $Z_aZ_bZ_c$ in the state $e^{-i\beta B}e^{-i\gamma C}|s\rangle$ into a classical average over bits. It requires conjugating three Pauli operators through the mixer at $\beta=\pi/4$, expanding the phase operator around the three bits, and showing that equations sharing two bits with the clause cancel. A direct computation in the $2^n$-dimensional space does not scale with $n$ and does not give a closed form.

For the variance, the naive bound by $m^2$ pairs gives nothing. The argument needs exact independence of clause terms whose sign dependencies are disjoint, which rests on (25) showing that each term depends only on its own sign and on the signs of the equations sharing exactly one bit with it, and then a combinatorial count of linked pairs.

Formalization scope

Bit strings are Fin n → Bool with true the bit $1$; the quantum layer reuses the published QAlgorithms definitions (Qubits, act, prob, uniformState, problemHamiltonian, qaoaMixer, qaoaUnitary). The phase operator is the full count of satisfied equations, which differs from the paper's $C$ of (6) by the constant $m/2$; the resulting states differ by a global phase and all probabilities agree. Triples are strictly increasing and pairwise distinct, which encodes "exactly three variables" and $d_{abc}\in\{0,\pm1\}$. $D$ is a natural number. $\mathbb E_d$ is the uniform average over all $2^m$ right-hand-side vectors, $\mathbb E_z$ over all $2^n$ strings.

Two pins are disclosed. The angle range $0\le\gamma\le\pi/2$ is added to (50) and the goal, since the lower bound needs $\sin\gamma,\cos\gamma\ge0$. The goal's threshold is (50)'s exact lower bound, not the paper's (54): $\big(\tfrac12+\tfrac1{2\sqrt{3e}D^{1/2}}\big)m$ is the large-$D$ limit and is false at every finite $D$, so (51)–(53) are stated as a limit instead. The goal is about the expected satisfied count of the measured state; the sampling procedure, circuit size and the search over $\gamma$ are out of scope.

A trivializing reading is excluded: the probability is over the $2^m$ instances on the fixed triples, not over a single instance, and the bound is about the quantum expectation at $|-\gamma,\pi/4\rangle$ (at $+\gamma$ the mean has the opposite sign and the statement would be false).

A complete development needs finite averages over $\{0,1\}^m$ with independence of coordinates, the single-clause formula (25) in the $2^n$-dimensional Hilbert space, and Chebyshev's inequality on a finite uniform space. The (25) computation and the second-moment count are reusable for other QAOA analyses. Contributions to any milestone are welcome, in any order.

Selected references

• E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem, arXiv:1412.6062v2, 2015. https://arxiv.org/abs/1412.6062
• E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv:1411.4028, 2014. https://arxiv.org/abs/1411.4028
• B. Barak, A. Moitra, R. O'Donnell, P. Raghavendra, O. Regev, D. Steurer, L. Trevisan, A. Vijayaraghavan, D. Witmer, J. Wright, Beating the random assignment on constraint satisfaction problems of bounded degree, APPROX/RANDOM 2015. https://arxiv.org/abs/1505.03424
• J. Håstad, On bounded occurrence constraint satisfaction, Information Processing Letters 74(1), 2000. (cited as [3] in arXiv:1412.6062v2)
• L. Trevisan, Non-approximability results for optimization problems on bounded degree instances, Proc. STOC 2001 (cited as [4] in arXiv:1412.6062v2)