Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A seller deciding whether to offer two products separately or as one bundle also changes what customers need to learn before buying. A customer can know what a familiar product is worth to her while remaining uncertain about a new one. She may pay to inspect the new product, buy it without inspection, or leave. The seller's price can move customers between those choices. Wu, Jin and Chen study this interaction in a tractable two-product market and identify the exact search-cost threshold at which the preferred selling scheme changes (Wu, Jin and Chen, 2022, §§3–5). The question matters for pricing a new product alongside an established one when customers can buy from a description but can also spend effort learning whether the new product suits them.
A monopolist faces a unit mass of risk-neutral customers and has zero marginal production cost. Each customer values products 1 and 2 at independent uniform valuations . Product 1 is mature: its valuation is already known to that customer. Product 2 is new: before search, the customer knows only that its valuation is uniform on , with mean . Searching product 2 reveals and costs . Search is non-obligatory: a customer can buy a new product without inspecting it. The model and the information available at each decision are specified in §3 of the working paper.
Under separate selling, the seller posts nonnegative prices and , and each product is purchased independently. The mature product sells when ; its revenue is . For the new product, buying without search gives expected payoff , searching gives , and leaving gives zero. If a customer searches, she buys only when the observed . Write for the resulting purchase probability, , and for total separate-selling revenue (§4).
Under pure bundling, the seller posts one nonnegative price for both products. A customer who knows compares leaving, buying immediately with expected payoff , and searching product 2 with expected payoff . After search she buys the bundle only when . Let be the probability of purchase after these choices, integrating over both independent uniform valuations, and let (eqs. (1)–(2), pp. 11–13).
The customer follows the paper's footnote-10 tie rule: when an immediate purchase and search have equal best payoff, she buys without search; otherwise she searches if its expected payoff is nonnegative and a valuation in the support can meet the price. If search and leaving tie at zero payoff beyond the support, she leaves. The rule matters at exact optimal prices. It also ensures a customer is counted once when the two demand segments printed in §5.2 overlap at .
The mission first identifies the optimal new-product and bundle revenues, including prices at which they are attained. The new-product maximum has three search-cost regimes: , , and . The bundle maximum likewise has three regimes, with boundaries and . These are the cases of Propositions 1 and 2, pp. 9–13, and form the central milestones. The mature product's optimal revenue is , attained at price .
The goal is the paper's Theorem 1, p. 15. Write for the maximum of over , and for the maximum of over . The theorem asserts that these maxima exist and
At , both revenues equal . The formal goal therefore also records the strict form, exactly when , under the standing assumption . It asserts no unique optimal price: the new product can have two optimal prices at .
The threshold gives an exact decision rule in this model: below it, bundling earns more; at it, the schemes tie; above it, separate selling earns more. It is a comparison of optimized revenues, after the seller chooses the best admissible price for each scheme, rather than a comparison at fixed prices. It also makes precise how the familiar product's known value changes the demand generated by searching for the new one (Theorem 1 and its discussion, pp. 15–16).
The paper gives the analytical results, but this mission targets machine-checked proofs of their formal statements. The development contributes a reusable payoff-based rule for non-obligatory search and a concrete uniform-valuation revenue model. It leaves the interval-integral demand definition in place so that deriving the piecewise optimal revenues remains genuine mathematical work. No proof of these results is included in the SSRN copy held for this mission; the supporting milestones are the results stated in its main text.
Search and purchase choices change discontinuously when a price crosses a payoff threshold. For a single new product the same choice is made by every customer, but under bundling the mature valuation sorts customers into buyers without search, searchers who may buy after observing , and nonbuyers. The bundle demand must integrate across these groups. Its maximizing price changes regime as moves through and (§5.2 and Figure 1, pp. 12–13). A fixed-price comparison cannot establish Theorem 1, because the best price itself depends on search cost and on the selling scheme.
Lean uses real prices and costs, with and every price restricted to be nonnegative. Uniform expectations are interval integrals over , and uniform tail probabilities are volumes intersected with that interval. Demand and revenue are built from the customer choice rule; optimal values are expressed as greatest elements of the image of the admissible price set. In particular, the goal does not substitute the closed formulas from Propositions 1 and 2 for those maxima. Such a substitution would reduce the intended economic comparison to arithmetic and leave the search model untested.
The formal choice rule implements footnote 10's immediate-purchase tie preference and selects leaving when zero-cost search could never result in a purchase. Bundle demand counts each customer once, including at , where the two weak-inequality demand segments in the printed text overlap. The mature and new valuations remain independent uniform variables; search reveals the new value only, and every search incurs cost . The real-valued interval integrals represent finite, bounded payoffs or bounded purchase probabilities, so their values are genuine expectations and probabilities rather than defaults for nonintegrable functions. No separate assumption of a unique maximizer is used. Contributions that establish the integral identities, measurable choice regions, piecewise demand formulas, and global optimality statements are within scope.
Health insurers pay providers in one of a few ways, and the choice shapes what providers charge. Under variable payment (co-insurance) the patient pays a fixed fraction of the provider's price. Under reference pricing the insurer announces a cap for a procedure: the patient pays a fixed co-payment at any provider charging at most , and in addition the whole excess above at a provider charging more. The authors motivate their model with the California Public Employees' Retirement System's reference-pricing program for knee and hip replacement (Nassiri, Adida and Mamani, 2022).
S. Nassiri, E. Adida and H. Mamani (Reference pricing for healthcare services, M&SOM 24(2), 2022; author manuscript SSRN 3176280) model the two payment systems as price games between competing providers whose patients choose by a multinomial logit rule, and compare the resulting equilibria. Their first comparison, Proposition 5, is about provider prices. Variable payment leads to higher prices than reference pricing exactly when the patient cost share is below a provider-specific threshold. This mission formalizes that result and the equilibrium characterizations it rests on.
Two providers, , offer a procedure to patients. Provider has a non-price attribute , with . Both providers have nonnegative treatment cost , and every patient has price sensitivity . The alternative to treatment has utility . If the patient's out-of-pocket cost at provider is , provider 's market share is
where is the price vector. Provider 's profit is .
Under each system the two providers choose prices simultaneously, and an equilibrium is a pure Nash equilibrium of that game: no provider can raise its own profit by changing only its own price. Each system also carries a standing assumption on best responses. Assumption 1 says that, as the rival's price tends to infinity, the limit of provider 's share at its VP best response is at most . Assumption 2 is the same condition under RP.
Assume, in addition, that the co-payment is below the reference price, . Let be an RP equilibrium. For each provider there is such that, for every and every VP equilibrium ,
The threshold is only claimed to exist; it is not given by a formula, and the statement fixes no constant.
The result. Proposition 5 sorts the two payment systems by cost share. When patients bear a small share of the price, co-insurance leaves providers free to charge more than they would under a reference-price cap. Above the threshold, co-insurance disciplines prices more than the cap does. The paper's later comparisons build on this price comparison: patient out-of-pocket and utility (Proposition 6), provider profit (Proposition 7) and insurer cost (Proposition 8). The equilibrium characterizations, Theorems 1 and 2, are also what the paper's numerical study computes with. Proposition 2 is the formal statement of shadow pricing: value-based providers charge exactly the cap.
The formalization. The result has a published proof but no machine-checked one. The paper cites external equilibrium results, leaves several inequalities to "some algebra", and does not separately state continuity of the VP equilibrium price in (Nassiri, Adida and Mamani, Appendix D). A formal development pins down which hypotheses each step uses; the co-payment condition is one that the theorem's sentence omits. It also yields reusable facts about two-firm logit price competition.
The central difficulty is the comparison of equilibrium prices across two different games. Under RP, a provider's out-of-pocket charge changes formula at , and its equilibrium status depends on the rival's price. Both providers may be value-based, both may be non-value-based, or only provider 2 may be non-value-based. In the second case, each best-response price depends on the other provider's price, so separate comparisons of the two providers' first-order conditions are insufficient. The VP equilibrium price must also vary continuously with for the strict inequality to define a threshold; strict monotonicity alone does not establish that.
All quantities are real numbers. Providers are Fin 2, and index 0 is the paper's provider 1. Prices range over instead of the paper's . This does not change the equilibria: an equilibrium price earns positive profit, and any price at or below earns non-positive profit. Equilibrium is the published generic pure-Nash relation CarbonDoubleCount.Planner.IsPureNash, with every price set equal to . "Value-based" is read as , following Proposition 2. The standing assumptions are , , and (implicit in the paper), and . The nonnegative cost bound is needed: negative treatment cost can make VP equilibrium prices rise with , contradicting Lemma 2(a). Assumptions 1 and 2 are encoded as follows: best responses exist, and along every best-response selection the share converges, as the rival's price tends to infinity, to a limit of at most . The goal assumes Assumption 1 at every , and it adds , which the proof uses and without which the statement fails numerically. "As approaches 1" in the proof is read as the value at .
The goal is stated about the Nash equilibria of both games and quantifies over every VP equilibrium at every . A version about solutions of the first-order systems would bypass Theorems 1 and 2 and is not the target. Neither is "VP is higher for small and lower at ", which is only milestones 3 and 10.
A complete development needs: derivative and quasi-concavity facts for logit shares in one's own price; existence of an equilibrium in a two-player game with continuous, quasi-concave payoffs on compact price intervals; uniqueness for the logit first-order system; implicit-function continuity of the equilibrium in ; and the RP case analysis. The logit and quasi-concavity lemmas are reusable for any logit price competition model. Proofs of individual milestones, and alternative arguments, are welcome.
An advance market commitment (AMC) is a promise to pay for a product if it is developed and supplied. For vaccines intended for low-income countries, a donor may use an AMC to encourage a manufacturer to invest before demand is certain. The investment decision happens before the firm and donor negotiate actual purchases. This timing creates a hold-up problem: once capacity is sunk, the firm receives only its negotiated share of the benefit from using it. Kremer, Levin, and Snyder analyze which commitments change that incentive in Designing Advance Market Commitments for New Vaccines. This mission concerns their framework AMC, in which a donor puts money in an interest-bearing escrow fund that pays a subsidy per vaccine until exhausted.
The result is specific to a temporary subsidy and a monopoly firm. It explains why depositing money in an escrow can transfer value to the firm without raising its chosen capacity. The paper also studies perpetual subsidies, supply commitments, forcing contracts, competing firms, and products farther from development. Those are different designs or regimes; their results are outside this mission.
A country receives a flow health benefit when citizens per period receive a vaccine. The benefit starts at , increases, and is strictly concave; its marginal benefit tends to zero as output grows. A donor values this benefit at fraction and pays for the vaccine. Its inverse demand is , with choke price and demand curve at positive price . Production costs per vaccine per period. The firm pays before trade to install capacity , and can produce at most in any period. Everyone discounts future flows at rate ; write for the flow equivalent of unit capacity cost. The paper maintains , so the integrated benchmark invests positive capacity. These assumptions and the interpretation of the donor and firm are from the BFI working-paper version, §§2–3.
After investment, the firm and donor bargain over vaccine purchases. Either can block trade, so both threat payoffs are zero. Efficient Nash bargaining chooses the output plan that maximizes their discounted joint surplus, and the firm receives fraction of that surplus. The firm anticipates this bargain when it chooses capacity. Without an AMC, denote its equilibrium capacity by ; with integrated control, denote the optimum by . The paper's first two propositions identify these benchmarks:
Under the framework AMC, the donor fixes a subsidy and deposits in escrow before the firm chooses . The escrow earns interest at the same rate as the participants' discounting. A subsidy is paid for each vaccine during the AMC period. If output is and , the fund is exhausted at a finite time ; afterwards there is no subsidy. The bargain chooses both AMC-period output and tail output , each bounded by capacity. If , the subsidy is perpetual at that output and there is no tail period. This branch matters when evaluating capacities the firm could have chosen instead.
The core comparison is the paper's Proposition 3. For any framework AMC whose equilibrium subsidy is temporary,
The goal covers every qualifying equilibrium. It also asserts that the displayed candidate is an equilibrium whenever , so the claim cannot hold merely because no temporary-subsidy equilibrium exists. It fixes the policy terms but does not assume the firm's capacity or bargained outputs in advance.
The milestones establish the inverse-demand property (Lemma 1), the integrated and no-AMC benchmarks (Propositions 1–2), the fund accounting identity (6), the discounted joint-surplus identity (7), full capacity utilization in the temporary regime, and the firm's ex ante profit identity (8). The last identity identifies the fund's contribution as on that regime. Their statements and numbering follow the December 2020 BFI working paper, with printed pages 6 and 10–13 and Appendix A, pages 37–38.
Proposition 2 measures the capacity lost to hold-up when a firm cannot keep all returns to investment. Proposition 3 then shows that this particular escrow design does not repair that loss when its subsidy is temporary: the fund changes the firm's payoff level while leaving the capacity choice at the no-AMC benchmark. That conclusion helps distinguish an AMC's payment amount from its effect on investment incentives. The paper's other contract designs address separate policy questions and should not be inferred from this result.
The formalization produces a reusable discounted-flow definition and a concrete capacity-and-bargaining game with an interest-bearing escrow. The source result has a paper proof; the Lean theorems here are proposed proof obligations, with no machine-checked proofs claimed. A complete development would verify the inverse-demand construction, existence and uniqueness of the relevant maxima, the escrow integral, and equilibrium optimality on both finite and perpetual subsidy branches.
The firm's value cannot be calculated by assigning full output at the outset. Bargaining chooses output after capacity is installed, and using fewer vaccines during the AMC period lengthens the subsidy period. Thus the escrow duration changes with the bargained output. The simple capacity comparison from the no-AMC benchmark only becomes applicable after the output and fund identities have been established. Moreover, the firm's alternative capacities can cross from a finite subsidy period to a perpetual one, so a statement proved only for the candidate equilibrium branch does not settle its investment choice.
All amounts, times, and discounted values are real. Discounted flows are Lebesgue set integrals over positive time; an open interval represents the AMC period, with endpoint choices irrelevant to its integral. Demand is the real infimum of nonnegative quantities at which . Its value at nonpositive prices is a Lean default and is never used in a result. The firm's value is times the real supremum of feasible joint-surplus values minus ; feasible output intervals are nonempty for admissible capacities, and the intended values are bounded and attained. Capacity is chosen over .
The Lean benefit function is twice continuously differentiable on all of , extending the paper's half-line convention so derivatives at zero are unambiguous; its sign assumptions are only for . Output is constant within the AMC and tail periods, following the paper's equation (A8) reduction. “Temporary” means at equilibrium. The model separately represents a perpetual subsidy for deviations. The framework profit is defined from bargained joint surplus and its discounted flows; equation (8) is a theorem target, and output is a bargain choice rather than a fixed capacity value. These choices keep the formal goal about the paper's investment game.
The development needs real derivatives, inverse functions, concavity, filters for the bargaining-weight limits, Lebesgue integrals of exponential flows, real suprema on compact feasible boxes, and optimization over nonnegative capacities. The discounted-flow and capacity-game infrastructure can be reused in other procurement models. Contributions that establish these interfaces or close any listed milestone support the goal.
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.
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 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 develop a formalism for distilling a classical key from a quantum state in a systematic way, expanding on our previous work on secure key from bound entanglement [K. Horodecki et. al., Phys. Rev. Lett. 94 (2005)]. More detailed proofs, discussion and examples are provided of the main results. Namely, we demonstrate that all quantum cryptographic protocols can be recast in a way which looks like entanglement theory, with the only change being that instead of distilling EPR pairs, the parties distill private states. The form of these general private states are given, and we show that there are a number of useful ways of expressing them. Some of the private states can be approximated by certain states which are bound entangled. Thus distillable entanglement is not a requirement for a private key. We find that such bound entangled states are useful for a cryptographic primitive we call a controlled private quantum channel. We also find a general class of states which have negative partial transpose (are NPT), but which appear to be bound entangled. The relative entropy distance is shown to be an upper bound on the rate of key. This allows us to compute the exact value of distillable key for a certain class of private states.
This mission is the statement-level formalization of General paradigm for distilling classical key from quantum states (arXiv:quant-ph/0506189v2). 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 1: twisting invariance (Theorem 1: twisting invariance, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
19 results of the paper are not stated yet, because the library lacks an interface they need:
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:
We present a framework to treat quantum networks and all possible transformations thereof, including as special cases all possible manipulations of quantum states, measurements, and channels, such as, e.g., cloning, discrimination, estimation, and tomography. Our framework is based on the concepts of quantum comb-which describes all transformations achievable by a given quantum network-and link product-the operation of connecting two quantum networks. Quantum networks are treated both from a constructive point of view-based on connections of elementary circuits-and from an axiomatic one-based on a hierarchy of admissible quantum maps. In the axiomatic context a fundamental property is shown, which we call universality of quantum memory channels: any admissible transformation of quantum networks can be realized by a suitable sequence of memory channels. The open problem whether this property fails for some nonquantum theory, e.g., for no-signaling boxes, is posed.
This mission is the statement-level formalization of Theoretical framework for quantum networks (arXiv:0904.4483v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
30 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1: trace preservation (Lemma 1: trace preservation, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
15 results of the paper are not stated yet, because the library lacks an interface they need:
On-demand service platforms (ride-hailing, delivery, home services) do not employ their workers. They set a price for customers and a wage per unit of work, and independent agents decide how much time to make themselves available. A recurring policy question, raised by regulators and labor advocates alike, is whether platforms should be allowed to recruit labor pools of unlimited size: a larger pool is often argued to depress what each worker earns. Benjaafar, Ding, Kong and Taylor (SSRN 3103447; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2020.0964) study this question in a model where customers care about delay. Their central result, Theorem 2, is that the answer depends on delay sensitivity: in a standard market a larger pool lowers average labor welfare, but when customers are delay-sensitive, average labor welfare first rises and then falls in the pool size.
The model has two populations, both treated as continua.
Agents. A labor pool of mass . An agent with opportunity-cost parameter who is available for time incurs cost ; has distribution on with . Given the wage , demand and labor supply , work is shared in proportion to availability, so the agent's effective wage is and his best response is . Aggregation gives the labor supply equation
Customers. Needs arise at rate (the market size); a customer with valuation seeks service if , where is the delay sensitivity and
is the delay. Demand is with the uniform cdf, and an equilibrium requires . In the benchmark demand is and the capacity constraint is .
Platform. The platform chooses , to maximize subject to these equilibrium conditions; the optimum is . The agent utilization is , and average labor welfare is
The pool sizes for which a positive optimum exists are , with for and for .
The thresholds are not given in closed form; the goal asserts only their existence.
The result. Theorem 2 separates two regimes. In a congestion regime (small pools, large delay cost ) extra agents reduce delay, stimulate demand faster than supply grows, and raise utilization, the effective wage and average labor welfare: agents exert a positive externality on one another. In a cost regime (large pools) the demand effect is exhausted and extra agents only dilute work. The paper uses this to argue against blunt caps on platform labor pools and as the baseline for its analysis of nominal and effective wage floors (§5). Without delay sensitivity the classical conclusion, that a larger pool lowers welfare, is recovered exactly.
Formalizing it. The theorem is proved in the paper, with an online appendix of implicit-function and envelope arguments. None of it is formalized. This mission produces a machine-checked model of a platform with endogenous supply and congestion-dependent demand, the reduced problem, and the comparative statics in . The paper's Lemma 11 needs a correction at (see below), which is the kind of gap a formal development exposes.
The optimum is defined implicitly by two nonlinear first-order conditions, and there is no closed form for . The obvious route, differentiating in , gives a quantity whose sign is the competition between the growth of and the factor , and that sign changes with . Monotonicity arguments of the usual kind (supermodularity in , which does give that increases) say nothing about such ratios. The obstacle is single crossing of a quantity defined only implicitly through the optimum, not differentiability. The boundary behaviour at and (Lemma 13) is also needed and is itself nontrivial at , where .
Everything lives in the namespace LaborWelfare.PoolSize, with one definitions file Setting.
vbar), (Lam), , real (beta), and a probability measure on carried by with . The density of is not required: only enters any result. is a real power.StrictMonoOn, StrictAntiOn), as the paper fixes on p. 11; the thresholds are three separate numbers.A complete development needs real analysis on implicitly defined functions (implicit-function theorem in one variable, envelope arguments, monotone limits) and an argmax framework for the two-variable profit; these are reusable for other platform-pricing papers. Proofs of any milestone are welcome, as are alternative routes to the threshold statements.
A city can reduce contacts by limiting activity in selected neighborhoods. Such a policy affects more than the residents of the closed neighborhood: people travel across neighborhood boundaries, meet there, and carry infection back to their home neighborhoods. A citywide closure ignores these differences in movement and economic cost. Birge, Candogan, and Feng model these links and ask how to curb infection while preserving activity where it is most valuable. Their 2020 working paper gives separate optimization formulations for a large infection regime and a small infection regime; this mission concerns the latter. The paper later uses movement and economic data for New York City, while the theorem here is independent of those data. Birge, Candogan, and Feng, BFI Working Paper 2020-57.
There are neighborhoods. Neighborhood has population , and its residents spend a fraction of their time in neighborhood . The row sum is at most one; remaining time is spent in isolation. An activity level controls contact at destination . This makes the number of infectious contacts depend on where residents of every neighborhood meet, not only where they live.
Each neighborhood has susceptible, exposed, clinically infected, subclinically infected, and recovered populations. The effective contact rate is , the progression rate from exposed to infected is , the clinical fraction is , the relative infectiousness of subclinical cases is , the removal rate is , and the natural birth and death rate is . The model uses and . At the disease-free equilibrium, the exposed and infected populations vanish and the susceptible population in neighborhood equals .
The paper separates the infected-coordinate dynamics into a vector of new infections and a vector of other transfers. In the coordinate order exposed, clinical, subclinical, their Jacobians at the disease-free equilibrium are and , each a real matrix. Define as the greatest modulus of a complex eigenvalue of . The effective reproduction rate in condition (6) is . This is a property of the full infected-coordinate system. Model and condition (6), pp. 7–13.
The intermediate targets identify the displayed inverse of , the smaller matrix sharing the nonzero eigenvalues of , and its diagonal similarity to a symmetric matrix. They connect condition (6) with a bound on the spectral radius of the reduced matrix. Each target is taken from the proof of Lemma 2.1 in the working paper.
The goal is the paper's Lemma 2.1. Let , , , and . With meaning that is positive definite, the target is
The strict inequality is the stability condition stated in the paper. The semidefinite program labelled (P2) uses a non-strict inequality to close its feasible region; that optimization problem is outside this mission. Lemma 2.1 and (P2), pp. 13–14.
The left side of Lemma 2.1 is a spectral test on a next generation matrix. The right side is a linear matrix inequality in the activity variables because is diagonal and depends linearly on . It therefore supplies the mathematical constraint used by the paper's small infection optimization problem. The theorem states equivalence for the paper's spatial epidemic model; it does not assert that the optimization problem has a solution or that a chosen activity vector minimizes economic loss. Birge, Candogan, and Feng, pp. 13–14.
The working paper proves the lemma in ordinary mathematics. The formalization task is to give its matrices and hypotheses precise Lean definitions, then prove the spectral and positive definiteness statements. The definition of the reproduction rate and the intermediate matrix identities can also support later formal statements about related compartmental models. No machine-checked proof of these draft items is claimed here.
The matrix is generally nonsymmetric and has three blocks of infected coordinates. A direct comparison between its entries and a symmetric positive definite matrix does not express the theorem. The paper first relates its nonzero eigenvalues to those of an matrix, then uses a diagonal similarity to obtain a symmetric matrix. The final equivalence relies on the activity and mobility bounds that make this symmetric matrix positive semidefinite. A matrix statement that starts directly from the reduced symmetric form would omit the spectral reduction at the heart of the lemma.
Lean uses Fin n for neighborhoods and Fin 3 × Fin n for infected coordinates, in exposed, clinical, subclinical order. All model matrices are real; takes the spectral radius after mapping a matrix to complex entries, so complex eigenvalues are included. The inverse in is Mathlib's matrix inverse, and is represented by positive definiteness of . The only numerical instance in the sanity file has one neighborhood, but the theorem quantifies over arbitrary finite .
The standing assumptions include positive populations and rates, nonnegative travel fractions with row sums at most one, clinical and subclinical fractions in , and activity levels in . The formalization also requires : the paper divides by this quantity without stating the exclusion of . If no one visits destination , its mixing denominator is zero. Under the standing assumptions that entire column of vanishes, so Lean's value has no effect on the theorem. These conventions are part of the model, not optional proof shortcuts.
The proposal includes the full and , their displayed inverse, the paper's reduced matrix, the diagonal similarity, and the Loewner form. Contributions may develop spectral identities for block matrices, diagonal similarity, and positive definite matrix bounds. The large infection linear program, the stability theorem cited from earlier epidemic literature, and the New York City numerical application are beyond this target.
Music and podcast streaming services such as Spotify, Apple Music and Deezer charge every subscriber the same monthly fee and pass a share of the collected revenue to the artists. How that share is split is contested. The industry default, pro-rata, pools all fees and pays each artist her share of total streams. The alternative, user-centric, splits each subscriber's fee according to that subscriber's own listening. The two rules pay identical amounts when all users stream the same volume, and differ whenever heavy users and light users listen to different artists; which artists gain and which lose under each rule is the subject of an active industry debate.
Alaei, Makhdoumi, Malekian and Pekeč (SSRN 3645521; published in Management Science 68(12), 2022, doi:10.1287/mnsc.2022.4307) model the question as a two-sided market in which every artist has an outside option: she can leave the platform and sell her content directly. A rule is only viable if it pays each artist at least what she would earn alone. The paper's first main result, Theorem 1, says exactly when each rule can keep every artist on the platform. This mission formalizes that theorem and the chain of results its proof rests on, citing the authors' submitted manuscript (SSRN 3645521) for all page and result numbers.
There is a finite set of artists and two user types . Type users consume content at usage rate and form a population of mass ; a type user wants artist with probability per use. Throughout,
Type 2 users are the heavy users.
Going solo. If artist sells directly at price , a type user buys when her value is at least , so the demand is , , or according to which of and hold. The solo revenue is
The platform. With all artists on the platform and both types subscribing, the fee is and the revenue is . A payout rate is the fraction of revenue paid to artists. The pro-rata payment (Definition 1) and the user-centric payment (Definition 2) to artist are
The platform is sustainable with a rule if some makes every artist's payment at least .
Assumption 1 is : it rules out the case where the platform would rather serve heavy users alone, in which the two rules coincide. Artists are sorted by the ratio into four regions
Under Assumption 1 (and for all ), the platform is sustainable with pro-rata if and only if, for all ,
and sustainable with user-centric if and only if, for all ,
Theorem 1 separates the two rules by the kind of artist they can retain. Both rules lose artists whose audience is concentrated among heavy users, since such an artist captures those users' full fee by going solo; pro-rata tolerates a larger ratio before losing her. User-centric, in turn, can retain artists listened to mainly by light users, which pro-rata pays too little. The later results of the paper (which rule artists and the platform prefer, Propositions 2–3, and the optimal artist sets of §3.4) all start from this characterization.
The result is proved in the paper. No part of it, nor the underlying model of subscription fees, outside options and payout rates, has a machine-checked proof. The platform already has an axiomatic treatment of pro-rata and user-centric indices on stream-count tables; this mission adds the economic model with prices, outside options and payout rates, and its sustainability theorem. A complete development gives a checked version of the paper's case analysis, including its boundary cases.
Each step is elementary, and the difficulty lies in the bookkeeping. The solo revenue is a supremum of a step function times the price, and identifying its value requires comparing three candidates on four regions with half-open boundaries. The payments must be simplified from their general form (with sums and a minimum fee) to the closed forms of (10)–(11), which uses the standing assumptions and Assumption 1. Finally, combining four region-wise conditions into two intervals does not go region by region: when the first pro-rata interval is empty and no artist in or can be sustained, and the upper intervals agree with the region boundary only because of Assumption 1. A transcription that treats the printed intervals as non-empty, or drops Assumption 1, gives a false statement.
Everything sits in the namespace ProRataUC.Sustain, in one definitions file and six theorem files. The setting is a structure Setting M over a type M of artists with [Fintype M], with real fields lam1 lam2 q1 q2 and listening probabilities pi1 pi2 : M → ℝ; the standing assumptions are one predicate Setting.Standing, and Assumption 1 is a separate predicate. Conventions:
Added hypotheses, each disclosed in the statement: (the paper's ratio presupposes it; Lean's division by zero would put an artist heard only by heavy users in the region and make part (b) false); Assumption 1 in equations (10)–(11) and Lemmas 6–7, whose proofs use it although the lemmas say "for a given and ".
Formalizations that would trivialize the goal are ruled out: sustainability is not defined as the printed intervals or as , is not defined by Lemma 1's case formula, is explicit, and Assumption 1 is kept.
Contributions welcome: proofs of the milestones in order, reusable lemmas on suprema of step functions times price (the two-type monopoly pricing problem) and on Finset.sup' of ratios, and the interval bookkeeping of Theorem 1.
This paper establishes a general theory of energy-constrained quantum and private capacities of quantum channels. We begin by defining various energy-constrained communication tasks, including quantum communication with a uniform energy constraint, entanglement transmission with an average energy constraint, private communication with a uniform energy constraint, and secret key transmission with an average energy constraint. We develop several code conversions, which allow us to conclude non-trivial relations between the capacities corresponding to the above tasks. We then show how the regularized, energy-constrained coherent information is equal to the capacity for the first two tasks and is an achievable rate for the latter two tasks, whenever the energy observable satisfies the Gibbs condition of having a well defined thermal state for all temperatures and the channel satisfies a finite output-entropy condition. For degradable channels satisfying these conditions, we find that the single-letter energy-constrained coherent information is equal to all of the capacities. We finally apply our results to degradable quantum Gaussian channels and recover several results already established in the literature (in some cases, we prove new results in this domain). Contrary to what may appear from some statements made in the literature recently, proofs of these results do not require the solution of any kind of minimum output entropy conjecture or entropy photon-number inequality.
This mission is the statement-level formalization of Energy-constrained private and quantum capacities of quantum channels (arXiv:1609.01997v2). 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 High-energy limit of the pure-loss expression (Unnumbered Eq.332: high-energy limit for degradable pure loss, PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
22 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum parallel repetition, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
There exists a real constant , independent of all sets and game data, with the following property. A game on finite question sets and finite answer sets consists of weights summing to and a Boolean acceptance predicate . Write for the supremum of over all finite-dimensional bipartite complex matrix systems, positive semidefinite states of trace , and positive semidefinite local measurement effects satisfying and for each question. For , has question and answer tuples of length , question weight , and accepts exactly when every coordinate accepts; takes a fresh supremum over arbitrary strategies for this tuple game. For every such with and nonempty and , and every natural number , . The weights may be any joint distribution, including distributions with zero weights; their normalization excludes empty question sets. The answer nonemptiness and positive gap make the displayed denominator positive. This bound does not assert an inequality at .
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, G_QuantumParallelRepetition.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Lie algebras describe how control Hamiltonians combine in closed quantum systems. In open Markovian systems, however, dissipation introduces irreversible directions that the Lie algebra alone does not retain. A dynamical Lie wedge preserves this information as a convex cone of locally admissible generators. The classical Levi decomposition separates a finite-dimensional Lie algebra into semisimple and solvable parts. In this work, we prove a corresponding decomposition and reconstruction theorem for dynamical Lie wedges. The theorem decomposes the wedge into semisimple and solvable data, records how these components are coupled, and provides a converse reconstruction of the wedge. The framework yields four structural types of the generated algebra. We further prove that the total dissipation strength of every admissible generator depends only on its coordinate in the solvable radical. In particular, if the generated Lie algebra is semisimple, every admissible generator is Hamiltonian. Together, these results extend Lie-algebraic structural methods to irreversible Markovian control and clarify how dissipation is encoded in the generator geometry.
This mission is the statement-level formalization of The Geometry of Dissipative Complexity: A Levi-Type Decomposition Theorem for Markovian Quantum Dynamics via Lie Wedges and Invariant Cones (arXiv:2608.27330v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
36 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4.9: Levi-Type Decomposition Theorem (seed abstract result) (Theorem 4.9: Levi-Type Decomposition Theorem (seed abstract result), PDF p. 26). 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:
A multiple access channel (MAC) consists of multiple senders simultaneously transmitting their messages to a single receiver. For the classical-quantum case (cq-MAC), achievable rates are known assuming that all the messages are decoded, a common assumption in quantum network design. However, such a conventional design approach ignores the global network structure, i.e., the network topology. When a cq-MAC is given as a part of quantum network communication, this work shows that computation properties can be used to boost communication speeds with code design dependently on the network topology. We quantify achievable quantum communication rates of codes with computation property for a two-sender cq-MAC. When the two-sender cq-MAC is a boson coherent channel with binary discrete modulation, we show that it achieves the maximum possible communication rate (the single-user capacity), which cannot be achieved with conventional design. Further, such a rate can be achieved by different detection methods: quantum (with and without quantum memory), on-off photon counting and homodyne (each at different photon power). Finally, we describe two practical applications, one of which cryptographic.
This mission is the statement-level formalization of Computation-aided classical-quantum multiple access to boost network communication speeds (arXiv:2105.14505v1). 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 Compute-and-forward message exchange (§II.C.1, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
12 results of the paper are not stated yet, because the library lacks an interface they need:
Within the framework of quantum memory channels we introduce the notion of repeatability of quantum channels. In particular, a quantum channel is called repeatable if there exist a memory device implementing the same channel on each individual input. We show that random unitary channels can be implemented in a repeatable fashion, whereas the nonunital channels cannot.
This mission is the statement-level formalization of Repeatable quantum memory channels (arXiv:0808.3851v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Random-unitary channels have finite repeatable implementations (Theorem 1, 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.
Quantum channel discrimination plays a crucial role in quantum information theory. Of particular interest is the case in which the channels can be discriminated perfectly. In this work, we focus on the perfect quantum channel discrimination task in a parallel scheme. We develop an SDP formulation combined with a bisection procedure to compute a quantum state for perfect discrimination in time linear in the number of copies. In addition, we obtain the minimal number of copies of quantum channels to achieve perfect discrimination. Thanks to that, we settle in the affirmative Conjecture 1 of Duan, Guo, Li and Li [arXiv:1605.02294, IEEE ISIT 2016], which characterizes the number of parallel uses needed to discriminate perfectly a distinguished family of operator subspaces. All our results are obtained using the notion and basic properties of the numerical range. In particular, the key fact that we prove and use is that the minimal angle of the numerical range of a tensor product of matrix subspaces equals the sum of the minimal angles of the numerical ranges of the individual subspaces. △ Less
This mission is the statement-level formalization of Parallel quantum channel discrimination and numerical ranges in tensor product subspaces (arXiv:2609.20781v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Perfect parallel discrimination and the minimum number of copies (Theorem 7, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We determine the two-way quantum, entanglement-distribution, private, and secret-key capacities of the pure-loss bosonic channel under an unconditional mean transmitted-photon-number constraint. For transmissivity and mean photon number , all four capacities coincide and are given by , where is the entropy of a thermal mode. This resolves the longstanding energy-constrained capacity problem by establishing the optimality of the reverse-coherent-information rate introduced in 2009. Our central tool is sector teleportation simulation, which we develop specifically to transfer the input-energy constraint to the shared entanglement resource, thereby preserving the constraint throughout converse arguments for general adaptive protocols. For every , we further show that the corresponding strong-converse thresholds coincide with the unconstrained value . For parallel protocols with a hard total-photon-number cutoff, the same energy-constrained capacity formula instead satisfies an exponential strong converse. As an extension, we determine the energy-constrained two-way capacities of the quantum-limited amplifier, showing that classical assistance does not improve its unassisted quantum and private rates. Together, these results establish a unified finite-energy framework for adaptive bosonic communication and reveal how energy constraints fundamentally reshape both attainable rates and converse bounds. △ Less
This mission is the statement-level formalization of Energy-constrained two-way capacities of pure-loss and quantum-limited amplifier channels (arXiv:2610.06832v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1 (Scalar entropy estimates) (Lemma 1 (Scalar entropy estimates), PDF p. 9). 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 investigate converse bounds on the average decoding error probability in finite-blocklength classical-quantum channel coding. We first present a lower bound for multiple quantum hypothesis testing in terms of pairwise trace distances and derive a corresponding fidelity bound. We then obtain a spectrum-based converse that depends only on the a priori probabilities and spectra of the states. We show that the converse bound remains tight for the quantum depolarizing channel under suitable conditions. For codes with product-state outputs, this converse takes an explicit form involving products of output-state eigenvalues. We apply it to binary codes over the quantum amplitude damping channel using the input states and . For this setting, we also discuss a normal approximation to the spectrum-based converse in the large blocklength regime. In all numerical examples considered, the spectrum-based converse is tighter than the other converse bounds at low noise levels. △ Less
This mission is the statement-level formalization of A Spectrum-Based Converse for Quantum State Discrimination and Its Applications to Classical-Quantum Channel Coding (arXiv:2610.06840v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4 (Spectral converse); seed paper result (Theorem 4 (Spectral converse); seed paper result, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need: