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?
Many service providers can infer how long a customer's request will take when the customer shares personal information. A customer who withholds that information may instead enter a queue as an unidentified request. Hu, Momot, and Wang study the resulting conflict between an individual's choice to disclose and the waiting times experienced by the whole customer population in a single-server system. Their comparison asks whether giving customers control over disclosure improves total customer surplus relative to a rule requiring full disclosure. The answer depends on which jobs the provider gives priority, even though the provider keeps the same priority order among identified and unidentified requests. Hu, Momot, and Wang, §3–4
The manuscript distinguishes shortest-processing-time priority (SPT), where the identified high-priority type has a shorter mean service time, from longest-processing-time priority (LPT), where it has a longer one. This distinction makes privacy control a queueing question as well as an information-choice question: withholding changes a request's priority class, so it changes waiting times for other customers. Theorem 1 gives the direction of the population-level comparison in both regimes. Hu, Momot, and Wang, Theorem 1, p. 15
Requests reach one server according to a Poisson process of rate . A request has type with probability and exponential mean service time , or type with probability and mean . The rate parameter is positive and differs from one. The average service rate of the combined population is , and stability requires . The manuscript also assumes a service reward at least , where is the cost per unit of time spent in the system. These are the parameters of the two-type service model. Hu, Momot, and Wang, §3.2, p. 8
Each customer chooses whether to disclose before observing the request type. If the fraction that discloses is , disclosed type- requests arrive at rate , disclosed type- requests at rate , and undisclosed requests at rate . The latter form a type- class with a mixture of the two service-time distributions. The server uses preemptive priority in the fixed order . For each class, , , and denote its mean time in the system, including service. The values are determined by the three-class formulas in Online Appendix A.1. Hu, Momot, and Wang, §3.3–3.4 and Online Appendix A.1
An infinitesimal customer compares the utility of disclosure, , with that of withholding, . The total customer surplus at population strategy is
An equilibrium disclosure probability is an endpoint supported by the appropriate strict utility comparison, or an interior point where the two utilities agree and their difference decreases nearby. The manuscript chooses the Pareto-dominant equilibrium when several exist. Hu, Momot, and Wang, Eq. (1), p. 10; equilibrium definition, p. 12; Eq. (9), Online Appendix p. 3
Let and . The target is
When and , the corresponding inequality is strict. The first regime is SPT and the second is LPT: under the fixed ranking , type has the shorter mean service time exactly when . The comparison holds for any equilibrium satisfying the paper's equilibrium conditions, including its Pareto-dominant selection. Hu, Momot, and Wang, Theorem 1, p. 15
The mission includes Lemma 1's closed forms for and , the closed form of and the auxiliary function in the proof of Lemma 4, its derivative and denominator-sign statements, and Lemma 4's monotonicity of on . Those statements connect the queueing model to the social comparison without replacing the final claim by a special case. Hu, Momot, and Wang, Lemma 1, p. 12; Lemma 4, Online Appendix p. 3; proof of Lemma 4, Online Supplement p. 2
Theorem 1 identifies a precise direction for the welfare effect of control over request-type information in this model. Under SPT priority, giving customers control cannot raise total customer surplus above full disclosure; under LPT it cannot lower surplus below full disclosure. The result therefore ties the social effect of the same disclosure option to a service discipline and to the mix of request types. Its strict clauses identify when withholding produces a genuine difference rather than equality. Hu, Momot, and Wang, Theorem 1 and discussion, p. 15
The paper establishes the theorem and the supporting identities mathematically. Here the remaining task is to prove the Lean statements from the definitions of the queue's class parameters and mean times. The formal development can leave reusable algebraic interfaces for finite-class preemptive-priority queues and for checking stability and denominator conditions in rational queueing formulas. These definitions and statements currently compile as a local draft; they are not yet machine-checked proofs of the paper's results.
An individual disclosure choice moves a request between the middle priority class and one of the two extreme classes. The direct utility comparison does not by itself determine the direction of total surplus: each choice also changes the class workloads and the waiting times faced by other customers. Thus the endpoint comparison cannot be read off from the sign of at a single . The analysis must account for the full dependence of , , and , including the hyperexponential residual time of undisclosed requests. The algebra has several denominators whose sign matters, and a formula in the source proof has a boundary exception at . Hu, Momot, and Wang, Online Appendix A.1 and Online Supplement A.2
Lean represents rates, costs, rewards, waits, disclosure probabilities, utilities, and surplus as real numbers. A generic three-class preemptive-priority interface stores mean service times, mean residual times, and workloads. The paper-specific model supplies the H, N, and L table from Online Appendix A.1, including the undisclosed class's hyperexponential residual time. It treats the resulting mean waiting times as formulas; it does not construct a stochastic queueing process. Lemma 1 then asserts genuine algebraic identities from those formulas, rather than following immediately from the definitions. Hu, Momot, and Wang, Online Appendix A.1
The standing assumptions retain , , , , and from §3.2. They state , , and explicitly because these are rates and a marginal cost, and because zero values would erase the strict comparisons. The theorem items restrict to whenever using the waiting-time formulas. The auxiliary closed-form, derivative, and bracket items exclude , where the source's displayed second fraction is undefined as a real quotient. Lemma 4 and the goal include that parameter value. The derivative of is strictly negative on and equals zero at ; its strict decrease across the whole interval is stated separately. Hu, Momot, and Wang, §3.2 and Online Supplement A.2
Strict monotonicity of surplus requires , since a population with only one service type has no type-mix effect. The goal's strict clause requires ; at , a withholding equilibrium can have exactly the same surplus as full disclosure. The goal still quantifies over an equilibrium, rather than an arbitrary point of . Contributions toward the queueing identities, rational-function sign conditions, monotonicity, and final comparison all serve this scope.
Retailers that sell through both a website and physical stores must choose how many stores to operate and which products to stock in them. Product returns change that decision: a customer who is uncertain about a product may inspect it in a store instead of purchasing it online and later returning it. Gao, Agrawal, and Cui study this tradeoff in a model where stores are uniformly spaced and every store carries the same assortment. Their Proposition 1 gives a counterintuitive comparison: when the product return rate rises, the optimal number of stores falls, while the range of products in each store grows. The present source is the authors' manuscript generated on 2020-12-25, with the relevant result on its p. 12 and proofs in its Online Appendix pp. 1–2; the journal pages are not used here.
Let be a finite set of products. The retailer offers every product online and chooses a store count and a store assortment . Stores are evenly located on a circle of circumference one, and each carries . Product has a customer class of deterministic size . A fraction of this class is uninformed about its valuation. An uninformed customer dislikes the product with probability , the common return rate; a customer who dislikes an online purchase returns it. Informed customers know their valuations already.
The online hassle cost is , the return hassle cost is , and travel to a store costs per unit of distance. The retailer earns per-unit margin and pays for each return. Each carried product uses display area and inventory area proportional to store sales, with coefficient . A store also requires common area ; facility area costs per unit. These assumptions and the symmetric circular-city setting come from §§3.1–3.2 of the paper.
Let denote uninformed online demand. The paper's full-market-coverage assumption yields the four online and store demand functions in equations (5)–(6). One store has size from equation (8). The total expected profit is equation (9):
An optimal decision maximizes this profit over all and . The paper relaxes the integrality of on p. 11. The retailer prefers stores at rate if a decision with has strictly greater profit than the online-only decision. This reading distinguishes strict preference from a tie at the store-opening threshold.
For , suppose stores are strictly preferred at both rates. For any optimal decisions and , the goal is
and, when ,
The goal includes the proposition's parenthetical equivalence and its necessary conditions and . The size condition is evaluated at the larger rate, so it holds across the interval being compared.
Lemma 1 identifies a threshold for opening stores. Above it, the positive-store count is , and the profitable assortment is specified by the inequality printed in the lemma. The milestones also record the authors' profit decrease beyond this count and the zero-or-turning-point bound. Further draft items state the incremental profit of each carried product, the increasing positive-store profit gap, the monotonicity of the closed forms, and the optimal-store-size expression in the Online Appendix. These are statements from the source rather than new targets selected by analogy.
The result links return behavior to two costly retail decisions at once. Stores can reduce online returns by letting uncertain customers inspect products, yet a higher return rate need not call for more locations. Within the model, fewer locations can be paired with a broader assortment, and the stores can become larger when the return and online hassle costs satisfy the stated condition. Without Proposition 1, the model's demand and profit equations alone do not establish the direction of these comparative statics. The paper also studies other hassle-cost changes and omni-channel services, but they use additional results and models.
The theorem is proved in the authors' manuscript. The remaining task here is a machine-checked development of its exact model, threshold, and comparative statics. The compiled mission items are statements with open proofs; a successful compile does not prove them. The demand and profit definitions, together with the lemmas about maximizing a piecewise expression over a continuous store count, can be reused when formalizing the paper's other sections.
The objective changes formula when all uninformed customers near a carried product switch to stores, and again when informed customers do. Therefore differentiating one expression for profit across all does not justify a global optimum. At the store-opening threshold, the profit from stores can tie online-only profit; an interior count can then also be optimal. Product-selection ties can likewise produce more than one optimal assortment. A statement only about one selected closed form would not control every optimal decision and would miss the tie cases in Proposition 1.
Products form a finite type, possibly empty, and assortments are finite subsets. The empty catalogue has no positive-store preference; a one-product parameter instance witnesses that strict store preference is possible. All monetary quantities and the relaxed store count are real numbers. The return rate is quantified separately in so the same parameters can be compared at two rates. The bounds and spell out “fraction” and “handling cost” on pp. 6 and 9. No sign condition is imposed on the exogenous margins , which cancel from the decision comparison.
The source assumes sufficiently high customer valuations to guarantee full market coverage on p. 8. The Lean model begins with the resulting demand equations (5)–(6); it does not introduce valuations or prices from utility equations (1)–(4). The formulas retain and the area expression divided by ; at , Lean's zero-division convention gives zero store demand, while the total facility cost is multiplied by zero. The target always quantifies over actual profit maximizers. Proving only that decreases would leave the retailer's optimization claim untouched. Contributions to the source-backed milestones and the algebra connecting the two printed assortment criteria are in scope.
Many firms that run their own delivery or service workforce have started to operate a hybrid workforce: salaried employees serve part of the demand, while a crowd of independent freelancers on a platform owned by the same firm serves the rest. A firm in this position faces a recurring allocation question. Every order sent to the platform pays freelancers and so attracts more of them, which increases the platform's market thickness (the size of its freelancer pool) and with it the platform's own future demand. The same order, served in house, earns the firm's margin today. He and Goh study this trade-off between profit now and platform growth later, with data from the Vietnamese delivery company AhaMove (He & Goh, SSRN 3537700; published in Management Science, 2021, doi:10.1287/mnsc.2021.4177).
The question the mission formalizes is whether a thicker platform is worth having at all. The paper's answer, its Theorem 1, is that it depends on two numbers: the mean and, centrally, the variance of the cross-network effect , the random number of platform orders generated per freelancer.
Time runs over periods . At the start of a period the platform has freelancers and the firm faces orders. The firm chooses a transfer quantity with and sends those orders to the platform. Customers pay per order; an order served in house earns the firm , with . The platform also receives its own demand , where is random with . To serve the total load it pays freelancers the payout ratio , where measures the inefficiency of freelancers relative to employees. The period profit is .
The state then moves to
with parameters and shocks that are square integrable and independent, with . Future profits are discounted by . The value functions are and
Write , , and (which is when ). Inside the paper defines three disjoint regions: (high variance), ; (low variance), ; and (moderate variance), strictly between the two bounds. Market thickness benefits the system in period if is increasing in for every fixed , and is costly if it is decreasing; both in the weak sense.
and when . "Costly as " means that for every , is decreasing on some tail .
The appendix proves the theorem through a structural result and three lemmas, which are the milestones, in attack order:
The theorem replaces the intuition that a larger freelancer pool is always an asset with a criterion that a firm can estimate. When is very volatile, matching supply to a random platform demand is expensive, because the wage bill is quadratic in the load, and a thicker market only amplifies that cost; when is stable, thickness pays in every period. In the moderate regime the value of thickness changes sign once over the horizon, which is what drives the paper's later results on the structure of the optimal transfer policy (Proposition 3) and on the gap between the dynamic and the myopic policy (Theorem 2).
The result is proved in the paper. It has no machine-checked proof. Formalizing it adds a checked model of a finite-horizon stochastic dynamic program with a continuous two-dimensional state, concavity of value functions under partial maximization, envelope formulas with right derivatives, and an explicit backward recursion for the bound . The formalization also records two printed slips that it corrects (see Formalization scope).
The obvious argument is a backward induction on the sign of , read off the envelope formula (13). That step does not close by itself: the formula contains the optimal transfer , its multiplier and expectations of the next period's partial derivatives at random states, so the induction needs a priori bounds on the derivatives, monotone limits as and , and exchanges of limits with expectations. The value functions are only concave, so all derivatives are one-sided, and the optimal decision can sit on the constraint . Part (c) needs, in addition, an explicit lower bound on the asymptotic slope and a proof that switches sign at most once.
All statements share one definition, HybridOrderAlloc.Thickness.Model. The data are a structure Sys Ω (a measure on , shocks , real parameters and ) and a predicate Sys.Standing with the page's assumptions. Conventions committed to:
variance.MonotoneOn, AntitoneOn). is indexed by integers.Hypotheses added to the page, each disclosed in the statements: (Theorem 1 is false for , because then puts points where thickness pays into ); , , almost surely (so the next state stays in the domain of for every feasible , which the page takes for granted); ; and in Lemma 3(c) alone (the printed lemma fails for ).
is never a free parameter constrained by a Bellman hypothesis, and never a closed formula. Square integrability of is assumed, so no integral takes a junk value. The regions carry the guard wherever appears, so a divergent series cannot be read as .
A complete development needs: concavity of a partial maximum over a convex graph, one-sided envelope theorems, dominated convergence for the derivative limits, and finite geometric sums. The concavity and envelope steps are reusable for other dynamic programs with continuous states. Proofs of any milestone are welcome, as are sharper variants that remove the added well-posedness hypotheses.
A blockchain miner pays for electricity and equipment while block rewards arrive at irregular times. A strategy that raises the average reward can still expose a miner with limited capital to ruin before those rewards arrive. Albrecher and Goffard study this tension for a simplified selfish mining strategy in which the miner temporarily withholds a discovered block. Their model connects the block discovery process to a dual risk process: capital falls continuously as costs accrue and jumps upward when the miner collects block rewards. The quantity of interest is the miner's expected remaining capital at a random evaluation time, counting paths that have already reached ruin as zero. The paper derives a closed expression for this quantity when the miner begins with no withheld block. Albrecher and Goffard, arXiv:2010.12577v1, §§2–3.
Network blocks are discovered at Poisson rate . The miner has a share of computing power, pays operating costs at rate , and receives per block for which the strategy earns a reward. On each discovery, records whether the miner found the block. If the miner has produced a fork and another participant finds the next block, records whether that participant extends the miner's branch; its probability is .
The state just before discovery records an empty buffer, one withheld block, or a public fork. From state , the miner withholds a newly found block and earns nothing. From state , a further miner discovery pays for two blocks and returns to ; a competing discovery creates a fork. From , the next discovery resolves the fork and returns to . It pays two rewards if the miner finds the block, one reward if another miner extends the miner's branch, and no reward otherwise. These cases define the reward count and the surplus
where is initial capital and is the number of network discoveries by time . The ruin time is . For initial state , the fixed-horizon value is . The paper replaces a fixed horizon by an independent exponential time of mean and defines . Thus the exponential law has rate . Source, equations (15), (16), and (19).
The goal is Theorem 3.1 for the initially empty buffer. Let be the parameter expressions in the paper's equation (22). Let and be precisely the roots with negative real part of
For satisfying the corrected boundary system (23), the target is, for all ,
The paper prints the third right-hand side of (23) as . Its boundary condition (33), together with its own coefficients (24), requires . The mission states this correction explicitly. Source, Theorem 3.1 and equations (23), (24), (33).
The three curated targets are the corrected advanced differential system (29) for the three starting states; Lemma A.1, which counts three characteristic roots in the left half-plane when ; and the explicit function in (39)–(40), including its corrected boundary equations. These are statements made in Appendix A and used in the discussion of Theorem 3.1. The root-count lemma has the narrower hypothesis that the authors print; the main result permits and while specifying the root set. Source, Appendix A.
The formula gives expected remaining capital for a specific block-withholding policy while accounting for the event of ruin before the evaluation horizon. It allows the model's cost rate, reward size, hash share, connectivity, and initial reserve to be compared through the same value function. The result addresses the limited-capital question that an average revenue rate alone does not answer. Its use is within this simplified strategy and the paper's Poisson and independent-mark assumptions. Source, §§3–4.
The result is presented in the paper, but a machine-checked proof of this corrected statement is still to be supplied. A complete development would establish the expectation's measurability and integrability, the differential properties of the three state-dependent value functions, the complex root count, and the identification of the explicit function with the expectation. The stochastic model and its value function can also support separate formalizations of the paper's ruin-probability and honest-miner results.
The reward at a discovery depends on withheld-block state, so the surplus alone does not describe the next reward. The value functions for all three states are coupled, and the resulting differential equations evaluate the empty-buffer function at larger reserves and . Those advanced terms prevent a direct application of ordinary differential-equation uniqueness results. The root count is a statement about a transcendental complex equation, and its left-half-plane roots must be isolated exactly.
Appendix A says that it constructs a solution of the advanced equation and assumes uniqueness, observing that simulations can check the result. That assumption leaves an identification step between the displayed candidate and the stochastic expectation that the paper does not prove. It remains part of the goal, without an invented source milestone. Source, p. 25.
Lean represents the network process through independent exponential interarrival times of rate and independent Bernoulli marks. Marks begin at index zero in code, corresponding to the paper's first block at index one. The state transition and reward map encode the cases of (16). The ruin time is extended nonnegative, so an empty set of ruin times has infimum . On the null event of infinitely many arrivals in finite time, the cardinality-based block count has Lean's default value zero; the model law excludes that event almost surely.
The horizon average uses the first expression in (19), integrating against the exponential measure of rate . The expected surplus must be obtained from this stochastic construction; defining it by the closed formula or by a differential equation would erase the target. The roots and coefficients are constrained by the characteristic equation and corrected boundary system, and integral defaults on nonintegrable inputs cannot establish the result. No net-profit condition is imposed on Theorem 3.1.
The paper-specific definitions, the three curated milestones, and the main theorem are open to contributions. General infrastructure for marked Poisson processes, extended ruin times, integration of stopped surplus, and complex root counting would be reusable beyond this case. The four printed discrepancies affecting (23), (29), (31), and (40) are recorded in the local moderation notes; this mission's Lean statements use the mathematically corrected forms.
We investigate the possibility of dividing quantum channels into concatenations of other channels, thereby studying the semigroup structure of the set of completely-positive trace-preserving maps. We show the existence of 'indivisible' channels which can not be written as non-trivial products of other channels and study the set of 'infinitesimal divisible' channels which are elements of continuous completely positive evolutions. For qubit channels we obtain a complete characterization of the sets of indivisible and infinitesimal divisible channels. Moreover, we identify those channels which are solutions of time-dependent master equations for both positive and completely positive evolutions. For arbitrary finite dimension we prove a representation theorem for elements of continuous completely positive evolutions based on new results on determinants of quantum channels and Markovian approximations.
This mission is the statement-level formalization of Dividing Quantum Channels (arXiv:math-ph/0611057v3). 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 Theorem 16 (Structure of infinitesimal divisible channels) (Theorem 16 (Structure of infinitesimal divisible channels), PDF p. 14). 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:
This paper establishes several converse bounds on the private transmission capabilities of a quantum channel. The main conceptual development builds firmly on the notion of a private state, which is a powerful, uniquely quantum method for simplifying the tripartite picture of privacy involving local operations and public classical communication to a bipartite picture of quantum privacy involving local operations and classical communication. This approach has previously led to some of the strongest upper bounds on secret key rates, including the squashed entanglement and the relative entropy of entanglement. Here we use this approach along with a "privacy test" to establish a general meta-converse bound for private communication, which has a number of applications. The meta-converse allows for proving that any quantum channel's relative entropy of entanglement is a strong converse rate for private communication. For covariant channels, the meta-converse also leads to second-order expansions of relative entropy of entanglement bounds for private communication rates. For such channels, the bounds also apply to the private communication setting in which the sender and receiver are assisted by unlimited public classical communication, and as such, they are relevant for establishing various converse bounds for quantum key distribution protocols conducted over these channels. We find precise characterizations for several channels of interest and apply the methods to establish several converse bounds on the private transmission capabilities of all phase-insensitive bosonic channels.
This mission is the statement-level formalization of Converse bounds for private communication over quantum channels (arXiv:1602.08898v3). 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 Covariant channels admit a fixed Choi-state teleportation simulation (Proposition 2, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
25 results of the paper are not stated yet, because the library lacks an interface they need:
Retailers sometimes ask every supplier in a production network to meet a common environmental or social responsibility standard. A program can fail to produce its expected value if even one firm declines to participate. The retailer therefore needs a way to pass commitments and payments through the network, including to suppliers with whom it has no direct purchase contract. Feng, Li, Lu, and Shanthikumar model that choice as a network of simultaneous bilateral negotiations and ask which negotiation links a retailer should use. Their examples distinguish direct engagement with distant suppliers from delegating those negotiations to intermediate firms. Feng et al., accepted manuscript, §§1, 3–4.2.
The paper's target is a structural decision. A retailer can arrange the same firms into different negotiation trees; those trees alter how much of a fixed total ESR surplus the retailer retains. The result formalized here identifies a preferred tree using path costs derived from bargaining power. The published article appeared in Management Science in 2021; this mission follows the authors' January 2021 accepted manuscript, whose theorem numbering and printed pages are the source for the statements below. Feng et al., accepted manuscript, pp. 9–21.
The firms are , with retailer . In the material network , an arc means downstream firm buys goods or services from upstream firm . The ESR network also permits when there is a directed material path from to . Thus a retailer can negotiate directly with a distant upstream supplier even when an intermediate firm handles the material purchase. A feasible implementation structure is a rooted tree of ESR arcs spanning all firms: every supplier has exactly one downstream parent, and every firm's parent chain reaches retailer . Feng et al., §3, pp. 9, 12–13, display (1).
Every firm must invest to create the program's revenue . Firm incurs cost , and universal participation leaves positive total surplus . In a negotiation on , downstream firm has bargaining power and upstream firm has power . Their relative bargaining power is . The route from the retailer to firm in is . Feng et al., §3, pp. 10–12; §4.1, pp. 16–17.
A payment goes from downstream to upstream . A firm's gain is its receipts less its payments and investment cost, plus if it is the retailer and all firms invest. A Nash–Nash equilibrium is a profile of arc payments in which each parent and child bargain over their own payment with the other payments fixed. They maximize their weighted Nash product subject to both gains being nonnegative; a negotiation breakdown generates zero disagreement gain. Feng et al., §4.1, pp. 15–17, displays (4)–(6).
For a feasible , Theorem 1 specifies the payment on each arc at universal participation. Corollary 1 then gives the retailer's gain and each supplier's gain in terms of products along root routes. In particular,
These are separate milestones because a formula for one payment does not by itself describe the network-wide gain distribution. Feng et al., p. 17, Theorem 1 and Corollary 1, displays (7)–(8).
The retailer maximizes its equilibrium gain by minimizing over feasible structures, as stated before and in display (9). Give each ESR arc the real cost . A shortest path tree has a minimum-cost route from to every supplier among simple directed ESR routes. Theorem 2 asserts
The first inequality is Theorem 2 as printed. The second records the retailer-gain interpretation immediately preceding display (9) and the paper's stated motivation for the structure result. Feng et al., §4.2, pp. 20–21, display (9), Theorem 2.
The theorem replaces a choice among potentially many feasible negotiation trees with a recognizable network object. It characterizes a retailer-preferred way to assign negotiations across tiers, while Corollary 1 also reports how each firm's share changes with the route linking it to the retailer. The paper uses the structure result to discuss delegation and engagement in supplier networks; its later extensions consider additional investment and negotiation settings. Feng et al., §§4.2–5.
The paper result is proved in its online appendix, which is not part of the held manuscript. The present mission supplies precise Lean statements for the network, bargaining equilibrium, gain allocation, and tree optimum. A local prior-art search found no published formalization of this particular network equilibrium or shortest-path-tree conclusion. Completing the mission would add machine-checked proofs of these statements and definitions that could be reused for other bargaining networks with a common surplus.
The arc costs are additive logarithms, but is a sum of multiplicative path weights. The paper explicitly warns that the total log cost of a shortest path tree is not the objective in display (9). A direct minimum-total-tree-cost argument therefore does not establish Theorem 2. At the bargaining layer, each payment affects the gains of two firms while the other negotiations remain in force; an independent two-person bargaining calculation does not yet establish a simultaneous network equilibrium. Feng et al., §4.1, pp. 16–17; §4.2, p. 20.
Lean represents firms as Fin (n + 1), so retailer exists even when . Material arcs are a directed relation, and ESR arcs are its nonempty-path transitive closure. A parent map represents a feasible implementation tree; the retailer is pinned as its own parent, and that value never contributes a payment. Parent iteration must reach from every firm. The tree's root route and subtree are derived from this map, rather than supplied as unrelated data. Payments are indexed by the supplier endpoint because every supplier has exactly one parent arc. Gains, powers, payments, and path costs are real-valued.
The manuscript permits , but the formal statements assume on ESR arcs. This disclosed restriction ensures the ratio and its logarithm retain their intended mathematical meaning; Lean assigns default values to division by zero and logarithms outside their positive domain. The manuscript's opposing-power identity is required on ESR arcs, including when material cycles permit both arc orientations. Investment costs are nonnegative, and . The formalization uses the manuscript's description of a rooted spanning tree; the in-degree condition printed in display (1) by itself also admits cycles disconnected from the retailer. Shortestness compares a tree route with every simple directed ESR route, so it does not define a shortest path tree by the desired inequality. The Nash comparison ranges only over payment deviations for which both firms' gains are nonnegative.
The definition layer needs finite directed paths, root-route products, contingent gains, and weighted Nash products. Reusable contributions include a rooted parent-map representation and a shortest-path-tree predicate for real arc costs. Solvers may contribute proofs and supporting lemmas for the three source milestones or the goal theorem; the additional delegation, Shapley, and extension results elsewhere in the paper are outside this mission.
We review Schmidt and Kraus decompositions in the form of singular value decomposition using operations of reshaping, vectorization and reshuffling. We use the introduced notation to analyse the correspondence between quantum states and operations with the help of Jamiolkowski isomorphism. The presented matrix reorderings allow us to obtain simple formulae for the composition of quantum channels and partial operations used in quantum information theory. To provide examples of the discussed operations we utilize a package for the Mathematica computing system implementing basic functions used in the calculations related to quantum information theory.
This mission is the statement-level formalization of Singular value decomposition and matrix reorderings in quantum information theory (arXiv:1011.1585v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Schmidt decomposition of a bipartite pure state (Theorem 2, Eq.(19), 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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
In Shannon information theory the capacity of a memoryless communication channel cannot be increased by the use of feedback from receiver to sender. In this paper the use of classical feedback is shown to provide no increase in the unassisted classical capacity of a memoryless quantum channel when feedback is used across non-entangled input states, or when the channel is an entanglement--breaking channel. This gives a generalization of the Shannon theory for certain classes of feedback protocols when transmitting through noisy quantum communication channels.
This mission is the statement-level formalization of On Feedback and the Classical Capacity of a Noisy Quantum Channel (arXiv:quant-ph/0305176v1). 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 No capacity gain across separable feedback cuts (III.B, 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:
Stinespring's dilation theorem is the basic structure theorem for quantum channels: it states that any quantum channel arises from a unitary evolution on a larger system. Here we prove a continuity theorem for Stinespring's dilation: if two quantum channels are close in cb-norm, then it is always possible to find unitary implementations which are close in operator norm, with dimension-independent bounds. This result generalizes Uhlmann's theorem from states to channels and allows to derive a formulation of the information-disturbance tradeoff in terms of quantum channels, as well as a continuity estimate for the no-broadcasting theorem. We briefly discuss further implications for quantum cryptography, thermalization processes, and the black hole information loss puzzle.
This mission is the statement-level formalization of The Information-Disturbance Tradeoff and the Continuity of Stinespring's Representation (arXiv:quant-ph/0605009v1). 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 Continuity with freely chosen common Stinespring dilations (§I, Eq. (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.
3 results of the paper are not stated yet, because the library lacks an interface they need:
We introduce various measures of forward classical communication for bipartite quantum channels. Since a point-to-point channel is a special case of a bipartite channel, the measures reduce to measures of classical communication for point-to-point channels. As it turns out, these reduced measures have been reported in prior work of Wang et al. on bounding the classical capacity of a quantum channel. As applications, we show that the measures are upper bounds on the forward classical capacity of a bipartite channel. The reduced measures are upper bounds on the classical capacity of a point-to-point quantum channel assisted by a classical feedback channel. Some of the various measures can be computed by semi-definite programming.
This mission is the statement-level formalization of Bounding the forward classical capacity of bipartite quantum channels (arXiv:2010.01058v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
42 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 21 (main paper result selected by page-1 seed) (Theorem 21 (main paper result selected by page-1 seed), PDF p. 14). 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:
An investor may care about reaching a target, avoiding a loss, or crossing an aspiration level rather than maximizing a concave function of final wealth. A target reward can jump from zero to one at a specified wealth. Such nonconcave utility is a natural model for goal-reaching portfolios, but its discontinuity changes what the associated Hamilton–Jacobi–Bellman equation can say at maturity. Portfolio bounds make the distinction sharper: an investor with finite leverage and short-sale limits cannot instantaneously smooth a jump in the payoff. Dai, Kou, Qian and Wan analyze this combination of nonconcavity, portfolio constraints, and a liquidation floor in their 2022 paper.
The paper proves a comparison principle and identifies the control value as the unique viscosity solution under a special terminal asymptotic condition. These are known mathematical results; this mission asks for their Lean proofs. The source is the authors' accepted manuscript, whose main theorem is Theorem 4.2 on printed page 12. The e-companion supplies boundary and terminal results supporting that theorem.
The market contains one risky stock and one riskless bond. After the paper's forward-wealth normalization, wealth started from follows
Here is the excess stock return, is volatility, is Brownian motion, and is the fraction of wealth invested in the stock. Portfolio weights satisfy , with ; either endpoint may be infinite. Wealth remains above the liquidation floor . For utility , the value function is
Assumption 3.1 permits utility to be nondecreasing and right-continuous without being concave or continuous. For some , it eventually satisfies . At it either has a finite value or, when , has the paper's CRRA form near zero. The second case includes logarithmic utility. These alternatives lead to different liquidation boundary conditions.
The formalized Hamiltonian is
and the HJB equation is for and . Definition A.1 tests upper and lower semicontinuous envelopes of candidate solutions against smooth functions and uses the corresponding envelopes and . It also imposes the liquidation boundary condition and a terminal asymptotic condition. For bounded portfolio weights the terminal condition retains the jump of through the normal distribution function and . For unbounded weights its target is the concave envelope .
The goal is Theorem 4.2: for both bounded and unbounded portfolio intervals, the control value satisfies Definition A.1 and is continuous on . In the growth class used by Theorem 4.1, every other viscosity solution agrees with it:
The goal keeps the actual stochastic-control supremum as and quantifies over competing solutions . It does not select a particular numerical method or a preferred proof. Theorem 4.1 gives comparison in this class. Proposition EC.3.2 gives the liquidation boundary behavior. Proposition EC.3.3 gives two terminal regimes, and Lemma EC.3.3 supplies the power-majorant statement used in the unbounded regime. The milestone list follows these stated results, specialized to the one-stock constant-coefficient model of the main theorem.
The characterization connects a portfolio optimization problem to an HJB equation even when the terminal utility jumps. It specifies the terminal behavior that distinguishes the bounded and unbounded portfolio regimes. In the bounded case a discontinuity can persist in the approach to maturity; in the unbounded case the limiting target is the concave envelope. The comparison statement then makes the characterization unique within the stated growth class. These conclusions are the analytical basis for the paper's later discussion of numerical schemes, although the numerical convergence theorem is outside this mission's scope (Dai et al., 2022, §§4 and EC.3).
A complete formalization would produce reusable definitions of the constrained control value, the extended-real Hamiltonian and its envelopes, and terminal limits for discontinuous payoffs. The paper's results are proved on paper but have no machine-checked proof in this proposal. The declarations here are compiled statements awaiting proofs. Independent work on the comparison theorem, boundary behavior, terminal asymptotics, and supporting real analysis can proceed against the same definition layer.
The usual terminal condition does not describe the limit of as approaches when jumps. Replacing the limit by would erase the singular behavior that the paper studies. The bounded-portfolio condition instead depends on the left limit , the size of the jump, and the scaled quantity . A viscosity comparison argument must handle this terminal profile while the Hamiltonian itself can be infinite or discontinuous in the unbounded portfolio regime. The liquidation boundary has a separate CRRA asymptotic when utility diverges at zero. Each of these clauses is part of the solution concept and must remain compatible with the value function.
The Lean market stores as real numbers and as extended real endpoints. It assumes , , , , and at least one nonzero admissible weight. The last three inequalities include the paper's standing bounds and exclude . Admissible controls are progressively measurable, obey the bounds and liquidation floor, satisfy the integral wealth equation through a Brownian Itô integral, and have integrable terminal utility. The supremum of their expectations is extended real so an infinite value is preserved; the goal explicitly proves finiteness before converting it to a real value. Brownian motions are quantified over filtered probability spaces and have independent future increments relative to their filtration.
The PDE domain is . Semicontinuous envelopes and boundary and terminal limits approach within . Smooth tests are real functions. The Hamiltonian and its envelopes are extended real; finite-width expressions involving are used only under bounded portfolio endpoints. The terminal point is included only for the finite-utility boundary branch, where the source defines . The CRRA formula uses a logarithmic branch at zero power, avoiding division by zero. These commitments rule out a vacuous solution notion or a value function defined as an arbitrary viscosity solution. Proving the control value finite, nontrivial comparison, and both terminal limits remains part of the mission. The e-companion's multivariate statements are included only in the one-stock constant-coefficient specialization used by Theorems 4.1–4.2.
We show that the new quantum extension of Renyi's \alpha-relative entropies, introduced recently by Muller-Lennert, Dupuis, Szehr, Fehr and Tomamichel, J. Math. Phys. 54, 122203, (2013), and Wilde, Winter, Yang, Commun. Math. Phys. 331, (2014), have an operational interpretation in the strong converse problem of quantum hypothesis testing. Together with related results for the direct part of quantum hypothesis testing, known as the quantum Hoeffding bound, our result suggests that the operationally relevant definition of the quantum Renyi relative entropies depends on the parameter \alpha: for \alpha<1, the right choice seems to be the traditional definition, whereas for \alpha>1 the right choice is the newly introduced version. As a sideresult, we show that the new Renyi \alpha-relative entropies are asymptotically attainable by measurements for \alpha>1, and give a new simple proof for their monotonicity under completely positive trace-preserving maps.
This mission is the statement-level formalization of Quantum hypothesis testing and the operational interpretation of the quantum Renyi relative entropies (arXiv:1309.3228v5). 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 Exact strong converse exponent in quantum hypothesis testing (Theorem IV.10, PDF p. 15). 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:
In this note we study in a finite dimensional Lie algebra the set of all those elements x for which the closed convex hull of the adjoint orbit contains no affine lines; this contains in particular elements whose adjoint orbits generates a pointed convex cone~. Assuming that is admissible, i.e., contains a generating invariant convex subset not containing affine lines, we obtain a natural characterization of such elements, also for non-reductive Lie algebras. Motivated by the concept of standard (Borchers) pairs in QFT, we also study pairs of Lie algebra elements satisfying for which pointed. Given , we show that such elements can be constructed in such a way that defines a -grading, and characterize the cases where we even get a -grading.
This mission is the statement-level formalization of Elements in pointed invariant cones in Lie algebras and corresponding affine pairs (arXiv:2110.07297v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
33 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.20: Characterization Theorem (Theorem 3.20: Characterization Theorem, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
14 results of the paper are not stated yet, because the library lacks an interface they need:
We study the loss of entanglement of bipartite state subjected to discarding or measurement of one qubit. Examining the behavior of different entanglement measures, we find that entanglement of formation, entanglement cost, and logarithmic negativity are lockable measures in that it can decrease arbitrarily after measuring one qubit. We prove that any convex and asymptotically non-continuous measure is lockable. As a consequence, all the convex roof measures can be locked. Relative entropy of entanglement is shown to be a non-lockable measure.
This mission is the statement-level formalization of Locking entanglement measures with a single qubit (arXiv:quant-ph/0404096v1). 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 One-qubit locking of formation, operational cost, and logarithmic negativity (Eqs. (1)–(3), continuation on p.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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Assume that two distant parties, Alice and Bob, as well as an adversary, Eve, have access to (quantum) systems prepared jointly according to a tripartite state. In addition, Alice and Bob can use local operations and authenticated public classical communication. Their goal is to establish a key which is unknown to Eve. We initiate the study of this scenario as a unification of two standard scenarios: (i) key distillation (agreement) from classical correlations and (ii) key distillation from pure tripartite quantum states. Firstly, we obtain generalisations of fundamental results related to scenarios (i) and (ii), including upper bounds on the key rate. Moreover, based on an embedding of classical distributions into quantum states, we are able to find new connections between protocols and quantities in the standard scenarios (i) and (ii). Secondly, we study specific properties of key distillation protocols. In particular, we show that every protocol that makes use of pre-shared key can be transformed into an equally efficient protocol which needs no pre-shared key. This result is of practical significance as it applies to quantum key distribution (QKD) protocols, but it also implies that the key rate cannot be locked with information on Eve's side. Finally, we exhibit an arbitrarily large separation between the key rate in the standard setting where Eve is equipped with quantum memory and the key rate in a setting where Eve is only given classical memory. This shows that assumptions on the nature of Eve's memory are important in order to determine the correct security threshold in QKD.
This mission is the statement-level formalization of Unifying classical and quantum key distillation (arXiv:quant-ph/0608199v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Pure-state intrinsic information equals twice marginal squashed entanglement (pure-intrinsic-squashed, 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.
21 results of the paper are not stated yet, because the library lacks an interface they need:
We provide a complete picture of contractivity of trace preserving positive maps with respect to -norms. We show that for contractivity holds in general if and only if the map is unital. When the domain is restricted to the traceless subspace of Hermitian matrices, then contractivity is shown to hold in the case of qubits for arbitrary and in the case of qutrits if and only if . In all non-contractive cases best possible bounds on the -norms are derived.
This mission is the statement-level formalization of Contractivity of positive and trace preserving maps under Lₚ norms (arXiv:math-ph/0601063v1). 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 Sharp general Schatten-norm bound and trace-map attainment (Theorem II.1 and following attainment clause, 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:
The entanglement cost of a quantum channel is the minimal rate at which entanglement (between sender and receiver) is needed in order to simulate many copies of a quantum channel in the presence of free classical communication. In this paper we show how to express this quantity as a regularised optimisation of the entanglement formation over states that can be generated between sender and receiver. Our formula is the channel analog of a well-known formula for the entanglement cost of quantum states in terms of the entanglement of formation; and shares a similar relation to the recently shattered hope for additivity. The entanglement cost of a quantum channel can be seen as the analog of the quantum reverse Shannon theorem in the case where free classical communication is allowed. The techniques used in the proof of our result are then also inspired by a recent proof of the quantum reverse Shannon theorem and feature the one-shot formalism for quantum information theory, the post-selection technique for quantum channels as well as Sion's minimax theorem. We discuss two applications of our result. First, we are able to link the security in the noisy-storage model to a problem of sending quantum rather than classical information through the adversary's storage device. This not only improves the range of parameters where security can be shown, but also allows us to prove security for storage devices for which no results were known before. Second, our result has consequences for the study of the strong converse quantum capacity. Here, we show that any coding scheme that sends quantum information through a quantum channel at a rate larger than the entanglement cost of the channel has an exponentially small fidelity.
This mission is the statement-level formalization of Entanglement Cost of Quantum Channels (arXiv:1108.5357v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Operational channel entanglement cost equals regularized maximum formation (Theorem 12 (Eq.22; paper-result seed), PDF p. 7). 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.
11 results of the paper are not stated yet, because the library lacks an interface they need:
We investigate the classical communication over quantum channels when assisted by no-signaling (NS) and positive-partial-transpose-preserving (PPT) codes, for which both the optimal success probability of a given transmission rate and the one-shot -error capacity are formalized as semidefinite programs (SDPs). Based on this, we obtain improved SDP finite blocklength converse bounds of general quantum channels for entanglement-assisted codes and unassisted codes. Furthermore, we derive two SDP strong converse bounds for the classical capacity of general quantum channels: for any code with a rate exceeding either of the two bounds of the channel, the success probability vanishes exponentially fast as the number of channel uses increases. In particular, applying our efficiently computable bounds, we derive an improved upper bound on the classical capacity of the amplitude damping channel. We also establish the strong converse property for the classical and private capacities of a new class of quantum channels. We finally study the zero-error setting and provide efficiently computable upper bounds on the one-shot zero-error capacity of a general quantum channel.
This mission is the statement-level formalization of Semidefinite programming strong converse bounds for classical capacity (arXiv:1610.06381v4). 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 11: β strong converse bound (original seed pinned from abstract) (Theorem 11, PDF p. 16). 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:
Entanglement distillation, an essential quantum information processing task, refers to the conversion from multiple copies of noisy entangled states to a smaller number of highly entangled states. In this work, we study the non-asymptotic fundamental limits for entanglement distillation. We investigate the optimal tradeoff between the distillation rate, the number of prepared states, and the error tolerance. First, we derive the one-shot distillable entanglement under completely positive partial transpose preserving operations as a semidefinite program and demonstrate an exact characterization via the quantum hypothesis testing relative entropy. Second, we establish efficiently computable second-order estimations of the distillation rate for general quantum states. In particular, we provide explicit as well as approximate evaluations for various quantum states of practical interest, including pure states, mixture of Bell states, maximally correlated states and isotropic states.
This mission is the statement-level formalization of Non-asymptotic entanglement distillation (arXiv:1706.06221v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact Hermitian hypothesis-testing characterization (Seed abstract main result pinned to Theorem 4, Eq. (25): exact hypothesis-testing characterization, 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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
In a buck-passing game, each participant chooses who will receive a task, burden, or token next. The eventual share of time spent holding it depends on every participant's choice. This makes a small network into a game: a local change of one outgoing edge can alter the long-run burden across an entire part of the network. Cominetti, Quattropani, and Scarsini study this setting in The Buck-Passing Game, including deterministic and stochastic versions. The deterministic result targeted here says that players can choose their outgoing edges without knowing where the buck will start and still reach a pure Nash equilibrium.
That independence from the starting distribution matters because an initial probability law can be unknown or disputed. A Nash equilibrium found for one chosen law may cease to be an equilibrium under another. The paper calls a profile that works for every law a prior-free Nash equilibrium. Its existence is the subject of Theorem 2 on p. 10 of arXiv:1808.03206v4.
Start with a finite directed graph without loops. Each vertex is a player and has a nonempty set of outgoing neighbors. Player chooses one neighbor ; the collection is a strategy profile. Once these choices are fixed, the graph becomes a functional graph: from each vertex there is exactly one selected outgoing edge, and the buck moves according to the map .
At time zero, Nature places the buck at a vertex drawn from a probability distribution on . At time , the buck is at if it started at . The cost of player is the expected limiting fraction of positive times for which holds it. Players minimize their own costs. The definition follows equation (3) on p. 6: for each possible start , count visits at times , divide by , take the limit, and average the resulting value with weights .
Every orbit on a finite functional graph eventually enters a directed cycle. The vertices whose orbits enter the same cycle form its basin, called a unicycle in the paper. The cycles are pairwise disjoint, and their basins partition the vertices. Equation (6) on p. 7 says that a player outside a cycle has zero long-run cost, while a player on cycle has cost . A unilateral change is profitable when it strictly lowers the changing player's cost; a profile with no profitable change is a pure Nash equilibrium. Definitions 1–3 and equations (3)–(6) fix these terms.
The main target is Theorem 2. The order of its quantifiers is essential: one profile must work for every initial probability distribution. Writing for the probability distributions on , the claim is
The proposed milestones match the claims leading up to this result in §3.1 of the paper. A component-wise minimizer of a generalized ordinal potential is a Nash equilibrium. Proposition 1 guarantees an equilibrium for a finite generalized ordinal potential game and also for the compact, lower semicontinuous case. Equation (6) identifies costs from the limiting visit frequencies. The p. 9 classification describes the two types of profitable deviation. Theorem 1 supplies a generalized ordinal potential that depends only on the selected cycles:
The full-support assertion in the second sentence of Theorem 1 is outside this mission's milestone list. The existence target uses its first assertion. Theorem 3's bound on improvement-path length and the paper's stochastic, constrained, and buck-holding games are also outside this target.
Theorem 2 guarantees a pure strategy profile with stability across all starting distributions, including distributions concentrated at a single vertex. It strengthens the statement that each fixed distribution has some equilibrium, which could choose a different profile each time. In this deterministic model the same strategy choices serve all initial laws. The paper's proof ties that claim to a graph quantity, , whose value has no parameter. Theorems 1–2, pp. 9–10 state the potential and equilibrium conclusions.
The research result is already proved in the paper. The work here is to give its definitions and statements precise Lean types and to establish machine-checked proofs of the limit identity, graph-change classification, potential property, and existence theorem. The drafted theorem files currently contain sorry, so their compilation checks statement well-formedness rather than proving the claims. The finite cost-game definitions and orbit-frequency statement can also support later formalizations of deterministic dynamics and potential games.
A finite orbit is eventually periodic, but the cost is defined using a limit of averages from time through . The formal development must establish that limit for every initial vertex before substituting the cycle-and-basin formula. It must then track what a one-player change does to the cycles of a functional graph. The changed edge can lengthen one cycle or remove it by sending its vertices toward a different cycle; costs also depend on how much initial mass reaches the affected basin. Merely knowing that a player's new out-neighbor is in the same basin does not show an improvement, because the new cycle may be shorter or unchanged. These are the concrete issues behind equation (6) and Theorem 1.
Lean gives the general cost-game predicates their own definition module. The deterministic model represents by a finite type, with the paper's loopless and nonempty out-neighborhood assumptions bundled into BPGraph. A strategy is an out-neighbor subtype, so every profile selects only legal edges. The distribution is a real vector with nonnegative coordinates summing to one. Costs and the potential are real-valued. The cost is built from the orbit's Cesàro limit in equation (3); equation (6) is a separate theorem asserting convergence and the resulting value. Cycles are finite sets of periodic points, deduplicated so that has exactly one summand per cycle; basins contain the vertices whose orbits reach that cycle. Classical decidability constructs these finite sets.
The empty vertex type is permitted by the Lean representation; it has one empty strategy profile and no probability distribution. A one-vertex graph cannot satisfy both the loopless and nonempty out-neighborhood assumptions. The prior-free goal explicitly places the profile before the quantifier over distributions. Defining cost by the cycle formula, or choosing a separate equilibrium after seeing each distribution, would change the target. Proposition 1 makes nonempty strategy sets explicit, as an empty compact strategy set has no profile. The first profitable-deviation case requires that the changed edge lengthen the cycle; membership in the basin alone does not do so.
The development needs reusable results on finite function iteration, periodic points, Cesàro frequencies, finite products, and lower semicontinuous minimization. The goal and its milestones invite proofs of those statements under the recorded hypotheses. All mission items are drafted locally and remain unproved until solvers supply proofs.
We present a bouquet of continuity bounds for quantum entropies, falling broadly into two classes: First, a tight analysis of the Alicki-Fannes continuity bounds for the conditional von Neumann entropy, reaching almost the best possible form that depends only on the system dimension and the trace distance of the states. Almost the same proof can be used to derive similar continuity bounds for the relative entropy distance from a convex set of states or positive operators. As applications we give new proofs, with tighter bounds, of the asymptotic continuity of the relative entropy of entanglement, , and its regularization , as well as of the entanglement of formation, . Using a novel "quantum coupling" of density operators, which may be of independent interest, we extend the latter to an asymptotic continuity bound for the regularized entanglement of formation, aka entanglement cost, . Second, analogous continuity bounds for the von Neumann entropy and conditional entropy in infinite dimensional systems under an energy constraint, most importantly systems of multiple quantum harmonic oscillators. While without an energy bound the entropy is discontinuous, it is well-known to be continuous on states of bounded energy. However, a quantitative statement to that effect seems not to have been known. Here, under some regularity assumptions on the Hamiltonian, we find that, quite intuitively, the Gibbs entropy at the given energy roughly takes the role of the Hilbert space dimension in the finite-dimensional Fannes inequality.
This mission is the statement-level formalization of Tight uniform continuity bounds for quantum entropies: conditional entropy, relative entropy distance and energy constraints (arXiv:1507.07775v6). 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 Remark 3: explicit near-tightness example for Lemma 2 (Remark 3: explicit near-tightness example for Lemma 2, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
12 results of the paper are not stated yet, because the library lacks an interface they need:
An entrepreneur who knows more about a venture than its investors can convey information through the share of the venture that she keeps. A larger retained share exposes her to more of its uncertain payoff. The cost of this signal depends on what investors buy: an equity claim receives revenue after production costs, while a token claim receives a share of gross revenue. Chod and Lyandres examine how that difference affects the ability of high- and low-quality ventures to separate in an initial coin offering. Their analysis identifies a range of venture heterogeneity and payoff volatility in which tokens support separation and equity does not. The source for this mission is their SSRN working paper, version of December 14, 2019, §4 and Proposition 6.
This result concerns a specific information problem. Investors cannot observe venture quality before buying; an entrepreneur knows her own type. If the same financing contract is used regardless of type, investors cannot identify quality from the offering. A separating outcome instead assigns different sale fractions to the two types and makes the resulting investor beliefs consistent with each type's incentives. The paper compares the feasibility of such outcomes for the two securities, under a model in which the agency effects studied in its earlier sections are set aside.
There are two venture types, high and low . The entrepreneur observes the type; investors observe the fraction offered for sale. Type has uncertain shock with a normal approximation of mean and standard deviation , where . Revenue is . The entrepreneur pays fixed production cost and initial investment . Her CARA utility at terminal wealth is
Under a belief that the venture has type , investors value the revenue using that type's distribution. An actual type who sells fraction therefore receives the cash value , retains fraction of her own realized revenue, and has expected utility
The financing method changes the smallest fraction she must sell. The equity financing threshold is , and the token financing threshold is . The cost appears in the equity denominator because equity buyers receive a claim after that cost. With a positive cost, the token threshold is strictly smaller.
Investors use a threshold belief: they infer when and when . A separating equilibrium requires both types to prefer the side of the threshold assigned to them, subject to their financing constraints. The paper's conditions (23) and (24) compare the best feasible payoffs on the two sides. A least-cost separating equilibrium is a separating equilibrium that is not Pareto-dominated by another such equilibrium. The paper defines an interior share in equation (25); Proposition 5 identifies its role as the least-cost threshold whenever separation is feasible.
The central question is when tokens have a signaling advantage: a separating equilibrium exists with tokens, and none exists with equity. Proposition 6 gives two parameter windows. For fixed values of the other parameters, there are thresholds and such that
and, in a separate comparison,
The first window varies the low-type mean while keeping the high-type mean fixed. Increasing reduces the difference between the types. The second varies payoff volatility. Both claims concern the game's equilibrium conditions, rather than only a numerical inequality between closed-form expressions.
The milestone sequence begins with the CARA-normal expected-utility formula (38) and the interior range of . It then records the low type's indifference at and the threshold form of condition (24). Proposition 5 characterizes the equilibrium under each security. The remaining milestones compare the financing thresholds and record the monotonicity of with respect to and . These are the paper's stated results and intermediate claims in §4 and its appendix.
The theorem isolates a case in which the form of the security changes what investors can infer. A token offering can permit the high type to sell enough to finance the investment while retaining a stake that the low type does not want to imitate. Equity may require a larger sale fraction, closing that opportunity. The window statement also says the advantage is limited: when types are too different or too similar, or when volatility is outside the relevant range, tokens do not uniquely enable separation under this model.
A machine-checked development would connect an explicit probabilistic payoff model, incentive comparisons over feasible actions, the equilibrium characterization, and comparative statics in one chain. The cited paper proves these results informally; the theorem files here are open proof targets. The CARA-normal calculation and the representation of threshold equilibria are reusable in other signaling models with normally distributed payoffs.
The direct comparison of financing thresholds is insufficient for the goal. Separation also depends on whether a low-quality entrepreneur would imitate a high-quality one, and whether a high-quality entrepreneur prefers to reveal her type. These conditions optimize utility over different feasible sale fractions, including a strict boundary on the low-belief side of the threshold. The paper's closed form for expresses the point at which the low type becomes indifferent, but the full result must also establish the high type's incentive and the uniqueness of the refined equilibrium.
The comparative statics require control of two moving parts: the threshold changes with the low-type mean and volatility, while the high-type financing thresholds remain fixed in those comparisons. The interval endpoints in Proposition 6 are existential, so their placement must reflect the feasible parameter domain and the strict or weak inequalities at each boundary.
Lean represents the normal approximation for directly with gaussianReal of mean and variance . This follows the paper's approximation even though a literal square is nonnegative and a nondegenerate normal variable is not. Revenue is . Expected utility remains a Gaussian integral; equation (38) is a theorem target, not a definition of that utility. All payoffs and thresholds are real numbers.
The parameter domain has , , , , , and . The last two substantive additions to the page's stated model are , needed for the strict token-equity threshold comparison, and the low-type financing condition, needed for the paper's action to be feasible. An equilibrium threshold satisfies . The least-cost refinement is represented by the paper's operational exclusion of Pareto-dominated separating equilibria, without claiming a general formalization of the Cho–Kreps intuitive criterion.
The high and low incentive conditions quantify only over feasible fractions. Equilibrium payoffs use real suprema on the corresponding action sets; within an equilibrium these sets are nonempty and the utility is bounded above. The goal defines signaling advantage through existence and nonexistence of separating equilibria, so it cannot be discharged by redefining the advantage as the closed-form inequality. Useful contributions include Gaussian expected-utility lemmas, optimization over the feasible intervals, equilibrium existence and uniqueness, and the real-analysis results needed for the parameter windows.
The squashed entanglement of a quantum channel is an additive function of quantum channels, which finds application as an upper bound on the rate at which secret key and entanglement can be generated when using a quantum channel a large number of times in addition to unlimited classical communication. This quantity has led to an upper bound of on the capacity of a pure-loss bosonic channel for such a task, where is the average fraction of photons that make it from the input to the output of the channel. The purpose of the present paper is to extend these results beyond the single-sender single-receiver setting to the more general case of a single sender and multiple receivers (a quantum broadcast channel). We employ multipartite generalizations of the squashed entanglement to constrain the rates at which secret key and entanglement can be generated between any subset of the users of such a channel, along the way developing several new properties of these measures. We apply our results to the case of a pure-loss broadcast channel with one sender and two receivers.
This mission is the statement-level formalization of Bounds on entanglement distillation and secret key agreement for quantum broadcast channels (arXiv:1503.08139v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal-entropy difference: monotonicity and finite or infinite limit (§7, paragraph containing (7.18), PDF p. 28). 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.
11 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum amplifier channels are at the core of several physical processes. Not only do they model the optical process of spontaneous parametric down-conversion, but the transformation corresponding to an amplifier channel also describes the physics of the dynamical Casimir effect in superconducting circuits, the Unruh effect, and Hawking radiation. Here we study the communication capabilities of quantum amplifier channels. Invoking a recently established minimum output-entropy theorem for single-mode phase-insensitive Gaussian channels, we determine capacities of quantum-limited amplifier channels in three different scenarios. First, we establish the capacities of quantum-limited amplifier channels for one of the most general communication tasks, characterized by the trade-off between classical communication, quantum communication, and entanglement generation or consumption. Second, we establish capacities of quantum-limited amplifier channels for the trade-off between public classical communication, private classical communication, and secret key generation. Third, we determine the capacity region for a broadcast channel induced by the quantum-limited amplifier channel, and we also show that a fully quantum strategy outperforms those achieved by classical coherent detection strategies. In all three scenarios, we find that the capacities significantly outperform communication rates achieved with a naive time-sharing strategy.
This mission is the statement-level formalization of Capacities of Quantum Amplifier Channels (arXiv:1605.04922v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Equation (66), Appendix B (B9)–(B10): coherent-detection capacity regions (Equation (66), Appendix B (B9)–(B10): coherent-detection capacity regions, 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.
10 results of the paper are not stated yet, because the library lacks an interface they need: