Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Quantum Information

127 missions · 63 completed

The study of information encoded in the states of quantum systems, where the qubit, superposition, and entanglement replace the classical bit and measurement is inherently probabilistic. Governed by the constraints of quantum mechanics, it underpins quantum computing and cryptography and the theory of optimal quantum measurements.

Missions

Completed

Captain: Elsie66

Grover's AlgorithmResearch Paper

Motivation

Searching an unsorted list of $N$ items for a single marked entry takes $\Theta(N)$ queries classically — there is no way to do better than checking items one at a time. Grover's algorithm (Grover 1996) shows that a quantum computer solves the same problem in $\Theta(\sqrt N)$ queries, a quadratic speedup that applies to any problem expressible as unstructured search over a black-box oracle (this includes brute-forcing NP-complete problems and inverting one-way functions, which is why post-quantum cryptography doubles key lengths to compensate). Unlike Shor's algorithm, Grover's algorithm is provably optimal: Bennett–Bernstein–Brassard–Vazirani (1997) showed $\Omega(\sqrt N)$ queries are necessary for any quantum algorithm solving unstructured search, so the quadratic speedup is the best any quantum algorithm can achieve on this problem.

Setting

Model an $N$ -item database as the standard basis of $E = \mathbb{C}^N$ (EuclideanSpace ℂ (Fin N)), with inner product $\langle x,y\rangle = \sum_i \overline{x_i}\,y_i$ . Fix a marked index $w_0 \in \{0,\dots,N-1\}$ . The algorithm starts in the uniform superposition

|s\rangle = \frac{1}{\sqrt N}\sum_{i} |i\rangle,

a unit vector assigning equal amplitude to every item. Two reflections drive the search:

the oracle $O = I - 2|w_0\rangle\langle w_0|$ , which flips the sign of the amplitude on the marked item and leaves every other basis state fixed;
the diffusion operator $D = 2|s\rangle\langle s| - I$ ("inversion about the mean"), the reflection about $|s\rangle$ .

One Grover iterate is $G = D\,O$ . The algorithm applies $G$ some number of times to $|s\rangle$ and measures; a measurement outcome equal to $w_0$ counts as success.

Formalization targets

Milestone — the iterate is an isometry

\|G x\| = \|x\| \quad \text{for every } x \in E

$O$ and $D$ are each reflections about a unit vector, hence isometries; their composition $G$ is therefore norm-preserving on the whole space, not just at $|s\rangle$ — the minimal fact needed for $G$ to be a legitimate quantum operation.

Milestone — the rotation formula

\langle w_0, G^k s\rangle = \sin\bigl((2k+1)\theta\bigr), \qquad \theta := \arcsin\!\left(\tfrac{1}{\sqrt N}\right)

The geometric heart of the algorithm (Nielsen & Chuang, Quantum Computation and Quantum Information, Section 6.1.2): restricted to the real two-dimensional subspace spanned by $|w_0\rangle$ and the component of $|s\rangle$ orthogonal to it, $G$ acts as rotation by a fixed angle $2\theta$ . Each iterate therefore advances the amplitude on the marked state along $\sin((2k+1)\theta)$ , exactly as claimed, with $\theta = \arcsin(1/\sqrt N)$ the rotation's initial offset (since $\langle w_0, s\rangle = 1/\sqrt N$ at $k=0$ ).

Goal

\exists\, k,\quad 1 - \tfrac1N \;\le\; \bigl|\langle w_0, G^k s\rangle\bigr|^2

Some number of iterations drives the probability of measuring the marked item above $1-1/N$ . The goal is stated existentially, without fixing $k$ to a specific rounded formula: the rotation angle $(2k+1)\theta$ can be made to land within $\theta$ of $\pi/2$ by an appropriate integer $k$ , and at that point $\sin^2((2k+1)\theta) \ge \cos^2\theta = 1-\sin^2\theta = 1 - 1/N$ . Pinning $k$ down to an explicit closed form (e.g. the nearest integer to $\pi/(4\theta) - 1/2$ ) is one valid strategy, but is not required by the statement — any correct choice of $k$ , and any correct proof it works, closes the goal.

Significance

Grover's algorithm is the second landmark quantum algorithm after Shor's, and the one with the widest applicability: because it treats the search space as a black box, it accelerates any brute-force search — SAT solving, collision finding, and generic key search among them — which is the concrete reason NIST's post-quantum cryptography standards double symmetric key lengths rather than replacing them outright. The mathematics itself has been fully settled since 1996, including matching optimality lower bounds; nothing here is open. What this mission adds is a machine- checked derivation of the amplitude formula and success bound directly from the definitions of the oracle and diffusion operators as concrete linear operators on EuclideanSpace ℂ (Fin N) — Mathlib has the finite-dimensional inner product space and rank-one operator machinery this needs (InnerProductSpace.rankOne, EuclideanSpace.single), but no existing formalization of the algorithm itself.

Difficulty

The obvious first attempt tries to track the full $N$ -dimensional state vector through $k$ iterations. This is intractable in general: $G$ 's action on an arbitrary basis vector depends on its overlap with both $|w_0\rangle$ and $|s\rangle$ . The move that makes the problem tractable is recognizing that $G$ preserves the two-dimensional real subspace $\mathrm{span}\{|w_0\rangle, |s\rangle\}$ — everything orthogonal to this plane is fixed by both $O$ and $D$ , and inside the plane $G$ is exactly a rotation matrix by angle $2\theta$ . Establishing this invariance and then tracking only the rotation angle (rather than the full vector) is the standard reduction, and the one this mission's milestones are built around; skipping it and attempting a direct $N$ -dimensional induction does not scale.

Formalization scope

Works over a general $N:\mathbb N$ together with a marked index $w_0 : \mathrm{Fin}\,N$ — no assumption that $N$ is a power of two, since the rotation argument is agnostic to how the $N$ basis states are physically encoded into qubits (that encoding is a separate, unrelated concern from the search dynamics proved here). Supplying w0 : Fin N already forces $N \ge 1$ ; no separate nonemptiness hypothesis is added. The oracle and diffusion operators are built directly from Mathlib's InnerProductSpace.rankOne rather than an ad-hoc pointwise definition, so their reflection structure (and hence unitarity) is visible from the definition itself. A trivializing formalization is ruled out explicitly: the goal is stated as an existential over $k$ rather than a fixed closed-form iteration count, so a correct proof must still exhibit a genuine successful $k$ and establish the bound — it cannot be discharged by an unrelated or degenerate choice. Contributions extending this to multiple marked items, or proving the matching $\Omega(\sqrt N)$ lower bound (Bennett–Bernstein–Brassard–Vazirani 1997), are welcome as follow-up missions.

Selected references

L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. https://arxiv.org/abs/quant-ph/9605043
M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Section 6.1.
C. H. Bennett, E. Bernstein, G. Brassard, and U. Vazirani, Strengths and Weaknesses of Quantum Computing, SIAM J. Comput. 26 (1997). https://arxiv.org/abs/quant-ph/9701001

8 thms1 active user

Combinatorics Quantum Error Correction·Captain: Winningatmath

Bivariate-Bicycle Codes: New [[336,20,12]] and [[360,24,12]] Codes and Certified DistancesResearch Paper

Motivation

A quantum memory stores logical qubits in many physical qubits so that errors can be detected and corrected. The overhead of doing so, measured by how many physical qubits are spent per logical qubit at a given error-correcting power, is one of the main costs of fault-tolerant quantum computation. Bivariate-bicycle (BB) codes are currently the leading low-overhead family: the gross code $[[144,12,12]]$ of Bravyi et al. (Nature, 2024) stores 12 logical qubits at distance 12 using 144 data qubits, roughly a tenth of the overhead of a surface code with the same distance, and it is the basis of a published hardware roadmap. The search for higher-rate members of the family is active, and the claims made in it are claims about the exact distance of explicit finite codes. These are finite but very large computations, and they are rarely checked independently.

Timeline.

2004 — MacKay, Mitchison and McFadden introduce bicycle codes: CSS codes built from a pair of circulant matrices.
2013 — Kovalev and Pryadko generalize the construction to commuting pairs of group-algebra elements (generalized bicycle codes).
2024 — Bravyi, Cross, Gambetta, Maslov, Rall and Yoder define BB codes over $\mathbb Z_l\times\mathbb Z_m$ and give the ladder $[[72,12,6]]$ , $[[90,8,10]]$ , $[[108,8,10]]$ , $[[144,12,12]]$ , $[[288,12,18]]$ , with $[[360,12,\le 24]]$ left with only an upper bound.
2026 — An evolutionary search by Cruz-Benito et al. (arXiv:2606.02418) reports $[[288,16,12]]$ as its best indecomposable weight-6 code at distance 12.
2026 — Daugherty, Ryan and Ward give two new $[[336,20,12]]$ codes and a new $[[360,24,12]]$ code. They certify the exact distances of the whole ladder, establish $d=24$ for $[[360,12]]$ , and show by enumeration that no connected three-term weight-6 BB code with $n\le 360$ and $k\ge 20$ has distance 13 or more.

Setting

Fix positive integers $l,m$ and let $G=\mathbb Z_l\times\mathbb Z_m$ . The monomial $x^iy^j$ of the ring $\mathbb F_2[x,y]/(x^l-1,\,y^m-1)$ is identified with $(i,j)\in G$ . A polynomial $P$ with coefficients in $\mathbb F_2$ is identified with its support, the finite set of monomials with coefficient $1$ . The circulant of $P$ is the $G\times G$ binary matrix with a $1$ in row $g$ , column $h$ exactly when $h-g\in P$ .

Given two polynomials $A,B$ , the BB code $\mathrm{BB}(A,B)$ acts on $n=2lm$ qubits, arranged in two blocks indexed by $G$ . Its check matrices are

H_X=[\,A\mid B\,],\qquad H_Z=[\,B^{\mathsf T}\mid A^{\mathsf T}\,],

where $A$ and $B$ also denote their circulants. Because $G$ is abelian, $H_XH_Z^{\mathsf T}=AB+BA=0$ over $\mathbb F_2$ , so this is a CSS code. Its parameters are:

the number of logical qubits $k=n-\operatorname{rank}H_X-\operatorname{rank}H_Z$ , with ranks over $\mathbb F_2$ ;
the Z-distance $d_Z$ , the least Hamming weight of a vector $v\in\mathbb F_2^n$ with $H_Xv=0$ and $v\notin\operatorname{row}(H_Z)$ (a nontrivial Z-logical);
the X-distance $d_X$ , defined dually: $H_Zv=0$ and $v\notin\operatorname{row}(H_X)$ .

The code is $[[n,k,d]]$ when $d_X=d_Z=d$ . Each check of a code built from two three-term polynomials touches six qubits (weight 6). The Tanner graph joins each qubit to the X- and Z-checks acting on it, and the code is connected when this graph is connected.

Formalization targets

Goal: the three new codes

\mathrm{BB}_{\mathbb Z_2\times\mathbb Z_{84}}\!\left(1+y+xy^{5},\;1+y^{4}+y^{62}\right)=[[336,20,12]],

\mathrm{BB}_{\mathbb Z_2\times\mathbb Z_{84}}\!\left(1+y+xy^{5},\;1+y^{20}+y^{46}\right)=[[336,20,12]],

\mathrm{BB}_{\mathbb Z_6\times\mathbb Z_{30}}\!\left(1+y+xy^{2},\;1+y^{8}+x^{2}y^{16}\right)=[[360,24,12]],

each with $d_X=d_Z=12$ (Table 9 of the source). Each new code is also a milestone on its own.

Milestones

Lemma 1 (minimality). In any parity system, no nonempty proper subset of a minimum-weight logical is even on every check.
Table 3, the certified ladder. $[[72,12,6]]$ , $[[90,8,10]]$ , $[[108,8,10]]$ , $[[144,12,12]]$ , $[[288,12,18]]$ and $[[360,12,24]]$ , all with $d_X=d_Z$ , for the polynomials of Bravyi et al.
Section 6, the weight-6 envelope. Every connected BB code built from two three-term polynomials with $n\le 360$ and $k\ge 20$ has a nontrivial X- or Z-logical of weight at most 12. In words, none has distance 13 or more.

Significance

The result. The new codes encode 25% and 50% more logical qubits at distance 12 than the best weight-6 code reported by evolutionary search, with figures of merit $kd^2/n$ of 8.57 and 9.60. The ladder distances turn published values, several of them previously supported only by heuristic searches or upper bounds, into exact statements. In particular $d([[360,12]])=24$ settles an upper bound left open by Bravyi et al. The envelope statement is a negative result: within this family and size range, distance 12 is the ceiling at $k\ge 20$ .

