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

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.

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

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 the copy count matters

Shadow tomography asks for predictions of many specified measurements of an unknown quantum state, while using as few prepared copies of that state as possible. The requested output is a list of acceptance probabilities, not a full description of the state. A procedure might exploit the fact that these are only $M$ numbers, even when the state has dimension $D$. The natural question is how far this saving can go. Aaronson's paper gives upper bounds and separates two sources of difficulty: one already present for ordinary probability distributions, and one arising from noncommuting quantum measurements.

This mission concerns the first source. It formalizes Theorem 16, which says that even when the state and every requested measurement are diagonal in the same basis, the number of copies must grow with $\min\{D,\log M\}/\varepsilon^2$ in the relevant asymptotic regime. In that special case, the unknown state is an ordinary distribution on $D$ outcomes. The theorem therefore puts a limit on any proposed improvement to shadow tomography that would promise fewer copies in all instances.

States, measurements, and estimates

A mixed state $\rho$ on a $D$-dimensional system is a positive semidefinite $D\times D$ complex matrix with trace one. A two-outcome measurement is represented by an effect $E$ satisfying $0\preceq E\preceq I$; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$. When $\rho$ is diagonal, its diagonal entries are the probabilities of the $D$ basis outcomes. When $E$ is diagonal too, it specifies a randomized yes-or-no test on those outcomes. These conventions are stated in Section 3 of the paper.

Given effects $E_1,\ldots,E_M$, a shadow-tomography strategy measures $k$ independent copies $\rho^{\otimes k}$ and outputs estimates $b_1,\ldots,b_M$. It succeeds on $\rho$ when every estimate differs from $\operatorname{Tr}(E_i\rho)$ by at most $\varepsilon$. The lower bound requires success probability at least $2/3$ for every diagonal mixed state. The strategy may make a joint quantum measurement on all copies and may choose its estimates from its observed outcome. This is the same measurement model used in Problem 1.

Formalization targets

Classical special-case lower bound

The goal is the classical clause of Theorem 16. There are absolute constants $c>0$ and $N_0$ such that, for $D\ge N_0$, $\log_2 M\ge N_0$, and $0<\varepsilon\le1/6$, there are $M$ diagonal effects with 0/1 entries, corresponding to the known Boolean functions in Section 6.1, for which every strategy successful on all diagonal states must use

The hard measurements are chosen before the strategy is quantified. The statement therefore also rules out a strategy with a smaller copy count that works uniformly for all quantum states and measurements. Its constants and threshold express the $\Omega$ notation in Theorem 16, rather than specifying a numerical optimum.

Supporting targets

Four milestones come from the proof on pages 20–21: the high-probability overlap bound for independently chosen half-size subsets (Eq. (1)); the acceptance probability of a subset under its associated biased distribution; an upper bound on the mutual information between the hidden subset index and the observed samples; and the exact entropy formula with a quadratic entropy deficit. These statements expose the combinatorial and information-theoretic parts of the lower bound while leaving the goal as the paper's copy-complexity result.

What the result supplies

Theorem 16 sets a floor for shadow tomography that survives even when all operators commute. Any uniform copy bound for the full quantum task must respect this floor. The result also distinguishes the difficulty of predicting many properties of a distribution from the extra difficulty possible for noncommuting states and measurements, which the paper treats in a separate lower bound. Section 6 presents both bounds.

A complete formalization would give machine-checked statements and proofs for the finite subset construction, the entropy calculation, the information inequality, and the reduction from a successful quantum measurement procedure on diagonal states to a lower bound on $k$. The theorem is proved on paper; these draft statements are open Lean goals and do not claim that its proof has been machine checked. The finite-distribution and information-theory infrastructure is reusable for other lower bounds based on hidden-index families.

Where the argument is delicate

