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?
A system of users sharing resources may have no stable configuration: whenever the users settle on their choices, somebody may prefer to change. Weighted congestion games describe this question when different users place different demands on the resources they choose. Routing and scheduling provide examples, but the mathematical question here does not impose a particular network or scheduling structure. It asks which resource cost functions guarantee stability regardless of the finite population, its demands, and its feasible choices. Harks and Klimm give a classification of such functions in their 2012 paper, Theorem 5.1.
There are two distinct requirements. A stable configuration may exist even when some sequences of individually profitable moves cycle forever. Guaranteeing that every sequence terminates is generally stronger. The result identifies the continuous function classes for which these two universal guarantees coincide. The word “universal” matters: the assertion concerns all games generated by a class of costs, rather than the behavior of one specified game.
A weighted congestion game has a nonempty finite set of players and a nonempty finite set of facilities . Each player has a positive real demand and a nonempty finite collection of available strategies. A strategy is a subset of facilities; it may itself be empty. A profile chooses one strategy for every player. Facility has a real-valued cost function defined on the nonnegative half-line. Its load and a player's private cost are
Costs can have either sign, and the game model imposes no monotonicity. A pure Nash equilibrium is a profile satisfying for every feasible unilateral change . A strict improvement lowers the deviating player's cost. The finite improvement property, or FIP, excludes improvement cycles, equivalently infinite improvement paths in this finite profile space. These conventions follow §2 and Definition 2.1.
For any set of cost functions, write for all such games with at every facility. The class is consistent if every game in has a pure equilibrium, and FIP-consistent if every such game has the FIP. The class can be infinite or empty. In the results below, continuity always includes the endpoint zero. “Monotonic” means nondecreasing or nonincreasing, with the direction allowed to differ between functions.
The goal is Theorem 5.1, p.427. For a set of continuous functions, the following are equivalent:
The exponential rate is shared by the entire class. No coefficient or rate is subject to a sign or nonzero restriction. The disjunction is inclusive, as printed in the theorem: classes of constant functions satisfy both alternatives.
Six source milestones support this target. Lemma 3.1 characterizes monotonicity by local right-hand comparisons with . Lemma 3.2 supplies positive loads with either or the reversed inequalities. Lemma 3.4 asserts monotonicity of the integer hull with offsets
under unrestricted consistency. Proposition 5.1 uses consistency for exactly three players to obtain monotonicity of both restricted hulls
Lemma 4.1 equates monotonicity of every integer combination of two continuous monotonic nonconstant functions with affine dependence between them. Lemma 5.1 equates monotonicity of the translated-function hull with each function being affine or exponential; its rate may depend on the function. The source locations are pp.422–427, §§3–5.
The classification separates structural guarantees from favorable individual instances. A class that fails the displayed alternatives cannot guarantee a pure equilibrium for every admissible game. Conversely, either alternative guarantees termination of strict improvement paths as well as equilibrium existence. This gives a precise answer to the unrestricted consistency question posed by Harks and Klimm, without imposing nonnegative or increasing costs.
The mathematical results are published results, not new conjectures. The remaining task is their machine-checked proof. This draft supplies compiled definitions and theorem statements; the seven theorem bodies remain proof targets. Its reusable components include the finite weighted game model, universal class predicates, and three different integer hulls. Published pure-equilibrium and improvement-path definitions are reused through their existing interfaces.
Monotonicity of individual resource costs does not settle the unrestricted problem. The selected statements impose conditions on combinations of functions, and those conditions distinguish the allowed class-wide structure. In particular, separate exponential representations for every member do not establish the common-rate alternative. Another logical obstacle is that an improvement cycle alone need not rule out an equilibrium elsewhere in a game's profile space. The source's nonexistence arguments must exclude every feasible equilibrium, not just exhibit cycling behavior. These distinctions are visible in §§3–5.
The findings accompanying this mission record local issues in printed proofs separately from their theorem statements. Such issues do not authorize stronger hypotheses or weaker conclusions in the faithful targets.
Players and facilities are indexed by finite initial segments with strictly positive sizes. Strategies are finite subsets, and feasible strategies are subtypes of the specified nonempty families. This represents every finite game up to relabeling. Demands are strictly positive nonnegative reals, loads are finite sums, and private costs are ordinary reals. Payoff-maximizing published definitions receive the negative of the private cost. Finite profile spaces justify the equivalence of the published infinite-path FIP convention and the paper's cycle convention.
Consistency is defined by quantification over all admissible games; neither potentials nor the classification are included in admissibility. The hulls are constructed from integer coefficients and the stated translates, without selecting only their monotonic members. Continuity is imposed on the whole nonnegative domain. These choices exclude vacuous proxy models and restricted strategy classes. The empty class and constant functions remain included. No asymptotic estimates or extracted constants occur.
The twelve new definition items precede the seven theorem items, and the six numbered source milestones retain their provenance. No optional variant is posed. The independent two-player characterization and the network and singleton results are outside the mission. In particular, the correction notice on p.436 concerning finite rather than polynomial termination does not introduce an algorithmic target here. Contributions should complete the faithful statements and their needed supporting theory while preserving these conventions.
Communication connections can demand bandwidth at rates that fluctuate over time. Reserving every connection's peak rate can leave substantial capacity unused, while reserving only its mean rate allows temporary overloads and queueing delays. Effective bandwidth provides a way to express the statistical cost of a source in terms that can be used in admission decisions. Chapter 6 of Kelly and Yudovina's Stochastic Networks develops this question first for an instantaneous aggregate load and then for a resource with a buffer.
The buffered model distinguishes the number of connections from the number of connection classes. The number of classes stays fixed while capacity, buffer size, and the number of connections all grow together. The object of interest is the exponential rate of the probability that the workload exceeds the buffer level. This rate measures rare overloads on a scale where ordinary convergence of probabilities to zero loses the relevant information.
A source increment is the work arriving during an interval from connection of class . The classes form a finite set . A source supplies nonnegative, additive increments, with no work on an interval of length zero. Each interval workload is a measurable real random variable. Different source processes are independent, copies within one class have the same process law, and increments have stationary distributions: the law of an interval's workload depends only on its duration. Independence between increments of one source is not required.
Let be the natural number of class- sources in a base system. At positive integer scale , there are copies. The aggregate arrival is
A server of capacity , where , processes this work. Its infinite-past workload at time zero is the random variable
This is the construction in equation (6.4), not an independently chosen stationary queue size. It can be infinite. With a positive base buffer , the overflow probability is .
The logarithmic moment generating function of a class- increment is
Exponential moments are assumed finite locally around zero for each finite duration, following the chapter's MGF convention; a larger tilt may have infinite expectation. The quantity is the nonsingular expression for the product in the book's effective-bandwidth formula.
The goal is Theorem 6.10, printed page 145 of the supplied Lecture Notes PDF:
The supremum over duration remains outside the infimum over tilt. Both the continuous time domain and the infinite horizon are part of the target.
Three source milestones accompany the goal. Equation (6.1) asserts, for a measurable real random variable and ,
including infinite exponential expectations. Theorem 6.2 asserts the exact logarithmic rate for an iid sum exceeding . Its assumptions include a mean below , a positive probability of exceeding , local MGF finiteness, and an optimizing tilt in the interior of the finite-MGF domain. Exercise 6.9 gives both the two-sequence and finite-sum largest-term principles, with finite real rates and positive sequences. It makes no assertion about a countable sum.
The goal relates the statistical characteristics of individual connections to the overload behavior of a large system. It retains duration as a variable, allowing temporal dependence within a connection to affect the rate. A fixed-time tail probability alone does not describe the workload accumulated from an unlimited past. This distinction is central to the buffered model in Chapter 6.
The formal deliverable specifies the source family, its scaling, the workload construction, and the variational expression in one consistent setting. It also separates extended expectations from finite real expectations, so the meaning of a rare event does not change when its probability is zero. These definitions can support later work on queueing large deviations without requiring a finite-state Markov model.
The local theorem files are declarations to be proved, not completed proofs. A published proved Chernoff bound is retained as a reference for the integrable exponential case. The separately published open Cramér theorem assumes finiteness at every real tilt and a closed tail event; it is not substituted for the chapter's local-MGF, strict-tail statement.
The source explicitly gives only a sketch for Theorem 6.10. Fixed-time exponential limits do not by themselves determine the exponential rate of a sum over infinitely many times. Exercise 6.9 establishes a finite-sum result, so it cannot close this gap. The continuous-time workload also raises a measurability and time-discretization issue. Finding F1 records the missing justification with an explicit array of exponentially small terms whose count grows exponentially.
Finding F4 gives an explicit counterexample to the printed goal, even with positive buffer and mean load below capacity. Independent sources have uniformly random phases of a periodic arrival rate taking values 0, 1, and 2. Each source contributes at most one unit of net input over any interval, so with the strict overflow probability is zero at every scale. At duration 2, however, the maximum input 3 has probability , giving a finite variational value . The faithful goal is retained as printed and is expected to be disproved; no corrected variant is proposed. This is a failure of the fixed-time application of Cramér’s theorem at a support endpoint, separate from F1’s infinite-time gap.
Finding F2 concerns a different finite-sample step in the proof of Cramér's theorem: convergence of a tilted-window probability to one half does not ensure it is at least one half for a given sample size. The limiting theorem is retained. Neither finding is converted into an extra hypothesis or a variant. The goal carries no uniform temporal decay estimate, mixing assumption, or fixed-time large-deviation conclusion as an assumption.
The formalization uses Mathlib probability measures, independence and equality-in-distribution predicates, nonnegative Lebesgue integrals, and extended-real order topology. Whole source paths are independent; this is stronger information than independence of one chosen interval's workloads. Natural multiplicities provide exactly copies without rounding. Source indices begin at zero, and the asymptotic scale is represented as to avoid a zero denominator.
The queue supremum is over all nonnegative real times and takes values in EReal. Zero overflow probability has logarithm ; infinite exponential expectation has logarithm . The rate subtracts only finite linear terms. Zero multiplicities contribute zero, including when an unused source has an infinite MGF. At zero time or zero tilt, the log MGF is zero under the source assumptions. No division by is introduced.
Nonnegative additive increments use the usual half-open interval convention for endpoint arrivals. Measurability of the constructed workload is explicit, as required for the source's random-variable language. The model API also requires a probability measure and the relevant measurability when forming an overflow probability or exponential rate. Capacity and buffer are positive; F3 records a deterministic counterexample to extending the goal to zero buffer. Empty class sets and zero source counts remain permitted and give no overflow. For Exercise 6.9, positivity and a nonempty finite index set prevent default logarithms or maxima.
The goal must not be replaced by a finite-horizon queue, a deterministic drift inequality, or a hypothesis already asserting the desired asymptotic. No selected result uses an unspecified asymptotic constant, so there is no constant to instantiate. No variant is posed. The model module supplies real definition bodies; theorem statements expand the relevant formulas so standalone blind read-backs can inspect their meaning without resolving unpublished imports.
ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a.A network of queues records both how many customers occupy each location and how they move between locations. These are different kinds of information. A simple distribution for the occupancies at one time need not make the arrival streams simple, or make the queues independent over time. Open migration processes provide a setting in which the distinction can be studied precisely: customers can move through a finite network, enter from outside, and eventually leave. Chapter 2 of Kelly and Yudovina, Stochastic Networks develops their equilibrium structure.
The target concerns what an observer sees when a stationary network is run backwards. It says that the reversed random process belongs to the same class of models, even when its rates differ from those of the original process. This structural result is the setting for the source's subsequent conclusion about Poisson exit streams. The mission treats the process statement itself, keeping the distinction between an equilibrium rate calculation and a statement about a random trajectory.
There are a finite positive number of colonies. The state is , where counts individuals at colony . There is no upper bound on an occupancy or on the total population. A transition can transfer an individual from colony to a different colony , remove one from the system at colony , or introduce one at colony .
The corresponding rates are , , and . The coefficients are nonnegative, , and the service factors satisfy and when . A departure requires an individual to be present. Immigration rates do not depend on the occupancy. These are the rates in Section 2.4 of the supplied source, printed pages 30–31.
A Markov process here consists of measurable random variables on one probability space, indexed by real time. Its conditional future distributions depend on the most recent state, through a time-homogeneous transition function. Transition rates are its right-hand infinitesimal transition probabilities. The standing assumptions from Section 1.1 are explicit: the process is irreducible, every state has a strictly positive finite exit rate, and sample paths have only finitely many jumps on each bounded interval. A stationary law is a positive normalized mass function giving the distribution at every time.
The goal is Theorem 2.9, printed page 32 of the supplied PDF:
Three milestones support this target. The partial-balance equations (2.3) and (2.4) are grouped as one milestone because one published theorem supplies both identities. They express equilibrium flux balance for transitions associated with a colony and with the outside world. Theorem 2.8 gives the normalized product-form distribution. With positive traffic parameters satisfying
and finite normalizing sums , that distribution is
The third milestone, Proposition 1.1, concerns a stationary process on a countable state space. Its reversed process has the same stationary law and rates
All three source statements are in Kelly and Yudovina, printed pages 16–17 and 31. The goal does not assume the product form, a reverse-process Markov property, or any of the reverse-rate identities.
The result identifies a class of stochastic networks that remains closed under reversal of stationary time. It does not assert detailed balance or equality of the original and reversed rates. It also does not infer independence of colony trajectories from independence of occupancies at one time; the source expressly distinguishes these statements on printed page 32. This separation is needed when interpreting the Poisson exit-stream consequence on printed page 33 of the source.
Published formal results already supply partial balance, normalized full balance, and the algebraic reversed migration rates. They are included as references rather than repeated as new theorem statements. The remaining formal targets concern the actual countable-state random processes: the Markov property of the reversal and preservation of the open-migration class. The new definition layer also provides finite-cylinder and nonexplosive-path specifications that can be reused for other countable-state stationary models.
A formula for a reversed rate matrix alone does not establish a theorem about the reversed process. The latter has finite-dimensional distributions, measurable coordinates, and nonexplosive paths. These must all be connected to the rates. The occupancy space is countably infinite even though the number of colonies is finite, so finite-state reversal theorems do not directly cover the goal. Similarly, assuming the candidate product distribution as part of the meaning of a stationary migration process would omit part of the source's claim. The definition deliberately leaves the stationary law unspecified.
Colonies are represented by with ; states are unrestricted functions from this type to natural numbers. The zero-based colony labels differ only typographically from the source's labels . The exact published migration operators and rate functions are reused. Their natural-number subtraction is protected by vanishing service factors at zero and a zero routing diagonal. Empty products equal one. Normalizing sums in the referenced product-form result use HasSum, so divergent real sums cannot acquire a default value and masquerade as finite normalizers.
The process definitions use probability measures, measurable coordinates, stochastic transition functions, finite-cylinder identities, and locally finite jump paths. Cylinder identities avoid conditioning by division at null events. The state space is countable with measurable singletons, and rate rows are explicitly summable. Positivity of the stationary mass function prevents a zero denominator in the reversal formula. Paths may take either adjacent value at a jump, accommodating the reversal of the right-continuous endpoint convention; isolated zero-duration spikes are excluded.
The goal must establish migration dynamics for the actual map ; an algebraic rate identity or independence at a single time is not a substitute. No asymptotic constants or failure probabilities occur in these targets. The infinite-colony extension, Poisson departure processes, Little's law, Bartlett's theorem, and renewal-reward variants are outside this mission. The findings register preserves observations about out-of-scope source displays, but no variant theorem is proposed. Contributions to the countable-state stochastic foundations and proofs of the two draft theorem statements are within scope.
ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a.A semidefinite constraint asks whether a symmetric matrix is positive semidefinite: every vector must have a nonnegative quadratic form under that matrix. In optimization, its entries can depend on a decision and on uncertain inputs. Requiring the constraint for every possible input can be restrictive, especially when rare inputs have very large magnitude. A chance constraint instead requires the matrix inequality to hold with a specified probability. Chapter 10 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization develops safe approximations for such constraints, including conic quadratic constraints represented through symmetric matrices.
The question here is how a known probability of a moderate matrix perturbation can imply a much higher probability at a larger threshold. The chapter gives explicit answers for bounded independent perturbations and for independent standard normal perturbations. The goal is its Corollary 10.1.3, including both distributional cases and the possibility that the reference matrix is singular.
Let be deterministic symmetric real matrices, with . The random perturbation is
The Loewner order means that is positive semidefinite. Thus the event controls the perturbation simultaneously in every vector direction. For normalized matrices, denotes the operator norm for Euclidean vectors, rather than a maximum entry or a row-sum norm.
The random coordinates are measurable and independent on a probability space. Under assumption A.I they have zero means and satisfy almost surely. Under A.II each has the standard normal law . The deterministic variance certificate is
This is precisely system (10.1.13) in the source. A separate premise supplies the base probability
where and . Neither this probability premise nor the certificate contains the amplified probability conclusion.
Write for , and for its inverse upper-tail quantile. The book writes these functions as Erf and ErfInv. Its Erf is a one-sided upper Gaussian tail; substituting the common analytic error function would change every Gaussian bound.
The goal, Corollary 10.1.3, asserts that under A.I, for every ,
Under A.II and the additional condition , it asserts
Both conclusions retain the constants and strict threshold of equations (10.1.15)–(10.1.16).
Three source-numbered milestones support this goal. Theorem 10.1.1 concerns symmetric with and defines . Its bounded-case conclusion is
Theorem B.5.1 concerns a closed convex set with standard Gaussian mass at least . It asserts that contains the centered ball of radius . If it contains a centered ball of radius , then for ,
Its further conclusion covers centered Gaussians with arbitrary positive semidefinite covariance: an outside probability at most becomes at most after dilation. This clause includes degenerate covariance matrices.
Theorem 10.1.2 is the normalized Gaussian matrix milestone. With the same variance normalization and exact base mass , it states, now for ,
The chapter’s bounds connect a matrix certificate and a base confidence level to explicit larger-threshold confidence guarantees. They preserve information about the reference matrix, including its null directions. A statement requiring positive definiteness would exclude part of this conclusion.
These are established textbook results whose Lean proofs remain the targets of this mission. The draft supplies concrete definitions and open theorem statements, not completed proofs. Mathlib already provides probability measures, normal distributions, matrix positivity, and a semidefinite Schur-complement equivalence. The published theorem PinningSync.Tree.lemma_2_13 supplies the positive-definite Schur-complement branch as a reference; it is not presented as a substitute for the full semidefinite lemma.
The target combines probabilistic concentration with inequalities that must hold in every matrix direction. Entrywise bounds do not state the same event. Likewise, an invertible reference matrix is a restricted case of the goal. The Gaussian branch also requires exact control of inverse-tail conventions and dilation probabilities for general closed convex sets. The source’s proof of Theorem B.5.1(i) has inconsistent tail arguments in its separating-halfspace paragraph, recorded as a proof warning; the theorem statement retains the printed .
All matrices are real, finite, and explicitly symmetric in the theorems. Matrix and perturbation dimensions are positive; indexing by Fin changes only the origin of the indices. The setup uses Mathlib’s positive-semidefinite predicate directly. The two matrix inequalities are defined by their positive-semidefinite differences, and the variance certificate is an existential block-matrix condition. The Gaussian geometric theorem uses the concrete standard and multivariate Gaussian measures on Euclidean space, with a positive-semidefinite covariance premise.
Formalization Note. Equation (2.3.22) specifies the inverse tail on , while the later statements allow base mass one and failure probability zero. The draft retains those cases by using the extended-real inverse quantile, with , , and the limiting exponential envelope zero at infinity. An infinite-radius centered ball is the whole space. All displayed formulas agree with the source on finite quantile arguments. This endpoint interpretation is recorded in the findings for review, rather than imposing an unprinted restriction.
The reusable components are the matrix perturbation, the two-sided order event, the block certificate, and the Gaussian tail conventions. Proof contributions must establish the full statements with their constants and endpoints. No variants are posed in this mission.
A production or allocation decision can satisfy a linear constraint for nominal data and violate it when those data change. Robust optimization asks for a decision that satisfies the constraint for every realization in a prescribed uncertainty set. The uncertainty set is part of the model: the requirement does not attach probabilities to its elements, and it does not permit a small violation at an unfavorable realization. Chapter 1 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization develops this interpretation for linear optimization.
This requirement initially gives infinitely many inequalities, even when the decision vector has only a few coordinates. The chapter's representation results identify uncertainty descriptions for which those inequalities can be replaced exactly by finite systems. The replacement matters to applications because it preserves the set of admissible decisions while expressing it in the language of linear, conic quadratic, or semidefinite optimization.
Let be the decision vector and the perturbation. The nominal coefficients are and , with shifts for each perturbation coordinate. The robust linear constraint is
A lifted conic description specifies the perturbation set by
Here are linear coefficient arrays, is an offset, and is a cone. The variable describes the uncertainty set; it is not a decision made after uncertainty is observed. The general theorem assumes that is closed, convex and pointed, with nonempty interior. The perturbation set is nonempty. For a nonpolyhedral cone, the description must have a point strictly inside the cone.
An equivalent representation has additional variables but projects to precisely the original feasible set. The interpretation is existential: a feasible decision must admit a certificate, and every feasible pair must project to a robust feasible . This is Definition 1.3.1 of the source, not a sufficient-condition approximation.
The goal is Corollary 1.3.5, printed page 21. If the description uses a nonnegative orthant, a product of Lorentz cones, or a positive semidefinite cone, the robust constraint has an explicit LP, SOCP, or SDP representation, respectively. Strict feasibility is required for the latter two cases. With auxiliary variable , the system is
The goal includes the polynomial size of this representation and the explicit dependence of its coefficients on the input data. It also records preservation of the set of feasible objective values for an objective depending only on .
Theorem 1.3.4 is the general supporting target. It gives the same system with , where , and allows either a polyhedral cone or a strictly feasible description. The two introductory examples give concrete representation targets:
The box target includes its further representation by finitely many linear inequalities with auxiliary upper bounds on the absolute values. These are Examples 1.3.2 and 1.3.3, not additional general duality assumptions.
The result identifies the finite certificate system appropriate to each uncertainty model. It distinguishes an exact reformulation from a conservative replacement that could exclude valid decisions. Because the original decision variables remain present, an objective can be retained without interpreting the auxiliary certificate as an additional physical decision.
The mathematical results are established textbook results. The work requested here is their formal proof against explicit Lean statements. The resulting definitions expose affine uncertainty, lifted perturbation sets and finite certificate systems for reuse. Published good-cone and dual-cone definitions are already available and are imported; the theorem statements in this mission remain open proof targets.
The equivalence requires existence of a finite certificate, not merely a sequence approaching a limiting objective value. Nonpolyhedral descriptions can fail to admit the asserted certificate without strict feasibility. In contrast, the polyhedral case does not need a strictly feasible point, so imposing that condition uniformly would lose part of the source result.
There is also a distinction between a finite worst-case value and a perturbation attaining it. The proof on printed page 20 writes a maximization problem and then discusses its optimal value; this does not require primal attainment. The formal target uses universal feasibility directly. The local findings record an explicit nonattainment example, without establishing a gap in the duality argument.
All coordinates are real and finite. Nominal coefficients are stored separately from perturbation shifts. Lorentz blocks contain a distinguished scalar coordinate and a finite vector part; their Euclidean norm is the square root of a sum of squares. PSD coefficients are symmetric matrices, and pairings sum all matrix entries, giving the trace pairing for symmetric inputs. Strict feasibility in that case means positive definiteness in the symmetric ambient space.
The representation is built from the coefficient arrays themselves. Robust feasibility is defined independently by universal quantification over perturbations; it is never defined as certificate existence. No rank condition is imposed on or . Nonnegative ball radii include zero, and zero-dimensional coordinate lists retain their ordinary empty-sum interpretation.
Formalization Note The explicit system has one scalar inequality, scalar equalities, and one standard cone block. If is its number of auxiliary scalar coordinates and its structural cone description length, the chosen dense counts are
The size target is , an explicit witness to the book's polynomial-size assertion. The constant is encoding bookkeeping, not a numerical complexity constant quoted from the book. PSD storage uses coordinates, including symmetric duplicates. These counts concern the finite representation, not bit complexity or the time needed to solve it.
Permutation operators encode the symmetries of many identical quantum systems. When one tensor factor is transposed, the resulting operators occur in questions about the commutant of mixed tensor representations and about partially transposed quantum states. The usual symmetric-group algebra no longer describes their multiplication: a product can acquire a factor equal to the local dimension . Mozrzymas, Horodecki, and Studziński determined the full algebraic structure of their span in their 2014 paper. Their description identifies its simple components even when a small local dimension makes the natural spanning family linearly dependent.
Let and . On tensor factors of , the permutation operator moves the computational-basis tensor indexed by to the tensor indexed by . Write for matrix transposition on the last tensor factor only. The object of this mission is the complex operator algebra
The subspace is spanned by those for which . Its complement in the result is an ideal that annihilates on both sides. The permutations of the first positions act on . For each irreducible representation of that occurs in this action, write . Definition 40 constructs operators from their matrix coefficients, the permutation operators, and partial transposition. Their span is .
Definition 29 assigns to a block matrix indexed by and , where and . Its block is , so every diagonal block is times the identity. Finally, a partition of labels an irreducible representation of ; counts the rows of its Young diagram.
Theorem 30 asserts that splits into mutually annihilating ideals, and that those ideals split further into full matrix algebras:
When , the summand has order . The goal also includes the multiplication law for the operators, with coefficient as in equation (6) of Proposition 44. This identity specifies how their natural generators multiply even when is singular. The two cases for printed in Theorem 30, and , give the same uniform restriction because every partition of has at most rows.
The theorem identifies the simple ideals and their sizes from representation data of two smaller symmetric groups. It separates the dimension-dependent part , where the rank of may drop, from the part controlled by partitions with fewer than rows. Consequently, it determines the irreducible representations of this concrete operator algebra and explains why its decomposition changes with .
The result is proved in the cited paper; this mission asks for a machine-checked proof of its precise statement. The published operator model and tensor-permutation definition already fix the underlying matrices. A completed development would add reusable facts about partial transposition, ideals of represented group algebras, matrix units arising from singular coefficient matrices, and occurrence of symmetric-group representations. The read side of this mission is an open theorem, not a claim that Theorem 30 has already been formalized.
The natural spanning elements are not a basis when , and the can also be dependent. Counting generators therefore cannot establish the orders of the matrix ideals. The matrix records those dependencies; its rank, not its number of rows, governs the summand. The complementary ideal requires tracking which representations of survive after the component is removed. A dimension count alone would identify neither the actual ideals nor their matrix-unit multiplication laws.
Operators are matrices indexed by functions Fin n → Fin d, a coordinate model of . The last-factor transpose is the published ptLast; and are the published complex spans algA and algM. The paper's labels become Fin (m+1), and its last label becomes Fin.last (m+1). Permutations multiply right to left. The irreducible family is represented by real orthogonal matrices, hence by unitary complex matrices after casting; the explicit completeness condition ensures that every irreducible of is present in the family.
Occurrence means that a nonzero intertwiner embeds an irreducible into the action on exactly . An ideal is a complex subspace of closed under multiplication on both sides. An assertion requires linearly independent matrix units spanning and obeying the matrix-unit law; it cannot be discharged by a dimension count. For this requires . The order is represented by the number of standard Young tableaux of shape , using the classical symmetric-group dimension formula. The goal permits and requires .
Theorem 30's displayed coefficient conflicts with Proposition 44's equation (6), ; the latter agrees with the matrix-index contraction and is used here. Contributions toward the listed source results, the partition occurrence criterion, and the singular-matrix algebra reduction are useful. An arbitrary family of subspaces with the right dimensions does not meet the target: the statements fix , , , , and the matrix-unit structure of each component.
A quantum circuit may create a state whose full list of amplitudes is far too large for a classical computer to store. That fact alone does not show that every observable feature of its output is hard to estimate. In Simulating quantum computers with probabilistic methods, Van den Nest asks when classical sampling can reproduce the accuracy of a quantum experiment that estimates an observable's expectation. The paper's Theorem 1 identifies a condition on the input state and on the observable after it is pulled back through the circuit, rather than requiring the circuit itself to have a sparse matrix. This separates the cost of describing a whole output state from the cost of estimating the particular quantity measured at the end. Van den Nest, §§1–3
The paper distinguishes weak simulation, which achieves the accuracy available from polynomially many experimental runs, from strong simulation, which asks for much finer numerical precision. This mission addresses the sampling estimate behind the former. The source's 2010 preprint proves an efficient classical algorithm under computational assumptions; the formal target below states its finite probability guarantee for the particular estimator in that proof. Van den Nest, pp. 2, 6–7
An -qubit computational basis has labels . A state has complex coefficient at each label, with . Measurement in this basis yields with Born probability . A state is computationally tractable (CT) in the paper when these probabilities can be sampled, and individual coefficients can be evaluated, in polynomial time. The finite development below represents the resulting sample and coefficient access directly. Van den Nest, Definition 1, p. 8
For a matrix , the entry is its transition from basis label to label . The operator is -sparse if each row and each column has at most nonzero entries. Its column data consist of coefficients and row labels for , with . Nonzero coefficients in a column occupy distinct rows. The paper calls such an operator efficiently computable sparse (ECS) when the nonzero entries can also be found efficiently. Van den Nest, §4.3, pp. 10–11
For two normalized states , write . The paper defines bounded complex functions and from the column data, separating each contribution according to whether . The estimator is the sum over of a sample mean of under and a sample mean of under . The same independent draws from each law are used for every in this formalization. Its target is the matrix element . Van den Nest, Eqs. (5)–(8), pp. 12–13
The main result concerns a unitary , a Hermitian observable with spectral norm at most one, and the pulled-back operator . When is -sparse and has the stated column data, the estimator targets the output expectation . For samples of each kind and , the target is
The paper states Theorem 1 as an efficient simulation claim. The displayed explicit tail is obtained from its Theorem 3, the pointwise bounds on and , and Appendix A's Chernoff–Hoeffding estimate. Its exact constants are a commitment of this finite accuracy target, not a constant printed in Theorem 1. Van den Nest, Theorem 1, p. 2; Theorem 3, p. 11; Eq. (18), p. 23
The milestones follow the paper's supporting statements: the real and complex sampling bounds, the sparse matrix-element decomposition, the two expectation identities, the bound on , the row-preimage count, the bound on , and the general matrix-element estimate of Theorem 3. Theorem 3 permits two different normalized states and a sparse operator that need not be unitary. Its specialization with and gives the target above. Van den Nest, pp. 11–13, 23
The theorem gives a concrete error probability for recovering an output observable's expectation from classical samples of the input state. The condition concerns ; it allows the circuit matrix itself to be dense. Thus it applies to circuit and observable pairs for which output-state enumeration is a poor guide to the cost of this particular expectation estimate. The paper develops consequences for local observables and other circuit families after Theorem 3. Van den Nest, Theorem 1 and §5
A formal development would make the finite probability claim, the sample-access model, and the spectral-norm assumptions independently checkable. The paper's theorem is proved mathematically, but this mission's Lean theorems are open statements awaiting proofs. In particular, machine-checking the explicit estimator's accuracy is separate from representing a polynomial-time classical machine, which this mission does not undertake.
Sparse columns make a sum of terms indexed by , but they do not by themselves give a bounded random variable when a term is sampled from . Dividing by a small may create a large weight. Sampling from has the analogous problem in the opposite direction, and the row labels need not be injective as functions of . The paper's two functions split those regimes; its row-sparsity condition controls the number of terms that can contribute to one . The proof must also keep the complex modulus, the strict failure event, and the shared sample sets consistent with the finite probability law. Van den Nest, proof of Theorem 3, pp. 12–13
Lean represents basis labels as functions Fin n → Bool, states as finite complex coefficient vectors, and operators as complex matrices. The operator bound uses the published spectral norm QAlgorithms.specNorm. Theorem 1 assumes a unit vector, a unitary matrix, and a Hermitian observable of norm at most one. The general Theorem 3 uses any finite basis and two normalized coefficient vectors. Column data can enumerate nonzero entries in any order; the proof needs their values and distinctness, while the paper fixes top-to-bottom order. All expectations and event probabilities are finite sums. No measurable-space conventions or Bochner-integral defaults enter.
The estimator is fixed by the definitions of , , and their two sample means. It reads sampled labels, state coefficients, and sparse column data. It cannot read the target matrix element, enumerate all basis labels to output the answer, or inspect and outside the supplied column data. The model asserts the accuracy that these accesses support; it does not certify that sampling, coefficient evaluation, column enumeration, or the circuit family run in polynomial time. This is the precise part of the paper's classical simulation statement represented here.
Positive avoids the undefined statistical meaning of an empty sample mean. The split assigns equality to . A zero Born probability has zero sampling mass; the corresponding totalized quotient is set to zero. For , the sparse matrix and estimator are zero, and the theorem's failure bound is zero. The displayed bound is the one derived from the paper's inequalities; the complex-valued intermediate constant is likewise derived from Eq. (18). Reusable contributions include the finite product-sampling concentration theorem, the column-data representation, and the matrix-element decomposition. Van den Nest, pp. 10–13, 23
Quantum devices rarely prepare the state they are asked for. A procedure meant to output a pure state on levels often outputs a mixed state , the result of noise during preparation. If the procedure can be run times, the copies can be processed jointly into a single output closer to . This task is quantum purity amplification (QPA), also called purification. It appears as a primitive in error mitigation, in state preparation on near-term hardware, and in the theory of quantum state estimation and cloning.
For qubits and depolarizing noise, Cirac, Ekert and Macchiavello found the optimal protocol in 1999 (Phys. Rev. Lett. 82, 4344), and Keyl and Werner determined the rate of optimal purification procedures (Ann. Henri Poincaré 2, 2001), with the minimum fidelity as figure of merit. For qudits () the optimal protocol remained open. Childs, Fu, Leung, Li, Ozols and Vyas gave a streaming protocol (arXiv:2309.16387), and Grinko and Ozols reduced unitary-equivariant SDPs of this type to linear programs (arXiv:2207.05713) without solving this one in closed form. Li, Fu, Isogawa, Silva and Chuang (arXiv:2409.18167, version 4 of 25 Dec 2025) solve the qudit case exactly: they give the Choi matrix of the optimal channel in closed form (Theorem II.1).
Let . An unknown pure state is corrupted by the depolarizing channel of strength :
A QPA protocol is a quantum channel from (the input registers) to (the output register). Its quality at is the fidelity , and the figure of merit is the minimum fidelity .
A channel is described by its Choi matrix , an operator on with and ; the channel is . Averaging the fidelity over a Haar-random gives the semidefinite program (SDP)
with , , and the Haar probability measure on .
The answer is phrased with Young diagrams. A Young diagram with boxes and at most rows labels an irreducible representation of of dimension , and denotes the projector onto the -isotypic part of (weak Schur sampling). The protocol must be covariant under the mixed representation . Inside the -sector this representation splits as , where removes the last box of row of (padded with zeros to rows). Row is feasible if it is the last row or . Let be the smallest feasible row; is with the bottom box of its last column removed. is the projector onto the -isotypic component of .
is feasible and optimal for the SDP. Its channel is a quantum channel. For every channel , . The statement asserts optimality, not uniqueness, and holds for every , , .
The theorem gives the exact optimal purification channel for every , and depolarizing strength, and the channel does not depend on . It has an operational form, worked out in the paper's Sec. II C: Schur sampling, a correction inside each sector, and a partial trace. From it the paper derives the optimal sample complexity for output infidelity (Theorem II.2) and an efficient circuit implementation (Algorithm 1). Both rest on Theorem II.1.
The result is proved on paper but not formalized anywhere. A formal proof would check a chain that mixes semidefinite programming, Haar integration, the Schur–Weyl duality of the mixed representation , and a combinatorial inequality for normalized Schur polynomials (Sra's theorem, European J. Combin. 51, 2016), which is cited and not proved in the paper. Several of these components are general results: the block decomposition of covariant operators, the cost-matrix projection argument for SDPs with a partial-trace constraint, and the dominance ordering of normalized Schur polynomials.
Symmetry reduces the SDP to a linear program in one coefficient per block, but the coefficients of the original cost matrix are hard to evaluate directly. The proof replaces by , whose block coefficients are characters of rational representations evaluated at the spectrum of , and shows that the replacement leaves the optimizer unchanged. The remaining step compares these characters across blocks. That comparison is the Cuttler–Greene–Skandera inequality for normalized Schur polynomials, a nontrivial combinatorial theorem. One natural guess fails: keeping the block of the largest feasible row instead of the smallest gives a channel that is not optimal in general. The optimal block removes the bottom box of the last column, which is generally a different row.
Operators are complex matrices indexed by , output register first. Partial traces are the published WildeQIT.partialTraceLeft/Right. The Haar measure is the published probability Haar measure QAlgorithms.Schur.unitaryHaar d on , and Haar integrals of matrices are taken entrywise. Young diagrams, Schur polynomials, dimensions (semistandard tableau counts), Schur modules with their polynomial representations, and the weak Schur sampling projector come from the published QAlgorithms.Schur layer; channels are QAlgorithms.IsChannel (finite Kraus families). Rows are 0-based in Lean.
The irreps of the mixed representation (Nguyen, arXiv:2310.01613) are rational: when has fewer than rows, has last row . They are encoded by the determinant shift , a Young diagram with boxes, with . The isotypic projector is the character integral .
Disclosed choices:
Trivializing formalizations are ruled out. is the explicit operator above, computed from and alone, never an argmax or a hypothesis. The cost matrix is the actual Haar integral, not a closed form. The competitors are all feasible and all channels , with no symmetry assumed.
Welcome contributions: the tracing and Pieri-type decomposition of ; Haar orthogonality of characters on ; the equivalence of Choi feasibility and Kraus channels; Sra's inequality. Each is reusable beyond this mission.
Light carries information in electromagnetic field modes. At optical frequencies, photon statistics affect the capacities of thermal-noise and broadcast communication channels. Bounds on these capacities depend on identifying the smallest entropy that a beam splitter can produce under specified input conditions. Guha, Erkmen, and Shapiro explain why two such minimum output entropy claims matter: their first supports the proposed thermal-noise channel capacity, and their second supports the proposed bosonic broadcast capacity region. The paper states both as conjectures and shows that they follow from its Entropy Photon-Number Inequality (EPnI).
The authors model the EPnI on the classical entropy power inequality, but its quantum version concerns density operators rather than probability densities. Their 2007 paper does not prove the EPnI. A later platform theorem, sourced from an OpenAI mathematics preprint codebase, is marked Proved for finite-energy inputs. It supplies this mission's referenced first milestone. The statements here express the paper's two consequences in that same model; their Lean proofs are still open in this proposal.
A bosonic mode has number states indexed by . An -mode state is a positive density operator on the full Fock space indexed by , with trace one. Its von Neumann entropy is . All logarithms are natural. A thermal state with average photon number per mode has weights in the number basis; for modes the state is the product of these single-mode distributions. At this is the vacuum, with zero photons in every mode. A pure state is a projector onto a unit Fock vector. A state has zero mean field when the expectation of the annihilation operator is zero for each mode.
Two independent input states and enter a lossless beam splitter with transmissivity . For each mode its retained output has annihilation operator ; the other output is discarded. The retained density operator is . Independence means that the joint input is ; correlations among modes inside either input are allowed. The thermal entropy per mode is
with the continuous convention at . The entropy photon-number of an -mode state is . Eq. (13) of the paper asserts that the output entropy photon-number is at least times that of the first input plus times that of the second. The source paper gives the definitions in §II.B, p. 2.
The first target fixes the second input to a thermal product state of mean , while the first ranges over zero-mean-field pure states. The second fixes the first input to the vacuum, while the second ranges over states with entropy . For each class, the claimed lower bound and attained minimum are
For the first class the vacuum first input attains equality. For the second, the product thermal second input attains equality. The goal states both claims together, including the existence of an attaining input and output. The shared attack path contains the EPnI, Eq. (13), the scalar properties of and its inverse, thermal state existence and entropy, zero entropy of pure states, the beam splitter's thermal output for vacuum and thermal inputs, and the inequalities of Eqs. (16)–(17). Each milestone uses the statement on pp. 2–3 of the paper.
An attained minimum gives the precise noise floor for the two input classes. In the paper's capacity arguments, the first class concerns the thermal-noise channel and the second the bosonic broadcast channel. The mission records the exact optimizer and the output entropy, including the endpoints and . Without the optimizer's output value, a lower bound alone would not identify the minimum.
The referenced EPnI is marked Proved on Prove2Me under finite-energy assumptions. This mission's thermal-state, pure-state, and beam-splitter statements are draft targets and have no machine-checked proofs here. Closing them would connect the platform's general inequality to the two applications explicitly worked through by Guha, Erkmen, and Shapiro. The thermal-state and entropy facts can also serve other bosonic-channel formalizations using the same Fock-space interface.
The EPnI supplies an entropy photon-number bound, but converting it into an attained output-entropy minimum requires more than substituting a pure input. One must justify that the inverse thermal entropy behaves as expected on nonnegative entropies, that thermal product states really exist in the chosen infinite-dimensional state space, and that vacuum mixed with thermal noise produces the specified thermal output. The last claim is a statement about the full beam-splitter matrix and its partial trace, not just a scalar entropy comparison. Infinite sums also demand care: a formal expression that defaults to zero when it diverges would give a spurious entropy value.
The development reuses OAI.EntropyPhotonNumber.State n, its number-basis matrix entries, real-valued entropy, , the infimum definition of , and the beam-splitter output relation. The new definitions express thermal, vacuum, pure, and zero-mean-field states on that same carrier. The thermal state uses Eq. (10)'s number-basis formula; Eq. (9)'s coherent-state integral is outside this mission. The beam splitter uses the sign convention in the published definition, which yields the paper's retained output . The zero-mean-field condition includes convergence of each annihilation expectation.
There is at least one mode, , since Eq. (11) divides entropy by . Inputs to which the EPnI is applied have finite energy. This assumption is additional to the paper's phrasing: it is required by the referenced platform theorem and prevents the real-valued infinite-series entropy from taking a default zero on a divergent input. The first optimized input is therefore a finite-energy pure state; the second is a finite-energy state of entropy . The thermal and vacuum witnesses themselves have finite energy. These conditions are disclosed in the theorem statements and are not assertions that the unrestricted conjectures have been settled here.
The goal quantifies over every feasible input and corresponding output, states equality for every output from the named optimizer, and asserts that the optimizer and an output exist. This rules out a vacuous result from an empty thermal-state class or a bound that omits attainment. Contributions to the scalar lemmas, thermal-state construction, pure-state entropy, and the beam-splitter output calculation are all within scope. Infrastructure for summable Fock-space matrix entries and operator entropy should remain reusable beyond this mission.
The cyclotomic Birman–Wenzl–Murakami algebra is an algebra of braids and contractions equipped with an additional cyclotomic relation. It connects diagram algebras, representation theory, and knot theoretic constructions. For calculations over a coefficient ring, one needs to know whether the diagrammatic spanning elements remain independent after parameters are specialized. The freeness theorem of Goodman and Hauschild Mosley answers that question for admissible integral ground rings: the algebra has a basis of the size predicted by labeled Brauer diagrams. The paper also identifies the algebra with a cyclotomic Kauffman tangle algebra. This mission targets the algebra's freeness and rank assertion.
The cited paper builds on admissibility relations developed with Wilcox and Yu. Its earlier definitions and preliminary statements already appear in Prove2Me mission 92e1197e-907f-4ab8-92be-01ea44f6cfef. The present mission reuses that published layer and poses the deferred freeness theorem and the intermediate results that support it. The distinction matters because two algebras with similar names but different generators or parameter conventions need not have the same rank statement.
A ground ring is a commutative unital ring with a positive integer and parameters . The parameters are units, and they satisfy
The algebra is generated over by invertible braids , contractions , and an invertible affine generator . It obeys the affine BMW relations of Definition 2.1 and the cyclotomic relation of Definition 2.8. The shared published presentation uses indices for and , corresponding to the paper's and . At there are no generators.
The parameters are admissible when is nonzero and not a zero divisor, weak admissibility holds for every integer shift of the relations, and are -linearly independent in . These are the conditions of Definition 3.3, expressed using condition (1) of Theorem 3.2. A morphism of ground rings preserves all and and permits exactly the four paired sign actions on and in Definition 2.13. Consequently, base change includes the sign twists allowed by the paper.
For the generic case, is the rational function field in algebraically independent variables. Put , set for odd and for even , and define , where is the rational expression in equation (3.6). A shape in is an -tuple of Young diagrams whose total number of boxes is at most and congruent to modulo two. An up–down tableau of shape is a path from the empty tuple to , adding or removing one box at each step. Its set is .
The central target is the freeness half of Theorem 6.1. For every admissible integral ground ring and every ,
Here , so the asserted rank at is one. A basis indexed by a finite type of that cardinality states both freeness and rank.
The milestone path includes the paper's admissibility equivalences, generic parameter construction, universal admissible integral domain, base change, the spanning family of elements, the relevant Jones ideal and Hecke quotient results, and the generic structure results. At the generic field, Theorem 4.8 supplies split matrix blocks indexed by , with block size . The count in the proof of Theorem 5.2 is
which agrees with the generic dimension asserted by Theorem 5.2. The final theorem applies over an admissible integral domain, rather than only over .
The result supplies an exact finite basis for throughout the admissible integral-domain regime. It fixes the module rank independently of a choice of specialization and gives a numerical benchmark for presentations and representations of these algebras. The generic matrix decomposition also records the simple-block labels and their sizes; the tableau identity explains how those dimensions total the same rank.
Goodman and Hauschild Mosley proved these results. This mission asks for machine-checked proofs of the statements already known in the paper. Its reusable output includes ground-ring morphisms with sign twists, the generic parameter model, and finite tableau types. The published preliminary layer in mission 92e1197e-907f-4ab8-92be-01ea44f6cfef contains two proved and four open results among the six referenced milestones; none of the eight new theorem statements is presented here as already machine proved.
A spanning family alone does not show a basis: specializations can introduce linear dependence, and an equality of dimensions over one field does not itself establish independence over every integral ground ring. The argument also has to maintain the exact admissibility conditions when moving between coefficient rings. Over the generic field, identifying the right semisimple blocks requires the branching shapes and tableau sizes, while the final statement concerns arbitrary admissible integral domains. These are distinct algebraic regimes, and the same presentation and parameter conventions must be kept through each one.
Lean uses the published GroundParameters, BMW, BMWAdmissible, UAdmissible, and equation (3.6) gamma expression from QAlgorithms.Papers.Independent.Support21.P14. The algebra is the quotient of a free algebra by the source's relations, with zero-based generator indices. The new definition layer records all four sign cases of Definition 2.13, the generic field as a fraction ring of a multivariate polynomial ring over , and shapes and tableaux as finite-indexed Young diagrams. A generic ground-parameter value is asserted to exist as a theorem because the required unit and compatibility proofs are substantive.
The universal-ring milestone states all five parts of Theorem 3.19 for and ; part (5) is read inside , where the universal -admissible ring is the subring generated by , , and . The base-change statement uses for the source's . Theorem 4.8 is expressed as a product of full matrix algebras with tableau-sized blocks, combining its split and labeling clauses with the block dimensions stated elsewhere in §4. Theorem 6.1's Kauffman-tangle isomorphism is not posed because a corresponding tangle algebra has not been provided here. The cited spanning set is expressed as an indexed family, which remains meaningful when a degenerate coefficient ring identifies elements.
The goal requires an actual basis of cardinality over an admissible integral domain. A mere dimension equality or spanning claim does not satisfy it. Contributions toward the missing generic decomposition, tableau count, base-change isomorphism, and passage to arbitrary admissible domains are all within scope. The ground-parameter and quotient-presentation definitions are reusable independently of this mission.
How correlated are two quantum systems from the perspective of a third? We answer this by providing an optimal quantum state redistribution protocol for multipartite product sources. Specifically, given an arbitrary quantum state of three systems, where Alice holds two and Bob holds one, we identify the cost, in terms of quantum communication and entanglement, for Alice to give one of her parts to Bob. The communication cost gives the first known operational interpretation to quantum conditional mutual information. The optimal procedure is self-dual under time reversal and is perfectly composable. This generalizes known protocols such as the state merging and fully quantum Slepian-Wolf protocols, from which almost every known protocol in quantum Shannon theory can be derived.
This mission is the statement-level formalization of The operational meaning of quantum conditional information (arXiv:quant-ph/0612050v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact state-redistribution rate region and optimal corner (Main result: exact state-redistribution rate region and corner, Eqs. (1)–(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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
We present in this paper a set of routines constructed to compute the rank of a matrix Lie algebra and also to determine a Cartan subalgebra from a given list of elements
This mission is the statement-level formalization of Algorithm to compute the rank and a Cartan subalgebra of a matrix Lie algebra with Mathematica (arXiv:math/0205235v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is so(n): BSo ordered basis (so(n): BSo ordered basis, PDF p. 5). 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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper, we introduce the notion of a normal form of one qubit quantum circuits over the basis , where , and denote the Hadamard, Phase and gates, respectively. This basis is known as the {\it standard set} and its universality has been shown by Boykin et al. [FOCS '99]. Our normal form has several nice properties: (i) Every circuit over this basis can easily be transformed into a normal form, and (ii) Every two normal form circuits compute same unitary matrix if and only if both circuits are identical. We also show that the number of unitary operations that can be represented by a circuit over this basis that contains at most -gates is exactly .
This mission is the statement-level formalization of Representation of Quantum Circuits with Clifford and Gates (arXiv:0806.3834v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (seed paper result): unique exact normal form (Theorem 1 (seed paper result): unique exact normal form, PDF p. 6). 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.
Matsumoto and Amano (2008) showed that every single-qubit Clifford+T operator can be uniquely written of a particular form, which we call the Matsumoto-Amano normal form. In this mostly expository paper, we give a detailed and streamlined presentation of Matsumoto and Amano's results, simplifying some proofs along the way. We also point out some corollaries to Matsumoto and Amano's work, including an intrinsic characterization of the Clifford+T subgroup of SO(3), which also yields an efficient T-optimal exact single-qubit synthesis algorithm. Interestingly, this also gives an alternative proof of Kliuchnikov, Maslov, and Mosca's exact synthesis result for the Clifford+T subgroup of U(2).
This mission is the statement-level formalization of Remarks on Matsumoto and Amano's normal form for single-qubit Clifford+T operators (arXiv:1312.6584v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §1 main result: MA existence, uniqueness, optimality and effective normalization (§1 main result: MA existence, uniqueness, optimality and effective normalization, PDF p. 1). 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.
4 results of the paper are not stated yet, because the library lacks an interface they need:
A direct proof of the relation between the one-shot classical capacity and the minimal output entropy for covariant quantum channels is suggested. The structure of covariant channels is described in some detail. A simple proof of a general inequality for entanglement-assisted classical capacity is given.
This mission is the statement-level formalization of Remarks on the classical capacity of quantum channel (arXiv:quant-ph/0212025v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Irreducible covariance gives bistochasticity and the capacity–entropy identity (§1, theorem; (1)–(3), 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.
This paper investigates properties of noisy quantum information channels. We define a new quantity called {\em coherent information} which measures the amount of quantum information conveyed in the noisy channel. This quantity can never be increased by quantum information processing, and it yields a simple necessary and sufficient condition for the existence of perfect quantum error correction.
This mission is the statement-level formalization of Quantum data processing and error correction (arXiv:quant-ph/9604022v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Coherent information bound and environment factorization criterion (§4, Eq.(4) and equality criterion, PDF p. 10). 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.
Agrawal, Kayal, and Saxena's "PRIMES is in P" (Annals of Mathematics 160 (2004) 781-793) settled a question open since the birth of complexity theory: primality has an unconditional, deterministic, polynomial-time test. The paper's algorithm is elementary - six steps: reject perfect powers; fix a small r; reject trivial factor witnesses; accept small inputs; test the congruence (X + a)^n = X^n + a modulo X^r - 1 for a = 1, ..., ell; accept. The mathematical heart is Lemma 2.1, a generalization of Fermat's Little Theorem to polynomial rings: for n at least 2 and a coprime to n, n is prime if and only if (X + a)^n = X^n + a in Z_n[X]. The correctness of the harder direction runs through the introspective machinery of Section 4: for a prime factor p of n with o_r(p) > 1, the numbers of I = {(n/p)^i p^j} are introspective for the polynomials of P = {the products of the generators X, X+1, ..., X+ell}; the residues of I generate a group G modulo r of size t > log^2 n; the images of P generate a group G-cal in the field F = F_p[X]/(h), h an irreducible factor of the r-th cyclotomic polynomial over F_p; Lenstra's lower bound and the Kalai-Sahai-Sudan upper bound on the size of G-cal collide unless n is a power of p, and step 1 excludes prime powers, so n is prime. Section 5 bounds the arithmetic work: O~(log^(21/2) n), unconditionally.
The mission formalizes the paper's mathematical content in Lean 4. The goal statement is Theorem 4.1: the algorithm of the algorithm layer returns PRIME if and only if n is prime. The milestones are the ingredients in attack order: the polynomial Fermat characterization (Lemma 2.1); the lcm lower bound (Lemma 3.1); the existence of a small r with large order (Lemma 4.3); the closure of introspection under multiplication (Lemmas 4.5 and 4.6); Lenstra's injectivity bound (Lemma 4.7); the Kalai-Sahai-Sudan collision bound (Lemma 4.8); and the polynomial work bound of Section 5 (Theorem 5.1, in generous integer form).
The source document is the uploaded paper (annals-v160-n2-p12.pdf in the mission materials).
The formalization is a two-layer development in the namespace AKS. The polynomial layer (AKS_poly) carries the congruences: congruence (1) as an equality in Z_n[X], congruence (2) as divisibility by X^r - 1 in Z_n[X], Definition 4.4's introspection relation over F_p[X], and the set P of products of the generators. The algorithm layer (AKS_alg) carries the arithmetic scaffolding and the algorithm itself: the integer logarithm, the multiplicative order, the lcm of the first numbers, the perfect-power predicate, the search for r, the loop bound, the six-step decision function, the set I and the residue group G, and the work measure of Section 5.
The following choices are disclosed explicitly.
Compile verification by CI substitution. The authoring environment has no local Lean toolchain, so the compile check demanded by the mission is performed by the continuous integration of the repository (Lean 4.33 with Mathlib): all Lean code below was compiled there before this proposal was submitted, and the code attached to the items is byte-identical to the compiled modules.
The theorem drafts carry sorry. The eight theorem statements are submitted as drafts for human review; each proof body is a single sorry marking the work the mission proposes to complete. The compilation therefore succeeds with exactly one "declaration uses 'sorry'" warning per theorem file.
Generous integer encodings of the logarithms. The paper's real-valued log n appears in the algorithm only through the threshold o_r(n) > log^2 n of step 2 and the loop bound ell = floor(sqrt(phi(r)) log n) of step 5. The mission encodes both with logUp n = floor(log2 n) + 1, which is strictly larger than log2 n: step 2 searches for the smallest r with ordR r n > logUp(n)^2, and ell is the floor of the product of the square root of phi(r) and logUp n, encoded exactly as the floor of the square root of phi(r) logUp(n)^2. Both encodings are generous in the directions that preserve correctness: primes pass congruence (2) for every a and r, so a larger threshold and a longer loop never reject a prime; and for the converse the larger threshold and loop only strengthen the group bounds that force composites out. The integer bookkeeping of the final chain - floor(sqrt t) logUp n + 1 at least sqrt t log2 n - is part of the proposed work of the goal, with the generosity supplying the slack.
The algorithm layer transcribes the six steps literally, with computable searches inside provable windows and classical decision where only the extension matters. ordR r a is the least k < r with a^k = 1 (mod r) - the window k < r is faithful because every multiplicative order divides phi(r) < r - and 0 when gcd(a, r) > 1. smallestR n searches the window bounded by the r_exists milestone's bound. aksDecide is stated with classical decision (open Classical, noncomputable): no execution of the test is ever needed, only its extensional behavior. aksWork is a computable schoolbook work measure charging logUp(n)^6 for step 1, r(logUp n + 1) for the searches of steps 2 and 3, and ell r n (logUp n + 1)(r + 1)^2 for the congruence loop of step 5.
The groups are encoded by witness windows, and the two bounds are stated in the paper's forms. G is the Finset of residues modulo r of the numbers of I, encoded by the witness window i, j < r - faithful under the coprimality of n/p and p to r, because both orders then divide phi(r) at most r, so every residue of an I-number is achieved inside the window. Lemma 4.7 is stated in the paper's form: two distinct polynomials of P, both of degree less than t, map to distinct elements of F = F_p[X]/(h) (the field is AdjoinRoot h; the hypotheses carry h dividing X^r - 1, the primitivity - h not dividing X^k - 1 for 0 < k < r - irreducibility by instance, the introspectivity of I for P, and t at most the size of G). Lemma 4.8 is stated in the collision form: unless n is a power of p, there are m2 < m1 at most n^(floor(sqrt t)), colliding modulo r inside the bounded set I-hat, such that every image of P in F satisfies y^m1 = y^m2. The cardinality bookkeeping between these forms and the size of G-cal - stars-and-bars for the lower bound with the unique factorization of the generator products, and the root bound of a polynomial over a field for the upper - is carried by Mathlib and is part of the goal's proposed work.
The field F = F_p[X]/(h) is taken with its factor h as an explicit parameter. The statements do not construct h; they carry h dividing X^r - 1, primitivity, and irreducibility as hypotheses (the latter two as Fact-class instances). The existence of h - an irreducible factor of the r-th cyclotomic polynomial over F_p of degree o_r(p), the standard fact of Lidl and Niederreiter cited as [LN] - is part of the mission's proposed work toward the goal.
The "is in P" claim is anchored by an explicit work measure, with the bit-cost correspondence in prose. Milestone 7 bounds aksWork by C logUp(n)^15, a generous integer form of Theorem 5.1's O~(log^(21/2) n) - the generous exponent absorbs the schoolbook charging model and the logUp slack. The correspondence between arithmetic-work measures and Turing-machine bit complexity - the standard O~(m) arithmetic on m-bit numbers of the paper's Section 5 - is carried in prose; a machine-level formalization is out of scope.
Pruned content. The paper's Section 5 refinements (Fouvry's Lemma 5.2 and the O~(log^(15/2) n) of Theorem 5.3, and the Lenstra-Pomerance variant), the conjectures (Artin's, the Sophie Germain density, Conjecture 6.1), and the historical survey of Section 1 are out of scope; the mission carries the unconditional Section 5 analysis only, in generous integer form, and the correctness theorem (Theorem 4.1) as the goal.
Due diligence. Before creating the proposal, the creation script searches the platform for prior definitions and theorems matching the paper's ingredients; the search results are recorded in the repository's results directory for the reviewer.
Definition names and module stems. The two definition bundles are published under names equal to their module stems (AKS_poly, AKS_alg), so that the platform imports Definitions.Def_AKS_* in the theorem preambles resolve, in dependency order poly, then alg (which imports poly).
The mission has ten items: two reference definitions and eight theorem drafts, in the following order.
Reference definitions (the formalization fragment):
AKS_poly: the polynomial layer. Congruence (1) as the equality (X + a)^n = X^n + a in Z_n[X]; congruence (2) as divisibility by X^r - 1 in Z_n[X]; Definition 4.4's introspection relation over F_p[X]; and the set P of products of the generators X, X+1, ..., X+ell.AKS_alg: the algorithm layer. The integer logarithm logUp; the multiplicative order ordR; the lcm of the first numbers; the perfect-power predicate; the six-step decision function aksDecide with its search smallestR and loop bound ell; the set I and the residue group G; and the work measure aksWork.Theorem drafts (milestones in attack order, then the goal):
AKS.poly_fermat: Lemma 2.1 - for n at least 2 and a coprime to n, n is prime if and only if (X + a)^n = X^n + a in Z_n[X] (Section 2).AKS.lcm_lower: Lemma 3.1 - the lcm of the first m numbers is at least 2^m for m at least 7 (Section 3).AKS.r_exists: Lemma 4.3 - for n > 1 there is an r with 1 < r at most max 3 (logUp n)^5 and ordR r n > logUp(n)^2 (Section 4).AKS.introspective_closure: Lemmas 4.5-4.6 - introspective numbers are closed under products, and introspectivity is closed under products of polynomials (Section 4).AKS.group_inj: Lemma 4.7 (Hendrik Lenstra Jr.) - two distinct polynomials of P, both of degree less than t, map to distinct elements of F = F_p[X]/(h), under the primitivity and introspectivity hypotheses, with t at most the size of the residue group G (Section 4).AKS.group_upper: Lemma 4.8 (Kalai-Sahai-Sudan) - unless n is a power of p, there are m2 < m1 at most n^(floor(sqrt t)), colliding modulo r inside the bounded set I-hat, such that every image of P in F satisfies y^m1 = y^m2 (Section 4).AKS.poly_time: the work bound - there is a constant C with aksWork n at most C logUp(n)^15 for every n, the generous integer form of Theorem 5.1 (Section 5).AKS.prime_iff (the goal): Theorem 4.1 - aksDecide n = PRIME if and only if n is prime (Section 4).Milestones 1 to 7 correspond to the theorem drafts 1 to 7; the goal is draft 8.
The paper is one of the landmark results of computational number theory: a problem open since the 1960s - an unconditional, deterministic, polynomial-time primality test - solved by elementary means, in a proof whose only ingredients are the binomial theorem, Euler's function, and the root bound of a polynomial over a field. The formal account forces exactly what the prose leaves to convention: the precise ring in which each congruence lives, the precise windows in which the searches find their witnesses, the precise generosity of each integer rounding, and the precise content of the two group bounds. The paper's difficulty lies not in any single deep theorem but in the assembly of many small lemmas under one bound chain; a formalization makes each link explicit and checkable, and the mission's readback discipline gives an independent restatement check of every statement before review.
Milestone 1 is a commutation: the forward direction is the freshman's dream in Z_p[X] plus Fermat's little theorem for the base; the backward direction isolates the coefficient of X^q for a prime q with q^k dividing n exactly and computes its q-adic valuation below k. Milestone 2 is Nair's argument: the product of the primes in (m/2, m] divides the lcm. Milestone 3 is the counting argument: every bad r divides a single product below the lcm of the window, so some r in the window escapes. Milestone 4 is two ring commutations: f^(m m') = f(X^(m m')) along f(X^m)^(m') = f(X^(m m')), and the product rule for introspectivity. Milestone 5 is Lenstra's argument: from a collision in F and introspection, f(Y) - g(Y) acquires the t distinct primitive r-th roots indexed by G, exceeding its degree. Milestone 6 is the pigeonhole of I-hat against G, the non-power distinctness, and the collision equation transported by introspection. Milestone 7 is arithmetic over the windows. The goal assembles: Lemma 4.2's direction is the congruences for primes; the step-4 case is the factor below the square root; and the step-6 case is the chain of Lemma 4.9 - the injectivity lower bound, the collision upper bound, and the integer bookkeeping that the generous encodings close with slack.
Included: the two congruences and the introspection relation; the set P and the set I with the residue group G; the six-step algorithm; and the eight statements - the Fermat characterization, the lcm bound, the small-r existence, the two closure lemmas, the two group bounds, the work bound, and the correctness theorem.
Excluded, as disclosed in items 7 and 8 of section 2: the machine-level bit-cost formalization of "is in P" (carried in prose, anchored by the explicit aksWork measure); the Section 5 refinements (Fouvry's Lemma 5.2, the O~(log^(15/2) n) of Theorem 5.3, the Lenstra-Pomerance variant of [LP1]); the conjectures of Section 5 and Conjecture 6.1; and the historical survey of Section 1.
Every value of a fundamental constant used in science — the fine-structure constant, the Newtonian constant of gravitation, the Rydberg constant — comes from one place: the least-squares adjustment periodically carried out by the CODATA Task Group on Fundamental Constants. The 2022 adjustment (P. J. Mohr, D. B. Newell, B. N. Taylor and E. Tiesinga, CODATA recommended values of the fundamental physical constants: 2022) takes 133 input data, determines 79 adjusted constants by weighted least squares with 54 degrees of freedom, applies expansion factors 1.7 and 2.5 to the uncertainties of certain groups of data to reduce all normalized residuals to two or less, obtains a final chi-square of 44.2 with Birge ratio 0.90, treats the sixteen values of the Newtonian constant of gravitation separately (16 data, one adjusted constant, 15 degrees of freedom, chi-square 12.9, expansion factor 3.9, Birge ratio 0.93), and obtains the recommended values from the adjusted constants by propagating their uncertainties and covariances.
The mission formalizes the mathematical skeleton of this process in Lean 4 and audits a representative slice of its output by exact rational arithmetic: the equivalence between minimizers of the chi-square statistic and solutions of the normal equations, the weighted mean as the rank-one case (the situation of the separate adjustment of G), the printed degrees of freedom and Birge ratios, the effect of uncertainty expansion on covariances and correlations, the algebraic laws of relative-uncertainty propagation, the exact derived constants determined by the exact defining values of h, e, k and N_A, and the mutual consistency of the printed uncertainties of the alpha family. The goal theorem packages these into the statement that the 2022 adjustment is self-consistent.
What is being formalized is the statistics and the arithmetic of the adjustment, not any physical measurement: the input data enter only through the abstract structure of a weighted least-squares problem, and the numerical audits compare exact rationals with the digit strings printed in the report's tables.
The source is the 2022 CODATA report in its two identical published versions: J. Phys. Chem. Ref. Data 54, 033105 (2025), doi 10.1063/5.0279860, and Rev. Mod. Phys. 97, 025002 (2025), doi 10.1103/RevModPhys.97.025002. The mission formalizes section XII, "Least-squares adjustment", and the exact and recommended values of Tables XXXII and XXXIII, under the following disclosed conventions.
Twelve conventions deserve disclosure. First, the platform publishes definitions as modules, so the three definition bundles — the least-squares model, the correlations and uncertainty propagation, and the exact rational values — are published as platform definitions (CODATA_lsa, then CODATA_uncert which imports it, and CODATA_values), attached to the proposal as reference items; the theorem drafts import them; and the creation script reads the definition code and the theorem statements directly from the repository modules that the CI has just compiled, so the code posted to the platform is byte-identical to the code whose compilation the CI verified. Second, the two uploaded PDFs are the same paper in its two published versions; citations reference both, and the table numbering follows the Rev. Mod. Phys. version (Tables XXXII-XXXIII, section XII). Third, the observational equations are taken in linear form; the report's observational equations are linear in the adjusted constants to begin with, but the values of the input data, the design matrix entries and the offset vector are interface data, not formalized: the theorems quantify over all weighted least-squares problems of the recorded dimensions. Fourth, the chi-square distribution and the printed probability values (83 percent for the main adjustment, 61 percent for G) are statistical statements about the chi-square distribution; they are printed data of the report and are not constructed, and no probability theory enters the mission. Fifth, the Newtonian constant of gravitation is treated separately, exactly as in the report: a second least-squares structure with sixteen input data and one adjusted constant, its own expansion factor 3.9, and its own Birge ratio; the goal theorem relates the two adjustments only through their common formalism. Sixth, the expansion factors 1.7 and 2.5 of the main adjustment are recorded in the description but not formalized, because the data they modify are interface data; the expansion factor 3.9 of the G adjustment is formalized through the covariance expansion law applied to the abstract covariance matrix of the sixteen values. Seventh, matrix inversion is expressed by two-sided inverse predicates, written entry by entry against the Kronecker delta, rather than through an inverse operator; this keeps the statements elementary and avoids any dependence on matrix inverse lemmas. Eighth, all arithmetic is rational or real: the exact constants are rationals, the derived quantities K_J, R_K, Phi_0, G_0, G_0⁻¹, F, R and the electronvolt are exact rationals, and the printed digit strings are captured by rational rounding intervals; exact quantities carrying a factor of pi (hbar, the Stefan-Boltzmann constant) and quantities with experimental uncertainty outside the audited family (the dalton, the Newtonian constant itself) are excluded because they are not rational. Ninth, the Birge ratios are captured by the rounding intervals [0.895, 0.905) and [0.925, 0.935), which the printed two-digit values 0.90 and 0.93 determine; the true values are sqrt(44.2/54) and sqrt(12.9/15). Tenth, the alpha family audit is an existential: the printed two-significant-digit uncertainties of alpha, 1/alpha, mu_0, eps_0 and Z_0 are jointly reproduced by a single rational relative-uncertainty witness of order 1.6 × 10⁻¹⁰, supplied explicitly by the prover (for example 156/10¹²); this witnesses consistency without asserting the (irrational, distribution-laden) exact relative uncertainty of alpha. Eleventh, the read-backs attached to the theorem drafts were authored by the same model that produced the statements (readback_model glm-5-latest-short); they are a self-check, not an independent audit, and human review of every item is required before submission. Twelfth, everything is developed against the platform's Mathlib build (0df444a); the compilation check of every item is the repository CI, which builds all definitions and theorem drafts with the same Mathlib version (no local Lean toolchain is available to the drafting agent, and this is disclosed).
Eleven items: three published definition bundles attached as references, seven milestone theorem drafts, and the goal theorem.
The CODATA adjustment is the mechanism by which the values of the fundamental constants become internationally accepted, self-consistent numbers; every precision measurement and every physical theory that quotes a constant inherits from it. The mission makes the three layers of the mechanism checkable by a proof assistant: the statistics (the least-squares theorem that the adjustment procedure is, by construction, the unique minimum of the chi-square statistic), the data hygiene (the effect of uncertainty expansion on covariances and correlations, and the propagation laws by which the recommended values and their uncertainties are derived), and the arithmetic (an exact rational audit confirming that the printed digit strings of the derived constants and the printed Birge statistics are consistent with the exact defining values and the reported chi-squares). Because the 2019 SI revision fixed h, e, k and N_A exactly, a growing family of derived constants is a pure rational computation; the mission verifies a representative slice of that family to the printed precision.
The milestones are honest and of mixed difficulty. The normal-equations milestone is the mathematical heart: the chi-square statistic is a quadratic form in the adjusted constants, strict positive definiteness of the weight matrix makes it convex, and the equivalence with the normal equations plus uniqueness at full column rank is a complete weighted least-squares existence-uniqueness argument, carried out entry by entry without matrix inverse lemmas. The weighted-mean milestone is a direct computation in the rank-one case, complicated only by the bookkeeping of the two-sided inverse predicate for the one-by-one normal matrix. The Birge milestone is real arithmetic: two subtractions and two square-root bounds, each reducible to exact rational comparisons by squaring. The expansion and propagation milestones are algebra over the reals: square roots of products of positive reals and the cancellation of equal factors; their difficulty is bookkeeping, not ideas. The derived-values and alpha-family milestones are exact rational computations with numerators and denominators up to thirty digits; they are fully decidable, and their difficulty is the size of the arithmetic — the prover must exhibit the witness ur and verify fifteen rational interval inclusions — for which norm_num-style automation is intended. The goal assembles the parts. Nothing in the mission requires mathematics beyond convexity of a quadratic form and exact rational arithmetic, and this is the point: the CODATA adjustment, the most authoritative computation in metrology, is at its core an auditable exact computation.
Every theorem quantifies only over abstract least-squares structures and rational values; no measurement, no physical theory, and no probability distribution enters. The fragment excludes: the 133 input data as concrete vectors and the 79 adjusted constants as concrete quantities; the chi-square distribution and all probability statements; the least-squares fitting of the theoretical expressions (atomic transition frequencies, muonic Lamb shifts, magnetic-moment anomalies); the 2022-versus-2018 value comparisons and the historical narrative; the mises en pratique and the experimental methods; the electroweak and particle-physics input data; the quantities whose exact values involve pi (hbar, the Stefan-Boltzmann constant) or whose values carry experimental uncertainty outside the audited family; and the correlations among the input data as concrete numbers. What is formalized is the statistical skeleton, the covariance algebra, and the exact rational audit of the printed output.
Quantum Max Cut assigns a qubit to each vertex of a weighted graph and a two-qubit energy term to each edge. It asks for a quantum state with high total energy. The problem is a quantum analogue of graph Max Cut, but states can be entangled and edge terms act on a Hilbert space whose dimension grows exponentially with the number of vertices. Approximation algorithms therefore need a compact way to reason about the best quantum state without describing that state explicitly. Gharibian and Parekh's 2019 algorithm used product-state rounding for a quantum Max Cut relaxation; Parekh and Thompson's level-2 work showed why stronger quantum relaxations matter. The present paper combines a level-2 relaxation with a different treatment of highly valued edges to obtain a one-half guarantee.
The target is a known result from the pinned version arXiv:2206.08342v2, not an open conjecture. This mission isolates its Quantum Max Cut theorem. The paper also treats other positive 2-local Hamiltonians and a separate guarantee for graphs of prescribed minimum degree; neither is part of this target.
Let be a finite undirected graph with a nonnegative weight on each edge, and put one qubit at each vertex. Write for the three Pauli operators acting on qubit . The edge Hamiltonian and total Quantum Max Cut Hamiltonian are
Every undirected edge appears once. A density matrix is positive semidefinite with trace one. Its energy is , and is the largest energy attainable by any density matrix, including an entangled one.
A Pauli polynomial is a real linear combination of tensor products of . A monomial's degree counts its nonidentity factors. A -positive pseudo-density is Hermitian, has trace one, and satisfies for every Pauli polynomial of degree at most . The level-2 quantum Lasserre relaxation maximizes over all such pseudo-densities. It is an upper bound on the unrestricted quantum optimum, even though itself need not be positive semidefinite. These definitions are from pp. 6–8 of the paper.
For an edge, its relaxed value is . The rescaled value is defined by . Algorithm 4 chooses a threshold , puts every edge with in , and calls vertices incident to no edge in the set . It assigns the two-qubit mixed state to each edge in . Vertices in receive single-qubit states obtained by normalizing three independent Gaussian projections of the relaxation's rounding vectors. The output is the product of those factors, as in equation (5), p. 14. The large edges form a matching at the selected threshold, so those factors occupy disjoint qubits. The Gaussian draw is the algorithm's only randomness.
The goal is the paper's Theorem 3, p. 17. A single threshold must work for every graph and every nonnegative edge weighting:
The level-2 solution used by Algorithm 4 is optimal for the given . The goal also says that the matrix output is a density matrix for every Gaussian outcome. Its threshold is existential because the theorem does not fix a decimal constant; the paper subsequently selects for its analysis.
The fourteen milestones follow the order in which the proof of Theorem 3 uses them.
Equation (7) (p. 17): Gaussian product-state rounding earns in expectation on edge . Lemma 6 (p. 18) reduces to two checks at ; Definition 13 (p. 19) asserts that passes them; Fact 1 (p. 16) is the resulting factor on edges with both ends in . 3. Monogamy. The SWAP Gram matrix of three qubits is positive semidefinite (p. 20). Lemma 8 (p. 22): and imply . Fact 2 (p. 16): if then . Remark 3 (p. 19): the large edges form a matching. 4. Edges touching . Equation (12) (p. 19): earns on a large edge. The last display of the proof of Theorem 3 (p. 19): an edge adjacent to earns exactly .
The theorem guarantees half of the optimum over all quantum states while returning a state built from one- and two-qubit product factors. This is stronger than a guarantee relative only to the best product state: the benchmark permits entanglement. It also explains why a level-2 relaxation has algorithmic value for this problem. The comparison and the claimed approximation factor are established in the paper; formalizing them would leave a reusable verified interface for finite-qubit Pauli polynomials, pseudo-densities, and Gaussian product-state rounding.
The formal work still needed is a machine-checked proof of the known theorem and its milestones. The published register, Pauli, density-matrix and standard-Gaussian-vector definitions can be reused. The source's separate results for other positive 2-local Hamiltonians would need additional models and theorems, beyond this mission.
Level-1 Gaussian product-state rounding alone does not reach one half uniformly: the paper identifies an edge range where its ratio falls below . Large edge values cannot be handled by the same rounding estimate. A level-2 pseudo-density supplies stronger constraints between adjacent edges, but it is not itself a physical state, so ordinary positivity of is unavailable. The source's SWAP matrix and threshold analysis express the needed restrictions. The paper's printed dual certificate for Lemma 8 has a coordinate-order erratum; the lemma's statement remains the target.
Qubits are indexed by Fin n (the paper uses ), with basis Fin n → Bool. Operators are complex matrices. The real part of a trace represents the expectation of a Hermitian expression. The maximum eigenvalue is stated through comparison with every density matrix; for Hermitian , this is equivalent to comparing with its largest eigenvalue. Expected energy is a Bochner integral over a probability measure carrying independent standard Gaussian coordinates. A zero Gaussian projection is assigned Bloch vector zero, giving the maximally mixed one-qubit state at that outcome.
The rounding vectors are given with unit norms and exactly the Gram matrix obtained from the level-2 solution. The output state is computed as the matrix product in equation (5); energy is traced against that matrix. Positivity is required for every real degree-2 Pauli polynomial, and the pseudo-density is required to be optimal. These choices exclude vacuous variants based on degree-1 positivity, free Bloch vectors, or edge energies supplied as assumptions. The finite operator model also covers an empty graph; the approximation inequality there is .
The statement formalizes the approximation guarantee and state validity. The polynomial running-time clause of the paper's general approximation definition is outside this Lean statement. Reusable contributions include the Pauli-polynomial interface, matrix and moment identities for pseudo-densities, integrability and measurability facts for the Gaussian rounding, and the SWAP semidefinite bound.
Gelfand duality identifies compact Hausdorff spaces with commutative unital C*-algebras: a space corresponds to the algebra of continuous complex functions, and continuous maps correspond contravariantly to unital *-homomorphisms (Gelfand 1941; in categorical form, Negrepontis 1971). Measure theory has an analogous expectation. A measurable space with a σ-ideal of negligible sets yields the commutative von Neumann algebra of bounded measurable functions modulo equality almost everywhere, and every commutative von Neumann algebra should arise in this way. Making that expectation precise as an equivalence of categories requires deciding which measurable spaces to allow and which maps between them to identify.
Timeline. Stone (1936–1937) established the duality between Boolean algebras and Stone spaces, and between complete Boolean algebras and extremally disconnected ones. Segal (1951) introduced localizable measure spaces. Dixmier (1951) characterized the Gelfand spectra of commutative von Neumann algebras as the hyperstonean spaces. Loomis (1947) and Sikorski (1948) represented σ-complete Boolean algebras as measurable sets modulo meager sets on their Stone spaces. Von Neumann (1932), Maharam (1958), Ionescu Tulcea (1965), Vesterstrøm–Wils (1969), Edgar (1976) and Graf (1980) gave criteria for lifting homomorphisms of measure algebras to point maps. Pavlov (arXiv:2005.05284, J. Pure Appl. Algebra) assembled these ingredients into one equivalence of categories. That equivalence is the subject of this mission.
An enhanced measurable space is a set , a σ-algebra of subsets of , and a σ-ideal of the power set , the negligible sets. A premap is a map defined on a conegligible subset of with and . Two premaps are weakly equal almost everywhere, , when for every . The space is compact if some compact class (a family with the finite intersection property for all subfamilies) has a non-negligible member inside every non-negligible measurable set. It is strictly localizable if it is isomorphic, through premaps, to a coproduct of a small family of spaces carrying faithful finite measures. CSLEMS is the category of compact strictly localizable spaces with -classes of premaps.
A frame is a complete lattice in which finite meets distribute over arbitrary joins; the category of locales is the opposite of the category of frames. A complete Boolean algebra is localizable if is the supremum of the elements for which carries a finite faithful continuous valuation. MLoc, the category of measurable locales, is the full subcategory of locales on the localizable Boolean algebras. A hyperstonean locale is a Stonean locale (coherent, regular, ) in which every nonzero open has a positive normal valuation not vanishing on it. A hyperstonean space is a sober space whose locale of opens is hyperstonean. HStoneanLoc and HStonean take open maps as morphisms. CVNA is the category of commutative von Neumann algebras (C*-algebras with a predual) and normal unital *-homomorphisms.
The goal is the existence of the four equivalences. It does not fix the functors.
The supporting milestones, in proof order:
The result. Theorem 1.1 replaces commutative von Neumann algebras, a class of operator algebras, by measurable locales, which are pointless spaces. It also gives a point-set model, CSLEMS, in which morphisms are measurable maps modulo a null relation. With it, constructions on commutative von Neumann algebras can be carried out measure-theoretically and transported back: products, pushforwards of measures, and the identification of the predual with valuations. It also explains why the obvious choices fail. With localizable instead of strictly localizable spaces, with equality almost everywhere instead of weak equality, or without compactness, the measure-theoretic category is not dual to CVNA (Remarks 4.23 and 5.18).
Formalization. The theorem is proved in the paper. None of the five categories, and none of the equivalences, has a machine-checked form in Mathlib or on the platform. Mathlib has W*-algebras (WStarAlgebra), locales, Stonean spaces and Baire-measurable sets, but no normal homomorphisms, measure algebras or lifting theorems. The published module QAlgorithms_Papers_Independent_Support21_P20 formalizes this paper's valuations, enhanced measurable spaces and premaps, and poses several lemmas, three of which are milestones here. Completing the mission means formalizing Stone and Stonean duality for locales, the spectral theory of commutative von Neumann algebras through projections, and the von Neumann–Maharam lifting theorem for strictly localizable spaces.
The equivalences in §2 restrict classical dualities and are mostly bookkeeping once those dualities are available. Even so, Mathlib's Stone duality is not stated for locales with open maps. The central difficulty is Proposition 5.16. An object of CSLEMS must be isomorphic, through point maps, to the Stone spectrum of its own measure algebra. In one direction this needs a lifting that is a Boolean homomorphism, and that uses strict localizability through the von Neumann–Maharam theorem. In the other direction it needs a point map from the spectrum back to , constructed from the compact class. The natural first idea, choosing representatives class by class, does not give a homomorphism: liftings exist only through a transfinite construction. A second difficulty is Lemma 5.11. A Boolean homomorphism induced by a measurable map preserves countable suprema, but in general it does not preserve arbitrary ones (Remark 5.12). Compactness and the measurable image of Proposition 4.65 are what rule this out.
All five categories live in one universe, with objects in Type u. The encoding commits to these conventions:
X → Option Y) modulo weak equality almost everywhere. Theorem 1.1's bullet speaks of maps of sets, but with total maps the theorem is false: has no map to (Remarks 4.9, 4.15). Strict localizability uses a small index family and isomorphism in PreEMS; the faithful finite measures of its σ-finite pieces are countably additive maps with absolutely convergent sums (Remark 4.29), because Definition 4.28's saturation clause alone would also admit merely finitely additive ones. Compactness quantifies over arbitrary subfamilies, not countable ones.Locale on localizable Boolean algebras.CStarAlgebras with WStarAlgebra. Normality is stated as "pulls normal functionals back to normal functionals", which is equivalent to Definition 3.3 by Sakai's uniqueness of the predual.The equivalence milestones assert an equivalence together with a description of its functor. They never take a functor as a hypothesis, so none of the statements reduces to rfl or to an instance argument.
Reusable parts:
Contributions are welcome at every level: proofs of the milestones, Stone and Stonean duality for locales, and a lifting theorem.
In quantum mechanics, a system that interacts with an environment is described by a density matrix: a positive semidefinite complex matrix of trace one. When nothing is known about the joint state of the system and its environment, a natural model is to take that joint state to be a uniformly random pure state and to trace out the environment. The resulting law on density matrices, the induced measure of Życzkowski and Sommers (Życzkowski–Sommers 2001), is a standard model of a "typical" mixed state. It is used in quantum information to study the typical entanglement of bipartite pure states, as in Page's conjecture on average entropy (Page 1993).
Nechita (arXiv:quant-ph/0702154v3, Ann. Henri Poincaré 2007) studies the asymptotics of this ensemble. In the regime where the system dimension and the environment dimension grow proportionally, the spectrum of the random density matrix, magnified by , has the same almost sure limit as the spectrum of a Wishart matrix: the Marchenko–Pastur law (Marchenko–Pastur 1967). The mission formalizes this result (Theorem 5) together with the chain of statements the paper uses to derive it.
Throughout, denotes the law of where are independent real Gaussians of mean and variance , so that .
is the induced measure on density matrices. Here is the partial trace over the environment.
Let , let be integers with , and let have law for every . Then, almost surely,
The result. Theorem 5 says that the reduced state of a large random bipartite pure state has a deterministic spectral profile at scale . When , the environment is smaller than the system, and an atom of mass at records that has rank . When , the spectrum fills the interval . The result transfers the classical Wishart limit to the induced measure, and with it quantitative information on the typical entanglement spectrum of bipartite pure states.
Formalizing it. The theorem is proved on paper, and none of it is machine-checked. The mission produces the induced-measure layer in Lean: complex Gaussian matrices, the invariant law on pure states, the partial-trace construction of , and the Marchenko–Pastur law with its atom. Lemma 1 and eq. (12) connect these objects to Wishart matrices. The step that needs the most new library is Theorem 2, the Marchenko–Pastur theorem itself, which the paper quotes without proof. The perturbation step is posed as a statement about weak convergence. The paper argues it through convergence of moments, and in that argument weak convergence of is used as if it gave convergence of moments. The statement posed here is true as stated and needs no moment control.
The reduction from Theorem 5 to Theorem 2 is short on paper. The work lies elsewhere.
The naive route of "taking moments" in the perturbation step fails: weak convergence does not give convergence of moments, so (52)–(53) cannot be compared without extra tightness or moment bounds.
IsPureDensity: Hermitian, idempotent, trace one). A law on is a probability measure on complex matrices carried by that set. Unitary invariance is invariance under (IsPureStateLaw).HasInducedLaw: the law of is the image under the partial trace of some unitarily invariant law on pure states of . Proposition 1 makes this law unique.Fin n × Fin k with the environment on the right. The partial trace is the published WildeQIT.partialTraceRight. is the published SpikedWishart.SoftEdge.stdComplexGaussian, with variance per real coordinate.Solvers are welcome to contribute in four places:
The ultimate rates of quantum communication over optical fibre — how many secret bits or entangled pairs per channel use a lossy line can carry with unlimited local operations and classical communication (LOCC) — are bounded through a technique called teleportation stretching (Pirandola, Laurenza, Ottaviani, Banchi, arXiv:1510.08863). The idea is that if a channel can be simulated by teleporting its input through a fixed resource state , then any adaptive protocol using times can be rewritten as LOCC acting on , and every LOCC monotone of bounds the protocol's output.
For the pure-loss channel the natural resource is the Choi state of an ideal Einstein–Podolsky–Rosen state, which is not a normalizable state: it is the limit of two-mode squeezed states and has infinite energy. R. Namiki (arXiv:1603.05292, 2016) observed that this limit can be avoided for lossy channels. Finite-squeezing teleportation, in the Braunstein–Kimble scheme (Braunstein and Kimble, PRL 80, 869, 1998), does not teleport perfectly, but its imperfection is itself a pure loss. Composing it with a second pure-loss channel therefore reproduces the target channel exactly, with a finite-energy resource.
A single bosonic mode is described on the Fock space with number basis . Every operator is handled through its number-basis kernel ; an operator on two modes has kernel , the first index labelling the first mode.
Alice holds a two-mode state ( the signal, a reference) and Alice and Bob share a resource . The unnormalized branch for outcome is the kernel on
For put and , the effective Choi state. For every two-mode density ,
entry by entry, with every series and integral convergent, and . The parameters and the protocol are independent of .
The result. The Theorem shows that one use of a pure-loss channel, on any input including half of an entangled state, is reproduced exactly by LOCC on the finite-energy state . In the paper's §II.C this is the step that would let entanglement-measure bounds for adaptive channel uses be evaluated on a genuine density operator, without the limit that the ideal-EPR argument needs. The relation (24) also makes precise in which sense the realistic teleportation family is not teleportation-stretching in the finite-dimensional sense, yet simulates the channel after an outcome-dependent displacement.
Formalizing it. The result is proved in the paper by a short computation through the Glauber–Sudarshan representation, which is heuristic for nonclassical inputs. No machine-checked version exists. A formal proof requires an argument valid for every density operator, together with all convergence statements. The formalization also records a sign slip: with the paper's own definitions (4), (16), (A4) and , the step in (20) should read . Consequently (20) and (23) hold with in place of , and the correction in (24) is rather than ; a numerical evaluation of the printed (24) for the input gives an error of in the output matrix, against (grid-limited) for the corrected one. The Theorem itself, existential in the protocol, is unaffected.
The obvious route is the paper's: write , compute everything for coherent states, and integrate. For nonclassical states is not a function, or even a measure, so this route is not a proof; passing from coherent inputs to all densities needs a density or continuity argument in trace norm, with interchange of the outcome integral and the infinite Fock series. The Bell projection itself is a contraction against improper vectors, here encoded as an absolutely convergent four-fold series whose convergence for arbitrary trace-class inputs is part of the work. Finally, the composition and the covariance (18) are standard on covariance matrices but must be established on number-basis kernels, where they are identities between infinite series with binomial weights.
QAlgorithms_Papers_Independent_Dependency50_P39; the loss channel is the vacuum-loss kernel of QAlgorithms_Papers_Independent_Frontier30_P21; coherent states use its coherentDensity.Frontier30.P21.coherentOutput and is not posed again.Quantum technologies usually prepare a desired state by isolating a system and driving it with carefully timed unitary operations; coupling to an environment is treated as noise. Dissipative state preparation reverses this view: one engineers the system–environment coupling so that the open-system dynamics itself drives every initial state into a prescribed target state. Because the target is a fixed point that attracts all initial conditions, the preparation needs no initialization and is self-correcting against perturbations that leave the dynamics unchanged.
In 2008 three closely related papers made this programme concrete. Diehl, Micheli, Kantian, Kraus, Büchler and Zoller showed how cold atoms can be driven into condensed many-body states by engineered dissipation (arXiv:0803.1482); Verstraete, Wolf and Cirac showed that dissipative dynamics can perform universal quantum computation and prepare matrix product and PEPS states (arXiv:0803.1447); and Kraus, Büchler, Diehl, Kantian, Micheli and Zoller, Preparation of entangled states by quantum Markov processes (arXiv:0803.1463), gave the general uniqueness criteria and the explicit construction this mission formalizes. The last paper's central claim is that every pure state of qubits is the unique stationary state of an explicitly given Markovian process, and that this process relaxes on a time scale independent of .
A quantum Markov process on a -dimensional Hilbert space is a master equation for a density matrix (a positive semidefinite complex matrix of trace one). In the paper's Eq. (2) the generator, or Liouvillian, is
where is a Hermitian matrix (the Hamiltonian), the are arbitrary complex matrices (the jump operators) and are rates. The solution is . The paper writes , and .
A stationary state is a density matrix with . A vector annihilated by every and an eigenvector of is a dark vector; the set of dark vectors, when it is a subspace (all dark vectors share one eigenvalue of ), yields the dark states, the density matrices with range inside .
For qubits, lowers qubit from to . Given any unitary , the target is , which ranges over all pure states, and the construction of §IV uses the jump operators with rates . The relaxation time is the inverse of the least value of over the nonzero eigenvalues of .
For , any unitary and rates :
Clause (a) allows every Hamiltonian that has the target as an eigenvector; (b) and (c) concern the purely dissipative process , the one the paper solves explicitly.
The result. The goal shows that dissipative preparation is universal for pure states: no pure state, however entangled, is out of reach, and the required jump operators are written down explicitly. Clause (c) states that the time to reach the target is governed by the weakest single coupling and does not grow with the number of qubits. Theorems 1 and 2 are general tools independent of the construction: Theorem 1 characterizes every pure stationary state of every Lindblad generator, and Theorem 2 is a checkable sufficient condition for the absence of other stationary states. The later sections of the paper (stabilizer and graph states, PEPS and the AKLT state, a driven condensate, the -condensate) apply these tools to physically local processes.
Formalizing it. The results are classical and proved in the paper, partly in sketched form ("straightforward", "the same arguments as above"). No machine-checked proof of any of them is known. The formalization supplies complete arguments for the sketched steps, fixes the guards the printed statements omit (listed below), and produces a reusable layer of statements about the spectrum and stationary states of Lindblad generators on finite-dimensional spaces.
The first idea for uniqueness is to show that the target is the only pure stationary state, using Theorem 1. That is not enough: a Lindblad generator can have mixed stationary states even when its pure stationary state is unique (with Hermitian jump operators the maximally mixed state is always stationary, Eq. (4)). Excluding mixed stationary states is the content of Theorem 2, whose proof requires a positivity argument for and a decomposition of along .
For convergence, uniqueness of the stationary state does not suffice either: a purely imaginary eigenvalue would make oscillate forever. Clauses (b) and (c) need the full spectrum of the -dimensional Liouvillian, obtained by reducing to and decoupling into single-qubit problems; in Lean this means relating the eigenvalues of a generator on matrices to those of tensor factors.
The generator, the semigroup (matrix exponential of the Liouvillian as a linear map), and the predicates stationary (density matrix with ), attractive and lazy (nonzero subspace invariant under all jump operators) are reused from the published definition QAlgorithms_Papers_Independent_Dependency50_P16. That layer normalizes the dissipator as ; the paper's rates enter through jump operators , which reproduces Eq. (2) exactly. Operators are complex matrices, states are vectors in , and qubits are indexed by with qubit 1 the most significant bit; is the basis vector of index . Density matrices are positive semidefinite of trace one, and is formed without normalization, so unit norm is assumed where the paper says "state". Convergence is entrywise.
Conventions added to the paper and disclosed in each statement:
A trivializing formalization is ruled out: the target is not fixed to , the jump operators are the conjugated and not , clause (a) quantifies over all Hamiltonians with the target as eigenvector rather than only , and the relaxation time refers to the actual nonzero spectrum of the generator.
A complete development needs: properties of the Lindblad generator under unitary conjugation; positivity arguments for completely positive maps on matrices; the tensor-product structure of matrices over qubit wires; and the spectrum and diagonalizability of a sum of commuting single-site generators. The spectral and stationary-state lemmas are reusable for any finite-dimensional open-system mission. Contributions to any milestone, and alternative proofs of Theorem 2 or of the spectrum, are welcome.
In a system driven away from equilibrium, a force changes a reference state and a dynamics, while a corresponding flux records the transported quantity. Statistical mechanics asks how the mean flux changes under a small force. A second question is whether the matrix of these changes is symmetric when the underlying dynamics admit time reversal. Jakšić, Pillet and Rey-Bellet derive both answers at a fixed, finite observation time from a generalized Evans–Searles fluctuation symmetry for classical dynamical systems in their 2010 preprint, §4. This finite-time statement does not require a large-time limit, a stationary nonequilibrium state, or an asymptotic fluctuation theorem.
The paper first develops the entropy cocycle and its time-reversal properties for a single system. Its Proposition 3.3 gives a scalar finite-time Evans–Searles identity. Section 4 lets the dynamics and reference state depend on a vector of forces and introduces a vector of fluxes. Proposition 4.6, the target here, is the section’s stated finite-time Green–Kubo and Onsager result Jakšić, Pillet and Rey-Bellet, pp. 18–21.
Fix a positive integer and a measurable configuration space . Each force vector determines a continuous-time measurable flow , a probability state , and an entropy-production observable . The evolved states of each system are equivalent to , and the regularity assumption (E1) makes the derivative of the evolved-state density in . The family also has a measurable flux vector satisfying the flux relation almost everywhere. These are the family and flux conventions of §4.1 Jakšić, Pillet and Rey-Bellet, pp. 17–18.
At equilibrium, . Assumption (T1) says only that is invariant under ; no stationarity is imposed on for nonzero . Assumption (T2) gives each -system a possibly different time reversal preserving , reversing the flow, and sending to almost everywhere. For , the -system time average is
and its force derivative at equilibrium is . The equilibrium correlation with indices is . Thus the time-shifted factor carries index .
The generalized Evans–Searles functional is the log-Laplace transform of the actual integrated flux,
with extended real values when the exponential moment diverges. Proposition 4.3 states under (T1)–(T2) Jakšić, Pillet and Rey-Bellet, p. 19.
Proposition 4.2 relates the law of the averaged flux to its reflection for nonzero : . Proposition 4.3 states the equivalent symmetry of . Lemma 4.4 is a calculus statement about a function with that symmetry. These are the three new numbered milestones; the earlier entropy-cocycle results, Propositions 3.1, 3.2 and 3.8, are reused as published references Jakšić, Pillet and Rey-Bellet, pp. 8–12, 19.
The goal is all of Proposition 4.6, at each fixed :
The first clause is the paper’s assumption (T3) as a conclusion. The second is the finite-time Green–Kubo formula and the third the finite-time Onsager reciprocity relation Jakšić, Pillet and Rey-Bellet, pp. 20–21.
The formula determines the first-order response matrix from correlations measured entirely in the equilibrium system. Its triangular weight records a finite observation window. Reciprocity then says that cross-responses agree after exchanging the flux and force coordinates. Both statements are exact at fixed time, so they can be used before an asymptotic transport coefficient is known to exist Jakšić, Pillet and Rey-Bellet, Proposition 4.6 and Remarks 1–2, pp. 20–21.
The paper proves these claims. The formalization task is to express and eventually verify the known result, including the dependent family of states and flows, the extended log moment, and all three clauses of the proposition. The published §3 definitions and cocycle statements provide a reusable base. A checked §4 development would also expose general measure and calculus lemmas for finite-time fluctuation relations. At drafting, these new statements compile as open Lean theorems; compilation does not supply their proofs.
The symmetry is an equality of potentially infinite log moments, while the response matrix uses real derivatives near the origin. Local finiteness must justify passage between those two regimes. The paper’s convention includes five families of continuous partial derivatives, including both orders of mixed differentiation, but does not demand two derivatives. Treating it as ordinary would change the theorem.
There is also a measure-theoretic gap between a time integral of fluxes inside an expectation and an integral of expectations over time. A formal statement must control that interchange and the two-time correlation integral. Stationarity is available only at equilibrium, although both the state and flow vary with in the response derivative. The one-line formula for on p. 20 leaves its state implicit; the first display of the proof on p. 21 and the entropy balance used in (4.30) identify it as the -system state for Jakšić, Pillet and Rey-Bellet, pp. 20–21.
The Lean family uses as Fin N → ℝ with , a measurable type , and one published RegularSystem M for each . That type supplies (F1), (F2), (C), and (E1); the new family supplies the flux relation and almost-everywhere time integrability of each coordinate on finite intervals, so the paper's integrated flux is defined. Observable identities in the flux relation and time reversal are -almost everywhere. The law is the pushforward of under the integrated flux divided by . The log-Laplace transform uses a nonnegative integral and EReal, retaining ; a real conversion occurs only on a neighborhood where finiteness is stated.
The goal requires , since its triangular kernel and time average refer to . Proposition 4.2 requires because otherwise contains a division by zero; Proposition 4.3 includes . To make the correlation and Fubini steps meaningful, equilibrium flux coordinates are assumed in and the -system flux is locally integrable on near . These are labeled analytic hypotheses, not new physical symmetry assumptions. Coordinate partials are derivatives along coordinate lines, with existence as well as continuity asserted for the five families on an open neighborhood.
The target uses the actual log-Laplace transform and the force derivative of the actual time average. It imposes stationarity only at , uses equilibrium correlations, and keeps precisely regularity. The family interface and the calculus and integration lemmas needed to prove the milestones are reusable; contributions that close any of the numbered milestones or the analytic interchange obligations fit this scope.
Integrals of polynomial functions of the matrix entries of a random element of a compact group appear across mathematical physics and probability: in random matrix theory (moments of Haar-distributed unitary, orthogonal and symplectic matrices), in lattice gauge theory (the link integrals of gauge fields), and in quantum information (averages of quantum channels over random unitaries, twirling, unitary designs). Weingarten first computed asymptotics of such integrals for in 1978 (Weingarten, J. Math. Phys. 19 (1978)); Collins (IMRN 2003) and Collins–Śniady (CMP 2006) gave exact formulas for the unitary, orthogonal and symplectic groups in terms of what is now called the Weingarten function.
The survey of Collins, Matsumoto and Novak, The Weingarten Calculus (arXiv:2109.14890), isolates the single statement underneath all these formulas, valid for every compact group and every finite-dimensional unitary representation. This mission formalizes that statement, Theorem 2.1 of the survey, together with the steps of its proof as written in Section 2.
Let be a compact Hausdorff topological group and its Haar probability measure, the unique Borel probability measure on invariant under left translation. Let with its standard orthonormal basis , and let be a continuous group homomorphism into the unitary matrices. Its matrix elements are , the entry of .
Fix . A multi-index is a function ; the set of them is . The Weingarten integrals of degree are
The tensor power has the orthonormal basis , and the tensor-power matrix has entries . The invariant tensors are
and the Haar average is the matrix . Given vectors , let be the matrix whose columns are their coordinates, its conjugate transpose, their Gram matrix, and, when it is invertible, the Weingarten matrix of .
If is a basis of , then for all
The identity is exact and holds for every compact group, every continuous unitary representation, every degree and every choice of basis; nothing is fixed beyond the data.
Theorem 2.1 reduces a family of analytic problems — Haar integrals of polynomials in matrix entries — to two algebraic ones: find a basis of the invariant tensors of in (classical invariant theory), and invert its Gram matrix. For the invariants come from Schur–Weyl duality and the Weingarten matrix becomes the Weingarten function on permutations; for and the invariants are indexed by pair partitions; for the symmetric group acting by permutation matrices the invariants are indicators of set partitions. Each of these case-specific formulas, surveyed in Sections 3–5 of the paper, is an instance of Theorem 2.1, so a formal proof of the theorem is the common entry point for formalizing any of them.
The theorem is classical and its proof is elementary once stated; it is not open. No machine-checked proof is known to exist in Mathlib or on this platform: Mathlib has Haar measure, unitary groups and Gram matrices (including the equivalence of linear independence with invertibility of the Gram matrix), but not the averaging projection of a representation in matrix form nor the formula for orthogonal projections. The mission produces both as reusable lemmas and the Fundamental Theorem itself.
The argument is short on paper; the formal work sits in three places. First, selfadjointness of needs , i.e. unimodularity of a compact group, which Mathlib does not provide as an instance for non-commutative groups. Second, identifying the image of with the invariant tensors needs both directions: invariant vectors are fixed by , and every vector is invariant, which uses left invariance of inside a matrix-valued Bochner integral. Third, the projection formula needs invertibility of from linear independence and an argument that a selfadjoint idempotent is determined by its image. Commuting the integral with matrix entries and products is routine but must be done with care for the matrix norm chosen.
G →* Matrix.unitaryGroup (Fin N) ℂ, assumed continuous. Indices are 0-based: is Fin N, multi-indices are Fin d → Fin N, tensors are (Fin d → Fin N) → ℂ.[IsTopologicalGroup G] [CompactSpace G] [T2Space G] [BorelSpace G], and is a Haar measure that is a probability measure. Right invariance is not assumed; it is a consequence that solvers must prove.LinearIndependent ℂ a and span (range a) = invariants U d, with the invariant subspace defined from the representation. Without independence Mathlib's matrix inverse returns on a singular Gram matrix, and the statement would be false; it is therefore not a trivializing gap but a necessary hypothesis.Needed infrastructure: matrix-valued Bochner integrals commuting with entries and with matrix multiplication; unimodularity of compact groups; the orthogonal-projection formula. All three are reusable well beyond this mission, and contributions of these general lemmas are welcome.