Formalizing it. In the source, each lower bound on a distance is a DRAT refutation or a replayable proof tree, checked by external programs. Only the pruning lemma (Lemma 1) has a machine-checked proof, in Lean 4. A complete formalization would make the code parameters kernel-checked facts about explicit Mathlib objects, independent of every external checker. Upper bounds on distance and the values of $k$ are finite linear-algebra facts. Lower bounds are exhaustive statements over $\binom{n}{w}$ -sized spaces and are the core of the work.

Difficulty

The upper bound $d\le 12$ needs one explicit weight-12 logical together with a proof that it lies outside the opposite row space. The lower bound $d\ge 12$ asks that no nontrivial logical of weight at most 11 exist among roughly $\binom{336}{11}\approx 10^{19}$ candidate supports. Direct enumeration is out of reach. A SAT encoding with a cardinality constraint is several orders of magnitude slower than the source's pruned search, and the resulting proof objects are large: hundreds of megabytes for the larger ladder codes. Kernel-checking such certificates, or finding structure that avoids them, is the central difficulty. Computing $k$ also requires an $\mathbb F_2$ -rank of matrices with up to 180 rows and 360 columns, and Mathlib's Matrix.rank is not computable by decide. The envelope statement additionally quantifies over 971 group shapes and every pair of three-term polynomials on each.

Formalization scope

All objects are in the definition file BBCode_Setting. $G$ is ZMod l × ZMod m, and a polynomial is a Finset of monomials, which makes it a set of distinct terms. The circulant has entry 1 at $(g,h)$ iff $h-g\in P$ . Qubits are G ⊕ G (left and right blocks). $H_X$ is Matrix.fromCols (circulant A) (circulant B) and $H_Z$ is Matrix.fromCols (circulant B)ᵀ (circulant A)ᵀ, over ZMod 2. The row space is the ZMod 2-span of the rows, and the weight counts nonzero coordinates. NumLogical A B k states $\operatorname{rank}H_X+\operatorname{rank}H_Z+k=n$ additively, avoiding truncated subtraction. HasZDistance A B d requires both a nontrivial Z-logical of weight exactly $d$ and the lower bound for every nontrivial Z-logical, so a code without logicals cannot satisfy it vacuously. IsCode A B n k d bundles $n=2lm$ , $k$ and both distances.

The envelope quantifies over all $l,m\ge 1$ with $2lm\le 360$ . The source enumerates 961 shapes; the 10 it omits ( $lm\le 5$ ) cannot have $k\ge 20$ , so the two ranges are equivalent.

Reusable infrastructure includes computable $\mathbb F_2$ rank certificates (explicit row-echelon or basis witnesses), a verified checker for DRAT or proof-tree certificates, and symmetry lemmas for group translations acting on BB codes. Contributions of any of these, of individual sectors ( $d_X$ or $d_Z$ separately), or of upper and lower bounds as separate lemmas are welcome.

Selected references

S. Bravyi, A. W. Cross, J. M. Gambetta, D. Maslov, P. Rall, T. J. Yoder, High-threshold and low-overhead fault-tolerant quantum memory, Nature 627, 778–782, 2024. https://doi.org/10.1038/s41586-024-07107-7 (arXiv: https://arxiv.org/abs/2308.07915)
B. W. Daugherty, S. Ryan, G. Ward, New distance-12 bivariate-bicycle codes with 20 and 24 logical qubits: an exhaustive classification and checkable distances to 360 qubits, certificate release v1.0.0, Zenodo, 2026. https://doi.org/10.5281/zenodo.23382175
D. J. C. MacKay, G. Mitchison, P. L. McFadden, Sparse-graph codes for quantum error correction, IEEE Trans. Inf. Theory 50(10), 2315–2330, 2004. https://arxiv.org/abs/quant-ph/0304161
A. A. Kovalev, L. P. Pryadko, Quantum Kronecker sum-product low-density parity-check codes with finite rate, Phys. Rev. A 88, 012311, 2013. https://arxiv.org/abs/1212.6703
J. Cruz-Benito et al., evolutionary search for bivariate-bicycle codes, arXiv:2606.02418, 2026. https://arxiv.org/abs/2606.02418

13 thms0 active usersReviewed