Counting how many possible measurements there are does not by itself show that samples reveal enough about which distribution generated them. The lower bound needs a quantitative relation between estimation accuracy and information about a hidden index, while each individual sample carries limited information. The paper's printed overlap condition (1) is too weak for the next displayed $\varepsilon/2$ estimate: at its boundary it gives $\varepsilon$. The milestone preserves Eq. (1) as printed; closing the goal requires the correspondingly sharper overlap fact with $N/24$, which follows from the same type of concentration statement after adjusting its constant. The printed assertion that learning the index requires mutual information at least $\log_2 K$ is also imprecise at success probability $2/3$; a quantitative decoding inequality is needed. Neither incorrect display is a draft milestone.

Formalization scope

Matrices are indexed by Fin D. WildeQIT.IsDensityOperator supplies the mixed-state predicate $\rho\succeq0$ and $\operatorname{Tr}(\rho)=1$. Diagonal states and effects use the standard matrix diagonal predicate. An effect is positive semidefinite together with its complement. The tensor power uses functions Fin k → Fin D as basis indices; at $k=0$ it is a one-by-one identity matrix. A strategy is a finite-outcome POVM on that tensor power, followed by a real estimate vector for each outcome. The output values are not restricted to $[0,1]$: clipping them to this interval cannot worsen an estimate of a probability. No restriction to classical estimators is placed in the goal; that would change the allowed strategies before the theorem has been proved.

The asymptotic threshold excludes the one-dimensional and single-measurement corners where the claimed rate does not describe the problem. The bound $\varepsilon\le1/6$ keeps the biased distributions used on page 20 nonnegative; $\varepsilon\ge1/2$ would permit a zero-copy constant estimate. Subset milestones require even $N$ or explicitly require a half-size subset, so $N/2$ has its intended meaning. The natural logarithm appears nowhere in the lower-bound rate; entropy, mutual information, and $\log_2 M$ use base two. At zero probability the entropy convention is $0\log 0=0$.

The finite distributions, entropy, conditional entropy, and mutual information reuse the published WildeQIT definitions. Contributions that prove the four source milestones, establish the sharper overlap fact, or supply the quantitative decoding step are welcome. The goal must retain its order of quantifiers: one hard measurement family, then every strategy, with success demanded on every diagonal state.

Selected references

• Scott Aaronson, Shadow Tomography of Quantum States, arXiv preprint arXiv:1711.01053v2, 2018. Preprint.

Motivation

Learning an unknown quantum state is expensive. Full quantum state tomography of a $D$-dimensional mixed state $\rho$ to accuracy $\varepsilon$ in trace distance needs on the order of $D^2/\varepsilon^2$ copies of $\rho$ (O'Donnell–Wright 2016; Haah et al. 2017), and this is optimal. For a system of $n$ qubits, $D = 2^n$, so full tomography is out of reach beyond a few dozen qubits.

Often one does not need the whole density matrix, only the behaviour of $\rho$ on a fixed list of tests: acceptance probabilities of verification circuits, expectation values of observables, or the answers a piece of quantum advice gives to a set of questions. Aaronson (arXiv:1711.01053, STOC 2018) named this task shadow tomography and asked whether the number of copies can be polylogarithmic in both the dimension and the number of tests. Measuring each test on separate copies costs $\tilde O(M/\varepsilon^2)$ copies, which is linear in $M$.

Timeline.

• 2016: the question was posed at a mini-course without a name (Aaronson, The Complexity of Quantum States and Transformations, §8.3.1).
• 2016: Harrow, Lin and Montanaro gave a correct "quantum OR" test, repairing an earlier flawed claim (arXiv:1607.03236, Corollary 11).
• 2017–2018: Aaronson proved the first polylogarithmic bound, the theorem of this mission.
• Later work improved the exponents, notably Bădescu–O'Donnell 2021, and introduced the related "classical shadows" of Huang–Kueng–Preskill 2020.

Setting

A mixed state of dimension $D$ is a $D\times D$ Hermitian positive semidefinite matrix $\rho$ with $\mathrm{Tr}\,\rho = 1$. A two-outcome measurement is a $D\times D$ Hermitian matrix $E$ with all eigenvalues in $[0,1]$. Equivalently, $0 \preceq E \preceq \mathbb 1$. It accepts $\rho$ with probability $\mathrm{Tr}(E\rho)$.

The state $\rho^{\otimes k}$ consists of $k$ independent copies of $\rho$. A measurement of $\rho^{\otimes k}$ with classical output is a POVM: a finite family of positive semidefinite matrices $P_\omega$ on the $k$-register space with $\sum_\omega P_\omega = \mathbb 1$. Outcome $\omega$ occurs with probability $\mathrm{Tr}(P_\omega\rho^{\otimes k})$. An adaptive procedure that measures the copies one after another is described by one such POVM.

Problem 1 (shadow tomography). Given an unknown $\rho$ and known two-outcome measurements $E_1,\dots,E_M$, output numbers $b_1,\dots,b_M\in[0,1]$ with $|b_i-\mathrm{Tr}(E_i\rho)|\le\varepsilon$ for all $i$, with success probability at least $1-\delta$. The output must come from a measurement of $\rho^{\otimes k}$, with $k=k(D,M,\varepsilon,\delta)$ as small as possible. The measurement may depend on the $E_i$, but not on $\rho$.

Formalization targets

Goal: Theorem 2, in the explicit form proved in §5

There is a universal constant $C$ such that, for $M\ge2$ and $0<\varepsilon,\delta\le 1/2$, Problem 1 is solvable with

copies. This is the last display of the proof (p. 19). The goal fixes no constant, so any improvement of $C$ remains consistent with it.

Milestones

• Theorem 13 (Harrow–Lin–Montanaro). A one-copy test that accepts with probability at least $(1-\epsilon)^2/7$ if some $\mathrm{Tr}(E_i\rho)\ge1-\epsilon$, and at most $4\Delta M$ if $\sum_i\mathrm{Tr}(E_i\rho)\le\Delta M$.
• Lemma 14 (Quantum OR Bound). Deciding whether $\max_i\mathrm{Tr}(E_i\rho)\ge c$ or $\le c-\varepsilon$ with $O(\log(1/\delta)\log M/\varepsilon^2)$ copies, independent of $D$.
• Lemma 15 (Gentle Search). Finding $j$ with $\mathrm{Tr}(E_j\rho)\ge c-\varepsilon$ with $O(\frac{\log^4M}{\varepsilon^2}(\log\log M+\log\frac1\delta))$ copies.
• Amplification claims (p. 16). The threshold tests $E^*_{i,t,\pm}$ on $\rho^{\otimes q}$ accept with probability at least $5/6$ when the hypothesis is off by $\varepsilon$, and at most $1/3$ when it is within $\varepsilon/2$.
• Markov claim (p. 17). The postselection test $F_t$ on an arbitrary, possibly entangled, $q$-register state accepts with probability at most $\frac{a q}{(a+\varepsilon/4)q}$.
• Lemma 12 (Quantum Union Bound, probability part). Measurements each accepting with probability at least $1-\varepsilon$ all accept in succession with probability at least $1-2M\sqrt\varepsilon$.
• Chernoff claim (p. 18). $1-\mathrm{Tr}(F_t\rho^{\otimes q})\le\varepsilon^4/\log^2D$.
• Proposition 20. Promise-gap thresholds for all $i$ at once can be decided with $O(\log(M/\delta)/\varepsilon^2)$ copies.

Significance

The result. Theorem 2 shows that a state of exponential dimension can be learned "for all practical purposes" on exponentially many tests from polynomially many copies. Applications in the paper include a bound on quantum advice and one-way communication, and implications for quantum money and copy-protection. It also shows that the information needed to predict many measurement outcomes is far smaller than the description of $\rho$.

Formalizing it. The theorem is proved in the paper, and later work improves its exponents. As far as is known it has not been machine-checked. A complete development formalizes the gentle-measurement toolkit (Lemma 12, Lemma 14, Lemma 15), the amplification of two-outcome measurements on tensor powers, and the postselection argument. These are standard tools of quantum learning theory and quantum complexity with no formal counterpart yet. Lemma 14 and Lemma 15 are reusable beyond this mission.

Difficulty

The naive approach measures the $E_i$ directly on shared copies. A measurement that is likely to reject disturbs the state, so later measurements see a damaged state, and separate copies per measurement cost $M$ copies.

The proof needs three ingredients:

• a gentle search that finds a measurement on which the current hypothesis is wrong while damaging the copies only slightly;
• a potential argument showing that postselection cannot happen too often;
• a uniform control of the damage.

The potential argument has to hold for the state after postselection, which is correlated or entangled across registers. Independence-based concentration fails there, which is why the Markov claim, not a Chernoff bound, governs that step. Theorem 13 itself rests on a delicate ancilla-based procedure of Harrow, Lin and Montanaro, and the mission cites it as a milestone without its proof.

Formalization scope

• Representation.
  • Operators are complex matrices over a finite index type, and states use the published WildeQIT.IsDensityOperator (positive semidefinite, trace one).
  • A two-outcome measurement is IsEffect E: both $E$ and $\mathbb 1-E$ are positive semidefinite.
  • $\rho^{\otimes k}$ is a matrix indexed by $k$-tuples Fin k → n.
  • A measurement with output is a POVM structure with a finite outcome type. Probabilities are real parts of traces.
• Quantifier order of the goal. $\exists C$, then for all $D,M,\varepsilon,\delta$ there is $k$; then for all $E_i$ there are a POVM and outputs $b$; then for all $\rho$. Choosing the measurement after $\rho$ would make the goal trivial (output the true values with $k=0$), and this order rules that out.
• Disclosed hypotheses.
  • Theorem 2 assumes $M\ge2$, $\varepsilon\le1/2$ and $\delta\le1/2$. These keep the logarithmic factors positive; at $M=1$ the bound would force $k=0$.
  • Lemma 14 assumes $M\ge2$, and Lemmas 14 and 15 bound $\delta$.
  • Theorem 13 assumes $\epsilon\le1/2$, as in Harrow–Lin–Montanaro's Corollary 11.
  • The Chernoff claim assumes $D\ge2$.
• Conventions.
  • All logarithms are natural, including inside $\log\log$.
  • Amplified tests use real thresholds.
  • "Applied in succession" in Lemma 12 uses Lüders instruments ($\sqrt{E}$ Kraus operators), in the order $E_1,E_2,\dots$.
  • The hypothesis $\rho_t$ enters the amplification claims only as the number $a=\mathrm{Tr}(E\rho_t)$.
• Printed steps not drafted.
  • The printed $\varepsilon^{-4}$ form of Theorem 2 relies on an external online-learning algorithm that is only sketched.
  • The halting rule of §5 is unspecified, because Lemma 15 always returns an index.
  • The asymptotic claims $p_t\ge0.9/D^q$ for $t=o(\log^2D/\varepsilon^4)$ and $t=O(q\log D/\varepsilon)$ use a circular $o(\cdot)$.
  • The trace-distance part of Lemma 12 has an unquantified $O(\cdot)$.
  • Lemma 12's printed bound $1-2M\sqrt\varepsilon$ is weaker than its use on p. 18. It is stated as printed. The proof of the goal must retune constants or use Wilde's stronger $1-2\sqrt{M\varepsilon}$-type bound.
• Contributions welcome. Proofs of any milestone; a formal Hoeffding bound for binomial counts of product effects; the gentle measurement lemma for Lüders instruments; Naimark dilation for effects.

Selected references

• S. Aaronson, Shadow Tomography of Quantum States, STOC 2018; arXiv:1711.01053v2, 2018. https://arxiv.org/abs/1711.01053
• A. W. Harrow, C. Y.-Y. Lin, A. Montanaro, Sequential measurements, disturbance and property testing, SODA 2017. https://arxiv.org/abs/1607.03236
• M. M. Wilde, Sequential decoding of a general classical-quantum channel, Proc. R. Soc. A, 2013. https://arxiv.org/abs/1303.0808
• 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, 2017. https://arxiv.org/abs/1508.01797
• C. Bădescu, R. O'Donnell, Improved quantum data analysis, STOC 2021. https://arxiv.org/abs/2011.10908
• H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics, 2020. https://arxiv.org/abs/2002.08953

Motivation

Quantum query algorithms are known to beat classical ones on problems with algebraic structure -- period finding, hidden subgroups, forrelation. No such speedup is known for a problem with no structure at all. Aaronson and Ambainis proposed making that observation into a theorem, and reduced it to a question with no quantum content: a statement about bounded low-degree polynomials on the Boolean cube (Aaronson--Ambainis 2009).

The question has resisted since. A timeline of what is actually established:

• 2009. Aaronson and Ambainis state the conjecture and prove that it implies almost-everywhere classical simulation of quantum query algorithms.
• 2012. Montanaro settles the case of block-multilinear forms whose coefficients all have the same magnitude.
• 2016. O'Donnell and Zhao reduce the general conjecture to a restricted class, the one-block decoupled polynomials.
• 2019. Aaronson surveys a decade of partial progress (retrospective).
• 2022. Bansal, Sinha and de Wolf prove the conjecture for completely bounded degree-$d$ block-multilinear forms, obtaining influence $1/\mathrm{poly}(d)$ at constant variance (arXiv:2203.00212).
• 2024. The conjecture is established for a non-negligible fraction of random restrictions (arXiv:2402.13952).

The cases that are settled are settled under structural hypotheses -- block-multilinearity, complete boundedness, symmetry, Boolean range. The general statement is open.

Setting

Let $N$ be a positive integer. The Boolean cube is $\{0,1\}^N$, carrying the uniform distribution; a point $x$ is identified with the $0/1$ real vector it names, so a real multivariate polynomial $p$ in $N$ variables has a value $p(x)$ at each cube point. For a function $f$ on the cube write

The variance of $p$ is $\operatorname{Var}[p]=\mathbb{E}\big[(p-\mathbb{E}[p])^2\big]$. Writing $x^{\oplus i}$ for $x$ with its $i$-th bit flipped, the influence of coordinate $i$ on $p$ is

These are the combinatorial forms of both quantities, as used in the source; no Fourier--Walsh expansion is required to state anything below. The degree of $p$ is its total degree as a polynomial. Call $p$ bounded when $0\le p(x)\le 1$ at every cube point -- a condition imposed only on the cube, not on all of $\mathbb{R}^N$.

Target

The goal is the conjecture in the shape stated by its authors: there is an absolute constant $C$ such that for all $N$, all $d$, every polynomial $p$ of degree at most $d$ that is bounded on the cube, and every $\varepsilon>0$ with $\operatorname{Var}[p]\ge\varepsilon$, some coordinate $i$ satisfies

The constant $C$ is quantified outermost and may depend on nothing. That uniformity is the entire content: bounds that degrade exponentially in $d$ are already known, and a goal naming a specific exponent would be superseded by the next improvement.

Significance

The result itself. Aaronson and Ambainis prove that the conjecture implies that the acceptance probability of any bounded-error $T$-query quantum algorithm on a Boolean input can be approximated, to small error on all but a small fraction of inputs, by a classical algorithm making $\mathrm{poly}(T)$ queries. Quantum speedups would then require structure in a precise sense. The conjecture also has purely classical content, asserting that boundedness plus low degree forces variance to concentrate on some single coordinate rather than spread across all $N$. Without it, no such concentration is known at any rate polynomial in $1/d$.

Formalizing it. The conjecture is open, so this mission does not formalize a known proof of the goal. What it produces is a machine-checked statement of the conjecture together with formalizations of the partial results above, each currently existing only on paper. The milestone chain also yields reusable infrastructure for analysis of Boolean functions, of which Mathlib currently contains none: no Fourier--Walsh expansion, no influence, no variance on the cube.

Difficulty

The elementary bound is the Poincare inequality on the cube, $4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]$, which yields a coordinate with influence at least $4\varepsilon/N$. This is tight for the dictator $p(x)=x_1$ and depends on $N$, so it says nothing: the conjecture demands a bound free of $N$ entirely.

The natural repair is the route available when $p$ takes only the values $0$ and $1$. A Boolean-valued polynomial of degree $d$ depends on boundedly many coordinates, which immediately produces an influential one. That argument does not survive relaxing the range to the interval $[0,1]$: a bounded real-valued polynomial of low degree need not depend on boundedly many coordinates, and every known substitute loses a factor exponential in $d$. Closing the gap between exponential and polynomial dependence on $d$ is the difficulty, and it is where all of the partial results stop.

Formalization scope

Polynomials are MvPolynomial (Fin N) ℝ and degree is Mathlib's totalDegree, so the statement needs no bespoke notion of degree. Expectation is a finite sum scaled by $2^{-N}$ rather than a measure-theoretic integral, keeping every definition elementary. Bit flipping is Function.update x i (!x i). Boundedness is asserted at cube points only. Variance and influence are the combinatorial definitions above, published as the definition AaronsonAmbainis.

Three points close off degenerate readings. The exponent $O(1)$ of the source is rendered as an existentially quantified natural number with no leading multiplicative constant, since admitting one weakens the claim. Taking that exponent to be $0$ would demand influence at least $1$ and is therefore not a trivializing choice, while larger exponents only weaken the bound; the content is that some fixed exponent suffices for all $N$ and $d$ at once. The hypothesis $\deg p\le d$ is universally quantified over $d$, which is equivalent to the source's exact-degree form because the smallest admissible $d$ gives the strongest conclusion. The cases $N=0$ and $d=0$ are vacuous, since $0<\varepsilon\le\operatorname{Var}[p]$ fails for a constant polynomial.

