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?
Traffic models in transportation and network design come in two kinds. Nonatomic congestion games, with Wardrop equilibria, treat traffic as a continuum of infinitesimal users. Atomic games have finitely many players, each with a non-negligible effect on congestion. The Wardrop model is the one used in practice, and the usual justification is that it is the limit of atomic games as the number of players grows. Cominetti, Scarsini, Schröder and Stier-Moses (arXiv:2001.02797v7, forthcoming in Mathematics of Operations Research) make this precise in two regimes. In the first, the players' weights vanish. In the second, each player is present only with a small probability.
This mission is about the second regime, Bernoulli congestion games. Each of many potential users takes part only with a small probability, for example a commuter who may or may not travel on a given day. The limit is a Wardrop model for the mean flows, but with modified costs, and the flows themselves stay random: they are Poisson. This links Wardrop equilibria with Myerson's Poisson games (Myerson 1998).
A congestion structure consists of a finite set of resources, each with a cost that is nonnegative and weakly increasing on , and a finite set of types. Each type has a nonempty family of feasible strategies.
In the nonatomic game with demands , a strategy flow and a load vector are feasible, , when , and . A feasible pair is a Wardrop equilibrium for costs when every used strategy is cheapest: implies for all .
A Bernoulli congestion game has finitely many players , each with a type and a participation probability . Player plays a mixed strategy on and is present () with probability , independently of the other players. The random flows and loads are
with means and . A present player on resource pays , where is the load of the others. A profile is a Bayesian Nash equilibrium when every strategy in its support minimizes .
The limit game is the nonatomic game with the same demands and the auxiliary costs
Consider a sequence with , and (14). Assume condition (18): there are and with for all , where and . For every sequence of Bayesian Nash equilibria :
and along that subsequence jointly and independently, and , in total variation.
The milestones are the results the proof of Theorem 2 uses, in attack order:
Theorem 2 justifies a Wardrop description for large games with rare participation, and it says which Wardrop model. The costs are not but their Poisson averages , which account for the player's own presence and for the randomness of the others. The theorem also describes the fluctuations: flows are asymptotically independent Poisson variables, while loads are Poisson but correlated. The paper builds its approximation rates (§6) and its price-of-anarchy convergence results (§7) on the same Poisson calculus.
The result is proved in the paper. As far as is known, none of it is formalized. Mathlib has the Poisson distribution but no Poisson approximation of Bernoulli sums. The platform has nonatomic routing models and one-variable Chen–Stein bounds, but no Bernoulli players and no convergence-of-equilibria theorem. Formalizing the mission therefore produces:
The obvious approach is to say that Bayesian Nash equilibrium inequalities pass to the limit because the expected costs converge. That step fails without control on : the costs are unbounded and evaluated at random loads, so convergence of the laws in total variation does not give convergence of . Condition (18) supplies the integrability, and the error must be bounded uniformly in the player and the profile. The Borisov–Ruzankin bound gives this, but at the Poisson parameter rather than at , so integrability has to be transferred between Poisson parameters. The other difficulties are independence of the limit flows, which is a joint statement on , and differentiating series in their Poisson parameter up to the end point .
Fin N, strategies are Finset E, and types and resources are finite types. Costs are c : E → ℕ → ℝ, nonnegative and monotone on ; is never read. The page prints and , which are read as real-valued, the weaker hypothesis. Nonempty is made explicit.MarkovChainCLT.tvDist, the supremum over events (15). Poisson laws are Mathlib's poissonMeasure.tsum, and Theorem 2 would become false. Derivatives are taken within . Lemma 1 and Theorem 9 assume and , so that is not Lean's .Many operations models ask how an optimal decision moves when a parameter moves. The classical answer is lattice programming (Topkis 1998): when the objective is supermodular, so that decisions and parameters are complements, optimal solutions are nondecreasing in the parameters. Inventory, assortment and resource-allocation problems often have the opposite structure. Stock already on hand, capacity already committed, or a budget already spent substitutes for new decisions, and one expects optimal decisions to be nonincreasing in such parameters. Supermodularity cannot express substitution between several decision variables at once, and before the work of Chen and Li no general tool covered this case.
Xin Chen and Menglong Li (SSRN 3431474; Operations Research, 2021, doi:10.1287/opre.2020.2070) supply that tool. They take the M♮-convex functions of discrete convex analysis (Murota 2003) and a quasi version of them, and show that maximizing a concave function of this kind over a box gives optimal solutions that decrease in the parameters. The paper then applies the result to multi-product inventory control with substitutable demand and to portfolio contracts.
All vectors here are integer vectors. For a finite index set , write for the -th unit vector of and . For , and .
A function has effective domain . It is SSQM♮-concave (semistrictly quasi M♮-concave; Definition 1, p. 8, applied to ) if for all and every there are and an integer such that for every integer , writing ,
Every M♮-concave function is SSQM♮-concave, and so is every strictly increasing transform of one.
The parametric problem (3), p. 10, has a parameter , a decision , and an objective ; the value encodes constraints beyond the box. A box is with , and . The problem is
and denotes its set of optimal solutions. A correspondence is nonincreasing on a set of parameters (the weak induced set ordering) if for all in , every dominates some , and every is dominated by some , with componentwise.
Let be SSQM♮-concave in and let be the set of parameters for which (3) has an optimal solution of finite value. Then for all with ,
Theorem 3 is the substitution counterpart of Topkis's monotonicity theorem. In the paper it yields Theorem 4 (for M♮-concave , also is nondecreasing, so a unit increase in the parameters lowers the total decision by at most one unit), and through Theorem 5 the monotone and bounded-sensitivity structure of optimal order quantities in multi-product inventory systems with substitution. Results of this shape are the usual route to structured optimal policies and to approximation and learning algorithms that exploit them.
The result is proved in the paper; it has not been formalized. The platform holds the discrete-convex-analysis vocabulary this mission reuses (characteristic vectors, positive and negative supports, effective domains of -valued functions, from Murota's book) and the supermodular, nondecreasing monotonicity theorems of Topkis, but no comparative-statics result for M♮-type objectives. A machine-checked Theorem 3 would be the base for formalizing Theorem 4 and the inventory application.
Topkis's argument compares and through their meet and join, which is exactly what fails here: under substitution the meet and join of two optimal solutions need not be optimal. The exchange property gives a single unit move at a time, and that move may lower one coordinate while raising another. The difficulty is to organize such moves so that a whole vector inequality is reached without undoing coordinates already fixed, and to handle objectives that take the value , where the exchange property says nothing.
finiteParams) keeps only parameters with an optimal solution of finite value, which is what the proof uses. It is not strengthened to " finite on the box".(Fin m ⊕ Fin n → ℤ) → WithBot ℝ with ; the joint point is Sum.elim s a. The index is none : Option K. The third alternative of Definition 1 is two equalities, equivalent to the paper's differences on . The definition quantifies over every integer , not one . Box ends are WithBot ℤ and WithTop ℤ. Over the proof's "small " is in the milestones.SSQMNatConcave keeps (restricting to gives Murota's narrower SSQM class), and the order in both halves is ; reversing either half gives the false nondecreasing statement. A sanity file checks that the hypotheses are satisfiable (the zero objective) and that the paper's fails on the example above.DiscreteConvex.MConvexFunctions.{CharVec, SuppPos, SuppNeg} and DiscreteConvex.EconomicEquilibrium.UDom. The SSQM♮-concave class, the box, and the weak induced set ordering are new and reusable for Theorem 4 and the applications.Contributions welcome: proofs of the milestones, and formalizations of Proposition 1 (M♮-concave implies SSQM♮-concave) and Theorem 4.
Large service systems (call centers, hospital wards, emergency departments) must decide how customers wait. In a pooled queue (PQ) all customers wait in one line served by agents; in dedicated queues (DQ) each server has its own line, which is what physical layouts, server-specific information and accountability often force. Classical queueing theory says pooling is more efficient: an idle server never coexists with a waiting customer. Cao, He, Huang and Liu (Operations Research, 2020) show that when customers may abandon and join the shortest queue, the efficiency loss of dedicated queues vanishes in large systems, and that in moderate overload the dedicated design has a strictly better delay probability than the pooled one. Service-level contracts are written in terms of this probability, so the comparison bears directly on staffing and design decisions.
There are servers. Customers arrive in a Poisson process of rate ; service times are exponential with mean ; each waiting customer has an exponential patience time with mean and leaves when its wait exceeds it. The traffic intensity is .
In the DQ–JSQ system each arriving customer joins a server with the fewest customers and stays in that server's FCFS queue. Let be the number of servers with at least customers. is a continuous-time Markov chain (genAb): an arrival joins a server with exactly customers when , and each of the servers with exactly customers loses one at rate . The PQ system is the M/M/n+M (Erlang-A) queue with the same .
The potential waiting time (PWT) is the time a customer would wait for service if it never abandoned; the actual waiting time (AWT) is , with the customer's patience. A customer who joins a server with customers has PWT distributed as , a sum of independent exponentials with rates .
Along a sequence of systems with arrival rates and (condition (21)), the fluid constants are
and the moderate overload condition (1) is , equivalently .
Under (21) and (1), with , nine pairs of steady-state limits hold as (subscripts D and P for the two designs), among them
together with the limits of the mean occupancy, mean AWT, the conditional means of and , and mean PWT. The goal is the full nine-part statement as printed.
The fluid model and its invariant state (Theorems 1 and 2), the steady-state limit (Theorem 3(ii)), the distribution of ((22), (23)), the PWT limit
(Theorem 4), its moderate-overload specialisation (Remark 3), and the pooled abandonment limit, already proved on the platform as ErlangA.Abandonment.theorem_1 (Garnett, Mandelbaum and Reiman, 2002).
The result separates two performance measures that are usually treated together. In moderate overload the two designs agree to first order in occupancy, abandonment and mean actual wait, so the capacity loss of dedicated queues is negligible; but the dedicated design lets a positive fraction of customers enter service immediately, while in the pooled design almost every customer waits. The cost is fairness: delayed customers in dedicated queues wait about one full service time, and the PWT variance stays positive, whereas the pooled PWT concentrates at . These limits drive the staffing comparison of §6 of the paper.
All statements are proved in the paper's e-companion; none is formalized. The mission produces machine-checked versions of a fluid model with reflection-type constraints, an interchange-of-limits theorem for a countable-state chain with unbounded rates, hypoexponential distributions, and many-server limits of Erlang-A waiting times (Whitt, 2004), most of which are reusable across the many-server literature.
The pooled system is a birth–death chain with an explicit stationary law; the dedicated system is not. Its stationary law has no closed form, so the DQ limits cannot be computed directly. The natural approach, a process-level fluid limit followed by , does not by itself give the steady-state statements: the two limits must be interchanged, which needs tightness of the stationary laws and global attraction to (Theorem 2). The fluid model itself is a reflection system in which may grow only when , so even its well-posedness (Theorem 1) is not a standard ODE result. Finally, weak convergence of (Theorem 4) does not yield convergence of means and variances without uniform integrability.
JSQHalfinWhitt.Tightness.State (0-based: Lean q.1 i is ) and IsStationaryDist (probability solutions of ); the chain is non-explosive, so these are its stationary laws. The arrival rate in genAb is the total rate .ErlangA.Abandonment.stationaryDist; and are the published probAbandon and probWait.expMeasure). The DQ PWT law is a definition: the arrival-seen mixture (PASTA). Patience is an independent expMeasure θ; conditional means are ratios.Contributions are welcome on the fluid model (Theorems 1–2), the hypoexponential facts ((22), (23)), the Erlang-A many-server limits, and the DQ–JSQ interchange of limits.
Markets in which goods pass through intermediaries (supply chains, interbank lending, procurement networks) do not fit the two-sided buyer–seller models of matching theory: one firm can buy inputs on some trades and sell outputs on others. Trading networks model such markets as a directed graph of possible bilateral trades. Hatfield, Kominers, Nichifor, Ostrovsky and Westkamp (J. Polit. Econ. 2013) showed that when every agent's preferences are fully substitutable, competitive equilibria exist and several notions of stability coincide with competitive equilibrium. Stability notions describe outcomes that agents cannot undo by renegotiating, and competitive equilibrium describes outcomes supported by prices. Knowing that the two coincide matters for market design: a decentralised market that only has to rule out simple deviations already achieves a price-supported, efficient allocation.
Candogan, Epitropou and Vohra (Operations Research, 2021; working paper version IHS Economics Series 323, 2016) rederived these results from the theory of M-convex submodular flows (Murota, Discrete Convex Analysis, SIAM 2003). Full substitutability is equivalent to M♮-concavity of the valuations, and efficient outcomes correspond to optimal flows.
Timeline:
A trading network is a finite directed multigraph . Each vertex is an agent, each arc a possible trade, with seller and buyer . Write for the trades sells, for the trades buys, and . An outcome is a set of trades , and a price vector is . Agent has a valuation and utility
For , the demand restricted to is ; with it is the ordinary demand .
If is chain stable, then there is with
Theorem 5.8 closes the hierarchy of solution concepts in trading networks. Combined with Theorem 5.7 (competitive equilibria are strongly stable, hence chain stable), every notion between chain stability and competitive equilibrium describes the same outcomes. Since chain stability is the weakest of them, it is enough to check deviations along chains to certify an outcome as price supported and, by the first welfare theorem, efficient. The result is also the basis of the paper's algorithmic section, which finds blocking chains as negative cycles.
The theorem is proved, in Hatfield et al. (2013) and again in this paper. No part of it is formalized on the platform. The mission produces a machine-checked trading-network model with M♮-concave valuations, the existence and second welfare theorems for it, and the chain-stability equivalence. The M♮-concavity definition reused here comes from the platform's formalization of Murota's book.
The lifting steps (milestones 6 and 7) are bookkeeping. The substance is in two places. First, Theorems 4.1 and 4.3 and Lemma 5.5 are where substitutability is used: existence of equilibrium prices is a duality statement for a nonlinear integer program, and Lemma 5.5 asserts that an improvement over no trade can always be found with the special shape of a chain. Neither follows from finite enumeration. Without substitutability both fail: with complementary valuations an inefficient no-trade outcome can need a non-chain set of trades to improve on it, and equilibria need not exist. Second, milestone 1 requires closure of M♮-concavity under adding a linear function and maximizing out a group of coordinates (projection). This closure is standard in Murota's book but is not on the platform.
Finset E, evaluated only on subsets of . Prices are functions E → ℝ.DiscreteConvex.EconomicEquilibrium.MNaturalConcave (values in , exchange axiom on the effective domain), applied to the signed representation sold, bought, off the box . The paper's printed axiom on PDF p. 8 has in its last term, a typo for , which is what the definition uses.{e // e ∉ X}.A pure Nash equilibrium (PNE) of a game is a strategy profile from which no player gains by a unilateral deviation. Unlike mixed equilibria, pure equilibria need not exist, and even when they do they can be hard to find: computing an equilibrium is PPAD-complete in general (Daskalakis, Goldberg & Papadimitriou 2009). The simplest learning procedure that searches for a PNE is best-response dynamics (BRD): repeatedly let some player who can strictly improve switch strategy. BRD is guaranteed to stop at a PNE only for special classes such as potential games (Monderer & Shapley 1996); in general it can wander forever inside a trap, the "sink equilibrium" of Goemans, Mirrokni & Vetta 2005.
A way to measure how often these failures occur is to draw the payoffs at random. The classical line of work, from Goldman (1957) and Goldberg, Goldman & Newman (1968) to Powers (1990) and Rinott & Scarsini 2000, studies the number of PNE when the payoffs are i.i.d. with a continuous law, so that ties have probability zero. The number of PNE then has mean one and is asymptotically Poisson. Amiet, Collevecchio, Scarsini & Zhong (2021) drop the continuity assumption. They show that the single parameter governing the asymptotics is the tie probability , and they relate the game to bond percolation on the hypercube. Their headline result is that, for binary players and small positive , BRD started from a fixed profile reaches a PNE with a failure probability that is summable in .
There are players , each with strategies . A profile is , and . In the random game the payoff of player at profile is , and the family is i.i.d. with a law on that may have atoms. With i.i.d. of law ,
Two profiles that differ only in coordinate are joined by an edge of the hypercube . The edge is oriented from to when , and is unoriented when the two payoffs tie; this gives the random partially oriented hypercube . The set of strictly profitable deviations consists of the heads of the arrows leaving , and is a PNE iff . BRD, , starts at and at each step moves to a uniformly random element of of the current profile. It converges to a PNE if for all large .
A profile is accessible from if an oriented path leads to it, and is the set of profiles accessible from . A trap is a set of at least two profiles that is strongly connected and that no oriented path leaves. In bond percolation each edge of is open independently with probability . Its giant component is the largest open cluster, and its fragment is the set of vertices outside the giant component.
If and (equivalently ), then
The theorem shows that the failure of BRD described in the game-theory literature, cycling in a trap, is asymptotically rare when payoffs tie with small positive probability. By Borel–Cantelli there is then a finite random beyond which BRD always reaches a PNE. The threshold is where the expected number of trapping 4-cycles stops being summable. The percolation coupling (Proposition 4.1) is the paper's new tool: it turns questions about accessibility under BRD into questions about clusters of the hypercube, where the results of McDiarmid, Scott & Withers apply. The same coupling yields the paper's phase transition at for the accessibility of all PNE (Theorem 3.3, not part of this mission).
The paper results are proved on paper, except for one gap. The paper derives (5.8), and through it Theorem 2.3, from the claim that the number of PNE has the same law as the number of isolated vertices of the percolation. That identity is false: the two laws already differ at . Statement (5.8) and Theorem 2.3 are nevertheless true; (5.8) follows from the Chen–Stein method (Arratia, Goldstein & Gordon 1989). Both are posed here as printed, and a correct proof of them is a contribution in its own right. None of these results has a machine-checked proof.
The obvious argument is a first-moment bound: count expected traps and sum over . The 4-cycles that are traps alone have expected number of order , summable exactly when , but traps can have any size up to , and the number of candidate vertex sets grows far faster than any single-shape first moment decays. Controlling traps of every size requires global information about which profiles BRD can reach from , and about how the exponentially many PNE sit relative to that set. That information comes from the component structure of percolation on the hypercube at a fixed edge probability, a deep theory (McDiarmid–Scott–Withers) of which nothing is in Mathlib.
Players are Fin N and profiles are Fin N → Bool; the payoffs of live on Fin N → Profile N → ℝ with the product law gameMeasure μ N. Each has its own probability space; every target is a per- bound or a sum over of per- probabilities, so no coupling across is needed. Sums of probabilities are ∑' in ℝ≥0∞ and are required to be ≠ ⊤. The BRD chain is built from the PMF iterates of its one-step kernel. At a PNE, where the page leaves the step undefined, the chain stays put. The probability of non-convergence is then , averaged with a lower Lebesgue integral. Percolation configurations are Edge N → Bool under a product of Bernoulli laws. " is not in the giant component" is read conservatively: on a tie for the largest cluster, counts as outside. Theorem 2.3 and (5.8) assume , as the page's does (both fail at ). Their constants are uniform over all payoff laws with the given . Lemma 4.3's is two-sided.
Trivializing encodings are excluded: no probability is a Bochner integral of a possibly non-measurable integrand, convergence is not defined by fiat, and a trap needs at least two vertices and closedness, so a single PNE is not a trap. The hypothesis (3.8) is kept literally. At it holds through Lean's , but the goal is then true for a genuine reason (every profile is a PNE).
A complete development needs the theory of finite Markov chains (absorption), Poisson approximation by Chen–Stein, a Berry–Esseen bound, and the component structure of percolation on the hypercube. The last of these is reusable well beyond this mission. Contributions of independent pieces, such as the trap reduction or the first-moment bounds, are welcome.
Interior point methods for convex optimization need a self-concordant barrier for the feasible set, and for many convex bodies, such as the subtour elimination polytope, membership can be decided in polynomial time while no efficiently computable barrier is known. The entropic barrier of Bubeck and Eldan (arXiv:1412.1587) is a self-concordant barrier defined for every convex body, and its gradient and Hessian are the mean and covariance of an exponential family of distributions on the body. Abernethy and Hazan (arXiv:1507.02528) proposed to run an interior point method with this barrier, estimating its derivatives by sampling. Badenbroek and de Klerk (arXiv:1811.07677) give a complexity analysis of such a sampling-based method when only a membership oracle for the body is available.
Any analysis of this kind has to control how badly conditioned the covariance matrices met along the way can be. Section 3.1 of Badenbroek and de Klerk supplies this control: a lower bound on the smallest eigenvalue of every Boltzmann covariance matrix over the body, in terms of the inner and outer radii of the body, the dimension, and the complexity parameter of the entropic barrier. This mission formalizes that section.
Fix and work in with the Euclidean inner product and norm . A convex body is a compact convex set with non-empty interior. Throughout, contains a Euclidean ball of radius and is contained in a Euclidean ball of radius .
The log partition function of is
For each , the Boltzmann distribution over with parameter is the probability law on with density proportional to ; at it is the uniform distribution on . Its mean is and its covariance matrix is
which is also the Hessian of at . The local norm at is . For a symmetric positive semidefinite , and .
The entropic barrier is the Fenchel conjugate , for in the interior of . Its complexity parameter is a number with for all interior and all directions ; the paper's is the least such number, (Definition 2.2). It is known that .
For every with ,
and for every with ,
In the order the proof uses them:
EntropicBarrier.Universal.nuBound_iff_covariance, whose forward direction is (13).The result. Theorem 3.1 bounds the condition number of every Boltzmann covariance over : together with display (12), it places the spectrum of in an explicit interval depending only on , , , and . In the paper this enters the analysis of the interior point method (display (52) and Lemma 6.3), where sampled estimates of must be accurate relative to the local norm. Lemma 3.2 on its own is a statement about the uniform distribution on a convex body that is of independent use in sampling and rounding algorithms.
Formalizing it. The results are proved in the paper, apart from Lemma 3.1 and display (4), which it cites (Kannan–Lovász–Simonovits 1995, Bubeck–Eldan 2014). None of them has been machine-checked. The mission builds on the published Lean layer of the Bubeck–Eldan entropic-barrier mission (convex bodies, the log partition function, the exponential family, its covariance form), so results proved here become reusable facts about that shared layer. The paper's headline, Theorem 6.2 (the complexity of the full sampling-based method), is not part of this mission: its complexity statement is asymptotic in form and its proof relies on results of other papers that the paper does not state.
The upper bound (12) is immediate, because has diameter at most . The lower bound is not: the Boltzmann law concentrates near the boundary of in the direction of as grows, and no direct estimate of the variance in the other directions is available. Near the obstacle is the base case itself, which needs a quantitative statement that a convex body in isotropic position is not too elongated (Lemma 3.1). For large the obstacle is that self-concordance only compares local norms at parameters within local distance less than one, so a single comparison with is not possible, and the number of comparisons must be controlled through the complexity parameter. On the formal side, the identification of with the Hessian of , the self-concordance of , and the relation between and all require differentiation under the integral sign over a convex body, which Mathlib supports only in pieces.
EuclideanSpace ℝ (Fin n) with Lebesgue measure; the inner product is the Euclidean one.IsConvexBody (compact, convex, non-empty interior), logPartition (), entropicBarrier (), expFamily K θ (the Boltzmann law), covForm K θ h k () and SatisfiesNuBound are the published Bubeck–Eldan definitions. New definitions: the local norm localNorm K θ v = √(covForm K θ v v), the sequence thetaSeq, and the step count mSteps (natural-number ceiling).SatisfiesNuBound K (entropicBarrier K) ϑ with . This is equivalent to the paper's reading: the least admissible satisfies the predicate, and the second bound of Theorem 3.1 weakens as grows. Milestones 7 and 8 additionally require , since the argument divides by .Real.logb 2.nuBound_iff_covariance, directly serve milestone 5 and are welcome contributions.In a contextual bandit a learner plays rounds; in round it observes a context , pulls one of arms and receives the reward of that arm in that context. In many applications the learner also learns what the pulled arm would have paid in other contexts. The motivating example of Balseiro, Golrezaei, Mahdian, Mirrokni and Schneider (arXiv:1809.09582) is a bidder in repeated first-price auctions: the context is the bidder's private value, the arm is the bid, and after the auction the bidder can compute the utility the same bid would have earned at every other value. Similar cross-learning structure appears in dynamic pricing with variable costs and in multi-armed bandits with side information about contexts.
Treating each context as a separate bandit problem costs regret of order , which is useless when the number of contexts is large or continuous. The paper shows that cross-learning removes, or reduces, this dependence on . For stochastic rewards it analyses UCB1.CL, a version of UCB1 that updates its statistics in every context it learns about, and bounds its regret by a graph quantity, the clique covering number of the cross-learning graphs. The authors describe this analysis as the main technical contribution of the paper (p. 5).
There are arms and contexts . On a probability space, the reward of arm in context at round is random; the reward vectors of different rounds are independent (rewards may be correlated within a round), and has the same law , with mean , in every round. The best mean in context is and the gap of arm is . The contexts form an arbitrary sequence fixed before the game (adversarial, oblivious contexts).
For each arm a directed cross-learning (CL) graph on the contexts is known: an edge means that pulling arm in context reveals . Every contains all self-loops. The clique covering number is the least number of subcliques (sets with an edge between any two members) that partition the contexts; .
UCB1.CL keeps, for every arm and context , the number of rewards of arm in context observed before round and their sum . In round it pulls an arm maximising
breaking ties arbitrarily. The pseudo-regret is .
For every , every context sequence and every UCB1.CL arm process,
These are the paper's and with the constants of its proof.
With complete cross-learning () Theorem 1 gives regret , independent of the number of contexts; with no cross-learning () it recovers the of independent UCB1 instances; in between, the clique covering number interpolates. The bound applies to bidding in first-price auctions with discretised values and bids, and the paper's lower bounds (Theorems 5–6) show that a dependence on graph invariants of the CL graphs cannot be removed in general.
The result is proved in the paper; nothing about it is formalized. A machine-checked proof would add to the platform its first contextual bandit with cross-learning, its first regret bound in terms of a clique cover, and a Hoeffding inequality for rewards sampled at rounds chosen adaptively by an algorithm, which is reusable in every UCB-type analysis. The formal statements also record corrected versions of four printed slips in the proof (listed under Formalization scope).
The standard UCB1 analysis counts, per arm and context, the pulls made before the arm has been observed times, and pays for each context. Summed over contexts this gives a bound linear in , which is exactly what cross-learning should avoid. The difficulty is that an observation of arm in context may come from a pull in another context, so the per-context counts are coupled through the CL graph and do not decrease independently. Lemma 3 handles this through a linear system over the cliques of a minimum clique cover, and Lemma 4 needs concentration for samples collected at random times determined by the algorithm itself.
Arms and contexts are Fin K and Fin C with . The reward process R t ω i c is defined for all ; the hypotheses are measurability, independence of the round vectors (iIndepFun), values in , and identical distribution of each coordinate across rounds. Contexts are a deterministic sequence ctx : ℕ → Fin C. G i c c' is the edge of , with all self-loops assumed. Rounds are 0-based in Lean (Lean's round is the paper's round ). The UCB index is EReal-valued, at ; the logarithm is natural and the algorithm knows .
The selection rule is a property of the arm sequence: in every round the pulled arm maximises the index, which reads only the rewards observed before round ; ties are arbitrary. The arm of round must be a measurable function of the rewards of earlier rounds. The regret is the expected pseudo-regret of p. 17, summed over all rounds.
Repairs relative to the page: is a positive lower bound on the positive gaps (as printed it is ); the gap-dependent constant is Lemma 3's , without the extra factor of (5); (4) carries on each right-hand side; throughout; Lemma 3 is pathwise for any arm sequence; the Hoeffding step is restricted to the event that the -th observation occurs within the horizon. Lean's , so every statement using restricts to positive gaps.
The formalization rules out the trivializing readings: the index cannot read the means, the gaps or unobserved rewards; the selection property is satisfiable (an explicit sequence exists); is a minimum over labellings whose classes are cliques, so it equals without cross-learning and with complete cross-learning; all constants are absolute.
Not part of the mission: Lemmas 1–2 (comparisons of graph invariants), Theorems 2–3 (EXP3.CL and EXP3.CL-U for adversarial rewards), Theorems 4–10 (lower bounds and the learning-to-bid applications) and the conjecture of Appendix D. Contributions of the optional-skipping Hoeffding inequality as a general lemma, and of clique-cover combinatorics on Fin C, are welcome and reusable.
This paper is devoted to systematic study of properties of the quantum entropy and of the Holevo capacity considered as a function of a set of quantum states. The properties of restriction of the quantum entropy to arbitrary set of states are discussed. For some types of sets necessary and sufficient conditions of boundedness and of continuity of restriction of the quantum entropy as well as necessary and sufficient conditions of existence of the Gibbs state are obtained. The Holevo capacity of an arbitrary set of states and its general properties as a function of a set are considered. The notion of the optimal average state of an arbitrary set of states with finite Holevo capacity is introduced. The condition of existence of optimal measure for a set of states is obtained. The general results concerning the quantum entropy and the Holevo capacity are illustrated by considering the several examples of sets of states.
This mission is the statement-level formalization of Entropic characteristics of subsets of states (arXiv:quant-ph/0510073v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
41 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (Theorem 1, PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
30 results of the paper are not stated yet, because the library lacks an interface they need:
Degradable quantum channels are among the only channels whose quantum and private classical capacities are known. As such, determining the structure of these channels is a pressing open question in quantum information theory. We give a comprehensive review of what is currently known about the structure of degradable quantum channels, including a number of new results as well as alternate proofs of some known results. In the case of qubits, we provide a complete characterization of all degradable channels with two dimensional output, give a new proof that a qubit channel with two Kraus operators is either degradable or anti-degradable and present a complete description of anti-degradable unital qubit channels with a new proof. For higher output dimensions we explore the relationship between the output and environment dimensions ( and respectively) of degradable channels. For several broad classes of channels we show that they can be modeled with a environment that is "small" in the sense . Perhaps surprisingly, we also present examples of degradable channels with ``large'' environments, in the sense that the minimal dimension . Indeed, one can have . In the case of channels with diagonal Kraus operators, we describe the subclass which are complements of entanglement breaking channels. We also obtain a number of results for channels in the convex hull of conjugations with generalized Pauli matrices. However, a number of open questions remain about these channels and the more general case of random unitary channels.
This mission is the statement-level formalization of The structure of degradable quantum channels (arXiv:0802.1360v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
37 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4: complete degradable qubit-output structure (original paper seed) (Theorem 4: complete degradable qubit-output structure (original paper seed), PDF p. 12). 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.
6 results of the paper are not stated yet, because the library lacks an interface they need:
Channel capacity describes the size of the nearly ideal channels, which can be obtained from many uses of a given channel, using an optimal error correcting code. In this paper we collect and compare minor and major variations in the mathematically precise statements of this idea which have been put forward in the literature. We show that all the variations considered lead to equivalent capacity definitions. In particular, it makes no difference whether one requires mean or maximal errors to go to zero, and it makes no difference whether errors are required to vanish for any sequence of block sizes compatible with the rate, or only for one infinite sequence.
This mission is the statement-level formalization of Tema Con Variazioni: Quantum Channel Capacity (arXiv:quant-ph/0311037v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
35 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract and Sections 2–7: equivalent quantum capacity definitions (Abstract and Sections 2–7: equivalent quantum capacity definitions, 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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Coding theorems in quantum Shannon theory express the ultimate rates at which a sender can transmit information over a noisy quantum channel. More often than not, the known formulas expressing these transmission rates are intractable, requiring an optimization over an infinite number of uses of the channel. Researchers have rarely found quantum channels with a tractable classical or quantum capacity, but when such a finding occurs, it demonstrates a complete understanding of that channel's capabilities for transmitting classical or quantum information. Here, we show that the three-dimensional capacity region for entanglement-assisted transmission of classical and quantum information is tractable for the Hadamard class of channels. Examples of Hadamard channels include generalized dephasing channels, cloning channels, and the Unruh channel. The generalized dephasing channels and the cloning channels are natural processes that occur in quantum systems through the loss of quantum coherence or stimulated emission, respectively. The Unruh channel is a noisy process that occurs in relativistic quantum information theory as a result of the Unruh effect and bears a strong relationship to the cloning channels. We give exact formulas for the entanglement-assisted classical and quantum communication capacity regions of these channels. The coding strategy for each of these examples is superior to a naive time-sharing strategy, and we introduce a measure to determine this improvement.
This mission is the statement-level formalization of Trade-off capacities of the quantum Hadamard channels (arXiv:1001.1732v2). 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 Unnumbered main result: Hadamard CQE single-letterization (Unnumbered main result: Hadamard CQE single-letterization, 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.
6 results of the paper are not stated yet, because the library lacks an interface they need:
We give here a self contained and elementary introduction to the Conley-Zehnder index for a path of symplectic matrices. We start from the definition of the index as the degree of a map into the circle for a path starting at the identity and ending at a matrix for which 1 is not an eigenvalue. We prove some properties which characterize this index using normal forms for symplectic matrices obtained from geometrical considerations. We explore the relations to Robbin-Salamon index for paths of Lagrangians. We give an axiomatic characterization of the generalization of the Conley-Zehnder index for any continuous path of symplectic matrices defined by Robbin and Salamon.
This mission is the statement-level formalization of The Conley-Zehnder index for a path of symplectic matrices (arXiv:1201.3728v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
43 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Classical integer Conley–Zehnder index: degree construction, independence and determinant parity (Classical integer Conley–Zehnder index: degree construction, independence and determinant parity, 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.
8 results of the paper are not stated yet, because the library lacks an interface they need:
We present a general necessary and sufficient criterion for the possibility of a state transformation from one mixed Gaussian state to another of a bi-partite continuous-variable system with two modes. The class of operations that will be considered is the set of local Gaussian completely positive trace-preserving maps.
This mission is the statement-level formalization of Conditions for the local manipulation of Gaussian states (arXiv:quant-ph/0109126v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2: exact LOG conversion criterion (Proposition 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.
6 results of the paper are not stated yet, because the library lacks an interface they need:
A necessary condition for reversibility (sufficiency) of a quantum channel with respect to complete families of states with bounded rank is obtained. A full description (up to isometrical equivalence) of all quantum channels reversible with respect to orthogonal and nonorthogonal complete families of pure states is given. Some applications in quantum information theory are considered. The main results can be formulated in terms of the operator algebras theory (as conditions for reversibility of channels between algebras of all bounded operators).
This mission is the statement-level formalization of Reversibility conditions for quantum channels and their applications (arXiv:1203.0262v3). 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 Theorem 3 (seed paper result): bounded-rank reversibility and the pure-state normal form (Theorem 3 (seed paper result): bounded-rank reversibility and the pure-state normal form, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper we give several equivalent formulations of the additivity conjecture for constrained channels, which formally is substantially stronger than the unconstrained additivity. To this end a characteristic property of the optimal ensemble for such a channel is derived, generalizing the maximal distance property. It is shown that the additivity conjecture for constrained channels holds true for certain nontrivial classes of channels. Recently P. Shor showed that conjectured additivity properties for several quantum information quantities are in fact equivalent. After giving an algebraic formulation for the Shor's channel extension, its main asymptotic property is proved. It is then used to show that additivity for two constrained channels can be reduced to the same problem for unconstrained channels, and hence, "global" additivity for channels with arbitrary constraints is equivalent to additivity without constraints.
This mission is the statement-level formalization of On Shor's channel extension and constrained channels (arXiv:quant-ph/0306196v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2: constrained versus asymptotic extension additivity (Theorem 2: constrained versus asymptotic extension additivity, PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
It is proven that recently introduced states with perfectly secure bits of cryptographic key (private states representing secure bit) [K. Horodecki et al., Phys. Rev. Lett. 94, 160502 (2005)] as well as its multipartite and higher dimension generalizations always represent distillable entanglement. The corresponding lower bounds on distillable entanglement are provided. We also present a simple alternative proof that for any bipartite quantum state entanglement cost is an upper bound on distillable cryptographic key in bipartite scenario.
This mission is the statement-level formalization of Quantum states representing perfectly secure bits are always distillable (arXiv:quant-ph/0602176v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Every exact nontrivial private state has positive GHZ distillable entanglement (Abstract; II.A–B, 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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
The quantum relative entropy is frequently used as a distance, or distinguishability measure between two quantum states. In this paper we study the relation between this measure and a number of other measures used for that purpose, including the trace norm distance. More precisely, we derive lower and upper bounds on the relative entropy in terms of various distance measures for the difference of the states based on unitarily invariant norms. The upper bounds can be considered as statements of continuity of the relative entropy distance in the sense of Fannes. We employ methods from optimisation theory to obtain bounds that are as sharp as possible.
This mission is the statement-level formalization of Continuity bounds on the quantum relative entropy (arXiv:quant-ph/0503218v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
25 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §VI, Theorem 4: sharp lower bound for every UI norm (seed headline) (§VI, Theorem 4: sharp lower bound for every UI norm (seed headline), 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:
The hypothesis testing problem of two quantum states is treated. We show a new inequality between the error of the first kind and the second kind, which complements the result of Hiai and Petz to establish the quantum version of Stein's lemma. The inequality is also used to show a bound on the first kind error when the power exponent for the second kind error exceeds the quantum relative entropy, and the bound yields the strong converse in the quantum hypothesis testing. Finally, we discuss the relation between the bound and the power exponent derived by Han and Kobayashi in the classical hypothesis testing.
This mission is the statement-level formalization of Strong Converse and Stein's Lemma in the Quantum Hypothesis Testing (arXiv:quant-ph/9906090v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quantum Stein lemma at every fixed positive error (§3, Theorem 2, (10): quantum Stein lemma, corrected positive-error domain, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum channels can be described via a unitary coupling of system and environment, followed by a trace over the environment state space. Taking the trace instead over the system state space produces a different mapping which we call the conjugate channel. We explore the properties of conjugate channels and describe several different methods of construction. In general, conjugate channels map M_d to M_d' with d < d', and different constructions may differ by conjugation with a partial isometry. We show that a channel and its conjugate have the same minimal output entropy and maximal output p-norm. It then follows that the additivity and multiplicativity conjectures for these measures of optimal output purity hold for a product of channels if and only if they also hold for the product of their conjugates. This allows us to reduce these conjectures to the special case of maps taking M_d to M_d' with a minimal representation of dimension at most d. We find explicit expressions for the conjugates for a number of well-known examples, including entanglement-breaking channels, unital qubit channels, the depolarizing channel, and a subclass of random unitary channels. For the entanglement-breaking channels, channels this yields a new class of channels for which additivity and multiplicativity of optimal output purity can be established. For random unitary channels using the generalized Pauli matrices, we obtain a new formulation of the multiplicativity conjecture. The conjugate of the completely noisy channel plays a special role and suggests a mechanism for using noise to transmit information.
This mission is the statement-level formalization of Properties of Conjugate Channels with Applications to Additivity and Multiplicativity (arXiv:quant-ph/0509126v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
30 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 / paper headline: conjugation preserves multiplicativity and entropy additivity (Theorem 5 / paper headline: conjugation preserves multiplicativity and entropy additivity, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
17 results of the paper are not stated yet, because the library lacks an interface they need:
We show the equivalence of two different notions of quantum channel capacity: that which uses the entanglement fidelity as its criterion of success in transmission, and that which uses the minimum fidelity of pure states in a subspace of the input Hilbert space as its criterion. As a corollary, any source with entropy rate less than the capacity may be transmitted with high entanglement fidelity. We also show that a restricted class of encodings is sufficient to transmit any quantum source which may be transmitted on a given channel. This enables us to simplify a known upper bound for the channel capacity. It also enables us to show that the availability of an auxiliary classical channel from encoder to decoder does not increase the quantum capacity.
This mission is the statement-level formalization of On Quantum Fidelities and Channel Capacities (arXiv:quant-ph/9809010v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
23 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entanglement and minimum-subspace capacities coincide (Abstract; Theorem 1 and Corollary 1, 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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Characterizing genuine multipartite quantum correlations in quantum physical systems has historically been a challenging problem in quantum information theory. More recently however, the total correlation or multipartite information measure has been helpful in accomplishing this goal, especially with the multipartite symmetric quantum (MSQ) discord [Piani et al., Phys. Rev. Lett. 100, 090502, 2008] and the conditional entanglement of multipartite information (CEMI) [Yang et al., Phys. Rev. Lett. 101, 140501, 2008]. Here we apply a recent and significant improvement of strong subadditivity of quantum entropy [Fawzi and Renner, arXiv:1410.0664] in order to develop these quantities further. In particular, we prove that the MSQ discord is nearly equal to zero if and only if the multipartite state for which it is evaluated is approximately locally recoverable after performing measurements on each of its systems. Furthermore, we prove that the CEMI is a faithful entanglement measure, i.e., it vanishes if and only if the multipartite state for which it is evaluated is a fully separable state. Along the way we provide an operational interpretation of the MSQ discord in terms of the partial state distribution protocol, which in turn, as a special case, gives an interpretation for the original discord quantity. Finally, we prove an inequality that could potentially improve upon the Fawzi-Renner inequality in the multipartite context, but it remains an open question to determine whether this is so.
This mission is the statement-level formalization of Multipartite quantum correlations and local recoverability (arXiv:1412.0333v3). 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 §2, (2.1); §3: local recoverability from the multipartite information gap (§2, (2.1); §3: local recoverability from the multipartite information gap, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
Majority vote is a basic method for amplifying correct outcomes that is widely used in computer science and beyond. While it can amplify the correctness of a quantum device with classical output, the analogous procedure for quantum output is not known. We introduce quantum majority vote as the following task: given a product state where each qubit is in one of two orthogonal states or , output the majority state. We show that an optimal algorithm for this problem achieves worst-case fidelity of . Under the promise that at least of the input qubits are in the majority state, the fidelity increases to and approaches as increases. We also consider the more general problem of computing any symmetric and equivariant Boolean function in an unknown quantum basis, and show that a generalization of our quantum majority vote algorithm is optimal for this task. The optimal parameters for the generalized algorithm and its worst-case fidelity can be determined by a simple linear program of size . The time complexity of the algorithm is where is the number of input qubits.
This mission is the statement-level formalization of Quantum majority vote (arXiv:2211.11729v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
61 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quantum majority vote: Theorem 1.2 (Quantum majority vote: Theorem 1.2, 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.
3 results of the paper are not stated yet, because the library lacks an interface they need:
Many large-population systems are modelled as aggregative games: each agent's cost depends on its own decision and on an average of everybody's decisions. Examples are electric-vehicle charging and demand response, where a household's cost depends on its own consumption profile and on the aggregate load through the electricity price, and congestion and routing, where a traveller's cost depends on the total flow on the links used. In these applications individual decisions are often non-convex: a charging profile may be on/off, a route is a discrete choice, an appliance runs in fixed blocks. Without convexity, the classical existence theorems for pure Nash equilibria (Rosen 1965, Debreu–Glicksberg–Fan) do not apply, and a pure Nash equilibrium may fail to exist.
The intuition that "non-convexity averages out when many small agents are aggregated" goes back to Starr's work on markets with non-convex preferences (1969), based on the Shapley–Folkman lemma. Liu, Oudjane and Wan (arXiv:2011.12604, Mathematics of Operations Research) make it quantitative for sum-aggregative games: they show that a non-convex aggregative game with players has an approximate pure Nash equilibrium whose error decays like , and they construct it from an equilibrium of a convexified game.
There are players . Player chooses an action in a compact, nonempty, possibly non-convex set , of diameter at most . Write for its convex hull. There are matrices with spectral norm , . The cost of player at a profile is
where is defined on and is a neighbourhood of the set of aggregates with .
Assumption 1 requires that (1) is lower semicontinuous on for every , and (2) is -Hölder on uniformly in : , with .
For , an -pure Nash equilibrium (-PNE) is a feasible profile such that no player can lower its cost by more than through a unilateral deviation: for all and .
The convexified game has action sets and costs
with the probability simplex in : is the convex envelope of . A generator is the set of points carrying positive weight in a minimizer of this infimum. A point satisfies the -stability condition with respect to generators if for all and .
Under Assumption 1, with
the non-convex game has an -PNE. More precisely, if is a pure Nash equilibrium of and are arbitrary generators, every profile
is an -PNE of . Both sentences are part of the goal.
If is only an -PNE of and satisfies the -stability condition with respect to a generator profile, the same disaggregation is an -PNE of with .
In attack order: Lemma 5.1 (a fixed point of the argmin map of a function continuous in , jointly lower semicontinuous and convex in ); Theorem 5.3 (existence of a PNE in games with convex compact action sets, convex lower semicontinuous costs and uniform equicontinuity in the other players' actions); Lemma 5.5 (1)–(2), (3) and (4) (properties of the convex envelope and of generators); Proposition 2.3 (the convexified game has a PNE); the Shapley–Folkman lemma (Lemma 5.4, first bullet, already proved on the platform); Starr's bound (Lemma 5.4, second bullet); Lemma 5.6 (1) ( at generator points); Theorem 2.7.
The result. Proposition 2.4 gives existence of approximate pure equilibria in a class of games where exact pure equilibria need not exist, with an explicit error bound that vanishes as the population grows, for fixed aggregate dimension . It also says how to obtain one: solve the convexified game, which is a convex game with lower semicontinuous costs, and round its equilibrium to generator points. Theorem 2.7 makes the construction robust to approximate solutions of the convexified game, which is what an iterative algorithm delivers. The paper's later sections (a randomized disaggregation and an application to flexible electricity consumption) rest on these two statements.
Formalizing it. The results are proved in the paper; none of them is formalized. The Shapley–Folkman lemma itself is proved on the platform and is reused here. The mission adds a quantitative Starr bound in Euclidean norm, an existence theorem for pure equilibria under lower semicontinuity (an extension of Rosen's theorem that the authors prove themselves because they found no reference), the basic theory of the -point convex envelope, and the disaggregation argument. Formalization also checks the paper's statements: the printed definition of a generator, read literally, makes Theorem 2.7 false (see Formalization scope).
The disaggregation step needs more than "average over many players". The convexified equilibrium gives each player a point in , but the deviation analysis has to happen in the original game, at points of . Two facts must be combined: the generator points of a best response of are best responses of against the convexified profile, and a profile of generator points can be found whose aggregate is within of the convexified aggregate. The first fails if a generator is allowed to contain points of zero weight. The second fails with the naive bound: picking arbitrary generator points for the at most exceptional players of the Shapley–Folkman lemma gives an error of order , not ; the bound requires a choice that exploits Euclidean geometry.
On the existence side, Rosen's theorem does not apply to : is convex and lower semicontinuous in the own action, but it need not be continuous even when is (the paper gives a three-dimensional example on p. 5).
is EuclideanSpace ℝ (Fin d) and players are Fin n. A matrix is a continuous linear map from to ; its operator norm is the spectral norm of the paper. Deviations are Function.update x i y, and inside is evaluated at the profile in which player plays , so the aggregate contains . One -PNE predicate, parameterized by action sets and costs, serves both and . Hölder powers are real powers, and is not assumed. is a neighbourhood of the aggregate set of , encoded with nhdsSet. The infimum defining is a real infimum; at every profile of its set is nonempty and bounded below, so Lean's default value for empty or unbounded sets is never reached.
Three readings differ from the printed text, and each is the one the paper's proofs use. (i) A generator is the set of components with positive weight, as in the paper's Lemma 5.7; keeping zero-weight components makes Lemma 5.6, Theorem 2.7 and Proposition 2.4 false (a two-player example with exists). (ii) Lemma 5.5 (2), printed "for all ", is stated on , as its proof and Definition 2.2 require. (iii) Action sets are assumed nonempty. Lemma 5.1 is stated in any finite-dimensional real normed space; the uniform equicontinuity of Theorem 5.3 measures closeness coordinatewise, an equivalent norm. Starr's bound is stated with any upper bound on the diameters, which is equivalent to the maximal diameter.
A trivializing formalization is ruled out: is an infimum over representations of the player's own action, not over all points, so equilibria of are not arbitrary profiles; a sorry-free sanity check confirms that the definitions are satisfiable and agree with on a singleton action set.
Out of scope: Theorem 3.3, Propositions 2.8, 3.2, 3.4, Lemmas 2.6, 3.1, 5.6 (2), 5.7, 5.8, the full stability condition, mixed strategies, and the numerical study of §4. Contributions welcome: proofs of the milestones, in particular a reusable Starr bound and a reusable existence theorem for lower semicontinuous convex games.
Interior-point methods minimize a linear function over a convex set by following the minimizers of , where is a self-concordant barrier for . The number of Newton steps the path-following method needs to reach accuracy is , where is the barrier's self-concordance parameter. A smaller is a better iteration bound, and the question of the smallest achievable for an arbitrary convex domain is a basic question of the theory.
A convex domain is a convex set with non-empty interior; it is proper if it contains no line with . need not be closed or bounded. For the polar set of with respect to is
a convex body, and the universal barrier is .
A function on is a barrier if as . A convex, three times continuously differentiable is self-concordant if, for all and ,
and -self-concordant if moreover (2).
The proof works with one-dimensional laws. For a convex body and , the marginal density is the density of for uniform on . For a density on , is its mean, its variance and its third central moment; . A density is -concave if is concave on its support (for : is constant on its support, up to endpoints).
The parameter is exact, so the goal carries no constant to improve.
The theorem settles the self-concordance parameter of the universal barrier for every proper convex domain: it is , and by the lower bound of Nesterov and Nemirovski no barrier does better in general. It implies the -self-concordance results for cones as special cases, and it gives a canonical barrier attaining the optimal iteration bound on any domain. Proposition 1, a pair of sharp moment inequalities for -concave distributions, is of independent interest; it extends the third-moment bound for log-concave laws used by Bubeck and Eldan.
The result is proved on paper; none of it is formalized. A complete development would give machine-checked statements of the universal barrier, its derivative formulas, Brunn's principle for hyperplane sections, and the moment inequalities, all of which are reusable for other barrier constructions (the entropic barrier missions on the platform use the same definitions of barrier and self-concordance). The two polynomial inequalities (milestones 4 and 7) are self-contained and the appendix proof of Lemma 4 is long elementary calculus, a natural target for automation.
The derivative formulas reduce -self-concordance to moment inequalities for the marginal of the polar body. The obvious argument uses only log-concavity of marginals (Prékopa–Leindler) and the log-concave third-moment bound; it yields and loses a constant. Exactness requires the stronger -concavity and moment bounds that are sharp for every , attained by on . Proposition 1 is an extremal problem over an infinite-dimensional class of densities, and the sharp constants surface only as polynomial inequalities in a parameter whose degree grows with (milestones 4 and 7); Lemma 4 must hold uniformly in the integer , and small behave differently. The localization lemma the paper cites for the reduction is not in Mathlib. On the analytic side, Lemma 1 requires differentiating three times under the integral for a possibly unbounded .
The space is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume. The goal's conclusion is the published predicate EntropicBarrier.Universal.IsNuSelfConcordantBarrier K φ n: barrier limits at every frontier point within ; convexity, and inequality (1) on through the published line-restriction form ConvexOptimization.IsSelfConcordantOn; and (2) in one-sided form, equivalent to the two-sided one. Lemma 1 uses Fréchet derivatives iteratedFDeriv. The universal barrier is a total function; its values off are junk and never read. All of 's standing assumptions (convex, non-empty interior, no line) are bundled in IsProperConvexDomain, together with .
Three conventions correct slips of the page and are disclosed in each item:
Densities are non-negative functions with integral , and moments are Bochner integrals; a -concave density has bounded support, so they are genuine. Not formalized: Brunn's principle for general , the localization lemma (Theorem 3) and its corollaries, the limiting reductions of §4.1.1–§4.1.5 and §4.2.1, and the internals of Appendix A. Contributions of any of these as supporting lemmas, of Brunn–Minkowski-type tools for sections, and of differentiation-under-the-integral results for polar volumes are welcome.
An online retailer decides, for every arriving customer, how to frame its catalog: which products are displayed, in which section or position, and at which of several price points. Framing changes demand. A product on a promotional banner sells more than the same product further down the page. The retailer must also decide which fulfillment center (FC) ships each order, and shipping costs depend on the distance from the FC to the customer. With limited inventory in each FC, framing and fulfillment interact: showing a product to a far-away customer can drain the stock that a closer, cheaper future order would have used.
Lei, Jasin, Uichanco and Vakhutinsky (SSRN 3282019; Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2021.1012) model this as the joint framing and fulfillment (JFF) problem. Customers choose by the multinomial logit (MNL) model. The paper builds the Randomized Framing and Fulfillment (RFF) policy from a deterministic relaxation, and proves that its relative loss against the optimal policy vanishes at rate as the market is scaled by . The work was carried out with data from a major U.S. retailer: 56 products in 27 FCs (§6).
There are products, customer regions, FCs and framing groups; group can hold at most products, and group means "not displayed". A framing assignment is a map . The feasible ones form
In each of periods at most one customer arrives, from region with probability . Product in group has attraction for , with , and price . A region- customer who sees buys with probability . The order is shipped from an FC that holds the product, at cost , and FC starts with units. is the optimal expected total profit (OPT').
The deterministic counterpart DET' replaces the 0/1 framing by fractions , with
Here
DET' maximizes , and its value is .
ConstrDist turns a fractional framing of one region into a distribution over , in three steps:
RFF runs ConstrDist on an optimal DET' solution for every region and period. Each period it samples , hides out-of-stock products, samples an FC with probability proportional to , and ships from , or from the cheapest FC with stock if is empty. The scaled problem has horizon and inventories ; its values are , and .
There are and such that for all , every optimal DET' solution and every choice of decompositions in ConstrDist,
and DET' has an optimal solution. Moreover, if , then for large and
The constants depend on the instance only.
The result shows that a policy computed once from a deterministic program loses only in absolute terms, despite three complications:
Lemma 3 is the reusable part. For MNL demand, any fractional framing can be realized exactly in expectation, for purchase probabilities and revenues simultaneously, by a randomization over feasible assignments. This makes fluid-based policies available for display, ranking and pricing decisions alike.
Status. The statement is published, but its printed proof is incomplete. EC 2 bounds RFF by a variant that ignores stock-outs and asserts that RFF "will generate zero profit" at a stock-out. RFF does not do that: it hides the product or re-routes the order, which changes all later inventories. The step is not justified. The statement was checked at planning by exact dynamic programming on four small instances, up to ; stayed between and . A complete proof, formal or informal, is new. None of these results has a machine-checked proof.
The obvious argument compares RFF with its deterministic plan period by period. Lemma 3 makes the expected sales and revenues match the plan exactly, and the total deviation of sales from plan is . That argument controls a policy that never runs out of stock. RFF does run out: after a stock-out it hides products and re-routes orders. So its later inventory, and hence its later framings and costs, differ from the plan in a path-dependent way. The difficulty is to bound the profit lost through this feedback by , uniformly over every optimal DET' solution, including time-varying ones, and every decomposition. A second, smaller difficulty is that DET' is not a linear program in . Lemma 5 and stationarity both need its reformulation as one.
Fin types; the no-display group is the last index. The standing assumptions are bundled in one predicate: