Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The Hubble constant , the present expansion rate of the Universe, is inferred in two largely independent ways: from the cosmic microwave background (CMB) assuming the flat ΛCDM model, giving km/s/Mpc (Planck 2018), and from the local distance ladder of Cepheids and Type Ia supernovae, giving km/s/Mpc (Riess et al. 2022). The 4σ–6σ gap between such estimates is the Hubble tension. The review of Hu and Wang (2023) surveys the independent probes used to arbitrate it (strongly lensed quasars, megamasers, gravitational waves, fast radio bursts, the tip of the red giant branch) and the evidence, from a possible redshift dependence of the inferred , that the late-time Universe may need modification.
Several probes in that survey turn an observable into a value of through an explicit formula in a flat ΛCDM background. This mission formalizes those formulas, Eqs. (1)–(8) of the review, and the mathematical properties that the inference relies on: that a measured time-delay distance determines uniquely, that the dispersion measure–redshift relation of fast radio bursts is invertible, and that a "running" diagnostic is a genuine test of flat ΛCDM.
Fix a matter density parameter and impose spatial flatness, so that the dark-energy density parameter is . The dimensionless expansion rate is
and the Hubble rate at redshift is .
Distances. For redshifts and speed of light , the angular diameter distance between them is (Eq. (2))
and the distance from the observer to redshift is the case (Eq. (3)). A lens at redshift in front of a quasar at has distances (to the lens), (to the source) and (lens to source), and the time-delay distance (Eq. (1))
is the quantity inferred from the time delay between lensed images.
Fast radio bursts. The mean intergalactic dispersion measure at redshift is (Eq. (5))
where is the baryon density parameter, the fraction of baryons in the intergalactic medium, and the electron fraction. The observed dispersion measure adds Milky Way and host contributions (Eq. (4)).
Redshift-dependent . Data binned in redshift are placed at the weighted redshift (Eq. (6)); the trend of across bins is fitted by the evolution function (Eq. (7)); and for an arbitrary expansion history the diagnostic is (Eq. (8))
For , and there is such that for every ,
The constant is left unspecified: the goal asserts only the shape of the dependence, which is what makes the quasar-lensing inference of well posed.
The results. The review's quantitative arguments use these formulas as black boxes. The goal and milestones 1–3 make precise the statement that the time-delay distance is "primarily sensitive to ": it is exactly inversely proportional to , with all other cosmological dependence in a positive constant. Milestone 4 is the invertibility of the dispersion measure–redshift relation on which FRB cosmology rests. Milestones 6–8 underpin the "descending " evidence of Section 5: the effective redshift of a bin is a redshift of that bin, a positive exponent in means a decreasing trend, and a non-constant diagnostic is equivalent to a departure from flat ΛCDM.
Formalizing them. These facts are standard and their proofs are short on paper. The mission also records a transcription issue in the source: Eq. (3) prints the integrand as , which is inconsistent with Eq. (2); the formalization uses the reciprocal square root, as in Eq. (2).
The algebraic statements (milestones 2, 5, 7, 8) require care only with Lean's total division and real powers. The analytic statements involve interval integrals: milestone 1 needs integrability of on and additivity of the integral, and milestones 3 and 4 need strict positivity of the integral of a positive continuous function over a nondegenerate interval. Unfolding the definitions and clearing denominators fails as soon as a denominator such as or might vanish; each such case has to be ruled out from the hypotheses.
All quantities are real-valued. Flatness is built in by writing for ; is assumed where needed, while is never needed and is not assumed. The angular diameter distances are interval integrals of ; division by zero evaluates to , so positivity of the relevant denominators is either assumed or proved. The power in Eq. (7) is the real power and the weights in Eq. (6) are integer powers. Physical constants (, , ) and the functions , are free parameters, not numerical values. The statistical analyses of the review (likelihood fits, Gaussian-process reconstructions, quoted σ-levels) are out of scope.
All definitions live in one shared definition file in the HuWang2023 namespace; the distance functions and the diagnostic are reusable for other flat-ΛCDM missions.
The general number field sieve (GNFS) is the most efficient classical algorithm known for factoring integers larger than about . Its heuristic running time for an integer is
super-polynomial but sub-exponential in the bit length of . Every record factorization of a general RSA modulus of recent decades (RSA-768, RSA-240, RSA-250) was obtained with it, so the security margins of RSA key sizes are calibrated against it (Pomerance, A Tale of Two Sieves, 1996; Boudot et al., 2020).
Like the rational and quadratic sieves, GNFS works by producing a congruence of squares and then taking . Its gain comes from searching for smooth values that are sub-exponential in the size of , which forces the algorithm to compute in algebraic number fields.
Let be a polynomial of degree and a root of . The number field is the set of complex numbers with ; it is -dimensional over when is irreducible over . The ring is the subring of generated by ; the ring of integers consists of the elements of that are roots of monic integer polynomials. It contains when is monic, and the two can differ.
GNFS chooses two irreducible integer polynomials with a common root modulo , i.e. and . A simple choice is the base- polynomial: write with digits , put and . Pairs of integers (relations) are sieved so that both homogenized values are smooth; up to the leading coefficient these are the norms . Linear algebra over then selects a set of relations for which
Because is a root of both polynomials mod , there are ring homomorphisms with . Both send to .
For irreducible in with complex roots , a common root mod , and , , as above:
This is the correctness statement of the algebraic part of GNFS: whatever relations the sieve and linear algebra produce, the square-root step yields , with .
The goal and milestones together certify that every output of the GNFS pipeline that passes the square-root step is a genuine congruence of squares, and that such a congruence splits with probability at least over the choice of square root. This is the part of the algorithm whose correctness is unconditional; the running-time bound is heuristic and is not a target here.
These results are classical and appear in standard references (Lenstra–Lenstra 1993; Crandall–Pomerance 2005, §6.2). The mission's contribution is a machine-checked formal version connecting number fields in , integer polynomials, and residue rings, which current libraries do not package for this purpose.
The ring homomorphism is the delicate point. is a subring of , not a quotient ring, so a map defined by is well defined only if every integer polynomial vanishing at is a multiple of in . This needs irreducible over (in particular primitive), via Gauss's lemma; for and , every is a root mod , but only admits . The norm identity requires identifying as the minimal polynomial of and expressing the norm as a product over conjugates. The probability milestone needs the Chinese remainder theorem and counting square roots of units modulo odd prime powers.
All statements live in the namespace GNFS. Number fields are realized inside : is ℚ⟮θ⟯ and is Algebra.adjoin ℤ {θ}. Residues mod are ZMod n with ( gives , consistent with every statement). Two definitions are shared: GNFS.baseMPolynomial n m, the polynomial whose coefficients are the base- digits of (via Nat.digits), and GNFS.homogenize f a b .
Irreducibility "over the rationals" with integer coefficients is encoded as irreducibility in (primitive and irreducible over ) where a homomorphism to is needed. Without primitivity the claimed homomorphism can fail to exist. The goal asserts both the existence of the homomorphisms and the equality for every such pair, so it cannot be satisfied by the trivial choice . The sieving, smoothness, linear-algebra and complexity aspects of the article are out of scope.
Reusable by-products: norms of linear elements in simple extensions, homomorphisms out of , and square-root counting in .
The Schwartz space of smooth, rapidly decreasing functions is the standard domain on which Fourier analysis on works without integrability caveats. Its defining property, singled out in the lead of the source article, is that the Fourier transform maps isomorphically onto itself. By duality this allows the Fourier transform to be defined on the dual space of tempered distributions, which is the setting of the modern theory of linear partial differential equations (Hörmander, Vol. I) and of much of mathematical physics (Reed–Simon, Vol. I). The space is named after Laurent Schwartz.
This mission formalizes the definition and the elementary analytic properties of exactly as stated in the Wikipedia article Schwartz space (revision 1360762580), with the Fourier-automorphism property as the goal.
Write for the coordinate space with the Euclidean norm and Lebesgue measure. A multi-index is a tuple , and . For a function , denotes the partial derivative in the -th coordinate direction and
For put
The Schwartz space is
Informally, and all its derivatives decay at infinity faster than any reciprocal power of .
The Fourier transform of is
In the Lean development these objects are SchwartzSpaceWiki.monomial, partialDeriv, iteratedPartialDeriv, schwartzSeminorm, schwartzSpace n and fourierTransform.
Formally: Set.BijOn fourierTransform (schwartzSpace n) (schwartzSpace n) together with for and .
The result itself. The automorphism property is what makes the natural test-function space for tempered distributions: the Fourier transform of a tempered distribution is defined by , which only makes sense because is again a Schwartz function. Density in (milestone 8) is what lets identities proved on Schwartz functions, such as Plancherel's theorem, extend to and other spaces. The closure properties (milestones 1, 5, 6) say that is an algebra and a module over smooth functions with bounded derivatives.
Formalizing it. All results here are classical. Mathlib contains a Schwartz-space type SchwartzMap built on iterated Fréchet derivatives and the norm , together with a Fourier transform on it. This mission instead states everything for the concrete, coordinate-wise multi-index definition used in the source. A complete development therefore includes a proof that the two definitions agree, which is reusable on its own.
The multi-index seminorms are coordinate-wise, while the standard library works with the total derivative and the full norm . The comparison needs inequalities in both directions between and powers of , and between the iterated partial derivatives and the norm of the -th Fréchet derivative. For the goal, surjectivity is the hard part: it needs the Fourier inversion formula on , not only the fact that preserves decay and smoothness. For milestone 8, density requires approximating arbitrary functions, e.g. by compactly supported smooth functions, and this does not follow from the definition of alone.
EuclideanSpace ℝ (Fin n) (Euclidean norm, Lebesgue volume). Functions take values in . is allowed.ContDiff ℝ (⊤ : ℕ∞), i.e. (not analyticity).fderiv ℝ f x (EuclideanSpace.single i 1), and applies in a fixed order. For smooth the order does not matter.ℝ≥0∞), so "" really means bounded. A real-valued supremum would return on unbounded sets and trivialize the definition.fourierTransform is a Bochner integral, which is for non-integrable integrands. Every target only applies it to Schwartz functions, which are integrable.schwartzSpace n onto itself plus linearity on it. It does not presuppose that schwartzSpace n has been given a module structure.Contributions welcome: the equivalence with Mathlib's SchwartzMap, coordinate–norm comparison lemmas for , and the Leibniz rule for iteratedPartialDeriv.
This mission develops Chapter 23 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be integers and let , and be complex matrices. Write for the Frobenius norm, , and for the spectral (operator) norm of , i.e. its largest singular value. Then
In the generalized adversary method this inequality bounds both the final value of the weight function for Boolean functions and how much one query can change it.
Formalization Note The index sets are and ; the Frobenius norm is frobNorm and the spectral norm is specNorm (Mathlib's operator norm on matrices). When or both sides are .
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 5 of A Survey of Quantum Learning Theory by Srinivasan Arunachalam and Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is a corrected form of the Atıcı–Servedio theorem on learning juntas from uniform quantum examples.
A function is a -junta if it depends on at most of its input bits. A uniform quantum example of is the -qubit state ; a uniform classical example is a pair with uniform on . The error of a hypothesis is for uniform .
Time is measured in the following hybrid cost model, which is the one the source's proof sketch counts in. A learner (1) applies a circuit over the gate set to uniform quantum examples and some ancillas in and measures every qubit in the computational basis; (2) maps the outcome by a Boolean circuit of AND/OR/NOT gates to a set of variables; (3) reads uniform classical examples and outputs the truth-table hypothesis for the first example that agrees with on ( if there is none). Its time is the number of quantum gates, plus the number of measured qubits, plus the number of Boolean gates, plus (one unit per classical example, which is read and written into the table cell indexed by its -bits), plus table cells (worst case over the outcomes).
For every there is a constant such that for all with and all there is such a learner with
which, for every -junta , outputs with probability at least (over the measurement outcomes and the classical examples) a hypothesis of error at most .
The theorem shows that quantum examples remove the search over candidate variable sets that the best known classical learners need, which is why juntas are a notorious bottleneck classically.
Formalization Note The source states no cost model, no confidence parameter, and classical examples. The cost model above, the fixed-confidence reading (constants depend on only), and the classical examples of the source's own proof sketch are the corrections. The thresholds and make and positive.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 3 of An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be the -qubit Pauli group and let generate a stabilizer , that is, an Abelian subgroup of with , and suppose the generators are independent, i.e. . The error syndrome of a Pauli operator is the vector in whose -th bit is if commutes with and if it anticommutes.
Then for every there is with syndrome :
This lemma is the step in the proof of the dimension count of stabilizer codes (Theorem 5) that shows all syndrome subspaces are nonempty.
Formalization Note The syndrome is relative to the generator list, as in the source's proof; the independence of the generators (used in the proof as linear independence of their binary vectors) is the hypothesis . The anticommutation clause is stated explicitly.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 4 of Stabilizer Codes and Quantum Error Correction by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let a stabilizer on qubits ( generators) be given in the standard form (4.3) of §4.1,
with rows in the first block, and assume its rows commute: . For a binary row write (the real form, sign ). Let be the generators and let be the logical operators in the standard form of p.40: with the -th row of and the -th row of .
Let be the encoding network of §4.2 (with the author's errata): first, for each , the controlled-NOTs that apply without its final , controlled on qubit ; then, for in turn, the Hadamard on qubit , a on qubit if , and without its qubit- factor, controlled on qubit (controlled- gates). Then for every ,
and in particular the vector on the right-hand side is nonzero.
This is the correctness of Gottesman's general encoding circuit for stabilizer codes: the network prepares exactly the encoded basis states, with no leftover global phase.
Formalization Note The errata are built in: the Hadamard on qubit comes just before that qubit's control operations, controlled- gates are controlled- gates in the real form, and every generator has sign . The page writes encoded states unnormalized; the unitary network yields the normalized vector. Since the real form , a generator with an odd number of positions is times a Hermitian Pauli operator; the identity is the one the page's network computes in this convention.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 3 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be a phase (in full turns), (), and let be the angle estimates used by the iterative phase estimation algorithm of §3.3.2, being the estimate of . The algorithm computes binary digits as follows: are the digits of rounded to the closest multiple of (modulo ); then for , if and otherwise. Here is the distance between and modulo .
Fix . If for every step , then
In particular, for the algorithm outputs binary digits of with error at most on the circle, which together with a union bound over the estimation steps gives the success guarantee of iterative phase estimation.
Formalization Note The page states the bound with plain absolute values and strict inequality. Both are corrected: angles are only known modulo (so all distances are on the circle), and the strict bound already fails at the base case ( is equidistant from and , and rounding gives error exactly ); the induction proves , matching the goal on p.66. The digits are the shared definition ipeDigits h ω and is binFracFrom.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 9 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let and let be the objective of the maximization problem (9.38). Define the -qubit Hamiltonians
where is the Pauli on qubit and the identity elsewhere. For and let
Then for every there are a unit vector with , that is an eigenstate of with maximum eigenvalue, and an integer such that for every there are angles with
Here is the uniform superposition, the maximum eigenstate of . The proposition says that with enough layers, the QAOA ansatz can reproduce adiabatic evolution along and so prepares a state close to one encoding an optimal solution of (9.38).
Formalization Note The source's limit over , with angles that depend on , is stated as "for all sufficiently large some angles achieve distance at most ", with the target eigenvector fixed before . The global phase allowed by Theorem 9.11 is absorbed into the choice of the eigenvector, since a phase multiple of a maximum eigenvector is again one. The informal claim that "approximates an adiabatic evolution" is represented by its stated "in particular" consequence.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 18 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let and let be a symmetric stochastic matrix (, for all , ) describing a random walk on the vertex set . Let be a set of marked vertices and let be the matrix obtained from by deleting the rows and columns indexed by . Let and .
Lemma. If the second largest eigenvalue of in absolute value is at most (that is, listing the eigenvalues of with multiplicity, at most one has absolute value greater than ) and , then
where is the spectral (operator) norm.
Together with , this gives the classical hitting time , and it is the input to the quantum walk search bound .
Formalization Note because the source speaks of a second eigenvalue, and because they are a spectral gap and a fraction; without these the statement fails (e.g. , , , , ). Symmetry is stated as Hermitian, which for a real matrix is the same thing; the eigenvalues are the Mathlib eigenvalue list of the Hermitian matrix. If , is the empty matrix, of norm .
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 2 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
For write for the group commutator. For let
be the -ball around the identity, with the spectral norm. For , is a -net for if every has some with .
The lemma says there are constants and such that, for every and every , the following holds. If is an -net for , then
This is the key step of the Solovay–Kitaev construction. Applied recursively, it turns a coarse net near the identity into nets of doubly-exponentially improving precision.
Formalization Note The source writes as . Here it is written as explicit constants and , chosen before , because the source's recursion uses one constant at every level.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 6 of Quantum Algorithms and Learning Theory — Part II by Srinivasan Arunachalam. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is Aaronson's shadow tomography theorem.
A two-outcome measurement on is a POVM with . A learner using copies of an unknown -dimensional density matrix performs a measurement (a POVM with finite outcome set ) on and outputs numbers .
There is a polynomial in four variables such that for all , all integers and all effects on there exist and such a learner (depending on and , but not on ) with
for every -dimensional density matrix .
The number of copies is exponentially smaller in and than for full state tomography or for estimating each separately.
Formalization Note The source writes ; the endpoints are excluded because there or is undefined. Internal randomness and post-processing of the learner are absorbed into the POVM; is the -fold Kronecker power and logarithms are natural (the base is absorbed by the polynomial).
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 6 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let , let be a unitary matrix, let be a Hamiltonian on qubits, that is, a Hermitian complex matrix, and let . With the matrix exponential ,
This is what makes diagonalizable Hamiltonians easy to simulate: if diagonalizes , simulating reduces to applying , a diagonal phase, and .
Formalization Note The matrix exponential is Mathlib's power series NormedSpace.exp; is the conjugate transpose (star U). Hermiticity of is kept because the source says Hamiltonian (Def. 6.1), although the identity holds for every square matrix.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 7 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be a unitary on qubits (a circuit without measurements) and , and suppose
where are orthogonal unit vectors (the good and the bad state). Let be a unitary with and , let fix and negate every other basis state, and let be one round (reflect through , then through ). Put .
So applications of , and raise the success probability from to nearly , a quadratic improvement over the classical repetitions. Grover's algorithm is the special case , .
Formalization Note is the conjugate transpose (as is unitary). is constrained only on and , as in the source. The hypotheses require , since two orthonormal vectors need dimension at least 2.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 2 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the correctness of the Bernstein–Vazirani algorithm.
Let and , and fix a hidden string . The input is given by for every , where . With the phase query and the -qubit Hadamard transform , the Deutsch–Jozsa circuit gives
In particular, measuring the final state in the computational basis yields with probability .
So one query and Hadamard gates (the other operations) recover exactly. Only the query depends on the input. Classically, queries are needed.
Formalization Note The input is bvInput a, i.e. . The circuit is the same fixed definition deutschJozsaState as in the Deutsch–Jozsa statement. The state equality is exact, with no global phase: the source says the result is the classical state , and that is what the computation gives.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 2 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the sampling bound behind the classical post-processing of Simon's algorithm.
Let and be integers, and let be the field with two elements. Fix a nonzero vector and let
be the -dimensional subspace of vectors orthogonal to . Draw independently and uniformly at random from . Then
The bound does not depend on , so runs of Simon's circuit suffice to determine the hidden string with high probability.
Formalization Note The probability is the fraction of all tuples for which there are distinct indices whose vectors are linearly independent; vectors of are functions .
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 8 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is Proposition 8.34 of Nannicini, the end-to-end cost of the quantum mirror-descent solver for the MaxCut SDP relaxation, stated in an explicit hybrid classical–quantum QRAM cost model.
Let . For a nonzero real symmetric put . Call a density matrix an -solution of (MaxCutSDP) if
A hybrid algorithm consists of (i) a classical preprocessing program, a straight-line program of real arithmetic operations (, rational constants), which is the only part that reads the entries of and which writes the input half of a QRAM (, Def. 5.39); (ii) quantum runs, each applying a circuit of two-qubit gates and QRAM calls to and measuring all qubits, where the circuit of each run and the contents of the work half of the QRAM are chosen classically from the outcomes of the earlier runs; (iii) an output, computed from all outcomes, in the form of a list of pairs , which stands for the matrix
The theorem: there are absolute constants and such that for all , all and all , with , there is a hybrid algorithm, fixed before , such that
The proposition is the payoff of the chapter's MaxCut analysis: the subgradient estimation of Prop. 8.28, the iteration count of Thm. 8.30 and the Hamiltonian structure of Lem. 8.33 combine into a quantum solver whose quantum cost is sublinear in the entries of .
Formalization Note The printed proposition has no cost model, no success probability, and no precise meaning for the tolerance over the binary search on ; these are fixed as above. The classical bookkeeping between quantum runs (tallying samples, forming the subgradients, updating and ) is not counted, matching the proof, which takes the classical cost from Prop. 7.29 alone; that bookkeeping never sees . The output is the source's own representation of the iterate (Rem. 8.27, Lem. 8.33): with an arbitrary decoder, the optimum could be read off for free.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 5 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
In the hidden subgroup problem (HSP) on a finite group , an algorithm has black-box access to a function , where is a finite set, promised to hide some unknown subgroup :
The goal is to determine . A deterministic classical algorithm is a decision tree: it queries group elements adaptively, each query returning , and finally outputs a subgroup of . It solves the HSP if, for every subgroup and every hiding , its output is . Its query count on input is the number of queries it makes on .
Theorem. There are an absolute constant and a threshold such that the following holds for every . Let be a finite group and a finite set with , and suppose has a family of distinct subgroups any two of which have only the identity in common, i.e. for all distinct . Then every deterministic classical algorithm that solves the HSP on (with values in ) makes, on some input hiding some subgroup of ,
The theorem shows that the HSP is classically hard whenever the group has many trivially intersecting subgroups (for example Simon's problem), in contrast with efficient quantum algorithms for abelian groups.
Formalization Note The algorithm outputs the subgroup itself rather than a generating set, which changes nothing for a query lower bound. The condition makes every subgroup of hideable; the proof's adversary labels each new query with a fresh value, and with a very small (say ) only can be hidden, so the bound would fail. The constants and are chosen before the group, the set , the family and the algorithm. The threshold is needed because for the trivial group and no queries are needed. The phrase "whose only common element is the identity" is read pairwise, as in the section's "trivially intersecting subgroups" and as the proof needs when it counts at most non-identity values against subgroups. Read as , the theorem is false: in the cyclic group of squarefree order , all subgroups intersect trivially, yet queries determine .
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 21 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the symmetrization lemma of Minsky and Papert.
Let be multilinear, meaning that every variable has degree at most in . For , let
where is the Hamming weight of (its number of 1s). Then there is a univariate polynomial with (total degree) such that for every .
Symmetrization reduces questions about multivariate polynomials that represent symmetric Boolean functions, such as parity or OR, to questions about univariate polynomials. Those questions can then be settled by counting sign changes or by Markov's inequality.
Formalization Note The statement that " is a polynomial" is formalized as agreement with a univariate polynomial on the points , the only points where is defined. For these the average is taken over a nonempty set.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 27 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Fix integers . There is a single colouring rule , chosen before the graph, that assigns to an ordered pair of vertices a colour that depends only on the two vertices, their sides of the bipartition, and their neighbour lists , with the following property.
Let be an undirected simple graph on the vertex set with a bipartition (every edge joins the two sides) and maximum degree at most , and let be any duplicate-free list of the neighbours of each vertex . Then the map is a proper edge colouring of :
In the source the colour of an edge with on the left is , where is the position of in the neighbour list of . The lemma is the colouring step of the simulation of sparse Hamiltonians: the edges of each colour class form a matching, whose Hamiltonian is simulated separately before the pieces are combined by a product formula.
Formalization Note The source's "efficiently computable" has no machine model, so the running time of the rule is not formalized; what is kept is that one rule serves every graph and reads only the two endpoints' local data (two neighbour-list queries per edge). Colours are pairs of natural numbers rather than elements of so that the rule is total at ; the bound is on the colours actually used on edges.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 9 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the classical post-processing step of period finding over the reals (Childs, Lemma 9.1).
Write for the integer nearest to the real number . Let be a real number (the period, possibly irrational), let be a positive integer (the size of the cyclic group used for Fourier sampling), and let be relatively prime integers with and ; Fourier sampling returns the integers and . If , then:
Thus, from two samples with coprime multipliers, one learns from the continued fraction expansion and then an approximation of to within .
Formalization Note The nearest-integer function is Mathlib's round (ties rounded up; the source leaves ties unspecified and its proof uses only that the rounding error is at most ). Convergents are Mathlib's Real.convergent, which coincide with the convergents of the regular continued fraction. The ranges are those the source's proof uses (they come from and the proof's appeals to and ); the proof's " without loss of generality" is not imposed. Under these hypotheses the denominator is at least , so no division by zero occurs.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 33 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be the number of gates of a quantum circuit and let . In the adiabatic simulation of the circuit, the interpolated Hamiltonian leaves invariant the -dimensional computational subspace spanned by the history states , and on it acts, by and , as the real symmetric matrix
whose entry is , whose first off-diagonal entries are , and whose other entries vanish. Let be its eigenvalues, counted with multiplicity, and the gap between the smallest and the second smallest.
Lemma. The gap is uniformly in : there are a constant and a threshold such that
This bound on the minimum gap along the whole interpolation path is what makes an adiabatic evolution time sufficient, and hence shows that adiabatic quantum computation can efficiently simulate the circuit model.
Formalization Note The matrix is the shared definition clockPathMatrix k s on ; the gap is spectralGap, the second smallest minus the smallest eigenvalue of the Hermitian matrix with multiplicity (so a degenerate ground level would give gap ). The constants and are quantified before and .
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 6 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the correctness statement of the standard quantum algorithm for the Abelian hidden subgroup problem.
Let be a finite Abelian group written additively (), with characters , , and quantum Fourier transform , . Let be a finite set, a subgroup, and a function hiding :
The standard algorithm starts in (registers of dimensions and ), prepares , computes in superposition with one query, , (measures the second register,) applies to the first register and measures it. For every the outcome occurs with probability
Since , the algorithm samples uniformly from the labels of the elements of ; each sample gives a linear constraint on , which is how the algorithm generalizes Simon's algorithm, period finding and discrete logarithms.
Formalization Note The finite set is given an arbitrary additive group structure so that computing is the unitary , which maps to as in the source. The intermediate measurement of the second register (step 4) is omitted: it does not change the distribution of the first register, so the output law is the first-register marginal of the state before the final measurement. The source's claim that can then be found efficiently from few samples is asserted without proof and is not part of this statement.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 2 of An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
An code is a subspace of of dimension such that every operator acting on at most qubits satisfies for all unit vectors , with independent of (eq. (34)); that is, has distance at least . Put . The code is nondegenerate if, for every unit vector , the Gram matrix over the phase-free Pauli operators of weight at most is nonsingular. Let .
then an code exists. 2. (Quantum Hamming bound.) Every nondegenerate code satisfies
The first two bounds are counting arguments. The third gives the rate window, eq. (37), between which the best nondegenerate codes lie.
Formalization Note The source's 'distance ' is read as distance at least , so existence is meaningful also for . The hypothesis excludes , where (36) is an empty sum and the claim would demand a -dimensional code for every . The asymptotic clause is read as an – statement. The lower rate bound is asserted only when it is positive.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 7 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Fix constants and (those of the assumption ). There are constants and such that the following holds. Let , , , write , and assume . Then there exist
all independent of the matrix, such that for every whose entries satisfy , the unitary obtained with the QRAM loaded by the program is an -block-encoding of :
This is the data-structure route to block-encodings of classically stored dense matrices, with subnormalization the Frobenius norm and only polylogarithmic quantum cost.
Formalization Note Corrected statement. The source gives no cost model for classical arithmetic, does not say in which parameters is polylogarithmic, and does not say how the costs depend on . Here classical cost is the length of a straight-line real-arithmetic program (the model of the Cor. 5.45 chunk), means for arbitrary , all bounds are polylogarithmic in and , and the QRAM size is rather than because the word size must grow with . A -bit entry is modelled by the magnitude bound on its real and imaginary parts.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.