A complete development needs, beyond the published definitions, a Fourier--Walsh layer with Parseval's identity, the level-$k$ machinery used by the partial results, and -- for the completely bounded case -- operator-space norms on multilinear forms. All of the Boolean-analysis material is reusable well beyond this mission. Contributions of any milestone are welcome, as are alternative formalizations of the definitions in function-level rather than polynomial-level form.

Out of scope: the quantum simulation consequence is not formalized here. Stating it requires a formal quantum query model, which no Lean library currently provides.

Selected references

• S. Aaronson, A. Ambainis, The Need for Structure in Quantum Speedups, Theory of Computing 10 (2014) 133--166; arXiv:0911.0996. Conjecture 6.
• N. Bansal, M. Sinha, R. de Wolf, Influence in Completely Bounded Block-multilinear Forms and Classical Simulation of Quantum Algorithms, CCC 2022; arXiv:2203.00212.
• Aaronson--Ambainis Conjecture Is True For Random Restrictions, 2024; arXiv:2402.13952.
• S. Aaronson, The Aaronson-Ambainis Conjecture (2008-2019), blog retrospective.
• S. Arunachalam, J. Briet, C. Palazuelos, Quantum query algorithms are completely bounded forms, SIAM J. Comput. 48 (2019); arXiv:1711.07285.
• AIM problem list, Analysis on the hypercube with applications to quantum computing, aimpl.org/hypercubequantum.

In a 1999 Vienna doctoral thesis, Gerhard Zauner conjectured that in every finite dimension d one can find d² unit vectors in complex d-space that are mutually as spread out as possible — any two sharing the same squared overlap 1/(d+1). Such a configuration, a symmetric informationally complete positive operator-valued measure (SIC-POVM), is the optimal minimal measurement for reconstructing an unknown quantum state, which is why the idea was rediscovered and named by Renes, Blume-Kohout, Scott, and Caves in 2004 and became central to quantum tomography, quantum cryptography, and the QBist reading of quantum mechanics. Geometrically these are maximal sets of complex equiangular lines; physically they are the most efficient quantum measurements; and, remarkably, they appear to be governed by deep number theory — recent work by Appleby, Flammia, Kopp, and others ties exact SICs to Stark units and Hilbert's twelfth problem on explicit class field theory. Exact solutions have been hand-built in scores of dimensions and numerical ones found in every dimension checked, yet a general existence proof remains out of reach. Formalizing Zauner's conjecture gives this problem — straddling quantum information, geometry, and algebraic number theory — a precise shared target.