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?
Thompson sampling (TS) is the standard randomized heuristic for the Bayesian multi-armed bandit: at each decision it samples a parameter vector from the current posterior and pulls the arm that would be best if the sample were true. It ignores the remaining horizon. Min, Maglaras and Moallemi (arXiv:1902.04251, Management Science, 2025) obtain horizon-aware generalizations of TS from the information relaxation duality of Brown, Smith and Sun (Oper. Res. 2010). Each penalty function yields an upper bound on the Bayes-optimal value and an IRS policy. Such a policy samples a whole future outcome and plays the first action of the penalized clairvoyant optimum. With the zero-information penalty it is exactly TS.
Two of these policies, IRS.FH and IRS.V-Zero, are designed to interpolate between TS and the myopic rule. When one period remains they pull the arm with the highest predictive mean (Remark 5 of the paper). This mission formalizes the other end, Proposition 1: when many periods remain, they randomize exactly as Thompson sampling does. The paper presents this as the sense in which IRS policies "behave like TS during the initial decision epochs" and shift smoothly from exploration to exploitation without a tuning parameter.
There are arms . Arm has an unknown parameter . Given , its rewards are i.i.d. with law . The prior of is , a member of a conjugate family indexed by a belief . A Bayesian update maps to the posterior belief after a reward . The arms are independent. Throughout, rewards are integrable: for every belief (display (3)).
At remaining horizon and belief , the three policies act as follows:
It then plays the arm to which the optimal allocation assigns the most pulls.
Each action is a random variable driven by the policy's own sample.
Assume almost surely under , for all . Then for every arm ,
This holds for every choice of the tie-breaking rules in the argmaxes and in the allocation problem.
Proposition 1 identifies the long-horizon behaviour of the two IRS policies with that of Thompson sampling. Together with Remark 5 it pins down both ends of the horizon. It explains why their simulated regret curves track TS early and the myopic policy late (§5 of the paper). It also shows that the design choice "play the arm with the largest allocation" in IRS.V-Zero is the one that recovers TS. Other selection rules, such as any arm with a positive allocation, need not.
The paper gives a complete proof in Appendix D.1–D.2. A machine-checked version adds three things. It fixes the probabilistic model of a conjugate Bayesian bandit with infinite reward sequences in Lean, which the companion missions on the same paper also need. It makes the role of tie-breaking explicit. And it repairs a step of the printed proof: the bound in §D.2 holds only for two arms, and the general case needs and a threshold growing with . No formalization of this result is known on Prove2Me or in Mathlib.
The IRS.FH half reduces to almost-sure convergence of posterior means, which is a martingale argument (Lévy's upward theorem). That argument needs to be measurable with respect to the limit -algebra of the reward sequence, a fact supplied by the strong law of large numbers. Building the outcome law, a mixture over of infinite product measures, and identifying the conjugate update with conditional expectation are where the measure theory lies.
The IRS.V-Zero half does not follow from convergence of the posterior means alone. The selected arm is a function of an optimal allocation of a combinatorial problem whose size grows with . The naive expectation that the arm with the best limit receives "most" pulls has to be proved by an exchange argument that handles the finitely many early terms, where the posterior means can still be badly ordered. The printed version of this argument is correct only for .
Fin K with NeZero K; the reward sequence of an arm is ℕ → ℝ, 0-based.The development needs Lévy's upward theorem (MeasureTheory.tendsto_ae_condExp in Mathlib) and the strong law of large numbers (ProbabilityTheory.strong_law_ae). It also needs a lemma identifying iterated conjugate updates with the posterior given finitely many rewards, and the measurability of . These last two are reusable for any Bayesian bandit or sequential-estimation development. Contributions of the two deterministic milestones are self-contained and welcome first.
Round-Robin is the simplest allocation rule for indivisible goods: agents take turns, in a fixed order, picking their favourite remaining good. When agents have additive valuations and report them truthfully, the outcome is envy-free up to one good (EF1) — every agent values its own bundle at least as much as any other bundle with one good removed, a notion going back to Lipton et al., 2004 and Budish (2011) — which makes Round-Robin a standard baseline in fair division (Markakis, 2017). The mechanism, however, only sees reported rankings, and agents can gain by misreporting; without monetary transfers no truthful mechanism has a meaningful fairness guarantee even for two additive agents. Amanatidis, Birmpas, Lazos, Leonardi and Reiffenhäuser (arXiv:2301.13652, Mathematics of Operations Research, 2025) therefore study equilibrium fairness of Round-Robin when valuations go beyond additive. This mission concerns their fairness result for submodular valuations: strategic play does not destroy fairness, it only degrades it by a constant factor.
Timeline. Aziz, Goldberg and Walsh (ADT 2017) proved that Round-Robin always has a pure Nash equilibrium for additive valuations. Amanatidis et al. (WINE 2021) initiated the study of equilibrium fairness and showed that, for additive valuations, Round-Robin has equilibria and each of them yields an EF1 allocation with respect to the true valuations. The 2023 paper extends equilibrium existence to cancelable valuations (exact PNE) and submodular valuations (1/2-approximate PNE, with 1/2 tight), and proves that approximate equilibria are approximately EF1: factor for submodular and for subadditive cancelable valuations.
There are agents and a set of goods. Agent has a valuation that is normalized () and non-decreasing. The marginal value of a good with respect to a set is , and is submodular if whenever and .
Each agent reports a ranking , a total order on . Round-Robin runs steps; in step (counted from ) agent receives its -top good among those still unallocated. The result is an allocation . An allocation is -EF1 if for all agents with some satisfies . A profile is an -approximate pure Nash equilibrium (PNE) if no agent can, by reporting any other ranking , obtain a bundle worth more than times its current one:
In Lean the objects are marginal, IsValuation, IsSubmodular, IsRanking, roundRobin, IsApproxEF1 and IsApproxPNE in RoundRobinEq.SubmodularEF1.Setting; the step-to-agent map agentAt n t = t % n comes from the shared module RoundRobinEq.CancelableBluff.Setting.
For and submodular valuations, every -approximate PNE of Round-Robin yields an allocation that is -EF1 with respect to the true valuations:
Companions (not milestones): Lemma 4.1 (the greedy response is 1/2-EF1 from the deviator's perspective) and Theorem 4.2 (two agents: ).
The theorem says that fairness of Round-Robin is robust to strategic misreporting for a class far beyond additive valuations: whatever approximate equilibrium agents settle in, each agent's envy up to one good is bounded by . Combined with the existence of a 1/2-approximate PNE (Theorem 3.7 of the same paper), it gives an equilibrium that is 1/6-EF1. Lemmas 4.6 and 4.7 are statements about two runs of Round-Robin that differ in one agent's report; they involve no valuations and are reused verbatim for subadditive cancelable valuations (Theorem 4.5).
The result is proved in the paper; nothing in it is formalized anywhere to our knowledge. The mission builds a finite fair-division layer (Round-Robin as a step-by-step process, rankings, α-EF1, approximate PNE) that does not exist in Mathlib, and checks the combinatorial coupling of two runs, which is where the paper's argument carries its weight.
The obvious argument compares agent 's equilibrium bundle with its bundle after a good deviation (Algorithm 4's greedy response) and then compares that with agent 's bundle. With two agents everything not in or goes to , and this closes the argument. With agents the deviation reshuffles goods among all other agents, and there is no direct control on what ends up holding relative to the deviation run. The proof needs a global statement (Lemma 4.6) about how much two Round-Robin runs that differ in one report can diverge before each of 's turns, and then a careful indexing of by allocation time in the other run, so that a counting bound turns into the good-by-good inequality (2). The bookkeeping of steps, rounds and two simultaneous runs is the main work.
Fin n with , 0-based; goods a finite type M. The paper's standing simplification (p. 7) is a hypothesis Fintype.card M = k * n of every theorem; the paper's reduction to this case (dummy goods) is not formalized.allocBefore σ (r*n + i), and the paper's bounds for , , appear as for .Trivializing formalizations are excluded: deviations over arbitrary lists (which would strengthen the hypothesis), , EF1 computed on reported rankings instead of the true valuations, or the EF1 witness fixed in the goal statement would each change the theorem, and none is used.
Contributions welcome: proofs of Lemma 4.6 by induction on rounds (the reusable core), basic API for allocBefore/roundRobin (every good is allocated once, ), and Theorem 2.1.
Data brokers sell consumer data to firms that use it to decide whom to target, whom to lend to, or where to open a store. Two kinds of products are common: a marketing list, which supplies contact information without which the buyer cannot act at all, and a data append, which enriches information about consumers the buyer can already reach (Federal Trade Commission, Data Brokers, 2014). A seller who does not know a buyer's cost of acting must screen buyers with a menu of plans that differ in price and in how informative the data are.
Liang Guo's paper Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) characterizes the optimal menu, first for a binary-value model (§3) and then for a general information structure ordered by rotation (§4), following Johnson and Myatt (2006). This mission formalizes Proposition 7: data appends under the rotation order. It is the fourth mission of a series built from the same manuscript; the first three cover marketing lists and data appends in the binary model and marketing lists under the rotation order.
A marketer can take an action (target a consumer) at cost ; the action's value is uncertain with prior mean . A data service of informativeness produces a signal, and its information is summarized by the posterior mean . For each , has cumulative distribution function on a support , with a strictly positive density and mean for every . The family is rotation ordered: there is a point with
A more informative service spreads the posterior mean away from .
A service plan charges a fixed fee . Serving a marketer with informativeness costs the seller , with and increasing. A marketer targets exactly when , so a marketer with cost who buys earns
Costs are with probability and with probability , . A data-append buyer can act without the data, so its outside option is .
The seller offers a menu and maximizes subject to individual rationality and incentive compatibility for both types. Call any maximizer an optimal menu, with levels . The benchmark with observable costs is
and its maximizers are the efficient levels .
Assume . If , then
and if , then
Here means that the set of -levels of optimal menus equals the set of efficient levels, and each strict inequality holds for every optimal menu and every efficient level.
Proposition 7 is the general-distribution form of a "double reversal". With marketing lists the low-cost marketers are the high type: they get efficient information, and the high-cost marketers' information is distorted (Proposition 5 of the paper). With data appends and costs below the prior mean, the outside option makes the high-cost marketers value data more. The roles of the types swap, and the direction of the distortion flips with the position of the costs relative to the rotation point. The result tells a data seller which customers to under- or over-supply, and shows that the answer depends on whether its data enable an action or only refine it.
The paper proves the result on a few pages, partly by phrases such as "it can be readily verified". No machine-checked version exists. A formalization makes explicit what the printed argument leaves implicit: that the dropped constraints hold at the reduced optimum, which regularity of and the strict inequalities need, and that statements about "the" optimum hold for every optimum when maximizers are not unique.
The obvious approach substitutes the binding constraints and compares first-order conditions. Two steps of it fail as stated. First, the reduction to (15) drops and ; holds at a maximizer of (15) only when the two informativeness levels are ordered as the rotation order dictates. That ordering is available only when both costs lie on the same side of . Second, first-order conditions say nothing at a corner of . The strict comparison needs the efficient level to be interior, where the derivative of exists. That comes from the conditions of footnote 5 together with the mean-preserving property of the family. The selling cost need not be convex, so maximizers can be non-unique, and every comparison must hold for every pair of maximizers.
RotationFamily with a bounded support (the paper allows an unbounded one). is continuous on with , and derivative , continuous on the closed support. exists on the closed support. The rotation order (9) holds on the open support, and the mean is for every . Condition (10) is not assumed; it follows.Model extends it with , , and with both costs in (a pin: the integrals presume it). It also fixes with monotone on . is written as .3SUM asks whether an input sequence contains three entries at different positions whose sum is zero. The classical quadratic running time makes it a benchmark for fine-grained algorithm design: even a small fixed improvement in the exponent changes its asymptotic complexity. The setting here is polynomially bounded integers and a deterministic word RAM; the input-size exponent, rather than an experimental speedup, is the quantity being studied.
Alman and Vassilevska Williams (2026) give a deterministic truly subquadratic integer 3SUM algorithm through thin matrix products and reductions involving Exact Triangle. Xu's manuscript, Deterministic Integer 3SUM in O(n^1.999017) Time via a Sharper Binomial-Tail Analysis, dated 13 October 2026, refines the analysis of that framework. Its claimed bound is the formalization target here. The Hexagon link identifies the author's submission page, which may require authentication; it is not presented as a public article identifier or evidence of peer review.
An input of size is a function . For a fixed natural number , every entry obeys . Acceptance means that there are pairwise distinct indices with . Repeated values at different positions are allowed. This is a decision problem, so the algorithm need not return a witness triple.
The word-RAM specification is the campaign's existing EndStatement definition, imported from its foundation mission. For each fixed , one finite deterministic program, one word-width threshold constant, and one time-bound function must work for all input sizes and all word widths above that threshold. Words have finite signed interpretations; arithmetic, indirect memory access, branching, acceptance, and rejection are defined operationally. The result concerns this exact model.
For the supporting analysis, let , with endpoint values . All logarithms are natural. For an integer , a positive integer , and , set , , , and
The sharp preprocessing saving, query exponent, and encoding exponent are
These auxiliary definitions describe costs; they neither redefine 3SUM nor assume the existence of a fast algorithm.
The campaign goal is the exact fixed bound
The first supporting milestone is the two-sided binomial entropy estimate. The second is the manuscript's normalized tail bound
A further milestone establishes strict improvement over the earlier preprocessing saving at fixed parameters. The algorithmic milestone combines the manuscript's Propositions 4.1 and 5.1: admissible sharp-tail parameters must yield a program satisfying the shared 3SUM specification, not merely a numerical inequality.
The final supporting milestone certifies the exact choice
It includes the preprocessing, query, encoding, prime-selection, and instance-construction inequalities, together with
Every terminating decimal denotes an exact rational number. The target is the fixed big- exponent 1.999017; the smaller cutoff is accompanied by residual asymptotic losses in the manuscript and is not asserted as the same fixed bound.
A complete proof would certify the manuscript's improved integer 3SUM bound in the campaign's common machine model. The gain is an analysis refinement of the inherited algorithm and reductions. It does not claim a new algorithmic framework, optimal parameters, global optimality, or priority over all other work.
The manuscript also gives an auxiliary bound by retuning the previous estimate. That weaker result is background, not this mission's campaign value. The existing upstream formalization is prior work; it does not automatically certify either refinement. The supplied rational interval verifier checks the parameter inequalities, but those checks alone do not prove a word-RAM running-time theorem. The main goal and the newly drafted supporting statements remain open Lean proof obligations.
A better tail estimate is insufficient unless every other cost remains within the final budget. Shared encoding work, all queries, deterministic prime selection, witness scanning, and instance construction must be included. The word-size and address bounds must remain valid after changing parameters. Ceiling operations, restricting to powers of four, and bounded-size exceptions must also be handled.
The central formalization burden is the connection between the analytic estimates and an actual deterministic program. Assuming an oracle with the desired running time would remove that burden and would not establish the stated target. Likewise, checking a finite range of sizes or a floating-point optimizer's output cannot establish the universal algorithmic statement.
The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The foundation reference and the campaign goal's import are retained. Supporting definitions use real logarithms, real powers, natural binomial coefficients, finite sums, and a natural ceiling. Domain hypotheses exclude invalid entropy-tail regimes; endpoint binomial cases are included explicitly.
For , the shared time predicate means that there exists such that for every . Correctness and termination still cover every input size, including . The manuscript's convention must be extended to the campaign's case, and its word-size analysis must justify uniform correctness at every sufficiently large word width. Both are explicit interface obligations.
Reusable contributions include entropy and tail estimates, rigorous logarithm enclosures, and parameterized cost-to-program results. Existing compatible library results should be reused where available. The manuscript and metadata were prepared with AI assistance; this mission makes no claim of completed human review or completed formal verification of the improved bound.
EndStatement.lean supplies the shared specification, not a proof of this mission's new exponent.A two-stage adjustable robust linear program chooses a first-stage decision before an uncertain right-hand side is revealed, and a second-stage (recourse) decision afterwards, minimising the worst case over an uncertainty set of the total cost. Computing the optimal value is hard in general (Feige et al., 2007), and the standard tractable restriction is to affine policies (Ben-Tal et al., 2004), whose optimal value is computed by a single linear program.
El Housni and Goyal (arXiv:1807.00163v2) show that, when the recourse matrix is non-negative and is a budget of uncertainty set, is within a factor of . Their Section 7 asks whether the non-negativity of is needed, and answers with a family of two-stage lot-sizing instances whose recourse matrix is a network matrix with entries in . On this family the adjustable problem has value while every affine policy costs at least . Lot-sizing and transportation recourse are among the most common uses of two-stage robust optimisation (see Bertsimas and de Ruiter, 2016), so the instance is a natural one, not an artefact.
Lower bounds on the gap between affine and adjustable policies were known before (Bertsimas and Goyal, 2012); the point of the present family is that the adjustable value is exactly , so the ratio is infinite and the difference grows linearly in .
The lot-sizing problem (7.1). There are nodes. Node stores inventory at cost per unit, up to a capacity , and faces an uncertain demand . After is revealed, inventory may be shipped from node to node in amount at cost per unit. A solution is feasible when and, for every ,
The objective is the first-stage cost plus the worst case over of the transportation cost . The optimum over all rules is , and the optimum over affine rules (one row of per arc, one column per node) is .
The family (7.2). Let , and split the nodes into and with . Set on and on , everywhere, for , , and otherwise. The uncertainty set is
Inventory can thus move only from to , at no cost; stocking is free and stocking costs one per unit.
In the Lean development the general problem is the structure LotSizing N E (nodes N, usable arcs E with tail src, head tgt, distances d), with the predicate Feasible, the cost cost, and the sets adjustableValues, affineValues of objective values. The family is lotSizingFamily k, on nodes Fin k ⊕ Fin k and arcs Fin k × Fin k.
For every ,
each stated as IsLeast of the corresponding set of objective values, which asserts that the value is attained and is the minimum. The unboundedness of the gap, , is immediate.
The result. The approximation guarantees of the paper ( for budget sets, for disjoint constrained budgets) assume . Lemma 7.1 shows that this assumption is not a convenience of the proof: with a network recourse matrix no bound on of any form holds, even for a budget set and a bipartite network. Any extension of the guarantees to transportation or flow recourse must therefore change the policy class or add structure, which is the open direction the paper states after the lemma.
Formalizing it. The lemma is proved in the paper; it has not been machine-checked. The mission produces a reusable definition of the two-stage robust lot-sizing problem with arc-based recourse, the precise instance family, and checked versions of the five steps of Appendix D. Two of those steps hold only for and one is printed with its indices swapped (see the scope section); the formal statements make those boundaries explicit.
The adjustable half is a transportation argument, and the affine upper bound is a direct verification of one explicit solution. The substance is the affine lower bound, which must hold for every feasible affine solution, not for a particular one. Comparing an affine policy with the adjustable optimum on a few extreme scenarios gives nothing: on any single scenario an affine policy can match the adjustable cost. What fails for affine policies is simultaneous feasibility over the whole of , and the lower bound has to extract a cost from that requirement alone. It is also sensitive to the size of the instance: two of the intermediate steps of Appendix D are false for , so a formal proof has to treat small separately.
IsLeast. No real infimum is used, so "" cannot hold on an empty feasible set; feasibility includes , on all of , and the coverage constraint at every node, including the outflow constraint (D.2) at .LotSizing (any node set, any arc set, any uncertainty set) can host other two-stage lot-sizing and transportation results. Proofs of any milestone, and alternative arguments for the affine lower bound, are welcome.The source is arXiv:1807.00163v2; its printed page numbers equal the PDF's.
Superconducting circuits built from capacitors, inductors and Josephson junctions are the dominant platform for current quantum processors (Google, IBM, Rigetti, IQM and others). The source article — the Wikipedia entry Superconducting quantum computing — states two facts about the gate model on this hardware that this mission makes precise:
Statement 2 is a mathematical theorem, not an engineering claim: it says that every unitary operation on qubits can be written exactly as a finite product of the hardware's elementary gates. Its classical form with CNOT as the two-qubit gate is due to Barenco et al. (1995); the iSWAP version follows because CNOT can be built from two iSWAPs and single-qubit gates (Schuch–Siewert 2003).
Timeline.
An -qubit register has computational basis states labelled by bit strings ; its operations form the unitary group . For a unitary and a qubit , the single-qubit gate applies to qubit and leaves the others unchanged. For a matrix and an ordered pair of distinct qubits , applies to qubits (qubit is the first tensor factor). Write
The gates used are
in the basis , and the Toffoli gate . Time evolution under a Hamiltonian is , and the coupling Hamiltonian is . A two-level unitary acts as the identity outside the span of two basis vectors.
For every ,
The goal theorem is the formal justification for compiling arbitrary quantum algorithms to superconducting hardware whose native entangling interaction is of XY/iSWAP type: any target unitary, however large, has an exact decomposition into the hardware's elementary operations. Milestone 1 connects the abstract gate to the physical Hamiltonian; milestones 3–4 are the textbook universality theorem in the CNOT form, reusable for any other two-qubit gate that can synthesise CNOT; milestone 5 is the Toffoli construction mentioned in the source.
All results are classical and proved in the literature. To the best of the drafter's knowledge they are not yet available as machine-checked statements in Mathlib in this form; the mission's contribution is a complete formal development.
The naive route — "decompose into two-level unitaries, then implement each with gates" — hides real work: a two-level unitary on basis states with differing in many bits must be conjugated by a Gray-code sequence of controlled-NOT style gates into one acting on a single qubit, controlled on all others, and multiply-controlled single-qubit gates must then be reduced to single-qubit gates and CNOTs. Keeping indices, tensor embeddings and controls consistent over qubits is the main formal burden. Milestone 1 requires computing a matrix exponential exactly, which in Lean means handling NormedSpace.exp on a non-diagonal matrix.
Fin n → Fin 2; two-qubit operators are indexed by Fin 2 × Fin 2 with the Kronecker product ⊗ₖ, first factor = first qubit.Subgroup.closure) inside Matrix.unitaryGroup equals ⊤; no approximation or topological closure is involved, which is why the full continuous family of single-qubit gates is included.onQubit, onPair) and multiply-controlled gates are reusable for any quantum-circuit mission.Grover's algorithm is a quantum algorithm for unstructured search: given black-box access to a function that takes the value at exactly one input , it finds with high probability using evaluations of . It was devised by Lov Grover in 1996 (Grover, STOC 1996). Classically the same task needs evaluations, since there is no better approach than trying the inputs one after the other. Bennett, Bernstein, Brassard and Vazirani showed that every quantum algorithm needs evaluations (BBBV, SIAM J. Comput. 1997), so the quadratic speedup is optimal.
Because many problems contain exhaustive search as a subroutine, the algorithm and its generalization, amplitude amplification, speed up a broad class of algorithms: brute-force attacks on symmetric-key cryptography (a 128-bit key in roughly iterations), algorithms for NP-complete problems such as 3SAT, and black-box problems such as element distinctness and the collision problem.
This mission follows the presentation of the algorithm and of its analysis in the Wikipedia article Grover's algorithm (revision 1373498442), which gives two analyses of the same algorithm, a geometric proof and an algebraic proof, following Nielsen–Chuang 2010, Chapter 6.
Fix . The state space is with standard basis and inner product . Let have exactly one index with .
The algorithm. (1) Initialize the system to . (2) Perform the Grover iteration times. (3) Measure the resulting state in the computational basis; by the Born rule the outcome is with probability .
Two further objects appear in the analysis: the ket perpendicular to , and the angles (geometric proof) and (algebraic proof).
This combines the article's headline claims: the algorithm outputs with probability at least (for ) using applications of , the success probability approaches for , and the number of iterations satisfies . The goal does not fix .
Listed in the article's order.
The result. The goal says that unstructured search over items costs oracle queries on a quantum computer, with failure probability at most for a single run, and hence that the expected number of queries until is found is still . It is the quantitative content behind the use of Grover's algorithm as a subroutine and behind its role in post-quantum key-length recommendations.
Formalizing it. The result is classical and fully proved on paper. The work here is to formalize the article's two proofs: the reflection/rotation picture and the algebraic diagonalization, together with the equivalence of the two oracle models and the explicit bound stated in the article. A separate platform mission, Grover's Algorithm, already contains machine-checked proofs of the amplitude formula and of a success guarantee with iteration bound , in a model where the oracle is given by the marked index. This mission differs in that it derives the oracle from the function , includes the ancilla-based standard oracle, the Householder and reflection statements, the algebraic Jordan-form analysis, and the bound in terms of . The lower bound of Bennett–Bernstein–Brassard–Vazirani (optimality) is out of scope.
None of the steps is deep; the difficulty lies in the bookkeeping. The plane is not spanned by an orthonormal pair, so the matrices of the algebraic proof are in a non-orthogonal spanning set, and the probability formula must be transported from that picture back to the -dimensional state. Passing from the exact formula to the bound requires choosing an integer , controlling to within of , and comparing with to reach . Edge cases matter: (where , is undefined and is singular) and the integer rounding of .
All statements import one definitions file, GroverWiki_Defs, and live in the namespace GroverWiki.
Fin N → ℂ; operators are matrices Matrix (Fin N) (Fin N) ℂ acting by mulVec; the two-register space is indexed by Fin N × Fin 2. Bit values are Fin 2, so ⊕ is addition in Fin 2.f : Fin N → Fin 2; uniqueness of the marked item is the hypothesis ∀ x, f x = 1 ↔ x = ω.x is ‖ψ x‖ ^ 2, applied to the state (U_s U_ω)^r |s⟩.The goal is not trivialized by the model: the state is the actual output of the algorithm, the iteration count is bounded explicitly, and the probability bound is the Born-rule probability of the marked index. Contributions of reusable lemmas on reflections and rotations in two-dimensional subspaces of are welcome.
A sequence of real numbers often arrives as a list of moments: averages of powers of a random variable, traces of powers of a self-adjoint operator, or coefficients of a continued fraction. The Hamburger moment problem, named after Hans Ludwig Hamburger (1920–21), asks when such a list really comes from a measure on the whole real line, and, when it does, whether the measure is determined by its moments. The question sits at the junction of probability (the method of moments, identification of limit laws), spectral theory of symmetric operators and Jacobi matrices, and the theory of orthogonal polynomials; standard monographs include Shohat–Tamarkin (1943) and Schmüdgen (2017).
Timeline (as summarized in the source article and its references):
Let be a sequence of real numbers. A solution of the Hamburger moment problem for is a positive Borel measure on such that every power is -integrable and
The sequence is a moment sequence if at least one solution exists.
The Hankel kernel of is the infinite matrix . It is positive definite (in the sense of the source) if
for every finitary complex sequence , i.e. for all but finitely many . Its finite sections are the Hankel matrices
In the Lean development these objects are IsMomentMeasure m μ, IsMomentSequence m, hankelForm m c, HankelPosDef m and hankelMatrix m n, all in the namespace HamburgerMoment.
The result. Hamburger's theorem turns an existence question about measures into a family of finite-dimensional positivity conditions that can be checked on the data. It is the basic tool behind the method of moments in probability (identifying a distribution from its moments, when the problem is determinate), behind the spectral theory of Jacobi matrices, and behind Gauss quadrature and orthogonal polynomials on the line. The uniqueness criteria decide when moments determine a law; the non-uniqueness examples (for instance the log-normal distribution) show that they do not always do so.
Formalizing it. All results here are classical and proved in the literature; to the best of the captain's knowledge none of them is currently available as a formal statement in Mathlib, which has neither moment problems nor Hankel kernels. The mission produces a reusable vocabulary (moment measures, Hankel forms and matrices) and machine-checked versions of the existence theorem, the uniqueness criteria and the non-uniqueness phenomenon.
The "only if" direction is a direct computation. The converse is the substance: from positivity of countably many finite quadratic forms one must produce a countably additive measure on a non-compact space with all moments matching. Compactness arguments on finite sections give measures whose low-order moments match, but mass can escape to infinity and higher moments need not converge; the source's route instead goes through the Hilbert space completion of finitary sequences, self-adjoint extensions of the (generally unbounded) shift operator and the spectral theorem for unbounded self-adjoint operators — machinery that is only partly present in Mathlib. An alternative route via positive linear functionals on polynomials (M. Riesz extension, Riesz–Markov–Kakutani) has to control the same escape of mass. The uniqueness criterion requires quasi-analyticity or Carleman-type estimates.
m : ℕ → ℝ; measures are Measure ℝ on the Borel σ-algebra of . A solution must have every power integrable, so in particular is finite with total mass .ℕ →₀ ℂ, and the Hankel form is the finite double sum over the support. "" is the order on (the value is a nonnegative real number), matching the source.Fin (n + 1); positive semidefiniteness is Mathlib's Matrix.PosSemidef.Needed infrastructure and welcome contributions: polynomial integrability under finite moments, positive linear functionals on , a Riesz–Markov or spectral-measure construction on , Vandermonde arguments for finitely supported measures, and Carleman / quasi-analyticity estimates. The definitions of moment measures and Hankel kernels are reusable for the Stieltjes and Hausdorff moment problems.
Shor's algorithm is a quantum algorithm that finds a nontrivial factor of an integer in time polynomial in , and its variants compute discrete logarithms in finite cyclic groups. It was developed by Peter Shor in 1994 (Shor, FOCS 1994; Shor, SIAM J. Comput. 1997). No classical polynomial-time factoring algorithm is known; the best classical method, the general number field sieve, runs in sub-exponential time. Because the security of RSA and of finite-field and elliptic-curve Diffie–Hellman rests on the hardness of factoring and of discrete logarithms, Shor's algorithm is the main reason these schemes are considered breakable by a large fault-tolerant quantum computer, and the main motivation for post-quantum cryptography.
This mission follows the presentation of the algorithm in the Wikipedia article Shor's algorithm (revision 1378862216), which describes the quantum part through quantum phase estimation, an approach due to Kitaev (Kitaev 1995) and standard in textbooks (Nielsen–Chuang 2010).
Let be integers with . The order is the smallest positive integer with .
Classical reduction. If is even and , then is a nontrivial factor of . Factoring therefore reduces to computing orders.
Quantum order finding. Let and . A state of an -qubit register is a vector in with standard basis . The modular-multiplication gate is the -qubit gate
With , the states are eigenvectors of with eigenvalues . The order-finding circuit acts on a -qubit first register and the -qubit second register: Hadamard gates on the first register, controlled gates for (qubit of the first register controls on the second), and the inverse quantum Fourier transform on the first register. It is applied to and the first register is measured, producing an outcome with probability . Finally the continued fractions algorithm is run on .
For every ,
and for every such some continued fraction convergent of equals in lowest terms, i.e. has numerator and denominator . Summed over , a single run yields with probability at least an outcome from which the continued fractions algorithm recovers some in lowest terms.
The goal is the quantitative statement behind the article's claim that phase estimation "gives as output a random integer of the form " and that a -qubit first register suffices to recover . Combined with the classical milestones, it is the correctness argument of Shor's factoring algorithm, minus the separate number-theoretic estimate of how often a random has even order with , which the article does not state.
The results are classical and their proofs are published. The work this mission asks for is a machine-checked proof against an explicit gate-level model of the circuit — Hadamard tensor power, controlled modular-multiplication gates, inverse QFT — rather than against a closed-form output distribution assumed up front. Related missions on the platform formalize Shor's 1997 paper, which analyses the circuit by a direct Fourier-sum computation with ; this mission follows the phase-estimation route with the article's constants.
The spectral facts about and the classical reduction are short arguments. The main obstacle is the circuit: showing that the product of the controlled gates acts on as multiplication by requires the binary expansion of and the commutation of the controlled gates, and the subsequent inverse QFT must be computed explicitly. The bound requires an estimate of for which is uniform in ; a crude estimate gives a weaker constant. The measurement identity requires the orthonormality of the , which uses that are distinct modulo .
States are coordinate vectors Fin d → ℂ, gates are complex matrices acting by Matrix.mulVec, two-register operators are Kronecker products on Fin d₁ × Fin d₂, and measurement probabilities are sums of squared moduli. The order is orderOf (a : ZMod N) and is Nat.clog 2 N. Convergents are Mathlib's Real.convergent, the standard continued fraction expansion. The goal is a statement about the specific circuit defined in the mission's definition file, so it cannot be satisfied by choosing a convenient output distribution, and the recovery statement is quantified over a fixed , so the trivial convergent (which equals ) does not discharge it for .
Reusable infrastructure welcome from this mission: the action of the Kronecker-product phase estimation circuit on eigenstates, the explicit inverse QFT computation, and the estimate for the Fejér-type kernel.
Generalized complex geometry, introduced by N. Hitchin (Generalized Calabi–Yau manifolds, 2003) and developed by M. Gualtieri (thesis, 2004; Annals 2011), treats complex and symplectic structures as two special cases of one notion. It replaces the tangent bundle of a manifold by the generalized tangent bundle and an almost complex structure on by an orthogonal almost complex structure on . The framework is used in string theory: supersymmetric flux compactifications require (possibly twisted) generalized complex structures (Graña 2006).
The pointwise theory is pure linear algebra, and the global statements of the subject rest on it: the equivalence between a generalized almost complex structure and its -eigenbundle, Gualtieri's classification of maximal isotropic subspaces by pairs , the type invariant and its behaviour under B-field shifts, and the two model examples (complex and symplectic). This mission formalizes that linear-algebraic layer as presented in the Wikipedia article Generalized complex structure.
Fix . A fiber of the tangent bundle is ; its dual is identified with through the standard dual basis, so a one-form acts by . The generalized tangent space is , whose elements are formal sums , with the natural inner product of signature
The same formula defines a complex bilinear form on the complexification , which carries the complex conjugation .
For every generalized almost complex structure , its eigenbundle satisfies
and conversely every complex subspace satisfying (i) and (ii) is the -eigenbundle of a unique generalized almost complex structure. Hence (i), (ii) form an alternative definition of generalized almost complex structure.
The goal makes the two descriptions of a generalized almost complex structure interchangeable: integrability (closure of under the Courant bracket), the canonical pure-spinor line and the type are all phrased in terms of , while the definition is phrased in terms of . The classification by is the normal form behind the type, the local classification near regular points, and the identification of the complex and symplectic extremes. All of these results are classical and proved in the cited literature; the remaining work is their machine-checked formalization. A formal library of this linear algebra is a prerequisite for later missions on the manifold-level theory (Courant bracket, generalized Darboux theorem).
The goal mixes real and complex linear algebra. Recovering a real map from a complex subspace requires knowing that is the whole complexification and that the map which is on and on commutes with conjugation and is orthogonal; each of these uses hypotheses (i) and (ii), and the dimension condition cannot be dropped. The classification needs a dimension count for (functionals on versus the annihilator of ) and, in the converse direction, the extraction of from an arbitrary maximal isotropic subspace. For the complex example, the type computation requires the dimension of the -eigenspace of a real complex structure, which is exactly .
Everything is fiberwise and in coordinates: is Fin N → ℝ, is GIdx N → ℝ with GIdx N = Fin N ⊕ Fin N (vector part on Sum.inl, one-form part on Sum.inr), endomorphisms are matrices over GIdx N, and the complexification is GIdx N → ℂ with the real matrix acting through . 2-forms on are skew matrices with ; 2-forms on a subspace are skew bilinear forms on . Nondegeneracy of is (the inverse used in is the matrix inverse). The type uses the article's real-dimension convention, so it is twice Gualtieri's complex type. The classification milestones are stated over RCLike fields, i.e. for both and , as in the article.
Out of scope for this mission: the Courant bracket and integrability, the canonical (pure spinor) bundle, upper semicontinuity of the type, the generalized Darboux theorem, local holomorphicity, and the -structure description. These need manifold-level infrastructure (Lie derivatives and exterior derivatives of forms on manifolds) and are left for later missions.
The AdS/CFT correspondence (Maldacena 1997) relates quantum gravity on anti-de Sitter (AdS) space to a conformal field theory (CFT) living on its timelike boundary. Gubser–Klebanov–Polyakov and Witten gave the CFT-from-AdS direction of the dictionary: CFT correlators are computed from bulk Green functions. Giddings (PRL 83, 2707, 1999) supplies an entry in the reverse direction. Because AdS confines particles and has no ordinary asymptotic states, a flat-space S matrix does not exist; the paper defines a boundary S matrix from in/out states built out of wave packets incident from the boundary, derives an LSZ-type reduction formula (eq. 42), and concludes that the boundary S matrix equals the boundary CFT correlator (eqs. 44–45).
Every step of that argument rests on the classical theory of the free Klein–Gordon field on global AdS: the parameters (eq. 4), the discrete normalizable spectrum with modes behaving like at the boundary (eqs. 5–7), the non-normalizable modes behaving like (eqs. 8–9), and the boundary limit (eqs. 19–20) that fixes the normalization of the bulk–boundary propagator.
Fix an integer , an AdS radius and a scalar mass . Global has metric (eq. 2)
Define (eq. 4)
A mode , with a spherical harmonic on , solves the free equation (eq. 3) exactly when the radial profile satisfies, on ,
A normalizable mode is a nonzero solution that is bounded as (regular at the centre of AdS) and has finite Klein–Gordon norm, i.e. . The explicit modes of eq. (5) are
with the Jacobi polynomial, and the eigenfrequencies of eq. (7) are .
For every , and radial profile ,
The goal is the precise mathematical content behind the paper's statement that free solutions "exist at arbitrary frequency but are only normalizable for a discrete set of frequencies". This spectrum is what makes the boundary operators of eq. (25) act as creation and annihilation operators (eqs. 27–29), and the boundary exponents and the constant determine the normalizations in eqs. (20), (21), (28) and (29). The physics derivation of eqs. (28)–(42) is not rigorous mathematics; milestone 8 isolates the final step from (42)–(43) to (44), which is an exact identity about integral kernels.
The radial results are classical (the paper attributes the explicit solutions to Balasubramanian–Kraus–Lawrence). This mission asks for machine-checked proofs of these results, together with the reusable Jacobi-polynomial and boundary-asymptotics infrastructure they require.
Verifying that solves the equation is a computation. The goal's converse direction is the hard part: one must show that a solution regular at can have finite Klein–Gordon norm only when equals some , and that it is then unique up to a scalar. This requires controlling both regular singular points and of the radial equation, including the resonant cases where or is an integer and logarithms appear. Since forces , the branch is never square-integrable, so the second quantization available for does not arise.
Real.rpow; on the relevant range.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 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 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 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 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.