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?
In view of controlling finite dimensional open quantum systems, we provide a unified Lie-semigroup framework describing the structure of completely positive trace-preserving maps. It allows (i) to identify the Kossakowski-Lindblad generators as the Lie wedge of a subsemigroup, (ii) to link properties of Lie semigroups such as divisibility with Markov properties of quantum channels, and (iii) to characterise reachable sets and controllability in open systems. We elucidate when time-optimal controls derived for the analogous closed system already give good fidelities in open systems and when a more detailed knowledge of the open system (e.g., in terms of the parameters of its Kossakowski-Lindblad master equation) is actually required for state-of-the-art optimal-control algorithms. -- As an outlook, we sketch the structure of a new, potentially more efficient numerical approach explicitly making use of the corresponding Lie wedge.
This mission is the statement-level formalization of Lie-Semigroup Structures for Reachability and Control of Open Quantum Systems (arXiv:0811.3906v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The generated Markovian semigroup has the full channel tangent wedge (Theorem III.3, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
30 results of the paper are not stated yet, because the library lacks an interface they need:
The classical capacity of a noisy optical channel is the maximum rate at which information can be transmitted reliably, given a constraint on the mean input energy. For the ubiquitous bosonic Gaussian channels, which include standard models of loss and noise in fibre and free-space optical links, determining this rate requires addressing whether entanglement between channel uses or non-Gaussian signals can outperform Gaussian encodings. More precisely, the question is whether the energy-constrained Holevo information is additive across arbitrarily many channel uses and coincides with its Gaussian counterpart. We answer these fundamental questions in the affirmative for every single-mode bosonic Gaussian channel at every input energy. Namely, we prove that independently prepared Gaussian states with Gaussian-distributed random displacements achieve the capacity, including in the low-energy regime where squeezing the signals competes with encoding information in their displacement. Our proof connects an entanglement inequality to a sharp, additive lower bound on output entropy. We then characterise communication above capacity: under a strict total photon-number cutoff, the probability of correct decoding decreases exponentially with the number of channel uses, and we derive explicit bounds on the decay exponent. When only the mean photon number is constrained, a simple energy-rescaling formula determines exactly the entire asymptotic rate--error trade-off: the capacity at mean photon number and allowed average decoding error equals the vanishing-error capacity at mean photon number . Together, these results identify the ultimate limits of classical communication for some of the most fundamental models of optical communication. △ Less
This mission is the statement-level formalization of Classical Capacity of Single-Mode Bosonic Gaussian Channels (arXiv:2610.22308v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Affine envelope and joint convexity of the moment-resolved entropy (Eq. (18), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
27 results of the paper are not stated yet, because the library lacks an interface they need:
We give a representation for entanglement-breaking channels in separable Hilbert space that generalizes the "Kraus decomposition with rank one operators" and use it to describe the complementary channels. We also give necessary and sufficient condition of entanglement-breaking for a general quantum Gaussian channel. Application of this condition to one-mode channels provides several new cases where the additivity conjecture holds in full generality.
This mission is the statement-level formalization of Entanglement-breaking channels in infinite dimensions (arXiv:0802.0235v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Radon–Nikodym representation of a POVM (Lemma 1: Radon–Nikodym representation of a POVM (9)–(10), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
18 results of the paper are not stated yet, because the library lacks an interface they need:
The work is devoted to study of quantum mutual information and coherent information -- the two important characteristics of quantum communication channel. Appropriate definitions of these quantities in the infinite-dimensional case are given and their properties are studied in detail. Basic identities relating quantum mutual information and coherent information of a pair of complementary channels are proved. An unexpected continuity property of quantum mutual information and coherent information following from the above identities is observed. An upper bound for the coherent information is obtained.
This mission is the statement-level formalization of Mutual and coherent informations for infinite-dimensional quantum channels (arXiv:1004.2495v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: complementary-channel mutual-information identity (22) (Theorem 1: complementary-channel mutual-information identity (22), PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
We analyse two possible definitions of the squashed entanglement in an infinite-dimensional bipartite system: direct translation of the finite-dimensional definition and its universal extension. It is shown that the both definitions produce the same lower semicontinuous entanglement measure possessing all basis properties of the squashed entanglement on the set of states having at least one finite marginal entropy. Is also shown that the second definition gives an adequate extension of this measure to the set of all states of infinite-dimensional bipartite system. A general condition relating continuity of the squashed entanglement to continuity of the quantum mutual information is proved and its corollaries are considered. Continuity bound for the squashed entanglement under the energy constraint on one subsystem is obtained by using the tight continuity bound for conditional mutual information (proved in the Appendix by using Winter's technique). It is shown that the same continuity bound is valid for the entanglement of formation. As a result the asymptotic continuity of the both entanglement measures under the energy constraint on one subsystem is proved.
This mission is the statement-level formalization of Squashed entanglement in infinite dimensions (arXiv:1507.08964v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Compactness of bipartite states from both marginal sets (Lemma 1, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
25 results of the paper are not stated yet, because the library lacks an interface they need:
A classification of one-mode Gaussian channels is given up to canonical unitary equivalence. A complementary to the quantum channel with additive classical Gaussian noise is described providing an example of one-mode Gaussian channel which is neither degradable nor anti-degradable.
This mission is the statement-level formalization of One-mode quantum Gaussian channels (arXiv:quant-ph/0607051v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Six canonical forms of one-mode Gaussian channels after displacement removal (§1, unnumbered Theorem, pp.2–4, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
15 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper we give a general integral representation for separable states in the tensor product of infinite dimensional Hilbert spaces and provide the first example of separable states that are not countably decomposable. We also prove the structure theorem for the quantum communication channels that are entanglement-breaking, generalizing the finite-dimensional result of M. Horodecki, Ruskai and Shor. In the finite dimensional case such channels can be characterized as having the Kraus representation with operators of rank 1. The above example implies existence of infinite-dimensional entanglement-breaking channels having no such representation.
This mission is the statement-level formalization of Separability and Entanglement-Breaking in Infinite Dimensions (arXiv:quant-ph/0504204v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Separable states are precisely probability mixtures of product states (§2, equation (2), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
9 results of the paper are not stated yet, because the library lacks an interface they need:
We give trade-offs between classical communication, quantum communication, and entanglement for processing information in the Shannon-theoretic setting. We first prove a unit-resource capacity theorem that applies to the scenario where only the above three noiseless resources are available for consumption or generation. The optimal strategy mixes the three fundamental protocols of teleportation, super-dense coding, and entanglement distribution. We then provide an achievable rate region and a matching multi-letter converse for the direct static capacity theorem. This theorem applies to the scenario where a large number of copies of a noisy bipartite state are available (in addition to consumption or generation of the above three noiseless resources). Our coding strategy involves a protocol that we name the classically-assisted state redistribution protocol and the three fundamental protocols. We finally provide an achievable rate region and a matching mutli-letter converse for the direct dynamic capacity theorem. This theorem applies to the scenario where a large number of uses of a noisy quantum channel are available in addition to the consumption or generation of the three noiseless resources. Our coding strategy combines the classically-enhanced father protocol with the three fundamental unit protocols.
This mission is the statement-level formalization of Trading classical communication, quantum communication, and entanglement in quantum Shannon theory (arXiv:0901.3038v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-block converse with explicit continuity corrections and a common classical refinement (Appendix F, (106)–(107), and both proof chains on PDF p.25, PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
14 results of the paper are not stated yet, because the library lacks an interface they need:
High-dimensional statistical learning (HDSL) fits a model with parameters from samples when may far exceed . The standard guarantees for sparse estimators, such as the Lasso, rest on restricted strong convexity (RSC) or restricted eigenvalue conditions on the empirical risk (Negahban et al., 2012; Loh & Wainwright, 2015). These conditions fail or are hard to verify for many losses that matter in operations research and machine learning: nonsmooth losses, losses of neural networks, and M-estimation problems whose population risk is not strongly convex near any sparse vector.
Liu, Ye and Lee (arXiv:1903.00616v2; Operations Research, 2022) remove RSC entirely. They regularize the empirical risk with a folded concave penalty, the minimax concave penalty (MCP) of Zhang (2010), and analyse not a global minimizer (intractable, since the problem is nonconvex) but any point satisfying a weak second-order stationarity condition. They also replace exact sparsity by approximate sparsity: the best sparse vector need only be -optimal for the population risk. Their main result, Theorem 1, gives an excess-risk bound whose sample complexity is poly-logarithmic in .
Observations are i.i.d. copies of a random element of a measurable space . A loss , with parameter , defines the population risk , assumed finite for every and bounded below, the empirical risk , and the regularized objective
with tuning parameters . Norms: is Euclidean, is , is the max norm and counts nonzero entries.
The standing assumptions are:
A vector satisfies the S³ONC (significant subspace second-order necessary conditions, Definition 1) at a sample if it is a KKT point of , with subgradients , and whenever . With , Theorem 1 fixes , where is the constant of the Bernstein inequality (12).
For and any random with satisfying the S³ONC almost surely:
(i) if almost surely and , then with probability at least ,
(ii) if is no worse in than a Lasso solution , the -free bound (22) holds under (21).
are universal constants. The goal fixes the polynomial rate ; the general-rate result is Proposition 1.
The theorem shows that second-order stationarity, which first- and second-order methods can certify (the paper's Theorem 2 gives a pseudo-polynomial algorithm), suffices for poly-logarithmic sample complexity in without convexity or RSC. The paper builds on it for nonsmooth losses through smoothing (Theorem 3) and for regularized neural networks (Theorem 4). The same definitions layer (MCP, S³ONC, A-sparsity) serves those results.
The result is proved on paper, in the electronic companion of the cited preprint. Nothing of it is formalized: the platform has no folded concave penalty, no S³ONC and no excess-risk bound for sparse M-estimation without RSC. This mission provides the definitions, the goal and the proof chain as stated by the authors, with two disclosed adjustments (see Formalization scope).
The obvious argument bounds uniformly over the box and then compares with . It fails: a covering of a -dimensional box costs a factor , not , in the sample size. The usual repair, RSC, which localizes the estimator near a sparse target, is exactly what the paper does without. is moreover only a stationary point of a nonconvex objective, not a minimizer, so no optimality inequality over the whole space is available. The probabilistic part requires keeping the constants consistent across several union bounds and two Bernstein inequalities, with failure probabilities that must stay summable in the sparsity level. In Lean, an additional obstacle is that suprema over uncountable sparse sets are not obviously measurable.
Fin p → ℝ is the sup norm). is the published Orlicz norm HighDimProb.Concentration.subexponentialNorm, always together with an explicit witness of sub-exponentiality. The paper cites the equivalent moment form; the difference is absorbed by the universal constants.bernstein_weighted supplies one.The trivializing formalizations are ruled out explicitly: constants chosen after the instance, junk values of non-integrable expectations, empty infima or undefined derivatives, the sup norm in place of the Euclidean norm, and an estimator chosen by the theorem.
Welcome contributions: proofs of the milestones in order; a Lean proof that Assumption 3 implies (12), via the published Bernstein inequality; a measurable-selection or outer-measure lemma for suprema over sparse boxes, which is reusable across high-dimensional statistics.
Tournaments and contests reward agents by their relative standing: sales bonuses for the top performers, promotions, prizes for the first to finish, research competitions. Since Lazear and Rosen (Rank-order tournaments as optimum labor contracts, 1981) such rank-order incentives have been a standard object in economics and operations research, and the design question of which reward schedule elicits which behaviour is central to the area. With a large population, the strategic interaction becomes a mean field game: each agent responds to the distribution of the others' outcomes rather than to individual opponents.
Bayraktar and Zhang (Terminal Ranking Games, arXiv:1906.09628v2, 2020; Mathematics of Operations Research 2021) study such a game in continuous time. Each player steers a Brownian project value by costly effort and is paid at a fixed terminal time according to her own value, her rank in the population, and the population mean. Their main result solves the equilibrium semi-explicitly. Related earlier work treats rank-based rewards by completion time (Bayraktar, Cvitanić and Zhang, Large tournament games, 2019) and by terminal rank in a strong formulation (Bayraktar and Zhang, A rank-based mean field game in the strong formulation, 2016).
Fix a horizon , a cost coefficient , a volatility and an initial value . On a probability space let be a real Brownian motion, and let be the terminal project value under zero effort.
A reward function depends on the player's terminal value , her rank and the population mean ; it is weakly increasing in each argument. The class collects the bounded ones. For a population law on with c.d.f. and mean , write : the payment received at terminal value when the others are distributed as .
Effort changes the law of the path. In the weak formulation used by the paper, a control is a probability measure equivalent to , and the quadratic effort cost becomes the relative entropy . Given the population law , the single player's value is
A law is an equilibrium if it is a fixed point of the best response: some optimal for gives the law .
The goal concerns the subclass of bounded rewards that do not depend on and are continuous in . Let be the standard normal c.d.f., its quantile function, the quantile function of , and
For :
No uniqueness is claimed.
The theorem reduces an infinite-dimensional fixed point, over laws on defined through a control problem on path space, to a scalar equation for the mean. Everything else is explicit: the equilibrium law is a reparametrized Gaussian quantile, and the game value is a closed form in . The paper's later results build on this: the comparison of game values under the Lorenz order of rewards (Theorem 4.1), the characterization of rewards that realize a target equilibrium (Theorem 5.1), and the tournament design problems of Section 5 all start from (3.2) and the value formula.
The result is proved in the paper, partly by appeal to the literature on Schrödinger bridges; Proposition 2.1 is stated there without proof. None of it is formalized. A formal development would supply the first machine-checked mean field equilibrium of a rank-based game, the entropic weak formulation of a control problem with a terminal reward, and a verified explicit solution against which numerical schemes can be checked.
The reduction from path measures to terminal laws, (2.6), needs the disintegration of along (the Schrödinger bridge) and the chain rule for relative entropy; only one inequality follows from data processing. The best response is a Gibbs variational principle on the line, but the optimizer must be lifted back to path space and every optimizer must be shown to have the same terminal law. In Theorem 3.2 the characterization requires inverting , which in turn requires differentiating through a quantile function when is only monotone in , not continuous. Existence needs integrability of , which is unbounded at both ends, uniformly in , and continuity of by dominated convergence. The natural shortcut, treating the equilibrium as a density solving (3.1), does not prove the theorem: the equilibrium is defined through the control problem, and connecting the two is the content of the milestones.
All declarations live in the namespace TerminalRank.Equilibrium, in one definitions module Model. Conventions:
IsBrownianReal. This is the paper's Wiener space up to relabelling, and also covers its Remark 2.1 (larger filtrations). has type ℝ≥0, and (the paper needs only ).klDiv, valued in . The suprema in (2.3) and (2.6) run over measures with finite entropy; the excluded ones have value in the paper, so nothing changes., optimality and equilibrium are defined from the path-space problem (2.3). A formalization that defines them by (2.6), (2.9) or (3.1), or replaces by a single Gaussian variable, would make the milestones definitional and is ruled out.
Needed infrastructure: Gibbs variational principle (published on the platform as DonskerVaradhan.integral_sub_klDiv_le_log_integral_exp and DonskerVaradhan.klDiv_tilted_self_eq), disintegration and the chain rule for klDiv, Brownian bridges, change of variables for quantile functions, and . The quantile and Brownian-bridge lemmas are reusable well beyond this mission. Contributions toward any milestone, and auxiliary lemmas on these tools, are welcome.
In prediction from experts (PFE), an online learner chooses one of actions in each of rounds, and an adversary assigns each action a loss in . Performance is measured by regret, the learner's total loss minus that of the best single action in hindsight. In many applications changing the action is itself costly: re-routing traffic, re-balancing a portfolio, re-deploying a model. The number of switches, rounds in which the action changes, is then a second resource to keep small.
It has long been known that both quantities can be kept at in expectation. Kalai and Vempala's multiplicative Follow the Perturbed Leader (Kalai–Vempala 2005) and Devroye, Lugosi and Neu's random-walk perturbation (Devroye et al. 2015) both achieve this. Devroye et al. asked for guarantees that hold with high probability. A bound in expectation says little about a single run: the switch count of these algorithms can have heavy upper tails. Altschuler and Talwar (arXiv:1803.01548, COLT 2018; Mathematics of Operations Research 2021) gave the first algorithms whose regret and switches are both with probability . They used this to characterise the optimal regret under a hard switching budget, both for PFE and for multi-armed bandits.
A loss sequence is with . The adversary is oblivious: it fixes the whole sequence before the game, independently of the learner's randomness. A randomized online algorithm draws internal randomness from a probability space . At round it plays an action that is a function of and of the past losses only. This is full-information feedback: after round the whole vector is revealed. Then
Follow the Perturbed Leader (FPL) with perturbations plays at round the minimiser of , with . FPL perturbs only once, with , where are i.i.d. standard exponential.
Framework 1 turns an algorithm into a batched algorithm . runs a copy of with fresh randomness. The copy sees only the losses since its epoch began. The epoch ends just before the copy would exceed switches, and a new copy starts there. is the number of epochs used in rounds. BFPL is Framework 1 applied to FPL with
There is an absolute constant such that for all and some randomized online algorithm satisfies, for every oblivious loss sequence,
The algorithm may depend on , and , as on the page, but not on the losses. The constant is left unspecified, so a sharper constant would not change the goal.
The result separates two notions of "optimal". Expected-value bounds on switching do not control a single run, and the paper shows (Appendix B) that naive restarting does not concentrate. Theorem 1 is the black box behind the paper's later results: the characterisation of minimax regret under a switching budget , with a phase transition at , and the switching-cost corollary obtained by mini-batching. Framework 1 is generic: any algorithm with an expected switching bound of order gains a high-probability one.
The paper result is proved, but none of it has been machine-checked. A formalization yields a verified online-learning protocol with oblivious adversaries, a restart framework with fresh randomness, and verified tail bounds for maxima of exponentials. Formalizing it also repairs four printed slips, listed under Formalization scope.
The obvious approach runs about times in fixed-length blocks and applies Markov's inequality in each. It fails: a single block can use far too many switches with probability that is not small enough. Framework 1 therefore uses epochs of random length, ended by the switch budget. The epoch lengths are then dependent, and the final epoch is truncated at . The concentration argument has to handle both. On the regret side, Lemma 5 is pointwise, but summing it over random epochs and then controlling the sum of perturbation maxima needs a sub-exponential tail bound for maxima of exponentials.
Rounds are 1-based, and losses are with values in . An online algorithm has type : at round it sees only and . The adversary is a deterministic loss sequence, quantified after the algorithm, which is the page's own reduction (p. 5). High-probability statements bound the outer measure of the failure event by . Expectations are lower Lebesgue integrals of natural-valued switch counts. The of Theorems 1 and 8 is an absolute constant chosen before , and . Argmins break ties towards the lowest index. Framework 1 takes randomness under the infinite product measure, one coordinate per epoch.
Three formalizations of the goal would be trivial, and all are excluded. An algorithm that could see or the future would simply play the best action in hindsight. A constant chosen after could be . A loss sequence chosen before the algorithm would let the algorithm depend on it.
The printed slips and how they are handled:
The development needs:
The online-learning layer (protocol, regret, switches, FPL, the restart framework) is reusable for other switching-cost results in the paper and elsewhere. Proofs of any milestone are welcome, as are alternative routes to Theorem 1, such as the random-walk perturbation of §2.5.
The Zero-Core Theorem establishes a fundamental structural property of Ramsey graph colorings: the obstruction preventing extension of the champion R(5,5) coloring from n=43 to n=44 is fully distributed across all constraints, with no individual bottleneck.
This is the first formalization of an essential core theorem in Ramsey theory.
Given an infeasible constraint system S = {c₁, ..., cₘ}, a constraint cᵢ is essential if S \ {cᵢ} is feasible. The essential core 𝓔 ⊆ S is the set of all essential constraints.
Goal: Prove that the essential core of the K₄₄ extension problem is empty (𝓔 = ∅).
The champion K₄₃ coloring (with 137 monochromatic K₅ violations) contains 2,480 monochromatic K₄ subgraphs. The theorem proves that removing any single K₄ constraint from this system leaves it infeasible.
This demonstrates that R(5,5) = 43 is a "deep" combinatorial fact arising from holistic constraint interaction, not from any individual forcing constraint. The distributed nature of the obstruction connects to permutation-invariant energy barriers in optimization landscapes.
The theorem requires:
A nonzero-sum game can have several Nash equilibria with different cost vectors. Selecting one equilibrium before asking how the game behaves over time loses information and may make a proposed dynamic rule depend on that selection. Feinstein, Rudloff and Zhang study the entire set of equilibrium cost vectors and ask whether it can be evaluated consistently after the game is stopped. Their continuous-time result is Theorem 3.9 of the pinned preprint, which the authors identify as the main result of the paper. It follows a discrete-time set-value principle developed earlier in the same work. The question is relevant to stochastic games whose controls use the observed path history and whose players need not share an objective.
Fix a horizon , a positive state dimension , and a positive number of players. The canonical path space is
Its coordinate process is . The measure is Wiener measure, and is the filtration generated by the coordinates through time , augmented by Borel -null events. Each player has a nonempty convex action set . A control profile consists of progressively measurable, -valued processes. A unilateral deviation may be any such process for that player.
The drift depends on the entire profile, while player 's running cost depends on that player's own action. The terminal cost vector is . Assumption 3.1 requires progressive measurability and boundedness of these data. Assumption 3.6 requires uniform continuity in time and path history, and uniform continuity in actions. For a history , concatenation holds the old path through and continues with the increment path afterward. The paper changes measure from with a Girsanov density , then defines the cost as the expected shifted terminal cost plus running cost.
An -equilibrium is a profile whose cost for every player is at most above the cost of every unilateral deviation. Let be the open Euclidean ball of radius around . The set value is the intersection of the relaxed value sets
The open lower envelope is the union of over . These objects are defined even if the game has no exact equilibrium.
The target is Theorem 3.9 in the form (3.12) treated in its proof, at the zero history and initial time. For a stopping time with , let denote the cost of the game stopped at with bounded -measurable terminal vector . The claim is
The seven milestones reproduce Proposition 3.4, the density moment bound (3.6), the cost-continuity estimate (3.4), Theorem 3.7(i), Theorem 3.8, and both parts of Lemma 3.10. They cover compactness, regularity and measurability of the set value, as well as approximation of stopping data and controls.
The equality relates the set of full-horizon equilibrium costs to stopped games whose terminal payoff is approximately compatible with the continuation set value. It gives a dynamic characterization without choosing a particular equilibrium. The relaxation by the same in equilibrium, value ball and exceptional-event probability is part of the result; removing one of those terms changes the game being characterized.
The result is proved in the cited preprint. The mission asks for machine-checked proofs of the stated theorem and its supporting results. The reusable development includes canonical finite-horizon Wiener paths, their augmented filtration, path concatenation, progressive control profiles, a coordinatewise stochastic integral interface, and set-valued equilibrium costs. The published Ethier–Kurtz definition of the Itô-integral relation is reused; it supplies a definition, not a proof of this paper's results.
At a stopping time, the continuation value is a set that depends on the observed path. A pointwise description does not by itself show that membership in this random set is measurable at the stopping time. Equilibrium conditions also compare a profile against every progressively measurable unilateral deviation, so their stability cannot be reduced to a comparison of finitely many actions. The Girsanov density introduces another dependency: its stochastic integral and the resulting costs must be genuine integrable random variables before inequalities between cost vectors have their intended meaning.
Lean represents and by Euclidean spaces, with Euclidean norms on costs and the action product. Paths are continuous maps on constrained to start at zero. The canonical process is clamped outside the horizon only to make its notation total. The Wiener law is pinned by Brownian finite-dimensional distributions through and independence of coordinate processes. The filtration adds Borel null sets, so it remains a sub-σ-algebra of the Borel space. Time-indexed controls live on ; the stopping times themselves use WithTop ℝ and are constrained to that interval.
Concatenation uses the second increment strictly after , resolving the overlapping endpoint in the printed indicator formula. Player 's running cost takes only . The moduli in Assumption 3.6 are common and uniform in the variables specified there. The stopped running cost integrates to , with an empty interval contributing zero only outside the theorem's admissible range. The goal uses bounded measurable representatives of terminal payoffs; changing a representative on a null set leaves the expected costs and exceptional probability unchanged.
The statement must retain the full Girsanov density, all progressive deviations, the open envelope , and a nonzero player count. A default-zero integral for a nonintegrable payoff, an arbitrary measure in place of Wiener measure, or a restricted deviation class would trivialize or alter it. Solvers can contribute the integrability and stochastic-integral existence facts needed to establish that the definitions have their intended values, followed by proofs of the listed milestones and goal.
A controller of a large population may choose a separate action for each participant while all participants experience the same random environment. The resulting optimization problem has a growing state space: with participants, the state records paths and controls. A McKean–Vlasov control problem replaces the empirical distribution of those participants by a conditional distribution given the common noise. Djete, Possamaï and Tan prove that this replacement preserves the optimal value asymptotically, even when the participants have different initial laws and the average of those laws does not converge along the full sequence. Their result is Theorem 3.6(iii) of the 2020 preprint, published in 2022.
The distinction between common and individual noise matters for this claim. Conditional on the common noise, particles can still be correlated through a controller that observes the full particle system. The paper's limit theorem concerns the supremum over all admissible predictable particle controls, rather than one prescribed feedback rule. This is the setting in which a finite population optimization problem can approximate its limiting stochastic control problem. The adjacent Proposition 3.7 describes how the limiting value changes with the initial law.
Fix a time horizon , state dimension , individual noise dimension , and common noise dimension . Let be a nonempty Polish control space with base point . A state or noise path belongs to , with its uniform norm. The coefficients determine the drift, individual diffusion and common diffusion; and determine running and terminal rewards. The Wasserstein distance measures the discrepancy between probability laws with finite th moments.
For an initial law , the strong problem lives on the canonical space . Its initial state has law , and are independent Brownian noises relative to the canonical past. An admissible control is predictable and has finite expected integrated th power of its distance from . The state solves the controlled equation (2.3). Its coefficients use the conditional law of the stopped state path and current control given the history of ; its terminal reward uses the conditional law of the stopped state path. The strong value , equation (2.4), is the supremum of expected reward over those controls and their solutions. These definitions appear in Section 2.1.
For , the particle problem has initial laws , separate Brownian noises , and one shared . Each particle follows equation (2.16) with the empirical state-control law inside its coefficients. The terminal reward uses the empirical state-path law . Equation (2.17) defines as the supremum of the average expected reward. The empirical laws are built from the very particles whose equations use them; they are not outside inputs. See Section 2.4.
The goal is the value comparison in Theorem 3.6(iii), equation (3.3):
The hypotheses include Assumptions 2.1 and 2.12, an embedding for some , continuity of and , and a uniform bound on the averages of the initial th moments, where . The goal does not assume that the averaged initial laws converge. The milestones are the value lower bounds of Propositions 4.15 and 4.16, the subsequence value limit used in equation (4.44), and the initial-law stability statement (3.4) of Proposition 3.7. Each milestone records the particular clause formalized when its printed result contains additional conclusions. Theorem 3.6 and its proof give the source order.
The theorem compares two optimization problems, rather than only the law of a fixed controlled particle system. The comparison permits heterogeneous initial distributions and keeps the common noise in both models. Proposition 3.7 gives a separate stability statement for the limiting value when initial laws converge in with uniformly bounded th moments. Together these statements identify which finite population values are represented by the limiting control formulation. They are proved in the paper; the open task here is a machine checked derivation from faithful statements.
The formal development fixes the interfaces for conditional laws, predictable controls, path dependent coefficients, Brownian Itô integrals, empirical probability laws and extended real rewards. Those interfaces can support later formalizations of common-noise control and propagation of chaos. The present mission does not state Theorem 3.1(i), the approximation clauses of Theorem 3.1(ii)–(iii), Theorem 3.6(ii), or the “In particular” sentence after Proposition 3.7's equation (3.4). Their different conclusions require further canonical and relaxed-control structures, and the last sentence has a topology ambiguity documented in the paper notes.
The usual fixed-control convergence question is smaller than the target: particle controls may depend on every observed particle and on the common noise, and the target takes a supremum before comparing values. The conditional law in the limiting equation depends on its own solution, while the empirical law in each particle equation depends on the full coupled particle system. Dropping either dependence changes the optimization problem. Uniform th moment control must also coexist with unbounded rewards and the extended real convention for their expectations. The source proof invokes compactness and equivalence between strong, weak and relaxed formulations; formalizing those links is substantial work beyond compiling the goal statement.
Lean uses EuclideanSpace and continuous maps on for the path spaces, and Frobenius norms for diffusion matrices. The control type carries a Polish Borel metric and a base point. is a finite-lintegral moment condition, and takes values in . Values are extended real suprema over admissible controls and actual solutions. Rewards use the paper's convention , rather than a default zero integral. Particle counts are positive; Lean player index zero denotes the paper's player one. The case remains included.
Assumption 2.1 includes the displayed Lipschitz, growth and coercive bounds, Borel measurability, nonanticipativity, and lower semicontinuity. Assumption 2.12 factors the coefficients through the state marginal, with independent of the control. The paper leaves the topology behind “continuous” unnamed; the formalization uses sequential continuity on finite-moment laws. Its is read as an isometric embedding. Solutions have continuous paths and are adapted to the completed canonical filtration, while conditional laws use the raw common-noise filtration. The goal states finiteness of both values so its real absolute difference is defined. Equation (4.44) is posed in the subsequence form used by its proof. These choices and the source's printed slips are detailed in the moderation notes.
The interface rules out a free conditional-law flow, a free particle empirical measure, and an uncharacterized Brownian law. The weak and relaxed formulations appear only as context for the paper's proof; this proposal contains the strong and particle layers needed by the four selected milestones. Contributions to the omitted equivalence and compactness results are welcome once their canonical-space definitions have been audited.
Off-policy evaluation (OPE) asks for the long-run value of a target decision policy, using only data collected under a different policy. It arises wherever running the target policy is expensive or unsafe: a new treatment rule in medicine, a new recommendation or pricing rule, a candidate controller in reinforcement learning. Importance-sampling estimators reweight whole trajectories. Their variance grows exponentially with the horizon, the curse of horizon (Liu et al. 2018, arXiv:1810.12429).
Kallus and Uehara (arXiv:1909.05850, Operations Research 2022) treat infinite-horizon discounted OPE as a semiparametric estimation problem. They derive the efficiency bound under three models: non-Markov, time-varying Markov and time-invariant Markov (MDP). They then propose double reinforcement learning (DRL), an estimator that combines a q-function estimate with an estimate of the ratio between the discounted state visitation of the target policy and the state distribution of the data. In the MDP model it attains the efficiency bound. This mission formalizes the transition-sampling version of that result, Theorem 6.
Timeline:
States lie in a measurable space and actions in a measurable space . A time-invariant MDP is a transition kernel and a reward kernel with rewards in . A policy is a kernel from to . Fix a discount , a known target policy with known initial law , and a behavior policy .
The estimand is the normalized discounted value
The q-function is , and . The discounted visitation is , where is the law of .
Transition sampling. The data are i.i.d. observations with law : , , and, given , independently and . The law of may differ from that of .
The density ratios are and . For candidate nuisances , with , the estimating function is
The cross-fitted estimator splits the sample into two folds. It fits on fold and averages over all observations, each evaluated at the nuisances of the other fold. The efficient influence function is , and the efficiency bound is .
Assume the following:
Then
No rate exponent or learner class is fixed. Only the product rate enters.
Theorem 6 shows that, in a Markov model, a -consistent and efficient OPE estimator exists whose variance scales with the number of observed transitions, not trajectories. It requires no complexity (Donsker or entropy) restriction on the nuisance estimators, only a product rate. Any black-box learners with , which allows two subparametric rates, give asymptotically valid confidence intervals at the efficiency bound. The mixed-bias identities (Eqs. (5)–(8)) and Lemma 1 are the same ingredients used by later minimax and adversarial estimators of and .
The result is proved in the paper; nothing here is presented as open. As far as is known, none of it has a machine-checked proof: no off-policy evaluation, density-ratio characterization or cross-fitting asymptotics exists in Mathlib or on the platform. Formalizing it checks the appendix argument, which is short and contains errors (below). It also produces a reusable layer: kernel-based discounted MDPs on general measurable spaces, discounted visitation measures, and the cross-fitting plus Slutsky template that other double-machine-learning results share.
The obvious route is "the estimator equals the oracle average plus negligible terms, then apply the CLT". Two of its steps are not routine.
First, the negligible terms are random functions evaluated at random data. The empirical-process term (28) is controlled only conditionally on the other fold, through a conditional Chebyshev argument that needs the independence structure of the split. Treating as fixed functions loses exactly this.
Second, the bias term (30) is second order only because of the mixed-bias structure. That structure rests on Lemma 1, a change-of-measure identity between the discounted visitation of and the data distribution. The printed constants are wrong. The Jensen step fails when is large: with one state, uniform on two actions and a point mass, the left side is and the right side is . The bound by is not a valid inequality for a triple product. Both need a bound , which the mission adds.
Kernel.rnDeriv). The MDP, the policies and the observation law are Mathlib kernels and measures. The paper's base measures are not used.toReal of Radon–Nikodym derivatives, not free functions satisfying an identity. Overlap (, ) is a standing assumption.TendstoInDistribution with TendstoInMeasure) and Mathlib's i.i.d. CLT tendstoInDistribution_inv_sqrt_mul_sum_sub. The occupancy and Lemma 1 layer and the cross-fitting template are reusable beyond this mission. Proofs of any milestone, and helper lemmas on kernel powers and discounted sums, are welcome.Mean-variance analysis (Markowitz, 1952) tells an investor which portfolio to hold once the mean vector and covariance matrix of asset returns are known. In practice both are estimated from a finite window of past returns, and the portfolio built from the estimates (the plug-in portfolio) performs badly out of sample: its weights are noisy and its realized utility is often far below the theoretical optimum. A long literature asks how to choose portfolio rules that take this estimation risk into account; Kan and Zhou (2007) treat the case with a risk-free asset.
Kan, Wang and Zhou (2022) study the case without a risk-free asset, where the investor must be fully invested in risky assets. There the optimal portfolio splits into the global minimum-variance (GMV) portfolio plus a scaled zero-investment portfolio, and estimation errors enter the two parts very differently. Their §2 derives the exact expected out-of-sample utility of the family of rules that rescale the estimated zero-investment part, and the coefficient that maximizes it. This mission formalizes that derivation.
An investor chooses weights with to maximize the mean-variance utility
where is the risk-aversion coefficient and is positive definite. The population quantities that matter are the GMV variance , the GMV mean , and the squared slope of the asymptote of the minimum-variance frontier, .
The returns of an estimation window of length are independent and identically distributed . The maximum-likelihood estimators are and . From them come the sample GMV portfolio and the sample zero-investment portfolio
with . For a constant combining coefficient the paper considers
is the plug-in rule. The expected out-of-sample utility evaluates at the true , and averages over the sample. The five random quantities , , , and determine it.
For and , with
the coefficient is the unique maximizer of over , and , with when .
For and every constant ,
together with the first and second moments of the auxiliary variables , of Proposition 1 that the proof of Lemma 1 uses.
The result gives a closed-form, implementable-in-principle correction to the plug-in rule: since , the investor should always under-weight the estimated zero-investment portfolio, by a factor that depends only on , and . Replacing by an adjusted estimator gives the paper's feasible rules (§2.4, §3), which are compared empirically in §4. The moment formulas (A9)–(A13) are of independent use: they give the exact out-of-sample mean and variance of the sample GMV and zero-investment portfolios, which recur in the shrinkage literature (for instance Lassance, Martín-Utrera and Simaan, 2024, who build on this paper's Proposition 1).
The result is proved in the paper, but the proof rests on Proposition 1, a stochastic representation of the out-of-sample moments whose detailed proof is in an online appendix. No machine-checked proof exists. On Prove2Me, Proposition 1 is posed (Open) as RiskEU.OOSUVar.kan_representation in Lassance et al.'s restatement, together with special cases (eq_IA60, eq_IA49) of the combinations and of the portfolio variance for and . The closed-form vertex of the quadratic (17) is already proved there (RiskEU.RobustShrink.proposition_IA_1_3). What this mission adds is the statement about the actual expectation over the Gaussian sample, for all real , under the paper's own threshold , with uniqueness of the maximizer.
Once Lemma 1 is available, the goal is the vertex of a concave quadratic. The difficulty is Lemma 1 itself: computing expectations of quadratic forms in and in the normalized vector . The weights are ratios of dependent random quantities, so linearity of expectation does not apply directly, and inverse-Wishart moment formulas alone do not cover the ratio in . The threshold is Lemma 1's hypothesis; the factor in the denominator of (A12) shows that it is what keeps the expected variance of the estimated zero-investment portfolio finite, so integrability is part of the content.
The model is the published definition RiskEU.OOSUVar.Setting: Market N carries , , ; sigmaG2, muG, psi2, U, sampleMean, sampleCov (divided by ), wHatG, wHatZ and IsGaussianSample are the objects above (that setting calls the window ; here it is ). The auxiliary family of Proposition 1 and , come from the published RiskEU.OOSUVar.KanRepresentation. The mission's own definitions (KanCombine.Optimal.Model) add the standing assumptions, the combining portfolio, the five sample moments, the expected utility, and .
Conventions committed to:
The goal is about the integral over the Gaussian sample. Stating it about the closed-form right-hand side of (17) would reduce it to the vertex of a quadratic, which is already proved, and is ruled out. The hypotheses are satisfiable: , , , , meets them with the product Gaussian sample, and gives .
A complete development needs Wishart and inverse-Wishart theory (the Bartlett decomposition, moments of chi-squared ratios) and a formal version of Proposition 1. These are reusable well beyond this mission; contributions proving (A9)–(A13) by any route, including directly from inverse-Wishart moments, are welcome.
A provable quantum advantage for approximate optimization via decoded quantum interferometry establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a rational rate . An admissible block count satisfies for an integer , and , where , and . Work over the publicly represented characteristic-two field , with a fixed public primitive element . Put and . A promised instance consists of arbitrary sets with , accessed only through separately callable fixed-block XOR membership oracles. Each call chooses its block classically and may query a superposition of whole symbols.
A coefficient vector represents the polynomial , including the zero polynomial. Its score is
Define
The construction uses the conventional unfolded scalar GRS dual syndrome decoder at cutoff , strictly below half its scalar minimum distance, the explicit top-window layer weights, and synthesis accuracy . Its polynomial resource bounds and classical circuit constructor are independent of the acceptance sets.
The probability is over the same sampled acceptance sets and independent algorithm randomness. Computation between queries and arbitrary finite advice are unrestricted, provided the description and advice are fixed before sampling.
This result separates the approximation scores attainable through the same whole-symbol membership interface. The quantum assertion is an expectation guarantee for every promised oracle; the classical assertions are distributional.
Formalization Note A fixed effective polynomial-basis binary field representation and uniform compilation over make the implicit public representation and polynomial runtime concrete. The DQI state, its coefficient output wires and its query count are tied to one circuit. The sampled probabilities are finite uniform averages of normalized classical output laws.
Fix a rational rate . An admissible block count satisfies for an integer , and , where , and . Work over the publicly represented characteristic-two field , with a fixed public primitive element . Put and . A promised instance consists of arbitrary sets with , accessed only through separately callable fixed-block XOR membership oracles. Each call chooses its block classically and may query a superposition of whole symbols.
A coefficient vector represents the polynomial , including the zero polynomial. Its score is
Define
The construction uses the conventional unfolded scalar GRS dual syndrome decoder at cutoff , strictly below half its scalar minimum distance, the explicit top-window layer weights, and synthesis accuracy . Its polynomial resource bounds and classical circuit constructor are independent of the acceptance sets.
The probability is over the same sampled acceptance sets and independent algorithm randomness. Computation between queries and arbitrary finite advice are unrestricted, provided the description and advice are fixed before sampling.
This result separates the approximation scores attainable through the same whole-symbol membership interface. The quantum assertion is an expectation guarantee for every promised oracle; the classical assertions are distributional.
Formalization Note A fixed effective polynomial-basis binary field representation and uniform compilation over make the implicit public representation and polynomial runtime concrete. The DQI state, its coefficient output wires and its query count are tied to one circuit. The sampled probabilities are finite uniform averages of normalized classical output laws.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
An Optimal Quantum Linear Systems Algorithm establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Consider the quantum linear systems problem for an invertible, complex, -sparse matrix , with , , and , where these are operator norms and is known. For a nonzero vector , a supplied preparation circuit prepares . The solver must output a success flag of probability at least and, conditioned on success, a normalized reduced density matrix within trace distance of , where . Both and have reversible row-location and XOR entry-value oracles; the locations listed in each row are distinct, cover all nonzeros, and may include zeros. Only matrix-oracle calls count, including inverse and controlled calls. Supplied preparation operations and known quantum operations are free.
Let be the supremum over positive dimensions and public finite exact entry encodings of the least natural worst-case matrix-query budget of a solver correct for every compatible promised input and oracle completion. Solvers are chosen before the hidden matrix, vector, and oracle completions. Empty sets of feasible budgets and unbounded suprema retain . There exist absolute constants , , , and such that, for every , , and ,
This gives matching upper and worst-case lower bounds jointly in sparsity, inverse-norm bound, and precision. The constants and thresholds are independent of dimension, encoding, and input.
Formalization Note Complexity is represented in using the frozen OptimalQLSP.queryComplexity. General matrices and general positive dimensions are retained; the Hermitian reduction and power-of-two registers used inside the proof do not restrict the headline.
Consider the quantum linear systems problem for an invertible, complex, -sparse matrix , with , , and , where these are operator norms and is known. For a nonzero vector , a supplied preparation circuit prepares . The solver must output a success flag of probability at least and, conditioned on success, a normalized reduced density matrix within trace distance of , where . Both and have reversible row-location and XOR entry-value oracles; the locations listed in each row are distinct, cover all nonzeros, and may include zeros. Only matrix-oracle calls count, including inverse and controlled calls. Supplied preparation operations and known quantum operations are free.
Let be the supremum over positive dimensions and public finite exact entry encodings of the least natural worst-case matrix-query budget of a solver correct for every compatible promised input and oracle completion. Solvers are chosen before the hidden matrix, vector, and oracle completions. Empty sets of feasible budgets and unbounded suprema retain . There exist absolute constants , , , and such that, for every , , and ,
This gives matching upper and worst-case lower bounds jointly in sparsity, inverse-norm bound, and precision. The constants and thresholds are independent of dimension, encoding, and input.
Formalization Note Complexity is represented in using the frozen OptimalQLSP.queryComplexity. General matrices and general positive dimensions are retained; the Hermitian reduction and power-of-two registers used inside the proof do not restrict the headline.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Sample-optimal learning of stabilizer states establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be the number of qubits and let be the allowed failure probability. An unknown normalized pure stabilizer state is provided as identical copies. Let be the least number of copies with which one quantum procedure can identify every such state with probability at least . The minimum permits arbitrary collective measurements, ancillas, internal randomness and adaptivity. Identification means outputting a valid tableau of independent signed Pauli generators whose common eigenspace is the input state; global phase and the choice of generators are irrelevant. Then
Furthermore, for every such and , there is a quantum learner receiving at most copies and retaining them through adaptive operations, which identifies every input stabilizer state with failure probability at most . There are absolute constants and , independent of , and the input state, such that this learner has computational time
Time counts elementary quantum gates, measurements, fair coins and Boolean operations, including classical and reversible arithmetic, finite-precision rotation synthesis and tableau reconstruction. The sample and success bounds have no asymptotic threshold. This determines the leading sample coefficient to be one and attains the bound with an efficient learner.
Formalization Note The minimum is represented in , with an empty feasible set assigned ; the upper bound implies finiteness. The lower inequality is written as to avoid natural subtraction. The theorem's printed statement leaves the qubit domain implicit; follows the lower-bound proof on PDF p.7, since the zero-qubit state requires zero copies.
Let be the number of qubits and let be the allowed failure probability. An unknown normalized pure stabilizer state is provided as identical copies. Let be the least number of copies with which one quantum procedure can identify every such state with probability at least . The minimum permits arbitrary collective measurements, ancillas, internal randomness and adaptivity. Identification means outputting a valid tableau of independent signed Pauli generators whose common eigenspace is the input state; global phase and the choice of generators are irrelevant. Then
Furthermore, for every such and , there is a quantum learner receiving at most copies and retaining them through adaptive operations, which identifies every input stabilizer state with failure probability at most . There are absolute constants and , independent of , and the input state, such that this learner has computational time
Time counts elementary quantum gates, measurements, fair coins and Boolean operations, including classical and reversible arithmetic, finite-precision rotation synthesis and tableau reconstruction. The sample and success bounds have no asymptotic threshold. This determines the leading sample coefficient to be one and attains the bound with an efficient learner.
Formalization Note The minimum is represented in , with an empty feasible set assigned ; the upper bound implies finiteness. The lower inequality is written as to avoid natural subtraction. The theorem's printed statement leaves the qubit domain implicit; follows the lower-bound proof on PDF p.7, since the zero-qubit state requires zero copies.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Efficient Exact Quantum Sampling from the Sun-Wootters Distribution for Optimal Polynomial Intersection establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be prime, , and let be distinct public evaluation points. Every hidden set has the same known cardinality , with . Put , for , and . A coefficient vector represents the polynomial ; its satisfaction ratio is . Access is through the indexed XOR oracle , with arbitrary full unitary behavior on invalid encodings.
For an integer cutoff , set , , and . Define , , and . On its positive-denominator domain the Sun–Wootters law is
Write , , , and . Suppose and the target denominator is positive. For every complete duplicate-free canonical shell list, padded to the same slots for every syndrome, the ideal attempt prepares , reversibly indexes and erases the error, applies to the index, and postselects using a match flag. It then applies the positive-character Fourier transform on the syndrome. Its success and conditional law satisfy
This finite identity preserves cancellation within fibers and asserts no running-time bound for an arbitrary unpriced list. For normalized ideal and implemented full-register states, ideal success at least , vector error at most , and final Fourier operator error at most , implemented success is at least and conditional total variation error is at most .
Now consider public parameter families with , , and . Constants, programs and preprocessing are uniform over all sets of the promised cardinality and every supplied membership oracle. Let , using natural logarithms and , and define
All denominators in these ratios must be nonzero and all entropy arguments must belong to . Fix , a positive rational , and in that domain with and . Put . Eventually the target is well defined, complete canonical lists admit one polynomial common padding length, and ideal success is at least . For every , a uniform quantum algorithm with time polynomial in satisfies
For every fixed default vector, the defaulted law has total variation distance at most from and expected score at least , for some nonnegative independent of the hidden sets; here on . Preprocessing, synthesized gates, queries, measurements, reversible/classical work, and capped restarts are counted.
The two balanced consequences are retained:
These conclusions turn the Sun–Wootters distributional improvement into efficient worst-case quantum optimization.
Formalization Note Theorem 7.1's printed “For each family member” is clarified to an eventual guarantee, matching its proof's positivity and decoder-feasibility bounds. This is an explicit proof-based scope clarification awaiting independent moderation. The finite exact identity is separate from the approximate universal-gate implementation. The paper's operator called inverse QFT has positive character and equals the frozen positive-sign QFT convention.
Correction to the printed source.
Printed: For each family member put ... and define Pu,m by equations (11) to (13) with largest active weight ell_m. Then ... there is a uniform bounded-error quantum algorithm.
Corrected: The finite target is defined on its positive-denominator and cutoff-at-least-three domain, and the sampling guarantees hold for every sufficiently large public parameter-family member.
Reason: Theorem 7.1 itself invokes the finite Johnson inequality and postselection estimate only for all sufficiently large m. Lemmas 3.2 and 6.4 are eventual, while equation (11) uses log log ell; early undefined targets cannot be normalized by total division.
Let be prime, , and let be distinct public evaluation points. Every hidden set has the same known cardinality , with . Put , for , and . A coefficient vector represents the polynomial ; its satisfaction ratio is . Access is through the indexed XOR oracle , with arbitrary full unitary behavior on invalid encodings.
For an integer cutoff , set , , and . Define , , and . On its positive-denominator domain the Sun–Wootters law is
Write , , , and . Suppose and the target denominator is positive. For every complete duplicate-free canonical shell list, padded to the same slots for every syndrome, the ideal attempt prepares , reversibly indexes and erases the error, applies to the index, and postselects using a match flag. It then applies the positive-character Fourier transform on the syndrome. Its success and conditional law satisfy
This finite identity preserves cancellation within fibers and asserts no running-time bound for an arbitrary unpriced list. For normalized ideal and implemented full-register states, ideal success at least , vector error at most , and final Fourier operator error at most , implemented success is at least and conditional total variation error is at most .
Now consider public parameter families with , , and . Constants, programs and preprocessing are uniform over all sets of the promised cardinality and every supplied membership oracle. Let , using natural logarithms and , and define
All denominators in these ratios must be nonzero and all entropy arguments must belong to . Fix , a positive rational , and in that domain with and . Put . Eventually the target is well defined, complete canonical lists admit one polynomial common padding length, and ideal success is at least . For every , a uniform quantum algorithm with time polynomial in satisfies
For every fixed default vector, the defaulted law has total variation distance at most from and expected score at least , for some nonnegative independent of the hidden sets; here on . Preprocessing, synthesized gates, queries, measurements, reversible/classical work, and capped restarts are counted.
The two balanced consequences are retained:
These conclusions turn the Sun–Wootters distributional improvement into efficient worst-case quantum optimization.
Formalization Note Theorem 7.1's printed “For each family member” is clarified to an eventual guarantee, matching its proof's positivity and decoder-feasibility bounds. This is an explicit proof-based scope clarification awaiting independent moderation. The finite exact identity is separate from the approximate universal-gate implementation. The paper's operator called inverse QFT has positive character and equals the frozen positive-sign QFT convention.
Correction to the printed source.
Printed: For each family member put ... and define Pu,m by equations (11) to (13) with largest active weight ell_m. Then ... there is a uniform bounded-error quantum algorithm.
Corrected: The finite target is defined on its positive-denominator and cutoff-at-least-three domain, and the sampling guarantees hold for every sufficiently large public parameter-family member.
Reason: Theorem 7.1 itself invokes the finite Johnson inequality and postselection estimate only for all sufficiently large m. Lemmas 3.2 and 6.4 are eventual, while equation (11) uses log log ell; early undefined targets cannot be normalized by total division.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Worst-Case Quantum Algorithm for Optimal Polynomial Intersection Beyond Decoded Quantum Interferometry establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Consider a growing public parameter family , where is prime, , , , and . Put . Assume eventually for fixed and . Each has its standard effective polynomial-basis binary representation, specified by its characteristic, extension degree and irreducible modulus. Fix a target and assume one of these two eventual regimes, with a common fixed margin :
Here , with .
Let tend to zero. There exist a uniform quantum oracle solver, a polynomial and an index such that, for every , every tuple of distinct evaluation points , and every hidden subset family satisfying
the solver outputs a polynomial for which
Its classical constructor receives only the public field description, , the evaluation points and the integer target . The sets are accessed through their individual quantum XOR membership oracles. Work counts queries, standard Clifford+T gates, measurements, preparations, classical control, workspace and coefficient decoding; constructor time and space are polynomial in . The constants and threshold are uniform over evaluation points and hidden sets, and probability refers to internal coins and measurements.
This gives an algorithm on every promised instance, including exact perfect satisfaction in the first branch. No random-instance assumption, efficient-decoder hypothesis, or pre-existing-solution hypothesis is imposed.
Formalization Note The asymptotic reading makes the bound and high-rate constant margin explicit using Theorem 6.1 and Remark 6.2. The printed informal high-rate sentence omits them. Unequal densities are retained under footnote 3. Rates tending to one and are retained through constructive dimension reduction. These bridges require independent mathematical moderation.
Consider a growing public parameter family , where is prime, , , , and . Put . Assume eventually for fixed and . Each has its standard effective polynomial-basis binary representation, specified by its characteristic, extension degree and irreducible modulus. Fix a target and assume one of these two eventual regimes, with a common fixed margin :
Here , with .
Let tend to zero. There exist a uniform quantum oracle solver, a polynomial and an index such that, for every , every tuple of distinct evaluation points , and every hidden subset family satisfying
the solver outputs a polynomial for which
Its classical constructor receives only the public field description, , the evaluation points and the integer target . The sets are accessed through their individual quantum XOR membership oracles. Work counts queries, standard Clifford+T gates, measurements, preparations, classical control, workspace and coefficient decoding; constructor time and space are polynomial in . The constants and threshold are uniform over evaluation points and hidden sets, and probability refers to internal coins and measurements.
This gives an algorithm on every promised instance, including exact perfect satisfaction in the first branch. No random-instance assumption, efficient-decoder hypothesis, or pre-existing-solution hypothesis is imposed.
Formalization Note The asymptotic reading makes the bound and high-rate constant margin explicit using Theorem 6.1 and Remark 6.2. The printed informal high-rate sentence omits them. Unequal densities are retained under footnote 3. Rates tending to one and are retained through constructive dimension reduction. These bridges require independent mathematical moderation.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Hamiltonian Decoded Quantum Interferometry for General Pauli Hamiltonians establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let and be integers. Let be a classically known Hamiltonian on qubits, where and the are distinct canonical Hermitian Pauli operators that commute pairwise. Let be a real polynomial of degree exactly , and assume . Write for the matrix whose columns are the symplectic labels of the , with the coordinates preceding the coordinates. Assume there exists a unitary decoder on the -qubit label register and the -qubit syndrome register satisfying
Here is Hamming weight and is the zero-string reference coefficient defined below. The zero-branch guarantee is required only when ; when , that decoder input is unrestricted. All other decoder inputs are unrestricted.
There is an exact quantum preparation circuit, chosen from the known Hamiltonian and polynomial before choosing the decoder, that works for every decoder with these guarantees and prepares
It starts with zeroed registers, uses exactly one plain forward application of , and uses no adjoint or controlled decoder calls. The output is the reduced density matrix after discarding the other registers, with no postselection or success-probability qualification.
For clarity, define the real reference coefficients and their normalization by
The reference is constructed by the algorithm, rather than supplied as input. In particular,
where ; both and have unit norm.
The circuit includes a concrete classical arithmetic program that computes and all boundary and local-matrix entries of the reference MPS from the coefficients alone. It may introduce only the numeric constants , and the entries of its quantum gates are obtained from that program's results. There exist an absolute , a polynomial with nonnegative integer coefficients, and thresholds and , all independent of sizes, Pauli terms, coefficients, and decoder, such that
Here classical cost counts actual arithmetic and memory instructions, and quantum cost counts the circuit's gate and oracle steps plus initialization of its qubits. This is the paper's ideal model with unit-cost real arithmetic and exact arbitrary one- and two-qubit unitary gates.
This result supplies an exact polynomial-filtered density matrix using a perfect decoder even for general real commuting Pauli coefficients, without assuming the reference state has already been prepared.
Formalization Note. The proof's convention replaces the theorem display's . Real polynomial coefficients, the nonzero condition, and the decoder's zero-branch guarantee for an occupied reference branch are explicit corrections needed for normalization and coherence. The conditional zero-branch guarantee strengthens literal Eq. (7) only when and is not inferred from it. Pauli-product phases are retained through the Bell basis change and its inverse. The ordinary positive- regime is explicit; nonzero constant polynomials are included, and asymptotic bounds are applied only above their stated thresholds.
Correction to the printed source.
Printed: Theorem 5 displays j=1,...,l, does not explicitly type a_j or exclude P(H)=0, and refers to Eq.(7), which specifies decoder action only for 1<=|y|<=l. The proof suppresses Pauli-product phases in its Bell-basis display.
Corrected: Use the proof convention j=0,...,l with real polynomial coefficients; require P(H)!=0; retain Eq.(7) and require D|0,0>=|0,0> only if the Eq.(10) coefficient w_0 is nonzero. Preserve product phases under the coherent Bell transform and its inverse.
Reason: The proof and MPS boundaries include a_0. Real coefficients and P(H)!=0 make P(H)^2/Tr[P(H)^2] a density matrix. Eq.(7) leaves an occupied zero branch uncontrolled; fixing only that occupied branch restores coherent erasure without excluding H=I,P=x, whose w_0 vanishes and whose positive-weight decoder necessarily moves |0,0>. A linear Bell transform must preserve Pauli-product signs.
Let and be integers. Let be a classically known Hamiltonian on qubits, where and the are distinct canonical Hermitian Pauli operators that commute pairwise. Let be a real polynomial of degree exactly , and assume . Write for the matrix whose columns are the symplectic labels of the , with the coordinates preceding the coordinates. Assume there exists a unitary decoder on the -qubit label register and the -qubit syndrome register satisfying
Here is Hamming weight and is the zero-string reference coefficient defined below. The zero-branch guarantee is required only when ; when , that decoder input is unrestricted. All other decoder inputs are unrestricted.
There is an exact quantum preparation circuit, chosen from the known Hamiltonian and polynomial before choosing the decoder, that works for every decoder with these guarantees and prepares
It starts with zeroed registers, uses exactly one plain forward application of , and uses no adjoint or controlled decoder calls. The output is the reduced density matrix after discarding the other registers, with no postselection or success-probability qualification.
For clarity, define the real reference coefficients and their normalization by
The reference is constructed by the algorithm, rather than supplied as input. In particular,
where ; both and have unit norm.
The circuit includes a concrete classical arithmetic program that computes and all boundary and local-matrix entries of the reference MPS from the coefficients alone. It may introduce only the numeric constants , and the entries of its quantum gates are obtained from that program's results. There exist an absolute , a polynomial with nonnegative integer coefficients, and thresholds and , all independent of sizes, Pauli terms, coefficients, and decoder, such that
Here classical cost counts actual arithmetic and memory instructions, and quantum cost counts the circuit's gate and oracle steps plus initialization of its qubits. This is the paper's ideal model with unit-cost real arithmetic and exact arbitrary one- and two-qubit unitary gates.
This result supplies an exact polynomial-filtered density matrix using a perfect decoder even for general real commuting Pauli coefficients, without assuming the reference state has already been prepared.
Formalization Note. The proof's convention replaces the theorem display's . Real polynomial coefficients, the nonzero condition, and the decoder's zero-branch guarantee for an occupied reference branch are explicit corrections needed for normalization and coherence. The conditional zero-branch guarantee strengthens literal Eq. (7) only when and is not inferred from it. Pauli-product phases are retained through the Bell basis change and its inverse. The ordinary positive- regime is explicit; nonzero constant polynomials are included, and asymptotic bounds are applied only above their stated thresholds.
Correction to the printed source.
Printed: Theorem 5 displays j=1,...,l, does not explicitly type a_j or exclude P(H)=0, and refers to Eq.(7), which specifies decoder action only for 1<=|y|<=l. The proof suppresses Pauli-product phases in its Bell-basis display.
Corrected: Use the proof convention j=0,...,l with real polynomial coefficients; require P(H)!=0; retain Eq.(7) and require D|0,0>=|0,0> only if the Eq.(10) coefficient w_0 is nonzero. Preserve product phases under the coherent Bell transform and its inverse.
Reason: The proof and MPS boundaries include a_0. Real coefficients and P(H)!=0 make P(H)^2/Tr[P(H)^2] a density matrix. Eq.(7) leaves an occupied zero branch uncontrolled; fixing only that occupied branch restores coherent erasure without excluding H=I,P=x, whose w_0 vanishes and whose positive-weight decoder necessarily moves |0,0>. A linear Bell transform must preserve Pauli-product signs.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Multivariate Decoded Quantum Interferometry for Weighted Optimization establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be prime and . Let with , and let have cardinality . Define on and otherwise. Partition into nonempty blocks , write , and assign positive weights . Put and , where is row of and .
Fix an exact degree ratio , with integer , and assume , where is the minimum nonzero Hamming weight in (infinite when this kernel is zero). Let be the supremum of over complex multivariate polynomials of total degree at most such that has unit norm. This supremum is attained by an admissible polynomial.
Write , , , and define
For each fixed , there are and an integer , chosen before all other instance data and , such that every admissible instance with satisfies
Along any admissible family with fixed , unbounded , and eventually bounded , the residual tends to zero. No convergence of block proportions is required.
This characterizes the asymptotically optimal signed weighted objective among multivariate DQI states. It does not impose decoder access or a preparation complexity bound.
Formalization Note The range is explicitly recalled by Appendix A (PDF p.30) and is carried as a standing assumption although omitted from the printed theorem sentence. Exact integer pairs are used; no rounding convention is added.
Let be prime and . Let with , and let have cardinality . Define on and otherwise. Partition into nonempty blocks , write , and assign positive weights . Put and , where is row of and .
Fix an exact degree ratio , with integer , and assume , where is the minimum nonzero Hamming weight in (infinite when this kernel is zero). Let be the supremum of over complex multivariate polynomials of total degree at most such that has unit norm. This supremum is attained by an admissible polynomial.
Write , , , and define
For each fixed , there are and an integer , chosen before all other instance data and , such that every admissible instance with satisfies
Along any admissible family with fixed , unbounded , and eventually bounded , the residual tends to zero. No convergence of block proportions is required.
This characterizes the asymptotically optimal signed weighted objective among multivariate DQI states. It does not impose decoder access or a preparation complexity bound.
Formalization Note The range is explicitly recalled by Appendix A (PDF p.30) and is carried as a standing assumption although omitted from the printed theorem sentence. Exact integer pairs are used; no rounding convention is added.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Randomized and quantum approximate matrix multiplication establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a classical exact-arithmetic matrix multiplication implementation with achievable exponent . Let , , and let be arbitrary matrices. Write , where . Given absolute accuracy and failure probability , there are fixed input-taking classical and quantum circuit families, with classical preprocessing time , which return classical matrices and satisfying
Apart from input/output and preprocessing overhead, their running times are respectively
The soft factors include the confidence logarithms and are uniform over dimensions, factors, matrix entries, accuracy, and confidence; constants may depend on the chosen multiplication implementation. Real numbers are represented exactly, and fixed-position retrieval and arithmetic are charged in both models. The quantum output is an ordinary classical matrix. No efficiently addressable classical or quantum memory is required.
The case returns the input matrix exactly. For and , both families return zero; this includes every zero factor. These branches still pay for the input and classical output. The displayed online scales are clamped below by , and the formal total bound includes explicitly. This result compares approximate products in two different error norms under the same circuit access model.
Formalization Note Lean uses interfaces and computes during charged classical preprocessing. Rounded, confidence-dependent sample budgets select members of circuit families fixed before the matrices. The classical law is computed from one fixed list of exact-real arithmetic, random-coin and comparison instructions, with each comparison writing a 0/1 register value and every instruction charged; quantum probabilities and work are computed from the frozen exact-real mean-estimation circuit language. No approximation guarantee or arbitrary runtime number is assumed as a field of an algorithm.
Fix a classical exact-arithmetic matrix multiplication implementation with achievable exponent . Let , , and let be arbitrary matrices. Write , where . Given absolute accuracy and failure probability , there are fixed input-taking classical and quantum circuit families, with classical preprocessing time , which return classical matrices and satisfying
Apart from input/output and preprocessing overhead, their running times are respectively
The soft factors include the confidence logarithms and are uniform over dimensions, factors, matrix entries, accuracy, and confidence; constants may depend on the chosen multiplication implementation. Real numbers are represented exactly, and fixed-position retrieval and arithmetic are charged in both models. The quantum output is an ordinary classical matrix. No efficiently addressable classical or quantum memory is required.
The case returns the input matrix exactly. For and , both families return zero; this includes every zero factor. These branches still pay for the input and classical output. The displayed online scales are clamped below by , and the formal total bound includes explicitly. This result compares approximate products in two different error norms under the same circuit access model.
Formalization Note Lean uses interfaces and computes during charged classical preprocessing. Rounded, confidence-dependent sample budgets select members of circuit families fixed before the matrices. The classical law is computed from one fixed list of exact-real arithmetic, random-coin and comparison instructions, with each comparison writing a 0/1 register value and every instruction charged; quantum probabilities and work are computed from the frozen exact-real mean-estimation circuit language. No approximation guarantee or arbitrary runtime number is assumed as a field of an algorithm.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Fast Convex Optimization with Quantum Gradient Methods establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be closed, bounded and convex, let , and let be convex and ambient -Lipschitz in the stated norm. Assume an attained constrained optimum , and . Both branches use coherent binary evaluations on sufficiently fine finite translated hypergrids: every grid index is preserved, the encoded value has error strictly below , and calls to the unitary and its adjoint are counted. The algorithm construction is fixed before the objective, optimum and oracle values; only geometry and supplied numerical scale bounds enter its construction.
A sufficient scale is a small absolute constant times
This retains both noise terms; a sufficient positive precision takes the minimum of the lemma guard and small absolute multiples of and .
In either branch the classical output is the average of the first iterates, and
The query costs are , with absolute constants common to all data, yielding and , respectively. Quantum arithmetic uses gates, with binary word length and inverse precision exposed as polynomial arithmetic factors. Supplied geometric operations cost at most and , respectively. All bounds apply on positive-probability branches. Conditional per-call failure control suffices; independence is not assumed.
Zero-dimensional, constant-objective, zero-radius, singleton, or already-accurate regimes return the feasible start with zero queries before divisions. In particular, a start is already accurate if , or in the Euclidean branch, or in the mirror branch.
The result shows that quantum zeroth-order methods attain the corresponding first-order nonsmooth query rates. Formalization Note: This uses the formal appendix scope, including ambient Lipschitz control, rather than the informal “on ” access description. The Euclidean precision corrects B.3's omitted independent ; its printed denominator follows in the domain-radius regime , which is not implied by an initial distance. The mirror radius is computed from the Bregman divergence, not introduced by an arbitrary equality. The finite-grid compilation and adaptive execution definitions are submitted for local definition review.
Let be closed, bounded and convex, let , and let be convex and ambient -Lipschitz in the stated norm. Assume an attained constrained optimum , and . Both branches use coherent binary evaluations on sufficiently fine finite translated hypergrids: every grid index is preserved, the encoded value has error strictly below , and calls to the unitary and its adjoint are counted. The algorithm construction is fixed before the objective, optimum and oracle values; only geometry and supplied numerical scale bounds enter its construction.
A sufficient scale is a small absolute constant times
This retains both noise terms; a sufficient positive precision takes the minimum of the lemma guard and small absolute multiples of and .
In either branch the classical output is the average of the first iterates, and
The query costs are , with absolute constants common to all data, yielding and , respectively. Quantum arithmetic uses gates, with binary word length and inverse precision exposed as polynomial arithmetic factors. Supplied geometric operations cost at most and , respectively. All bounds apply on positive-probability branches. Conditional per-call failure control suffices; independence is not assumed.
Zero-dimensional, constant-objective, zero-radius, singleton, or already-accurate regimes return the feasible start with zero queries before divisions. In particular, a start is already accurate if , or in the Euclidean branch, or in the mirror branch.
The result shows that quantum zeroth-order methods attain the corresponding first-order nonsmooth query rates. Formalization Note: This uses the formal appendix scope, including ambient Lipschitz control, rather than the informal “on ” access description. The Euclidean precision corrects B.3's omitted independent ; its printed denominator follows in the domain-radius regime , which is not implied by an initial distance. The mirror radius is computed from the Bregman divergence, not introduced by an arbitrary equality. The finite-grid compilation and adaptive execution definitions are submitted for local definition review.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.