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?
Prox-functions determine how subgradient and mirror-type optimization methods turn a direction of improvement into the next feasible point. On a probability simplex, that step should respect the geometry of probability vectors and be computable from the current direction. The entropic prox-function gives the softmax rule, familiar from the logit model of discrete choice. Müller, Nesterov and Shikhman ask whether a wider family of random-utility choice models supplies prox-functions with the same operational link between optimization and choice probabilities. Their 2019 preprint, published in Mathematics of Operations Research in 2022, states that it does: the convex conjugate of the model's surplus is a prox-function on the simplex.
This question matters to optimization because the random-utility law specifies a geometry and a computable update together. It matters to discrete-choice modeling because the update from an optimization problem can be interpreted as a vector of probabilities of choosing each alternative. The mission covers the general result in Section 2 of the preprint, rather than its later specialized generalized-extreme-value parameters or economic application.
There are alternatives. A deterministic utility vector is perturbed by a random shock vector with law . Assumption 1 requires a finite mean, absolute continuity with respect to Lebesgue measure, and full support in . The surplus function is the expected best perturbed utility,
The convex conjugate of this function is taken over every utility vector, with extended-real values:
The candidate domain is the simplex . The model's choice probability is the chance that attains the largest perturbed utility. Absolute continuity makes ties null, so including ties in this event does not change its probability. The paper identifies with the th derivative of in equation (1).
A prox-function on is continuous and strongly convex there, and the optimization step that maximizes over has a unique, directly available answer. Here strong convexity uses . The relevant smoothness of uses the dual norm .
The goal combines the three claims that form the paper's Section 2 main result. First, Theorem 1 says that the finite domain of is exactly , and that is continuous even at the boundary of that simplex. Second, Theorem 2 supplies an explicit strong-convexity parameter. For distinct alternatives , let be a density of and let be a mode of that density. Then
for and . The double sum is over ordered pairs. Third, under the strong-convexity premise stated at the opening of §2.2.3, Theorem 4 identifies the optimizer and the attained value:
The milestones record Lemmas 1, 2, 3 and 5, equation (1), and Theorems 1, 2 and 4. They cover the paper's elementary surplus properties, the choice-probability identity, the relation between strong convexity and strong smoothness, the Hessian norm criterion, the matrix trace bound, and the three final clauses.
The result gives a family of simplex prox-functions indexed by shock laws, rather than by a single entropy formula. The optimizer in the auxiliary problem is a choice-probability vector, so a prox update has an explicit behavioral interpretation. The strong-convexity bound supplies the geometric constant used when such a function enters first-order optimization estimates. The paper's later sections derive parameters for generalized extreme-value models and apply the update to a consumption cycle; those consequences motivate the general theorem but are outside this mission's goal.
The result is proved in the cited paper; this mission asks for its Lean formalization. The current draft has compile-checked statements with proof placeholders. A complete development would add machine-checked proofs of the listed lemmas and goal, together with reusable results about conjugacy, probability laws of differences, and norms of finite matrices. No proof of this specific paper result is claimed here.
Continuity in the relative interior of a simplex does not by itself establish continuity at its boundary, which is part of Theorem 1. The choice-probability formula connects differentiation of an expected maximum with an event defined by inequalities; ties, measurability, and integrability must all be handled. The strong-convexity constant then depends on controlling the Hessian with the norm induced from to , while retaining the ordered-pair sum of density values. A direct substitution of the default norm on finite coordinate functions would change the theorem because that norm is .
Alternatives are Fin n with [NeZero n]; vectors are Fin n → ℝ. The law is a probability measure on shock vectors. Assumption 1 explicitly includes coordinate integrability, absolute continuity and full support. Its integrability clause keeps the Bochner integral defining meaningful, rather than allowing the integral's default value on a nonintegrable function. The choice event includes ties, which have zero measure under Assumption 1. The conjugate is EReal valued and takes its supremum over all utility vectors; defining it by a maximum over the simplex or by an entropy formula would change the result.
The real value of is used only alongside its finiteness on . Strong convexity uses an explicit sum, while Mathlib's norm on Fin n → ℝ represents . Coordinate derivatives and the Hessian are formed from Fréchet derivatives. The differences have fixed, nonnegative measurable density versions tied to their pushforward laws; each mode maximizes its selected version pointwise. Theorem 4 carries the positive strong-convexity premise stated in its section preamble. The paper uses twice differentiability of on page 7 without deriving it from Assumption 1. This mission explicitly adds ContDiff ℝ 2 E to the Hessian-dependent result and the goal. It is a necessary disclosed strengthening of the paper's stated assumptions.
For one alternative the simplex is a point, and the displayed denominator in is zero. Lean evaluates the reciprocal as zero. The strong-convexity inequality is then vacuous between distinct points; the draft asserts positivity of the displayed only when and separately asserts that some positive parameter exists for every , as Definition 1 requires. No empty set of alternatives is admitted. Contributions should keep the unrestricted conjugate, the law-dependent densities, the exact inequality, and the paper's constants. General finite-dimensional convex duality and induced matrix-norm lemmas would be reusable beyond this model.
"Buy , get one free" (BXGO) programs are among the most common loyalty schemes: coffee shops, car washes, golf courses and hotel chains hand out a free unit after a fixed number of paid purchases. A long empirical literature documents that such programs change behaviour, most visibly through point pressure, the acceleration of purchases as a customer approaches the redemption threshold (Kopalle et al. 2012; Lewis 2004). Whether that acceleration is worth the free units given away is a question for the firm's pricing and marketing operations.
Liu, Sun and Zhang (2021) study the question in a fully rational model. A forward-looking consumer facing a BXGO program solves a dynamic program, and her optimal decisions induce a Markov chain on her point inventory. The paper shows that discounting alone produces point pressure, and then asks whether the program raises the firm's long-run profit. Its answer without transaction utility (the consumer's extra enjoyment of a free unit) is negative under explicit conditions: Proposition 3. This mission formalizes that result together with the structural lemmas its proof rests on.
A monopolist sells a nondurable product at marginal cost , so revenue and profit coincide. A BXGO program is a pair : a fixed price and a threshold . A consumer earns one point per purchase, and holding points she may redeem them for a free unit, returning to points.
In each period the consumer is in the market with probability . In the market she values the product at and has an outside option , equal to with probability and to otherwise, where . A redemption gives her a transaction utility on top of . She discounts with factor .
Her value function on the point inventories solves the optimality equations
for , and the analogous equation at with (redemption) in place of . She buys, or redeems, when this is at least as good as the outside option. Her decisions turn the point inventory into a Markov chain on that moves from to (from to ) or stays put. The firm's profit is times the long-run purchase probability per period.
Two constants recur throughout:
So do the boundary prices and of the paper's p. 10, which separate the price ranges of the consumer's four response patterns (Proposition 2). The benchmark is the profit of the best price without a program, : selling to the consumer only when her outside option is , or always, at the price .
Assume and either (a) and , or (b) and . Then for every program and every solution of the optimality equations, the average expected revenue over the first periods, of a consumer who starts with points, satisfies
The statement covers every price, including those between the ranges of Proposition 2, where the paper asserts but does not show that the consumer drops out.
Proposition 3 separates two effects of a reward program. Point pressure raises the purchase probability above that of a consumer who never accelerates. Discounting forces the firm to lower its price to keep her in the program, and without transaction utility the second effect dominates. The paper's Proposition 4 shows that a small positive reverses the conclusion, and its §6 shows that an expiration term reverses it too. The result therefore locates exactly where the profitability of BXGO programs comes from: transaction utility or expiration, not the threshold alone.
The result is proved on paper but not machine-checked. The paper's proof of Proposition 3 works with the closed-form profits of four behavioural cases. Formalizing it requires connecting those closed forms to the consumer's dynamic program and to the long-run behaviour of the chain her decisions induce, and that connection is part of the mission. Machine-checked proofs of Propositions 1–2 also give a reusable template for monotone threshold policies in discounted point-accumulation problems.
The value function has no closed form until the consumer's behaviour is known, and her behaviour is defined by the value function. The paper breaks the circularity case by case: assume a behaviour, solve the linear equations it induces, and read off the price range in which that behaviour is consistent. A formal proof has to show that the four ranges, together with the gaps between them, account for every price. At a gap price the consumer either never buys from points or behaves as in a neighbouring case.
Reading profit as "price times stationary demand" also needs care. At high prices, at or at the induced chain is reducible, and the long-run revenue from points need not equal the revenue under an arbitrary stationary law. Lemmas 2 and 3 bound only the four closed forms; turning them into a bound on the Cesàro averages of the actual chain is the remaining step.
All quantities are real. Params bundles , and Params.Standing is the list of standing assumptions: , , , . The value function is a hypothesis, IsValueFn P p X J, meaning that J : ℕ → ℝ satisfies the optimality equations on . The equations have exactly one solution there, and its values beyond play no role. Decisions break ties in favour of buying or redeeming, as in the paper's Corollary 1 and Proposition 2. The chain lives on Fin (X+1). Profit is the Cesàro average avgRevenue of expected revenues from state , computed from the transition matrix of the consumer's own decisions. Stationary distributions use the published MarkovChain.IsStationary.
The goal cannot be made true by construction. Profit is computed from the decisions of , never from the paper's closed forms, and the goal quantifies over every price and every threshold with no assumed behaviour.
Hypotheses added to the paper's statements:
Proofs of individual milestones are welcome. So are general lemmas about Cesàro averages of finite stochastic matrices and the two-sided comparison of discounted value functions, both of which are reusable beyond this mission.
Payments for ecosystem services compensate landowners for conservation that a program values but cannot directly provide. A contract designer must decide how to pay when landowners differ in the amount of forest they would conserve without a payment. That baseline conservation type is privately known, so a contract can pay for forest that would have remained anyway. Li, Ashlagi and Lo study this problem for forest conservation and ask how much payoff a simple, uniform price can guarantee relative to an optimally tailored contract (Li, Ashlagi and Lo, 2022, §§1–2).
The paper's Theorem 1 establishes a guarantee that does not depend on the type distribution: a price equal to half the program's value per unit secures at least half of the optimal contract payoff. This matters to a designer who can estimate the conservation value but cannot reliably estimate the distribution of landowners' private baselines. The guarantee concerns the principal's payoff after payments, rather than the total area conserved or the agent's utility (Li, Ashlagi and Lo, 2022, §4, Theorem 1).
An agent owns an initial forest area . Their type is the fraction of that area they would conserve without incentives. The publicly known type distribution is supported on . The agent selects a conserved area . Conservation above the baseline has cost , where and
The principal values each conserved unit at . A direct revelation contract specifies an action and payment for each reported type. It is feasible when the action respects the forest-area bounds, payments are nonnegative, truthful participation gives nonnegative utility (individual rationality, IR), and truthfully reporting the type maximizes utility among all reports in the type interval (incentive compatibility, IC). Its payoff is . These are the model and contract constraints on pages 4–5 of the source preprint.
A linear contract pays the same price for every unit of conserved area, including area the agent would conserve without incentives. The agent's action at price is on the type interval. The principal then receives ; the best such payoff is . The price and payment apply to the whole action , as in Equation (3) of the source preprint.
For every probability law on the stated type interval, every feasible direct contract with a defined expected payoff, and every best-response action to the price , Theorem 1 gives
It follows that every feasible direct-contract payoff is at most . The universal bound expresses the comparison with an optimal contract even if a maximum over contracts is not attained. The milestone list contains the linear best response, the doubled payoff identity of Equation (7), the information-rent-free upper bound of Equations (4)–(5), and the pointwise comparison from Appendix A.4. All four come from the paper's §4 and Appendix A.4.
The guarantee makes the price a distribution-independent benchmark for this conservation model. The paper's Example 3 gives a single type at where the factor of two is attained, so a larger universal fraction cannot be claimed under the same assumptions (Li, Ashlagi and Lo, 2022, p. 9). The result also implies the best linear contract has the same worst-case guarantee, even though finding its maximizing price may depend on the distribution.
The result is proved in the paper but is not yet machine checked in this mission. Formalizing it will give a reusable definition of this conservation-contract model, with explicit IR and IC constraints, and Lean statements for the price guarantee and its central comparisons. It can also support later formalizations of the paper's conditional contracts and convex-cost extensions, which are outside this mission.
The benchmark is the payoff of an optimally designed contract with actual payments, under private information. Replacing those payments by conservation cost changes the benchmark: the agent may receive an information rent. Likewise, optimizing independently for each type describes an unconstrained surplus, not the direct contract in Theorem 1. A formal statement that uses either quantity as the goal's “optimal payoff” would miss the paper's claim. The paper compares the linear payoff with a bound on the contract payoff, and its Appendix treats type distributions that need not satisfy the monotone-hazard-rate condition used in the shorter proof sketch (Li, Ashlagi and Lo, 2022, pp. 10, 24–26).
Lean represents types, areas, prices and payoffs as real numbers. The law is any probability measure on the reals concentrated on ; atoms, including a point mass, are allowed. The standing parameter conditions are , and . Positive is made explicit because the paper uses . The theorem adds as stated in Theorem 1. Feasibility and best-response conditions range over supported types, and IC compares every pair of types in that interval. The contract's action and payment are integrable so their expected payoff is defined. The bounded best-response action needs no separate integrability assumption.
The formalization uses a supremum over nonnegative linear prices. Under the standing conditions its values are bounded above, so this is the ordinary best-payoff bound rather than a default value of a total supremum operation. The goal ranges over feasible direct contracts with IR, IC, action bounds and nonnegative payments; it retains the actual in the payoff. A goal stated only for an unconstrained surplus or with an empty feasible class would not represent Theorem 1. Useful contributions include proofs of the four milestones, measure-theoretic facts about supported type laws, and lemmas about the price-payoff supremum.
Clustering methods must infer a partition from noisy observations, while the quality of a partition is usually judged against labels that the method cannot see. Fei and Chen study a balanced sub-Gaussian mixture model in which a semidefinite program (SDP) estimates a cluster matrix from pairwise distances. Their Theorem 1 relates its error to a simpler integer program allowed to know the true cluster centers. This comparison makes the SDP's error interpretable through an explicit benchmark, even when exact recovery is unavailable. The paper also investigates semi-random perturbations, but this mission targets the Model 1 comparison on which that broader discussion builds.
The tension is that an SDP solution may be fractional. Its entries express pairwise affinities, whereas an assignment matrix places each point in exactly one cluster. The result bounds the fractional matrix's entrywise error by an integer assignment error without assuming that the SDP solution itself is integral. That is the hidden-integrality claim relevant to this mission.
There are observations in and clusters. The true label of point is , and every cluster contains exactly points. For unknown centers , the observations have the form
The noise vectors are independent, measurable, zero-mean, and sub-Gaussian. Their vector sub-Gaussian norms are at most . The minimum center separation and signal-to-noise ratio are
The SDP uses the squared-distance matrix . It minimizes over real matrices with row sums , diagonal entries one, nonnegative entries, and symmetric positive semidefiniteness. Write for any optimum. The true cluster matrix is when and otherwise. Its error is measured by the entrywise norm .
The benchmark is an Oracle Integer Program. An assignment matrix has zero-one entries and exactly one one in each row. The true assignment is . The oracle sees the centers and augmented observations with the fixed , so its noise is four times the realized noise in . It minimizes
The Oracle error is the largest among assignments satisfying . The Oracle feasible set has no balance constraint. In contrast, the SDP retains the row-sum constraint inherited from balanced clustering.
The goal is the paper's quantitative comparison. It asserts that universal constants and exist such that, when
an event of probability at least has, for every realized SDP optimum , the bound
The constants are independent of , the centers, the labels, and the noise law. The event and the SDP optimum are chosen after the random observations are realized. The theorem fixes the factor two and the failure-probability expression exactly as printed.
The eight milestones follow the statements in Section 5: the six structural properties of the SDP error matrix (Fact 2), the basic inequality (16), the signal estimate (Proposition 3), the two noise estimates (Propositions 1 and 2), the representation of the remaining term (Lemma 1), the identity between the integer program and Oracle error (Lemma 2), and the final deterministic bound. Each milestone keeps the paper's constants and its own hypotheses. Together they expose the interfaces needed to close Theorem 1.
Theorem 1 transfers a question about a real matrix optimum to a finite assignment benchmark. The Oracle benchmark can itself be bounded under additional assumptions, as Fei and Chen do in their separate Theorem 2. The present target preserves the comparison even in regimes where the benchmark does not vanish. It therefore expresses an error guarantee rather than an exact-recovery assertion.
A complete Lean proof would connect a probability model, finite-dimensional semidefinite feasibility, and the paper's integer assignment comparison. At present these mission statements are draft proof obligations: compiling a statement with sorry checks its formulation but does not prove the result. The development reuses published definitions of scalar and vector sub-Gaussian norms; proving the new lemmas and the main theorem remains open within this mission.
SDP optimality gives an inequality for the squared-distance objective, but it does not directly bound the entrywise difference from . Noise enters that objective through both a Gram matrix and mixed center-noise terms. A direct entrywise comparison also ignores the row-sum and positive-semidefinite structure that constrains the SDP error.
On the benchmark side, replacing a fractional matrix error by an arbitrary rounded assignment would not retain the stated factor. The paper identifies an intermediate linear program whose value can be controlled at integer cardinalities. Formalizing the result requires preserving that cardinality constraint, the exact coefficient , and the distinction between the observed points and the oracle's augmented points.
Points, clusters, and coordinates use finite index types; Lean indices start at zero while the paper's and start at one. All matrices are real. The trace inner product is represented by a double sum, the matrix norm is entrywise, and the spectral norm in Proposition 2 uses the operator norm. The minimum separation ranges over distinct center pairs, which is nonempty when . Oracle maxima are finite, nonempty, bounded sets; the true assignment is a feasible candidate. The normalized denominators are nonzero under and with balanced labels.
The random model uses one probability space and the same noise realization in both and . Measurability, zero mean, independence, and the extended-nonnegative vector sub-Gaussian norm bound are explicit. High-probability conclusions use measurable events and quantify over every optimum at each realized data set. Deterministic milestones take a fixed realization and do not add a probability space. The universal constants occur before all model parameters. These choices rule out a vacuous instance-dependent SNR constant, a norm that assigns zero to heavy-tailed noise, and an SDP optimum chosen before observing the noise.
The scope is Theorem 1 and its selected Section 5 statements. Theorem 2's separate Oracle-error rate, the rounding algorithm, semi-random Model 2, and the stochastic-ball special case are outside this proposal. Reusable work includes the SDP and assignment interfaces, matrix-error identities, and finite integer-program comparisons. Contributions that prove the eight source milestones or establish their supporting concentration and finite-dimensional optimization results are welcome.
Revealed-preference theory asks which observed choices can be explained by a decision procedure. The classical answer, maximization of a single preference, explains only choice functions that satisfy consistency conditions such as the weak axiom, and observed choices, including the menu effects in Luce and Raiffa's dinner example, often violate them. A large literature therefore studies richer procedures and characterizes the behaviour each one can generate.
The pro-con model of Dogan and Yildiz formalizes Benjamin Franklin's "prudential algebra": an agent lists reasons for and against each alternative and chooses the one whose reasons for outnumber its reasons against. Each reason is an ordering of the alternatives, and an ordering counts as a reason for (or against) an alternative at a menu when it ranks that alternative first among those available. The paper's main result is that this model is universal for deterministic choice: every choice function is pro-con rationalizable. The paper also proves the random-choice analogue (every random choice function is pro-con rational with signed weights in ), derives that every choice function is plurality-rationalizable, and recovers McGarvey's theorem on majority relations as a corollary.
Let be a finite set of alternatives. A choice set is a nonempty , and a choice function assigns to every choice set an element . An ordering is a strict linear order of ; is the -top-ranked alternative of .
A pro-con model consists of two sets of orderings, the pro-orderings and the con-orderings , with no ordering in both. For ,
is pro-con rational (Definition 1) if one pro-con model serves every choice set: for every and every , if and only if .
The proof works with signed weights on classes of orderings. For , a -prefix is the list of the first alternatives of an ordering, and is the family of sets with more than elements. A weight function on -prefixes represents a random choice function on if is the total weight of the prefixes along which is the first element of . The Möbius transform of is , extended by for .
The milestones follow the paper's proof, which runs the inductive construction of Section 6 and makes each step integral in Section 7:
Theorem 1 says that pro-con rationality imposes no testable restriction on deterministic choice: no data set of single-valued choices can refute it. A characterization of a choice procedure is therefore informative only once the model is restricted further (fewer orderings, structured orderings), and the representation of Theorem 1 serves as a starting point for building other universal models, such as the plurality representation of Section 2.4. The paper shows that universality is delicate: it fails for multi-valued choice rules when each ordering may be used only once (Section 2.3).
The result is proved in the paper; nothing in this mission is open mathematics. No part of it has a machine-checked proof. The formal work is to verify the proof. That covers its combinatorial core (Möbius inversion, the estimate, the generalized Ford–Fulkerson theorem), the integrality step, and the corrections the formalization needed: Lemma 4 requires an integral right-hand side; the paper's description of the con-orderings in the random case (inverses of negative-weight orderings, p. 16) is not what the deterministic assembly uses; and the induction of Section 7 uses a bound for the previous step that the paper establishes only for the real-valued construction.
The obvious approach, assigning pro- and con-orderings menu by menu, fails because every ordering affects every menu at once: changing one ordering changes the top element of all sets. The paper therefore builds a signed measure on orderings level by level, prefix length , and each level must solve a transportation problem with signed margins and box constraints . Classical Ford–Fulkerson theory covers nonnegative margins only. Moreover, a solution at one level has to leave the next level feasible, which is the role of the column bound in Theorem 3 and the source of the integrality gap noted above. The integrality itself rests on total unimodularity, which neither Mathlib nor the platform currently provides as a usable criterion (Heller–Tompkins) or vertex theorem (Hoffman–Kruskal).
The alternative set is a type X with [Fintype X] [DecidableEq X]; it may be empty, in which case every statement holds trivially. An ordering is a rank bijection X ≃ Fin (Fintype.card X), rank being the best, and means and for all . A pro-con model is a structure with two Finsets of rank bijections and a disjointness proof. A choice function is C : Finset X → X with C S ∈ S for nonempty S; its value at is irrelevant. ProConRational C includes this choice-function condition. Random choice functions are real-valued p : X → Finset X → ℝ, -prefixes are injections Fin k ↪ X, and weight functions are maps from prefixes to ℝ (to ℤ in the integral step). Representation on is stated with n < |S| + k to avoid natural-number subtraction. Matrices are Matrix (Fin m) (Fin n) ℝ or indexed by finite types; total unimodularity is Mathlib's Matrix.IsTotallyUnimodular, and vertices are Set.extremePoints ℝ.
The definition rules out each trivializing reading: orderings cannot be repeated (sets, not lists), cannot be both pro and con, are linear orders (unique top), count as cons at their top element, require a strict majority, and one model must serve all choice sets with the equivalence holding at every . A formalization that drops any of these makes Theorem 1 easier or false in a different way and is not this mission's goal.
Theorem 2 (random choice) is not a target; its proof steps appear as milestones. Reusable beyond this mission: the Möbius transform and its bound, the generalized Ford–Fulkerson theorem, Heller–Tompkins, and Hoffman–Kruskal for box-constrained systems. Proofs of any milestone, alternative proofs of Theorem 1 (for instance, a direct induction avoiding the gap in Section 7), and Lean infrastructure for total unimodularity are welcome.
Shortest remaining processing time first (SRPT) is the scheduling rule that always works on the jobs closest to completion. For a single server it minimizes the number of jobs in the system at every time, on every sample path (Schrage 1968). Service systems with many parallel servers and customers who leave when they wait too long, such as call centers, hospital wards and cloud platforms, are a different setting. There an overloaded system must turn customers away somehow, and the scheduling rule decides who. How SRPT behaves in such systems had resisted analysis: the state of the queue is a vector of remaining service and patience times of unbounded dimension, and preemptions couple all customers together.
Dong and Ibrahim (2021) analyze SRPT in the queue in the overloaded many-server regime. They show that SRPT asymptotically behaves like a two-class priority system with a sharp threshold on the service time. Short jobs are served with vanishing delay, long jobs almost all abandon, and the resulting waiting-time measures depend on the patience distribution only through its mean. Under first-come-first-served, by contrast, performance depends on the whole patience distribution (Whitt 2006).
Customers arrive according to a Poisson process of rate to identical servers. Customer brings a service time and a patience time . The are i.i.d. with a continuous law , density , cdf and mean ; the are i.i.d. with a continuous law and mean . Arrivals, services and patience times are mutually independent.
A schedule says which customers occupy the servers at each time. From it one reads off each customer's remaining processing time and cumulative time in queue . Customer abandons when reaches . Her patience clock keeps running across preemptions and is not reset. Under SRPT, at every time the servers are busy whenever customers are waiting, and every customer in service has remaining work no larger than that of any waiting customer. Customer is served () if she completes service and abandons () otherwise. Her waiting time is the total time she is present but not in service.
The traffic intensity is . The paper fixes and lets and grow together, with . The threshold is defined by equation (1),
so the work brought by jobs shorter than exactly matches capacity. Class 1 consists of the customers with and class 2 of those with .
The analysis couples the SRPT queue with a loss system . This system has the same customers and servers but no waiting room. Class 1 customers preempt class 2 customers, and a class 1 customer who finds all servers busy with class 1 work is lost. Its class 1 throughput is .
As , under SRPT and for a tagged customer in steady state:
The goal states all four parts. The constants , , and are those of the paper.
Proposition 1 (p. 8) is the coupling inequality , where is the throughput of the SRPT queue. The capacity constraint (5) (p. 16) says that work is completed at rate at most . Two steps in the proof of Lemma 4 (p. 17) concern Erlang's loss formula. The first is the identity . The second is the limit . Lemma 4 (p. 16) gives . Problem (7) (p. 18) is a linear program over service-probability profiles. Lemma 5 (p. 17) says the limiting service probability is ; the mission states the analytic step that concludes its proof (p. 18), not Lemma 5 itself. Theorem 2(a) is the goal's first part.
Theorem 2 is a state-space collapse: an infinite-dimensional preemptive system becomes, in the limit, a two-class priority rule with an explicit threshold. Several consequences follow from it. SRPT asymptotically minimizes the waiting time of served customers and maximizes that of abandoning ones (Corollary 1). It also asymptotically maximizes throughput among all disciplines (Proposition 3). Its performance measures are insensitive to the patience law beyond its mean.
The paper proves Theorem 2 on paper. To our knowledge none of it is machine-checked. The mission asks for a formal model of a multi-server preemptive queue with abandonment and a formal proof of the coupling. It also asks for the Erlang-formula asymptotics and the variational step that pins down . Two parts of the published argument need care in a formal proof. The proof of (b) switches to patience laws with , while the statement is for general patience laws. The proof of Lemma 5 presupposes that exists. A complete development must close both points or replace them with arguments that avoid them.
The SRPT queue has no finite-dimensional Markov description. Preemptions mean that the order in which customers are served is not their arrival order, and a preempted customer's patience keeps running. Standard fluid or diffusion limits for many-server queues track the number of customers, or a measure-valued state under first-come-first-served, and SRPT fits neither. The coupling with the loss system avoids this, but proving it requires a matching argument along the sample path that survives every preemption. Converting throughput bounds into statements about conditional waiting times then requires control of steady-state quantities that the model does not provide in closed form.
The model is a single definitions file in the namespace SRPTManyServer.Collapse, with these conventions.
IsLeast statement over measurable .The discipline in the goal is SRPT on the actual arrival stream. It is not the two-class priority system, the threshold does not appear in the scheduling predicate, and the throughputs and service probabilities are not free parameters: a statement in which they were would reduce the goal to Lemma 5. The non-idling clause is part of the SRPT predicate, so the empty schedule does not qualify.
A complete development needs a sample-path theory of preemptive multi-server queues with abandonment. It also needs renewal or regenerative arguments that connect time averages with customer averages, and the insensitivity of the blocking probability, which the paper cites from the literature and does not prove. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The Erlang identities, problem (7) and the final step of the proof of Lemma 5 are self-contained analysis.
Not formalized here: Corollary 1, Proposition 3 (Appendix B), inequality (4), and the numerical comparisons of §4.
Firms that advertise online choose whom to target from the customer data they hold, and the industry's working assumption is that more granular data can only help: a firm that knows more about each consumer can at worst ignore the extra information. Despotakis and Yu (SSRN 3900394; Management Science, 2022, doi:10.1287/mnsc.2022.4604) show that this fails once consumers draw inferences from being targeted. A consumer who receives an ad learns something about how well the product suits her, and she decides whether to spend effort clicking on that basis. When the firm uses more dimensions of data, the set of consumers it targets changes shape, and the signal that being targeted conveys becomes weaker. In equilibrium the firm can then earn strictly less with more data than with less.
The result belongs to a line of work on targeted advertising as a signal, and on the value of customer data to a firm whose actions consumers observe and interpret. It is a commitment problem: the firm would like to promise to use less information, but cannot.
A unit mass of consumers is interested in a product sold at an exogenous price . A consumer's utility from the product is
where are her matching values on two components of the product and is her private weight on the first. The three are independent and uniform on . The consumer does not know and until she clicks.
The firm sends ads at unit ad cost . Under single-dimensional (sd) targeting it observes and chooses a targeting set ; under multidimensional (md) targeting it observes and chooses .
A targeted consumer does not see but expects a set . Her posterior is uniform: under sd targeting is uniform on and uniform on ; under md targeting is uniform on . She clicks at click cost if and only if her posterior expected surplus is at least ; the weights that click form the click set . After clicking she learns and buys if and only if .
Against a click set , the ad value of a consumer is times the probability that she clicks and buys, minus ; under md targeting . The firm's profit from targeting is the integral of the ad value over .
A non-trivial equilibrium is a targeting set of positive measure that maximizes the firm's profit over all targeting sets, against the click set that consumers who correctly expect produce. An md equilibrium is symmetric if is symmetric about the 45-degree line. and denote equilibrium profits. Two thresholds from the paper enter the statements: the click-cost threshold of Equation (7), above which no non-trivial symmetric md equilibrium exists, and the ad-cost threshold from the proof of Proposition 1.
For every there is such that for every there is such that for every both a non-trivial sd equilibrium and a non-trivial symmetric md equilibrium exist, and
for every such pair. The goal fixes neither nor ; the right end of the click-cost interval is the explicit threshold of Equation (7).
The result is a clean counterexample to the monotonicity of the value of information for a firm whose actions are observed by strategic receivers. It isolates a mechanism, inference from being targeted, that does not need competition, price discrimination or privacy costs to make extra data harmful. The paper uses it to explain why firms might coarsen the data they act on, and §5 revisits the comparison with endogenous pricing and with consumers who do not know which dimension the firm targets on.
On the platform this mission is the first model of targeting with consumer inference. The model layer, uniform posteriors on an expected targeting set, click sets defined by posterior expected surplus, and equilibria defined as fixed points over arbitrary measurable targeting sets, is reusable for other signalling-through-targeting results. The result is proved on paper, with Lemmas 4 and 5 argued in sketch form; to our knowledge no part of it has a machine-checked proof.
Both equilibria are fixed points: the firm's best response depends on the click set, and the click set depends on the expected targeting set through a posterior average. The md firm may choose any measurable subset of the square, so the reduction to the two-line class of Equation (6) is part of the work, and Proposition 2 asks for uniqueness among all symmetric measurable equilibria, not only within .
The comparison itself is not a monotonicity argument. As approaches , the md click set shrinks to the threshold where the md equilibrium disappears, while the sd profit stays positive only because lies strictly below , where the sd profit vanishes. Making this precise requires the piecewise closed forms of the expected surplus (with logarithms) and control of both profits uniformly as , which the page leaves implicit. Comparing the closed forms at a single numerical point does not give the statement for every price.
All quantities are real numbers. Consumer populations are Lebesgue measure on and , so probabilities are lengths and areas. Targeting sets are measurable subsets of the unit interval or square, "non-trivial" means positive measure, "symmetric" means invariance under , and "unique" means unique up to a null set. The tie-breaks follow the page: buy at , click at equality, and indifference is allowed in the firm's optimization. Click thresholds are arbitrary reals, so an empty click set is expressible.
Equilibria are defined as fixed points, never by the paper's closed forms and ; otherwise Propositions 1 and 2 would be definitional and the goal a comparison of two formulas. The paper's is defined as the least click cost at which , which would make a literal statement nearly true by definition; the goal therefore asserts the existence of the region instead, and it includes existence of both equilibria so that the comparison is not vacuous.
Added or restricted hypotheses: Propositions 1 and 2 are stated only in the regimes Proposition 3 uses; Proposition 1 uses strictly (at equality the cutoff is and the targeting set is null); Lemma 4 adds ; Lemma 5 is stated in – form because its limit is not shown to exist; and the price is throughout.
A complete development needs set integrals and product measures from Mathlib, convexity of the expected surplus in , and real analysis of the piecewise closed forms. Proofs of any milestone, and alternative arguments for Lemmas 4 and 5, are welcome.
Interior-point methods solve a conic optimization problem by following the minimizers of a barrier function for the cone. Their iteration count is governed by the barrier's parameter : the best known algorithms need iterations to reach accuracy (Nesterov and Todd, 1997). A cone can be used natively by a solver only once a logarithmically homogeneous self-concordant barrier (LHSCB) with a small parameter is known for it, together with efficient oracles for its derivatives.
Coey, Kapelevich and Vielma (arXiv:2103.04104v2; Mathematics of Operations Research, 2022) study cones defined by spectral functions on Euclidean Jordan algebras. This framework covers vectors, real symmetric matrices and complex Hermitian matrices at once. The paper implements the resulting cones in the solver Hypatia. One of its two new barrier results concerns the root-determinant cone, the hypograph of the geometric mean of the eigenvalues. For symmetric matrices this is the hypograph of over the positive semidefinite cone, a standard modelling device for D-optimal experimental design and for determinant maximization. Before this paper, the usual way to represent it was an extended formulation with auxiliary variables and a semidefinite constraint.
A Jordan algebra is a real vector space with a bilinear product that is commutative and satisfies the Jordan identity , where . It has a multiplicative identity . It is Euclidean if . An idempotent is a with . It is primitive if it is non-zero and is not the sum of two orthogonal non-zero idempotents. A Jordan frame is a family of pairwise orthogonal primitive idempotents summing to . Every Jordan frame of has the same size , the rank of .
Every has a spectral decomposition over a Jordan frame, with real eigenvalues . From these, , , and a real function acts by . The inner product is the trace form . The cone of squares is ; means . The quadratic representation is , where .
The root-determinant is on . With and , the root-determinant cone and its candidate barrier are
A function is a -LHSCB for a cone if it is and convex on and tends to at the boundary. It must also satisfy and , and the parameter satisfies .
The goal holds for every finite-dimensional Euclidean Jordan algebra of rank , not for one matrix algebra.
which are (105), (107) and (108). 6. The scalar inequality (109c): for every . 7. The compatibility inequality (103) on :
The result gives the root-determinant cone a barrier whose parameter is one more than the optimal parameter of its domain , so it cannot be improved by more than one (p. 24). It also removes the extended formulation: a solver works with the cone in its natural dimension. The paper pairs the barrier with closed-form oracles for the gradient, Hessian product and inverse Hessian product (§7.4, Lemma 7.1), and reports computational gains in Hypatia. Because the statement is uniform over Euclidean Jordan algebras, it covers the vector, real symmetric and complex Hermitian cases at once.
The result is proved in the paper; this mission formalizes it. To the best of the curators' knowledge, it has no machine-checked proof, and Lean's Mathlib has no theory of Euclidean Jordan algebras, spectral decompositions in them, or barrier functions for their cones. Formalizing Proposition 7.1 therefore also yields a reusable layer: the Jordan-algebraic setting, the cone of squares, the quadratic representation, and an LHSCB predicate on arbitrary normed spaces.
The obvious route checks self-concordance of directly. That requires bounding the third derivative of by the -power of its Hessian in every direction. The two logarithmic terms interact, and no simple direct estimate is available. The paper instead uses a compatibility criterion of Nesterov and Nemirovskii, which reduces the barrier property to the single inequality (103) between derivatives of and . In Lean that criterion is not available and must be established for this cone; it is the deepest milestone.
The derivative identities (105), (107) and (108) require differential calculus of spectral functions on a Jordan algebra: derivatives of , of , and of , expressed through the eigenvalues of the scaled direction . Deriving them from the structure axioms needs, among other things, the fact that the eigenvalues of and are those of scaled and squared, uniqueness of the spectral decomposition, and positivity of the eigenvalues on . Only the final scalar inequality (109c) is elementary.
is a real finite-dimensional inner product space carrying a structure EJA V d. The structure bundles the Jordan product (bilinear, commutative, Jordan identity), the unit and the Euclidean property. It also bundles, for every , eigenvalues and a Jordan frame of primitive idempotents with , and the identity . The spectral theorem (Faraut–Korányi III.1.2) says such data exist for every Euclidean Jordan algebra of rank , so this is the paper's setting. Primitivity forces to be the rank: without it, a frame could be padded with zeros and would change.
The ambient space is . Directional derivatives are iterated Fréchet derivatives on the diagonal, and "boundary" is the topological frontier. The barrier limit is taken within the interior at every frontier point.
The following conventions are fixed:
Properness is a separate predicate from LHSCB, because is not pointed.
A trivializing formalization is ruled out by these choices. Specializing to or , dropping primitivity, allowing , dropping convexity, or imposing the barrier limit at only some boundary points would each prove a different, weaker or vacuous statement.
Proposition 6.1 (the -LHSCB for the matrix monotone derivative cones) and Lemma 7.1 (the inverse Hessian oracle) are deliberately absent. The first needs matrix monotonicity and Löwner's integral representation and is independent of Proposition 7.1. The second is an oracle formula that the goal does not use.
Contributions are welcome at every level: the scalar inequality (109c); the cone and homogeneity facts; the spectral calculus behind (105)–(108); and the compatibility reduction. The Jordan-algebraic infrastructure and the LHSCB predicate are reusable beyond this mission.
Resource allocation mechanisms distribute a divisible good among users who report numerical signals. In a network, the good can represent capacity; in a computing system, processing time. The mechanism sees the signals, allocates shares, and charges payments, but it does not know each user's value for a share or the most the user can pay. Those private budgets change both strategic behavior and the meaning of an efficient allocation. A share with a high nominal value may add little to the usable welfare if the recipient's budget is small. Caragiannis and Voudouris study this gap through liquid welfare, which caps each user's value at her budget, and the liquid price of anarchy, which measures the worst loss at a pure Nash equilibrium (Caragiannis and Voudouris, arXiv:1707.03551v3, §§1–2).
The Kelly mechanism is a basic proportional rule: a player's share is proportional to her submitted signal, and her payment is that signal. Its simplicity makes it a reference point for the efficiency of mechanisms that ask for only one number per user. Earlier work had bounded its liquid price of anarchy between 2 and 2.78, then improved the upper bound to 2.618. The paper establishes the exact value 2 for pure Nash equilibria (Caragiannis and Voudouris, pp. 4 and 14–15).
There are users and one divisible resource of unit size. User submits a signal . A resource allocation mechanism returns shares that either sum to one or are all zero, and payments . The mechanism is anonymous under relabeling of users, gives no allocation and charges no payment to a zero-signal user, and, as a function of a user's own signal, is strictly increasing and differentiable as Section 2 requires (the allocation of a sole positive bidder is the whole resource); the payment of a user deviating alone from the zero vector is continuous at zero, as p. 5 uses. The set consists of nonnegative signal vectors with at least two strictly positive entries. On that set, the own-signal derivative of each player's allocation is strictly positive, as recorded in footnote 5 (Caragiannis and Voudouris, pp. 4–6 and 9).
User has a nonnegative, nondecreasing, concave, differentiable valuation and a budget . A signal profile is a pure Nash equilibrium if every player's payment is affordable and no player can improve by changing her own signal to another nonnegative affordable one. An unaffordable choice has utility in the paper. Valuations need not vanish at zero; their value outside has no role in an admissible allocation (Caragiannis and Voudouris, p. 5 and footnote 1).
For a feasible allocation , liquid welfare is . Write for its maximum over feasible allocations and for the pure Nash equilibria of the game induced by . The game's liquid price of anarchy is the supremum of over ; takes the supremum over admissible games. For Kelly, and (Caragiannis and Voudouris, pp. 6–7 and 9).
The mission's goal is the full claim of Theorem 5.1, including both its upper and lower bounds:
The milestone path includes the affine worst-case game of Section 4, the structural bounds of Lemmas 4.1 and 4.2, and Lemma 4.3's equilibrium condition for the class of own-signal concave allocation and convex payment mechanisms. For each , the paper defines
The goal also needs the Kelly instance of , the displayed value of , and the supremum calculation on p. 15. Two Section 2 claims address equilibria outside : a profile with exactly one positive Kelly signal is impossible, and a zero profile is impossible when some user has a positive budget and gains value from receiving the whole resource (Caragiannis and Voudouris, pp. 5–6 and 9–15).
The equality 2 gives a tight worst-case efficiency guarantee for proportional allocation with private budgets under pure Nash behavior. It identifies the exact loss in the budget-capped welfare benchmark rather than a loose approximation factor. The structural Section 4 statements apply beyond Kelly: they translate the mechanism's allocation and payment derivatives into a numerical bound and identify a condition under which that bound is exact (Caragiannis and Voudouris, Lemmas 4.1–4.3, pp. 10–14).
The result is proved in the paper; the mission asks for a machine-checked proof of that known theorem and its stated supporting claims. The definitions of signals, mechanisms, budgeted games, and extended liquid welfare can support formalizations of other proportional or pay-your-signal mechanisms. The paper's companion lower bound for all resource allocation mechanisms, Theorem 3.1, belongs to a separate result and is outside this mission (Caragiannis and Voudouris, p. 8).
An equilibrium statement alone does not control the optimal liquid welfare: the optimum may assign the resource to a user whose equilibrium share is small, while other users' contributions are capped by budgets. The paper's central obstacle is to compare these different allocations uniformly over all valuations, budgets, and equilibria. Another obstacle is the boundary of the signal space. The structural bound is stated over , whereas the goal's price of anarchy includes every equilibrium. A proof therefore has to account for profiles with zero or one positive signal, as well as the possibility of infinite budgets or zero liquid welfare (Caragiannis and Voudouris, pp. 5–6 and Lemma 4.2, p. 13).
Players are Fin n, indexed from zero in Lean; the paper's player 1 is index zero. Signals and allocations are real vectors with explicit nonnegativity conditions. The formalization uses ℝ≥0∞ for budgets, liquid welfare, ratios, and suprema. Thus an infinite budget stays infinite and a positive optimum divided by zero welfare has value . Kelly pays its signal at every profile, matching the explicit payment formula on p. 9. At the all-zero profile, Lean's real gives the zero allocation. Own-signal derivatives use derivWithin on , including one-sided derivatives at zero. Valuations are arbitrary outside ; all admissibility conditions concern that interval.
The paper's Section 2 description of pay-your-signal mechanisms charges no one when fewer than two users submit positive signals. Applying that convention to Kelly makes the full Theorem 5.1 false for some games. The mission uses the paper's explicit Kelly payment instead. The mechanism axioms include the continuity of a lone deviator's payment at the zero signal vector, which the paper invokes on p. 5; with it Lemma 4.2 is stated, as printed, for the liquid price of anarchy over all equilibria. The paper's footnote 2 preference for games with at least two positive budgets and nonzero valuations is not imposed. Section 2's "increasing" is read as strictly increasing, since the paper writes "non-decreasing" for the weak notion and Lemma 4.2 fails for mechanisms with flat payments. The class is read in each player's own signal, as its use in Lemma 4.3 requires. The zero-profile milestone specifies to express an actual gain in value. These choices rule out vacuous bounds from real supremum defaults, converting budgets to zero, silently taking , or allowing unaffordable deviations.
The development needs Mathlib's finite sums, real analysis on intervals, extended nonnegative reals, and finite function updates. Contributions to the general mechanism definitions, the affine-game lemmas, the Kelly derivative calculation, and the boundary-equilibrium cases all serve the exact goal.
Cournot competition is the standard model of firms that compete by choosing quantities: each firm picks an output, the total output sets the market price, and an equilibrium is a profile in which no firm can gain by changing its own output alone. In practice firms rarely compete in one market. A manufacturer allocates a limited production capacity across regions, an advertiser allocates a budget across channels, a retailer allocates inventory across stores. The capacity couples the markets: what a firm sells in one market it cannot sell in another, so the markets can no longer be analysed one at a time.
Existence of equilibria in such games follows from general fixed-point arguments, and uniqueness under concave demand is known in several settings (for example Alsabah, Bernard, Capponi, Iyengar and Sethuraman, Multiregional oligopoly with capacity constraints, 2019–2021). What is usually missing is a description of the equilibrium itself: which firms enter which markets, and how much each firm allocates. R. Caldentey and M. B. Haugh (Operations Research, 2024) give that description for linear demand. Their Theorem 1 states the unique equilibrium in closed form, in terms of two scalar quantities per firm and per market, the augmented budgets and the cutoff budgets. The rest of their paper (participation thresholds, monotonicity, the limit of many small firms with a fixed aggregate budget, and merger effects) is read off from this formula.
There are firms and markets. Firm has a budget and chooses an allocation to each market subject to . Market has linear inverse demand
where is the total allocated to market . Firm 's profit is . Markets are ranked and budgets .
A Cournot equilibrium is a profile of feasible allocations such that, for every firm , no feasible allocation of firm yields a higher profit when the other firms keep their allocations.
Three derived quantities appear in the answer.
Finally , with when no firm qualifies, is the threshold index used in the formula. For it counts the firms active in market ; at the threshold index can be positive while every allocation to that market is zero.
Under the standing assumptions there is exactly one Cournot equilibrium, and it is
It is stated as an equivalence: a profile is a Cournot equilibrium if and only if . This single statement contains existence, uniqueness and the formula.
The milestones follow the proof in Appendix B.
Theorem 1 turns an equilibrium problem with coupled constraints into a formula that can be evaluated in closed form once is computed at points. It shows that firm 's allocation depends on the budgets only through , so a firm's behaviour is unaffected by the sizes of larger firms, only by their number. The paper's Proposition 1 (participation iff , monotonicity of allocations, and which budget constraints bind) and Proposition 2 (the limit of many firms with a fixed aggregate budget) are corollaries, as are its comparative statics on consumer surplus and welfare.
The result is proved in the paper, by a derivation through Lagrange multipliers. It has no machine-checked proof. A formalization would check the derivation, including the case of tied budgets, which the paper's proof sets aside in a footnote ("straightforward to handle"), and would make the closed form and the function available for the follow-up results.
Each firm's problem is a strictly concave quadratic program, so best responses are easy to describe one firm at a time. The difficulty is that the best responses are coupled through the market totals and through which firms are active in which market. The obvious approach, solving the first-order conditions market by market, requires knowing the set of active firms in each market, and that set depends on all the multipliers at once, while the multipliers depend on which budget constraints bind. Uniqueness requires showing that every equilibrium has multipliers of this form; existence requires that the formula's profile satisfies every firm's optimality conditions, including the inactive markets.
Firms are Fin N and markets Fin M; the paper's firm is the Lean index i.val + 1, so the factors and in (6) become i + 2 and (k+1)(k+2). Profiles are firm-first, x i j. All quantities are real numbers. The price is not truncated at zero. The equilibrium notion is the published CarbonDoubleCount.Planner.IsPureNash, which compares a firm's payoff against every feasible unilateral deviation.
The standing assumptions are bundled in one predicate: monotone, , , antitone, . The orderings that §2 makes "without loss of generality" are hypotheses, because the formulas (5) and (6) depend on them. Ties among budgets are allowed (the paper's proof assumes distinct budgets in a footnote; the theorem does not). and are allowed.
Pinned readings: the empty maximum in is ; is a real infimum, used only at nonnegative arguments; "the smallest real such that the budget holds" for a multiplier is complementary slackness; Lemma 1 is an identity for any non-decreasing and does not assume the market ordering; "greater than one" after (B-17) is read as "greater than zero".
The sentence after (7) calls the number of firms operating. At the allowed boundary this is not literally true: a one-market instance with positive budgets has and for every firm. The formal goal retains (7) and the closed form (6), and does not assert the false boundary interpretation.
The formula is a definition computed from the data. A statement that only asserts the existence of a unique equilibrium, or that defines by choice from an equilibrium, would not be Theorem 1; the goal is the equivalence with the explicit formula.
A complete development needs: KKT conditions for a separable concave quadratic program with one linear constraint (milestone 3), elementary properties of a water-filling level function (milestones 1–2), and finite summation identities (milestones 5–7). The water-filling lemmas and the summation identities are reusable beyond this mission. Proofs of any milestone, and alternative proofs of the goal that bypass the multiplier derivation, are welcome.
Given two Banach spaces and , we introduce and study a concept of norm-attainment in the space of nuclear operators and in the projective tensor product space . We exhibit positive and negative examples where both previous norm-attainment hold. We also study the problem of whether the class of elements which attain their norms in and in is dense or not. We prove that, for both concepts, the density of norm-attaining elements holds for a large class of Banach spaces and which, in particular, covers all classical Banach spaces. Nevertheless, we present Banach spaces and failing the approximation property in such a way that the class of elements in which attain their projective norms is not dense. We also discuss some relations and applications of our work to the classical theory of norm-attaining operators throughout the paper.
This mission is the statement-level formalization of Norm-attaining tensors and nuclear operators (arXiv:2006.09871v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
44 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract main negative result, pinned to Theorem 5.1 (Abstract main negative result, pinned to Theorem 5.1, PDF p. 20). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
We relate the structure of cyclotomic and degenerate cyclotomic BMW algebras, for arbitrary parameter values, to that for admissible parameter values. In particular, we show that these algebras are cellular. We characterize those parameter sets for affine BMW algebras over an algebraically closed field that permit the algebras to have non--trivial cyclotomic quotients.
This mission is the statement-level formalization of Remarks on Cyclotomic and Degenerate Cyclotomic BMW Algebras (arXiv:1011.3284v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Cellularity of all cyclotomic BMW algebras over fields (Corollary 6.5 (abstract main result), PDF p. 17). 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:
Let be a hypersurface that is strictly star-shaped about the origin. The standard Liouville form restricts to a contact form on , and its Reeb vector field is a reparametrization of the Hamiltonian flow of any function with as a regular level. Weinstein conjectured in 1978, motivated by results of Rabinowitz, that Reeb flows on closed contact manifolds have periodic orbits; H. Hofer established this for the three-sphere and further three-dimensional cases in 1993 (Invent. Math. 114), with finite-energy pseudoholomorphic curves in the symplectization as the central objects. Since then these curves have been the main source of periodic orbits, global surfaces of section and invariants of Reeb flows, for example in U. Hryniewicz's characterization of the Reeb orbits that bound disk-like global surfaces of section (arXiv:1105.2077).
The basic fact about these curves is their behaviour near a puncture: a finite-energy curve on a punctured disk either extends over the puncture or approaches a periodic Reeb orbit there. This mission formalizes that statement for the symplectization of a strictly star-shaped level in , following C. Wendl, Lectures on Symplectic Field Theory, Lecture 9 (arXiv:1612.01009), together with the results on planes, cylinders and energy concentration that accompany it in Hofer's and Hryniewicz's papers. It is the seventh mission in a series on symplectic field theory and builds on the sixth, which defines almost complex structures and pseudoholomorphic maps on open subsets of a vector space.
Let be a finite-energy -holomorphic curve on the punctured unit disk . Then either extends smoothly and -holomorphically over with values in , or the charge at exists and is nonzero, as with the sign of , and for every sequence a subsequence of the loops converges in to for a periodic Reeb orbit (Wendl, Theorem 9.8, without the nondegenerate and Morse–Bott clause and without the linear asymptotics of along the end).
HryniewiczCriterion setting, with period equal to action.The results. The goal is the local half of SFT compactness and of the Fredholm theory of punctured curves: it says every finite-energy end is cylindrical over a Reeb orbit, which is what makes asymptotic operators, Conley–Zehnder indices and the index formula of the earlier missions applicable to actual curves. Milestones 9–14 (from Hofer, Hryniewicz and Wendl) describe planes, cylinders and bubbling in the form in which they enter Hofer's work on the Weinstein conjecture for and Hryniewicz's work on global surfaces of section; milestone 15 connects them to the open HryniewiczCriterion mission. Milestones 6–8 are general results about pseudoholomorphic maps into any finite-dimensional space.
Formalizing them. All results are classical and proved in the cited sources. None of them has been formalized in a proof assistant, as far as a literature search shows; Mathlib has no symplectizations, no Hofer energy and no Reeb dynamics. The mission produces these objects in general dimension , with the energies as lower Lebesgue integrals.
The target is not compact and is not the standard structure, so the curves can escape to or to infinity; the goal has to decide which happens and produce a limit orbit, though the limit orbit is not assumed nondegenerate and may depend on the chosen sequence of radii. Hofer's energy is a supremum over a family of integrands rather than a single integral, and its finiteness does not bound the Euclidean area of the curve. The Euclidean size of the derivative grows with , so all scale-sensitive statements are made with the size , which is invariant under . Milestones 7–8 hold for an arbitrary norm on the target and an almost complex structure defined only on an open set.
FiniteEnergyPlane; the definition module FiniteEnergyPlane_Setting imports JHolomorphic_Setting (the sixth mission) for IsAlmostComplexOn and IsJHolomorphicOn. The bridge item also imports HryniewiczCriterion_Basic.Fin (2 * (n + 1)) → ℝ with interleaved coordinates; matches HryniewiczCriterion.R4. Its default norm is the sup norm.scaleToS H y is the with (default , used only at ), proj H y = scaleToS H y • y, aCoord H y = -½ log (scaleToS H y).ℝ≥0∞-valued lower integrals of ENNReal.ofReal of the integrands, so is a genuine restriction (a Bochner integral would return on non-integrable integrands and make it vacuous).Contributions welcome: general lemmas on lower integrals over planar domains and on radial projections to star-shaped hypersurfaces.
We study admissibility conditions for the parameters of degenerate cyclotomic BMW algebras. We show that the u-admissibility condition of Ariki, Mathas and Rui is equivalent to a simple module theoretic condition.
This mission is the statement-level formalization of Admissibility Conditions for Degenerate Cyclotomic BMW Algebras (arXiv:0905.4253v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The four equivalent admissibility conditions (Theorem 5.2, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Let G be an affine algebraic group and let X be an affine algebraic variety. An action is called observable if for any G-invariant, proper, closed subset Y of X there is a nonzero invariant such that f(Y) =0. We characterize this condition geometrically as follows. The action is observable if and only if (1) there is a nonempty open subset consisting of closed orbits, and (2) the field of G-invariant rational functions on X is equal to the quotient field of . In case G is reductive, we conclude that there exists a unique, maximal, G-stable, closed subset of such that is observable. Furthermore, the canonical map is finite and bijective.
This mission is the statement-level formalization of Observable actions of algebraic groups (arXiv:0902.0137v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Observability, invariant rational functions, and generic closed orbits (Abstract main characterization; Theorem 3.10, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
12 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper all of the classical constructions of A. Young are generalized to affine Hecke algebras of type A. It is proved that the calibrated irreducible representations of the affine Hecke algebra are indexed by placed skew shapes and that these representations can be constructed explicitly with a generalization of Young's seminormal construction of the irreducible representations of the symmetric group. The seminormal construction of an irreducible calibrated module does not produce a basis on which the affine Hecke algebra acts integrally but using it one is able to pick out a different basis, an analogue of Young's natural basis, which does generate an integral lattice in the module. Analogues of the "Garnir relations" play an important role in the proof. The Littlewood-Richardson coefficients arise naturally as the decomposition multiplicities for the restriction of an irreducible representation of the affine Hecke algebra to the Iwahori-Hecke algebra.
This mission is the statement-level formalization of Skew shape representations are irreducible (arXiv:math/0401326v2). 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 Local intertwiners on generalized weight spaces (Proposition 3.2, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
10 results of the paper are not stated yet, because the library lacks an interface they need:
A representation of the exceptional Lie algebras is presented. It reflects a simple unifying view and it is realized in terms of Zorn-type matrices. The role of the underlying Jordan pair and Jordan algebra content is crucial in the development of the structure. Each algebra contains three Jordan pairs sharing the same Lie algebra of automorphisms and the same external su(3) symmetry. Applications in physics are outlined.
This mission is the statement-level formalization of Exceptional Lie Algebras, SU(3) and Jordan Pairs Part 2: Zorn-type Representations (arXiv:1403.5120v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is G2 realized by the closed special Zorn commutator (§4, (4.4)–(4.7): G2 Lie realization, PDF p. 11). 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:
We derive the class of covariant measurements which are optimal according to the maximum likelihood criterion. The optimization problem is fully resolved in the case of pure input states, under the physically meaningful hypotheses of unimodularity of the covariance group and measurability of the stability subgroup. The general result is applied to the case of covariant state estimation for finite dimension, and to the Weyl-Heisenberg displacement estimation in infinite dimension. We also consider estimation with multiple copies, and compare collective measurements on identical copies with the scheme of independent measurements on each copy. A "continuous-variables" analogue of the measurement of direction of the angular momentum with two anti-parallel spins by Gisin and Popescu is given.
This mission is the statement-level formalization of Covariant quantum measurements which maximize the likelihood (arXiv:quant-ph/0403083v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §III, Eq.(12): finite-component weak twirling formula (§III, Eq.(12): finite-component weak twirling formula, 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.
6 results of the paper are not stated yet, because the library lacks an interface they need:
We start with Fannes' type and Winter's type tight continuity bounds for the quantum conditional mutual information and their specifications for states of special types. Then we analyse continuity of the Holevo quantity with respect to nonequivalent metrics on the set of discrete ensembles of quantum states. We show that the Holevo quantity is continuous on the set of all ensembles of m states with respect to all the metrics if either m or the dimension of underlying Hilbert space is finite and obtain Fannes' type tight continuity bounds for the Holevo quantity in this case. In general case conditions for local continuity of the Holevo quantity for discrete and continuous ensembles are found. Winter's type tight continuity bound for the Holevo quantity under constraint on the average energy of ensembles is obtained and applied to the system of quantum oscillators. The above results are used to obtain tight and close-to-tight continuity bounds for basic capacities of finite-dimensional channels (refining the Leung-Smith continuity bounds).
This mission is the statement-level formalization of Tight continuity bounds for the quantum conditional mutual information, for the Holevo quantity and for capacities of quantum channels (arXiv:1512.09047v7). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
28 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2, (35): optimized energy-constrained QCMI continuity; original seed (Proposition 2, (35): optimized energy-constrained QCMI continuity; original seed, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
11 results of the paper are not stated yet, because the library lacks an interface they need:
In order to study multipartite quantum cryptography, we introduce quantities which vanish on product probability distributions, and which can only decrease if the parties carry out local operations or carry out public classical communication. These ``secrecy monotones'' therefore measure how much secret correlations are shared by the parties. In the bipartite case we show that the mutual information is a secrecy monotone. In the multipartite case we describe two different generalisations of the mutual information, both of which are secrecy monotones. The existence of two distinct secrecy monotones allows us to show that in multipartite quantum cryptography the parties must make irreversible choices about which multipartite correlations they want to obtain. Secrecy monotones can be extended to the quantum domain and are then defined on density matrices. We illustrate this generalisation by considering tri-partite quantum cryptography based on the Greenberger-Horne-Zeilinger (GHZ) state. We show that before carrying out measurements on the state, the parties must make an irreversible decision about what probability distribution they want to obtain.
This mission is the statement-level formalization of Multipartite Classical and Quantum Secrecy Monotones (arXiv:quant-ph/0202103v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The two classical multipartite secrecy monotones (Abstract; §III, (12)–(17),(24),(28),(30),(35), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
5 results of the paper are not stated yet, because the library lacks an interface they need:
We give an explicit characterisation of the quantum states which saturate the strong subadditivity inequality for the von Neumann entropy. By combining a result of Petz characterising the equality case for the monotonicity of relative entropy with a recent theorem by Koashi and Imoto, we show that such states will have the form of a so-called short quantum Markov chain, which in turn implies that two of the systems are independent conditioned on the third, in a physically meaningful sense. This characterisation simultaneously generalises known necessary and sufficient entropic conditions for quantum error correction as well as the conditions for the achievability of the Holevo bound on accessible information.
This mission is the statement-level formalization of Structure of states which satisfy strong subadditivity of quantum entropy with equality (arXiv:quant-ph/0304007v2). 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 Theorem 6: structure of equality in strong subadditivity (original seed) (Theorem 6: structure of equality in strong subadditivity (original seed), 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.
5 results of the paper are not stated yet, because the library lacks an interface they need:
The purpose of this work is to extend the result of previous papers quant-ph/9611023, quant-ph/9703013 to quantum channels with additive constraints onto the input signal, by showing that the capacity of such channel is equal to the supremum of the entropy bound with respect to all apriori distributions satisfying the constraint. We also make an extension to channels with continuous alphabet. As an application we prove the formula for the capacity of the quantum Gaussian channel with constrained energy of the signal, establishing the asymptotic equivalence of this channel to the semiclassical photon channel. We also study the lower bounds for the reliability function of the pure-state Gaussian channel.
This mission is the statement-level formalization of On Quantum Communication Channels with Constrained Inputs (arXiv:quant-ph/9705054v1). 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 Proposition 2: constrained discrete classical–quantum capacity, (10) (Proposition 2: constrained discrete classical–quantum capacity, (10), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
We consider quantum devices for turning a finite number N of d-level quantum systems in the same unknown pure state \sigma into M>N systems of the same kind, in an approximation of the M-fold tensor product of the state \sigma. In a previous paper it was shown that this problem has a unique optimal solution, when the quality of the output is judged by arbitrary measurements, involving also the correlations between the clones. We show in this paper, that if the quality judgement is based solely on measurements of single output clones, there is again a unique optimal cloning device, which coincides with the one found previously.
This mission is the statement-level formalization of Optimal Cloning of Pure States, Judging Single Clones (arXiv:quant-ph/9807010v1). 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 Sharp single-clone error bound and explicit attainment (Theorem 1, inequality and Eq.(3), 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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
The more than thirty years old issue of the (classical) information capacity of quantum communication channels was dramatically clarified during the last years, when a number of direct quantum coding theorems was discovered. The present paper gives a self contained treatment of the subject, following as much in parallel as possible with classical information theory and, on the other side, stressing profound differences of the quantum case. An emphasis is made on recent results, such as general quantum coding theorems including cases of infinite (possibly continuous) alphabets and constrained inputs, reliability function for pure state channels and quantum Gaussian channel. Several still unsolved problems are briefly outlined.
This mission is the statement-level formalization of Coding Theorems for Quantum Channels (arXiv:quant-ph/9809023v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: general quantum-channel coding theorem (seed) (Theorem 1: general quantum-channel coding theorem (seed), PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
We show that no distillation protocol for Gaussian quantum states exists that relies on (i) arbitrary local unitary operations that preserve the Gaussian character of the state and (ii) homodyne detection together with classical communication and postprocessing by means of local Gaussian unitary operations on two symmetric identically prepared copies. This is in contrast to the finite-dimensional case, where entanglement can be distilled in an iterative protocol using two copies at a time. The ramifications for the distribution of Gaussian states over large distances will be outlined. We also comment on the generality of the approach and sketch the most general form of a Gaussian local operation with classical communication in a bipartite setting.
This mission is the statement-level formalization of On the impossibility of distilling Gaussian states with Gaussian operations (arXiv:quant-ph/0204052v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-copy Gaussian no-distillation under the restricted Fig.1 protocol (Theorem (p.2); restricted two-copy Gaussian no-distillation result announced p.1, 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.
1 results of the paper are not stated yet, because the library lacks an interface they need: