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?
Managers who run a firm also trade its stock. Accounting and finance research has long asked how the opportunity to trade on private information changes what managers do inside the firm. Real activities manipulation means that a manager distorts operating choices (production, investment, discretionary spending) rather than accounting numbers. The usual concern is that insider trading pushes such choices away from value maximization (Roychowdhury, J. Accounting and Economics, 2006).
Chen and Jorgensen (SSRN 2358668; Management Science, 2021, doi:10.1287/mnsc.2020.3915) combine a product-market decision with the one-period insider trading model of Kyle (Econometrica 53, 1985). The trading stage is Kyle's linear equilibrium: an informed trader, noise traders and a competitive market maker. What is new is that the variance of the asset's value is not exogenous. The manager chooses it through the firm's output. Their basic result, Proposition 1, determines the equilibrium output of a monopolist whose manager will later trade. The later sections (Cournot duopoly, cross-trading, the board's choice of the manager's stake) all reuse this computation.
A monopolist faces the inverse demand , where is output and marginal cost is . The demand intercept has prior . Before producing, the manager observes and publicly discloses a signal , with . Given the realized , the demand intercept has the posterior
After the manager chooses , the firm value is . The manager learns and submits a demand for the firm's shares. Noise traders submit , independent of . A market maker sees only the total order flow and sets the price . Strategies are linear: the manager's demand is and the price is .
A linear equilibrium of the trading stage at is a pair of such strategies with two properties. For every realized , the demand maximizes the insider's expected profit over all . And the price equals almost surely. The manager owns a stake in the firm and chooses to maximize
A linear equilibrium is a quantity together with a trading-stage equilibrium at , such that no other quantity , followed by any trading-stage equilibrium at , does better. Write .
Under , and , there is exactly one linear equilibrium. Its output is
and its trading strategies are
The goal is stated as an equivalence: a pair is an equilibrium if and only if it is this one.
These are the steps of the paper's proof in Appendix A:
Without insider trading the manager would choose (§2.1). Proposition 1 gives . When the manager can trade, the firm overproduces. The distortion shrinks as the stake grows, and it grows with the noise-trading variance and with the residual demand uncertainty. The paper's consumer-welfare remark, the comparative statics in Corollaries 1.1–1.2, and the contracting analysis of §4 all start from these closed forms. So do the duopoly results (Propositions 2–4), which repeat the same computation with two firms.
The result is proved in the paper, by a first-order-condition argument. As far as we know it has no machine-checked proof. The formal development adds two things to the paper's argument. First, the trading-stage equilibrium is unique among all linear pairs, not only the one the first-order conditions produce. Second, the production choice is compared against every real quantity, including negative ones (footnote 7), each followed by any of its trading equilibria. The paper's appeal to "the first-order condition" leaves both checks implicit.
The algebra of the closed forms is routine. The work is in the trading stage, where the price is a conditional expectation. To identify with an affine function of , one needs the regression formula for a jointly Gaussian pair built from independent normals. One also needs uniqueness: two affine functions of a non-degenerate Gaussian that agree almost surely have the same coefficients. Mathlib has the one-dimensional Gaussian law and conditional expectation, but no ready-made Gaussian conditioning lemma of this form.
Uniqueness of the trading-stage equilibrium also requires ruling out . In that case the insider's quadratic payoff has no maximizer for some realized value. Finally, the production comparison runs over all real quantities. The insider's gain is , not , so the objective has two concave branches. The global maximizer is only when .
Everything is real-valued and lives in the namespace KyleProduction.Monopoly. The variances are named Sa, Sθ, Su and is lam. The model is analysed conditional on the realized signal :
gaussianReal (postMean P) (postVar P).toNNReal;gaussianReal 0 Su.toNNReal;Deriving the posterior from the prior and the signal is not part of the mission. Market efficiency (4) is stated with Mathlib's condExp with respect to the σ-algebra generated by the order-flow map, almost surely under the joint law. Insider optimality (3) is required for every realization of . Quantities range over .
The formalization commits to these hypotheses and conventions:
Three printed slips are corrected in the Lean statements and kept as printed in the milestone texts:
A trivial formalization would define the price by the regression formulas, or define the objective by the closed form in place of the trading profit of an equilibrium. The first makes milestone 3 a tautology. The second collapses the goal to milestone 7. Neither is done here: the price is the conditional expectation, and the objective integrates the realized trading profit.
The work needs a lemma for the conditional expectation of a Gaussian given an affine Gaussian observation, together with the a.s. identification of affine functions of a non-degenerate Gaussian. Both are reusable beyond this mission, for other Kyle-type and rational-expectations models. Contributions of these lemmas, of the trading-stage uniqueness and of the production comparison are all welcome.
Near-term quantum processors have few qubits, while the circuits one would like to run (variational eigensolvers, sampling benchmarks, error-mitigated algorithms) often need more qubits than any single device has. Peng, Harrow, Ozols and Wu (arXiv:1904.00102, Phys. Rev. Lett. 125, 150504, 2020) show that a circuit which is only loosely connected (a few qubits pass between otherwise separate parts) can be simulated by running the parts separately on a smaller device and combining the outcomes classically. The overhead is exponential in the number of qubits that cross between parts and polynomial in everything else. The technique is now usually called circuit cutting or wire cutting.
Timeline:
A tensor network is a finite directed multigraph with a complex tensor at every vertex. Every edge carries an index , with elementary matrix . A state , a gate and an observable on one qubit have the tensors
The value of the network is
For the network of a quantum circuit followed by a classical post-processing , the value is the expected output of the algorithm.
A clustering fixes the final observable vertex (no outgoing edges) and puts every other vertex into one of clusters . The cut edges are the edges between different clusters (edges into excluded). The qubit count is the number of input vertices ◁ of (vertices without incoming edges) plus the number of edges entering from other clusters. The network is -clustered if and for all .
Cutting an edge. With the Pauli matrices , the eight triples are , , , , , , and . For , the cut network replaces every cut edge by and , and .
The estimator. For each , running the pieces of on the device yields an outcome whose expectation is . One sample draws uniformly and outputs . The estimate is the average of independent samples.
For a -clustered network with clusters, any device laws as above and , let . Then
Moreover, every cut network splits into clusters with no edges between them, each needing at most qubits. Together, these give the paper's " runs of a -qubit device": samples, each running pieces.
The theorem turns the qubit budget of a device into a parameter of the simulation: a circuit on qubits can be run on qubits at a cost of , which is efficient whenever only qubits pass between clusters. Its edge-cutting identity (Lemma 1) is the basic quasi-probability decomposition of the identity channel. It is reused in the paper's own Theorem 2 (decomposable post-processing, contraction-complexity bounds) and in its Hamiltonian-simulation application.
The theorem has a complete proof with explicit constants on pp. 8–10 of the paper. No machine-checked proof of the theorem or of its edge-cutting lemma is known. Formalizing it gives a machine-checked tensor-network semantics for the cut, the Pauli measure-and-prepare decomposition, and a concrete Monte Carlo guarantee. The general two-sided Hoeffding bound is already proved on the platform (Concentration.hoeffding_two_sided) and is included as a reference.
The decomposition of the identity channel is a finite matrix identity. The difficulty is in carrying it through the network. Cutting edges at once changes the vertex and edge types of the graph, and the sum over must be re-indexed over the new edge set. The obvious route, cutting one edge at a time, changes the type of the graph at every step and does not compose cleanly. The statement is therefore made for a set of edges at once.
A second difficulty is probabilistic. The samples are drawn from a mixture over strings of pushforwards of device laws. Applying Hoeffding's inequality requires the product law of such samples, a bound on their support, and the identification of their mean with the complex value .
Fin 2 × Fin 2. Single-qubit operators are Matrix (Fin 2) (Fin 2) ℂ. The eight cases are Fin 8, and Lean's is the paper's .src tgt : E → V, and tensors A : V → (E → Π) → ℂ that read a full edge labelling. Locality is not imposed, so all statements hold for slightly more general networks than the paper's. Vertex kinds are not recorded: a ◁ is a vertex without incoming edges.Fin r, and empty clusters are allowed. The qubit count is #◁ plus the incoming cut edges. This is the paper's p. 3 form; the paper's "out-degree" phrasing on p. 2 is not used.The moving sofa problem, posed by Leo Moser in 1966, asks for the planar shape of largest area that can be moved around a right-angled corner in a hallway of unit width — one of the most famous unsolved problems of everyday geometry. Joseph Gerver exhibited in 1992 a sofa of area 2.2195... built from five boundary curves solving a system of balancing ordinary differential equations, and conjectured it to be the largest possible; Dan Romik later derived the curves' exact formulas, and Kallus and Romik proved the best upper bound before the source. The source resolves the problem: Baek proves that Gerver's sofa is optimal, so the sofa constant is Gerver's area 2.2195..., and the sixty-year-old problem is closed.
The mission formalizes the proof of Theorem 1.1.1 of the source — Gerver's sofa attains the maximum area among all moving sofas — following the paper's own attack path: reduce to monotone sofas and their supporting rotation paths, express the sofa area through the cap and niche of the path, control the rotation angle of large sofas, take Hausdorff limits of maximum polygon sofas to obtain balanced maxima, establish the injectivity of the supporting path of a maximizer, and dominate every injectivity-constrained path by a Gerver sofa through the concavity of the area upper bound Q.
The arena is the L-shaped hallway L, the union of the horizontal side (-∞, 1] × [0, 1] and the vertical side [0, 1] × (-∞, 1]. A shape is a nonempty compact subset of the plane — the source's standing convention, adopted here — and a moving sofa is a nonempty, compact, connected shape that admits a movement around the corner. A movement is encoded by two continuous paths: a rotation angle path Θ and a translation path W, producing the rigid motion Φ_t(p) = rot(Θ t) p + W t of the unit interval, with Θ 0 = 0, the initial image inside the horizontal side, every intermediate image inside the hallway, the final image inside the vertical side, and total clockwise rotation -Θ 1 = ω, the movement's rotation angle. The area of a planar set is its two-dimensional Lebesgue measure as a real number; the maximum sofa area α_max is the supremum of the areas of all moving sofas.
The monotone arena replaces sofas by their supporting rotation paths. A rotation path x with angle ω ∈ (0, π/2] determines strips, quarter-planes Q_t⁺ \ Q_t⁻ at the outer and inner corners of the translated hallways, the parallelogram P_ω, the fan F_ω, the cap (Equation 1.3), the niche (Equation 1.4), and the monotone sofa of the path — the common part of the strips and the hallways (Equation 1.2). A supporting path pins down the canonical inner-corner path through contact: both outer walls of every supporting hallway touch the sofa. Balanced maximum sofas are stated at the level of sofas: a moving sofa that is the Hausdorff limit of maximum polygon sofas whose uniform angle sets run over a strictly increasing sequence of powers of two, with Hausdorff convergence phrased through Euclidean ε-neighborhoods rather than Mathlib's metric thickening API. The Gerver sofa is characterized by the paper's own structural properties: a moving sofa equal to the monotone sofa of its rotation path, whose supporting-hallway structure is carried by the five curves of Definition 8.4.3 with contact on the outer and inner walls and satisfying the balancing ODEs of Theorem 8.4.2 on the five intervals cut by angles 0 < φ < θ < π/4, derivatives taken one-sided within each interval. The source defers the curves' explicit formulas to Gerver's and Romik's papers; the existential form — some sofa satisfying this structure — is used for the goal and the dominating bound, since that is what the proof of Theorem 1.1.1 actually produces.
Six conventions deserve disclosure. First, the platform publishes definitions as modules Definitions.Def_<definition_name>, so the three definition bundles — the hallway arena, the monotone arena, and the Gerver sofa structure with Mamikon's swept region — are published as platform definitions (Gerver_arena, Gerver_monotone, Gerver_sofa) and attached to the proposal as reference items; the theorem drafts import them. Second, the injectivity condition abridges the source's Definition 6.1.2 by dropping its auxiliary clause on the boundary curve σ_K, keeping the continuous differentiability and the two strict derivative inequalities that the endgame consumes. Third, balancedness is stated at the sofa level rather than through the paper's rotation-path data, the sofa-level form being what the compactness argument yields. Fourth, the generalized Mamikon theorem is stated for continuously differentiable tangent segment families with continuous lengths and pairwise non-overlap on the open parameter rectangle, over turning intervals of length below π — exactly the smooth, non-self-overlapping families to which the endgame applies it. Fifth, the movement's initial term is a pure translation (Θ 0 = 0), matching the source's Definition 1.1.2 with its footnote. Sixth, all statements are developed against the platform's Mathlib build (0df444a), with inner products, rotations, scalings, and neighborhoods given by small self-contained definitions so that every draft compiles without instance-hunting.
The goal is Theorem 1.1.1: some Gerver sofa has area at least that of every moving sofa. The supporting chain, in the paper's order, each step a milestone except the last:
The goal follows by assembling the chain: every moving sofa sits under a monotone one, maximizers are balanced maxima admitting the full right angle, their supporting paths are injectivity-constrained, and the dominating bound caps them by a Gerver sofa.
The moving sofa problem is a benchmark of planar geometry that has resisted exact solution since 1966; the source closes it. The proof is not a computational verification but a structural argument — compactness produces extremal objects, contact geometry pins their supporting paths, injectivity rules out self-overlap, and a concavity argument of a kind familiar from calculus of variations delivers the dominating bound. Each layer is a theorem of lasting value independently of the goal: the cap-niche decomposition, the existence of balanced maxima, the injectivity of maximizer paths, and the generalized Mamikon theorem all predate or outlive the final step. A Lean formalization makes each layer independently checkable, and the mission's chain structure lets solvers claim credit for any layer while the community assembles the whole.
The formalization spans real analysis, topology, convex geometry, and measure theory, at a level well beyond elementary competition material but below the frontier of ongoing formalization projects. The monotone reduction and the cap-niche identity require careful handling of intersections of translated half-planes and the additivity of Lebesgue measure; the balanced-maximum existence requires sequential compactness in the Hausdorff topology; injectivity requires differentiability arguments on paths defined by contact conditions; the endgame requires the concavity of the functional Q on triples of convex bodies. The definitions are engineered to be self-contained — plain real arithmetic for inner products, rotations, and neighborhoods — so that the labor concentrates on the geometry rather than on API friction. Individual milestones are of moderate difficulty; the goal requires assembling all of them, which is the source's own achievement.
Every item quantifies only over the objects it needs — hallways, shapes, rotation paths, angle sets, segment families; no item carries a vacuous hypothesis: moving sofas, monotone sofas, polygon intersections, and Gerver sofas all exist, and the inequalities are in the intended directions. The fragment excludes the explicit trigonometric formulas of Gerver's curves (the goal needs only their structural characterization), the source's sections on the ambidextrous sofa and non-convex generalizations, the computer-search evidence for the sofa constant's decimals, and any statement about shapes that are not moving sofas. Nothing in the mission asserts the uniqueness of the Gerver sofa or the value of the sofa constant as a decimal; it formalizes what the source proves — optimality.
An advertiser observes customer paths through a sequence of states and advertising actions, then wants to assign credit for a purchase to the actions that occurred. Giving the last action all the credit misses earlier interactions; dividing credit by the number of visits can overreward a repeated action. Credit should also reflect what would have happened under the baseline no-ad action. Singal, Besbes, Desir, Goyal, and Iyengar formulate these requirements in a Markov model and a cooperative game, then connect their counterfactual adjusted Shapley value to a path-based quantity (Singal et al., SSRN version, §§3–5).
The paper is a known research result, published in Management Science in 2022. This mission uses the authors' August 21, 2021 SSRN version, whose displayed equations and page numbers are the formalization's citation basis. Its objective is to formalize the paper's characterization theorem, together with the intermediate claims that identify what a coalition is worth and how the ordinary Shapley value treats a converting customer path.
The transient states are ; a customer eventually reaches either the absorbing conversion state or the absorbing quit state . The actions are , with action designated as the baseline no-ad action. A customer begins at state with probability . At state , the advertiser takes action with probability . The probabilities , , and govern the next transient state, conversion, and quitting. The initial and action distributions sum to one, each transition row sums to one, and all probabilities are nonnegative. The paper's absorption assumption says that every customer eventually converts or quits, starting from any transient state (§2.1, pp. 6–8).
A player is one state-action pair , and the player set is . To value a coalition , only its players keep their actions. Action probability assigned to a pair outside instead takes an artificial zero-value action that sends the customer to . If is the resulting transient-state transition matrix and its one-step conversion vector, the coalition value is the conversion probability . Conversion has value one, so there is no additional revenue parameter (§2.3, p. 9; §4.2, pp. 14–15).
The Shapley value averages the marginal value over coalitions that omit , weighted by . For the counterfactual adjusted Shapley value, or CASV, the baseline value is instead : the frequency assigned to is spent on the no-ad transition row, in addition to any existing no-ad frequency. Thus CASV compares an advertising action with its specified no-ad alternative (§4.2–4.3, pp. 15–16).
A path lists the state-action pairs encountered before quitting or conversion. Write for the number of distinct pairs, regardless of repetitions. The unique-uniform weight is when the path converts and contains , and zero otherwise. It rewards each distinct participating pair once (§3.3, p. 12; Proposition 1, p. 20).
The first target is Proposition 1, which identifies the ordinary Shapley value of the coalition game with the expected unique-uniform weight:
The mission goal is Theorem 2. Let be the counterfactual chain for . It characterizes CASV as a difference of two path expectations:
The milestone list also records display (6), the matrix and path forms of coalition value in Step 1 of the proof of Proposition 1, and the Step 3 carrier-game identity. These are the paper's intermediate statements, with the carrier-game fact linked to an already proved general Shapley theorem (pp. 16, 20–22).
Theorem 2 gives a path-based meaning to a value defined by averaging over coalitions. It separates the credit earned in the observed Markov chain from the credit that the same player identity would earn under a baseline no-ad transition. This distinction matters in the paper's Example 5: an ad and a no-ad action both guarantee conversion, so the ad receives zero counterfactual credit despite having ordinary Shapley value one (pp. 15–16, 20, 22).
The paper also develops estimation methods after the characterization, but those algorithms and their numerical performance are outside this mission. Formalizing the known theorem would supply a reusable connection among absorbing finite chains, coalition conversion games, and Shapley values. The linked general Shapley definition and carrier-game result are already available as platform content; the paper-specific model and theorem statements here remain draft formalization targets.
A coalition changes which state-action pairs can contribute to a path. The Shapley definition averages marginal coalition values, whereas a path expectation assigns a weight to a realized sequence, including sequences that revisit the same pair. Identifying these two descriptions requires accounting for the distinct set of players on every converting path. Counterfactual adjustment adds another chain whose player identities and action frequencies must align with the original model; simply removing or merging the player changes the quantity in Theorem 2 (proof of Proposition 1, p. 21; Appendix B, p. 46).
States and actions are Fin m and Fin n, so the paper's index is Lean index . The model designates a noAd action rather than assuming it is Lean index zero. Players are pairs in Fin m × Fin n; the ordinary Shapley value transports them to Fin (m*n) to reuse the published Shapley definition. The separate general action-chain definition contains the initial, action, and transition probabilities; the attribution model adds the no-ad action and the coalition game.
The Valid predicate states every distribution and row-sum condition. Absorbing states convergence of powers of the original averaged transient matrix to zero. Theorem 2 additionally assumes absorption of the counterfactual chain, because absorption of the original alone does not imply it. This makes the inverse in each coalition value represent the conversion probability under the paper's Assumption 1; a singular matrix's totalized Lean inverse must not supply a default answer.
The counterfactual chain keeps at frequency and as a player, while replacing its transition row by the no-ad row. This reading matches the counterfactual marginal displayed in Appendix B. Pairs outside a coalition take the artificial quit action; that action is never a player. Path expectation is a real tsum over finite converting paths, each weighted by its initial probability, action frequencies, transitions, and final conversion probability. Nonconverting paths contribute zero. The Shapley weight and the conversion value one are exactly the paper's constants. CASV is defined by display (5), and path expectation is defined independently, so Theorem 2 does not follow by unfolding a prearranged identity. Work on path summability, matrix-series convergence, coalition path expansions, and the connection to the general Shapley theorem is welcome.
An innovation contest gives several agents a fixed period to submit solutions and awards prizes according to their final ranks. A platform choosing that period faces two practical effects: more time lets agents improve their submissions, while it delays the value of the best solution and can make the effort needed to participate more costly overall. The question is how the chosen duration changes when the quality of submissions becomes more uncertain or when agents become more productive over time. Korpeoglu, Körpeoğlu, and Tunç study this decision in a contest model motivated by crowdsourcing platforms and distinguish organizers by how strongly they discount a late solution. Their patient organizer result is the target here. Korpeoglu, Körpeoğlu, and Tunç, 2020.
There are agents and a fixed present-value award scheme. Agent chooses a nonnegative per-time effort path during a contest of duration . The path improves deterministic output at rate , where productivity is positive. The final output adds an independent random shock with a common mean-zero, log-concave density . The organizer values the best final output. The model uses the scale transformation to vary uncertainty without choosing a special distribution; its density is for . When studying changing productivity, the paper sets , so is the productivity exponent. Model, pp. 8–9.
Effort costs per unit time, with and . Write for total deterministic output improvement. The least cost of producing is , where . A participant also bears a fixed cost . An agent with the th-largest output receives a present-value award , with , nonnegative, nonincreasing shares , and . The contest's symmetric equilibrium effort is represented by , where and measures the effect of a small effort increase on the probability of rank . Lemma 1 and equations (3)–(5), pp. 10–12.
For this mission the award scheme is held fixed, as it is in the paper's duration analysis. The organizer chooses among positive durations satisfying the agents' best-response and participation conditions. At duration , the organizer's profit is , where is the organizer's discount factor and is the largest shock. An optimal duration maximizes this profit among feasible durations. The patient regime is , with evaluated from the model at the solution of the participation equation (9). The paper's footnote 11 requires the agent's best-response condition to hold at for that duration to be available. Equations (6)–(9) and footnote 11, pp. 12–13; threshold, p. 27.
The goal is Theorem 1's pair of comparative statics. For each parameter value satisfying the patient regime and the stated regularity assumptions, let be the unique optimal feasible duration. Holding the productivity function and award scheme fixed, the uncertainty-scale target is
With uncertainty normalized to its unscaled distribution and productivity , the productivity target is
The regime is checked at both values in each comparison, since itself changes with the density or productivity. The milestone statements cover optimal effort allocation, the equilibrium effort formula, the patient case of Lemma 2, the scale identities for the expected maximum and rank incentives, and the duration expression under exponential productivity. Theorem 1, p. 14; proof, p. 27.
The result links the contest's deadline to two distinct features of the agents' work. Greater output uncertainty changes the return to effort, while a larger productivity exponent changes when effort is most effective. For a patient organizer, the paper concludes that the first change lengthens the selected contest and the second shortens it. The statements concern an actual maximizer of profit under participation, so they can inform a duration decision for a specified award scheme, rather than merely compare algebraic expressions. Discussion of Theorem 1, pp. 14–15.
The paper proves these results mathematically. This mission supplies compiled Lean declarations for the model and its main claims; their theorem proofs remain open. A completed development would give machine-checked versions of the fixed-award, patient-organizer conclusions and reusable definitions for real shock densities, scaling, order statistics, effort allocation, and constrained duration optimization. It would also make the assumptions behind the paper's comparative statics visible in one interface.
The organizer cannot choose duration by looking only at the direct effect of more time on output. Longer contests alter equilibrium effort and agent costs, which changes participation, while discounting changes the value of the best output. The organizer therefore maximizes profit over a feasible set whose boundary depends on the same effort response. Identifying the patient regime requires the threshold from the proof of Lemma 2. Under shock scaling, the expected maximum and the rank-incentive coefficient transform differently; both must be accounted for in the same optimization problem. For negative , the integral can have a finite upper bound, so the participation equation need not have a positive solution. Lemma 2, p. 13; proof of Theorem 1, p. 27.
The Lean representation uses real-valued densities and integrals, natural-number ranks , real powers on positive bases, and a positive-duration feasible domain. The standing model has , , , , , , , ordered nonnegative award shares summing to one, a continuous positive productivity function, and a mean-zero log-concave shock density. Published CrowdContest.Pooling.Density supplies the general density, CDF, and expected-maximum operations; its symmetric-shock condition is not used. Published ConvexOptimization.LogConcaveOn supplies log-concavity. The paper's stated assumptions that profit is unimodal and has a positive derivative at zero are explicit; unimodality is read as strict increase throughout or strict increase followed by strict decrease. The added condition excludes equal awards, for which the paper's cited auxiliary lemma supplies only . A positive solution to equation (9) is required; this avoids assigning meaning to a missing inverse or a nonpositive logarithm argument. The agent's best-response condition at is required, matching footnote 11 on p. 13.
An optimal duration is defined by maximization of the paper's profit (6) under the best-response condition (7) and participation (8). It is not defined to equal or the logarithmic expression: that characterization is theorem content. The effort inserted into profit is equation (5), as in the paper's reduction; a rank-probability integral states what it means for that effort to solve (7). The open development needs results about interval integrals, real powers, log-concave density moments, the change of variables under scaling, best responses, and maximization under the participation constraint. The impatient case of Lemma 2 and later award-design results are outside this mission.
Advertising pays for content that many readers receive without a direct subscription charge. An adblocker changes two parts of that arrangement: some readers see fewer ads, and the publisher may earn less from investing in content quality. Readers can benefit from the first change and lose from the second. A comparison of consumer surplus therefore has to account for the publisher's response, rather than hold quality fixed. Gritckevich, Katona, and Sarvary's Ad Blocking studies this question in a game where an adblocker can also obtain a payment from the publisher by threatening to block all ads for its users.
The paper's Proposition 3 says that the direction of the consumer-surplus comparison depends on heterogeneity in readers' sensitivity to advertising and content quality. It provides a reason why a tool that visibly removes an annoyance need not raise the total surplus of its users and other readers once the content market adjusts. The result is relevant to people assessing ad-supported publishing and adblocker policies, especially when a partial-blocking tool and its publisher payment are part of the business model.
One publisher chooses content quality at cost , where , and earns a positive price for each advertising impression. The publisher later chooses advertising volume . A unit mass of consumers differs in three independent characteristics. Their quality sensitivity is uniform on , their ad sensitivity is uniform on , and their cost of downloading an adblocker is uniform on . The paper assumes , , and that the upper download-cost bound is large enough for its equilibrium analysis. At or , the corresponding characteristic is constant.
Without an adblocker, a consumer's utility is . A consumer visits when . With an adblocker available, the adblocker commits to a maximum ad volume for downloaders. A consumer who downloads pays and, in the equilibrium studied here, sees ad volume . The resulting utility is
The consumer downloads when the middle option strictly exceeds both alternatives. This tie convention affects only boundary consumers under a nondegenerate distribution, but it fixes a precise event for the formalization.
The adblocker sets after quality is chosen. It can threaten to block all ads to its downloaders during negotiation with the publisher. In the paper's basic model, the publisher accepts an offer when indifferent, so the adblocker receives all advertising revenue generated by downloaders. The publisher's retained revenue comes from readers who do not download. The paper shows that, when is large enough, the publisher's ad choice remains the benchmark-optimal even with the adblocker. Equilibrium here means that maximizes benchmark ad revenue at each quality, maximizes the adblocker's payment at each quality, and quality maximizes the publisher's resulting profit.
The goal is Proposition 3 of the paper. Write for expected total consumer utility without an adblocker and for expected total consumer utility with one, each evaluated at equilibrium. There are positive tolerances and such that, for all sufficiently large ,
The tolerances are uniform over positive and . The point beyond which is large enough may depend on . The inequalities apply to every equilibrium selection, so the target does not assume the paper's equilibrium formulas as inputs. The milestones, in attack order, are the benchmark optimum (Lemma 1), the download rule and the adblocker's payoff (6) at fixed quality, the adblocker's optimal limit (Proposition 1), the publisher's lost revenue (9), the publisher's quality response (Proposition 2), the fixed-quality consumer-surplus identity (11), the sign criterion used to compare the two regimes, and the strict inequality that settles the case .
On the two edges of the parameter square the paper gives exact thresholds: for all large ,
with on the other side, threshold included. This is a sharper statement along the edges than the goal's "sufficiently high".
At fixed quality, downloaders can gain from seeing fewer ads, and the paper's surplus identity makes that gain positive. The equilibrium result determines when that gain outweighs the loss caused by lower publisher quality. Its low-heterogeneity region gives a precise setting in which total consumer surplus increases, while either sufficiently broad ad sensitivity or broad quality sensitivity makes the same intervention lower total consumer surplus. This is the distinction a fixed-quality comparison cannot make. The paper's separate total-welfare and extended bargaining results are not implied by this mission's goal.
A machine-checked development would connect an economic game's timing and best responses to explicit probability laws, integrals of consumer utility, and the resulting welfare comparison. The paper proves Proposition 3, but the Lean theorem and its supporting milestones are currently statements with open proofs. Completing them would also leave reusable formal components: a normalized interval law with point endpoints, a model of mixed discrete and continuous consumer types, and optimization statements for a staged publishing game. No machine-checked proof of this specific result is claimed here.
The immediate benefit to a downloader is easy to see only when the publisher's quality is held constant. That argument fails for total equilibrium consumer surplus because the adblocker captures downloader ad revenue, reducing the publisher's return to quality. The size of that quality response depends on the distribution of consumer sensitivities, while the direct benefit depends on who downloads and still consumes content. The case split at changes the benchmark ad formula; the general fixed-quality gain has no simple closed form in the paper. The endpoint cases and also require genuine point-mass distributions rather than formulas that divide by or .
Lean represents all prices, choices, utilities, and coefficients in . The three consumer characteristics have independent uniform laws, represented by iterated integrals. A point interval is represented by a Dirac law, preserving the source's and cases. Quality, ad volume, and the adblocker's limit are optimized over the nonnegative reals. Benchmark visits include a zero-utility tie; downloading requires a strict gain over both visiting without the tool and not visiting. The support bound is positive and sufficiently large wherever the paper's calculations require it.
The base game uses the paper's equilibrium convention that the publisher retains the benchmark-optimal ad volume with the adblocker present. Negotiation is represented in reduced form: the adblocker receives the entire ad revenue from downloaders, and the publisher keeps revenue from other visitors. Positivity of the ad price and quality-cost coefficient, implicit in the economic setup, is explicit in Lean. The source's phrase “ high enough” in Proposition 3 is read as “ high enough,” since is an individual's cost and sets its population range. A corrected normalization factor in the printed first branch of is recorded in the definition and moderation notes. Closed-form milestones such as (6) and (9) carry an explicit lower bound on , namely the upper limit of the paper's -integral. The paper's weak inequality is stated strictly, which is true on and is what the goal needs.
The goal uses expected utility and best-response conditions, not values manufactured from the closed-form formulas. A proof therefore must establish that the modeled equilibria exist and satisfy the paper's formulas; otherwise a universal comparison over an empty set of equilibria would have no economic content. Contributions that prove the interval-law facts, measurable and integrable consumer events, benchmark and adblocker best responses, or the sign criterion all advance the same target.
Research funders and investors choose how many innovators to support and how much to give each one. The allocation affects an innovator's chance of success, but it also changes the competition that successful innovators face. Gao, Fan, Huang and Chen study this interaction in a two-stage model: a principal allocates an essential resource, then two agents choose costly innovation efforts. Their main result identifies when the principal supports nobody, one agent, or both agents equally. The source is the February 2021 SSRN preprint, especially §3 and Theorem 1 on p. 15. The paper presents a known result; the mission asks for a machine-checked account of its mathematical statement.
The principal has resource capacity and selects an allocation with and . An agent receiving chooses effort at cost . The agent succeeds with probability ; the two innovation outcomes are independent. An unfunded agent has zero chance of success at every effort and optimally chooses zero effort. These are the primitives of §3.1, pp. 6–7, and equation (1) of the preprint.
A successful product earns if the other innovation fails. If both innovations succeed, each product earns . The profit-sharing rate gives the successful agent the fraction of its own product's profit; the principal receives the rest. Agent 's expected payoff, as a function of both efforts, is . The agents choose efforts simultaneously. An effort equilibrium means both efforts are nonnegative and each is a best response among all nonnegative efforts to the other's choice.
The principal's expected profit at an allocation and its equilibrium efforts is
The two-product term counts both successful products, while the other terms count outcomes with exactly one success. Equation (7), p. 11, asks the principal to maximize this profit over feasible resource allocations and the agents' equilibrium behavior. Here denotes the amount invested in a comparison strategy; remains the available capacity. The paper distinguishes them in §3.3 even where a text extraction loses the overbar.
The goal is Theorem 1, p. 15. Put and . Where and , define
The claimed allocation is when ; it is when . For , it is when . When , the theorem selects an equal split for , and the one-agent allocation otherwise. When , the equal split becomes optimal at and above the lower threshold; below that threshold the one-agent allocation is optimal. At the threshold is , the continuous value of the printed expression.
The theorem names an optimal allocation in each region; symmetrically exchanging the agents gives another named form. At a boundary where the two strategies tie, either can be optimal. The six milestones cover the single-agent effort and profit formulas, the equal-split failure rate and profit, the endpoint reduction for a fixed total investment, and the two profit comparisons that locate the competition threshold and the middle band. All indices and formulas come from pp. 9–15 and 39 of the preprint.
The theorem translates the interaction between resource scarcity and product-market competition into an explicit allocation rule. Its middle regime has a bounded interval of resource abundance in which supporting both innovators is best. Past the upper end, supporting one can again be better even though additional resources raise each agent's potential success. This matters whenever an allocation changes both innovation incentives and the rewards available after success; the paper discusses venture investment and grant allocation as examples in §1 and §3.3 of the preprint.
The published paper supplies the mathematical result. A complete Lean development would additionally establish that its equilibrium model, profit comparisons, and boundary cases imply the region theorem under explicit standing assumptions. The goal and milestones here are open statements with compiled Lean syntax; they do not yet have machine-checked proofs. The mission reuses a published generic two-player Nash predicate, while its paper-specific effort-game definitions could support formalizations of related allocation games.
More resources make success easier at a fixed effort, yet an allocation also changes each agent's effort incentive through the other agent's chance of entering the product market. Consequently, increasing an individual resource share cannot by itself rank the principal's profits across allocations. The equal-split profit can even decrease as total investment grows when ; Lemma 3 (i), p. 14, identifies its peak. A comparison of only the one-agent and equal-split formulas would leave every asymmetric split unchecked. The principal's optimization therefore needs a statement that covers all feasible splits and all their effort equilibria. The paper's Proposition 1 addresses the fixed-total allocation question, while its later comparisons determine which endpoint wins.
Lean uses real-valued resources and efforts, Real.exp for the success function, and nonnegative real action subtypes for the reused two-player pure Nash predicate. The bounds , and are explicit. The goal's IsOptimal predicate requires a feasible named allocation, at least one equilibrium there, and profit dominance for every equilibrium of it over every equilibrium of every feasible allocation. This requirement prevents a missing equilibrium from making the claim vacuous. The principal's profit is defined from innovation probabilities, not from the closed-form one-agent and equal-split answers.
Effort is the model's primitive so the allocations and retain their intended meaning; a failure-rate substitution would divide by zero there. Closed forms involving Real.log, Real.sqrt or division appear only in the source's parameter regimes where their arguments and denominators are valid. At an equal split may have many equilibria; the formula milestone asserts existence there and states uniqueness only for . The paper's Proposition 1 says an optimum “must” have endpoint form, but zero-profit cases allow other optima. Its milestone states the endpoint-domination conclusion supplied by its proof. Theorem 1's region-c threshold is corrected to at , where the printed fraction is .
The definitions and six milestones provide targets for equilibrium existence, payoff analysis, comparisons across asymmetric allocations, and the exact threshold algebra. Further contributions can develop those proofs and reusable results on best responses of real-action games. The paper's endogenous profit-sharing and other §4 extensions use different optimization problems and are outside this mission.
We investigate the possibility of dividing quantum channels into concatenations of other channels, thereby studying the semigroup structure of the set of completely-positive trace-preserving maps. We show the existence of 'indivisible' channels which can not be written as non-trivial products of other channels and study the set of 'infinitesimal divisible' channels which are elements of continuous completely positive evolutions. For qubit channels we obtain a complete characterization of the sets of indivisible and infinitesimal divisible channels. Moreover, we identify those channels which are solutions of time-dependent master equations for both positive and completely positive evolutions. For arbitrary finite dimension we prove a representation theorem for elements of continuous completely positive evolutions based on new results on determinants of quantum channels and Markovian approximations.
This mission is the statement-level formalization of Dividing Quantum Channels (arXiv:math-ph/0611057v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
23 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 16 (Structure of infinitesimal divisible channels) (Theorem 16 (Structure of infinitesimal divisible channels), PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
This paper establishes several converse bounds on the private transmission capabilities of a quantum channel. The main conceptual development builds firmly on the notion of a private state, which is a powerful, uniquely quantum method for simplifying the tripartite picture of privacy involving local operations and public classical communication to a bipartite picture of quantum privacy involving local operations and classical communication. This approach has previously led to some of the strongest upper bounds on secret key rates, including the squashed entanglement and the relative entropy of entanglement. Here we use this approach along with a "privacy test" to establish a general meta-converse bound for private communication, which has a number of applications. The meta-converse allows for proving that any quantum channel's relative entropy of entanglement is a strong converse rate for private communication. For covariant channels, the meta-converse also leads to second-order expansions of relative entropy of entanglement bounds for private communication rates. For such channels, the bounds also apply to the private communication setting in which the sender and receiver are assisted by unlimited public classical communication, and as such, they are relevant for establishing various converse bounds for quantum key distribution protocols conducted over these channels. We find precise characterizations for several channels of interest and apply the methods to establish several converse bounds on the private transmission capabilities of all phase-insensitive bosonic channels.
This mission is the statement-level formalization of Converse bounds for private communication over quantum channels (arXiv:1602.08898v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Covariant channels admit a fixed Choi-state teleportation simulation (Proposition 2, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
25 results of the paper are not stated yet, because the library lacks an interface they need:
In Shannon information theory the capacity of a memoryless communication channel cannot be increased by the use of feedback from receiver to sender. In this paper the use of classical feedback is shown to provide no increase in the unassisted classical capacity of a memoryless quantum channel when feedback is used across non-entangled input states, or when the channel is an entanglement--breaking channel. This gives a generalization of the Shannon theory for certain classes of feedback protocols when transmitting through noisy quantum communication channels.
This mission is the statement-level formalization of On Feedback and the Classical Capacity of a Noisy Quantum Channel (arXiv:quant-ph/0305176v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is No capacity gain across separable feedback cuts (III.B, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Stinespring's dilation theorem is the basic structure theorem for quantum channels: it states that any quantum channel arises from a unitary evolution on a larger system. Here we prove a continuity theorem for Stinespring's dilation: if two quantum channels are close in cb-norm, then it is always possible to find unitary implementations which are close in operator norm, with dimension-independent bounds. This result generalizes Uhlmann's theorem from states to channels and allows to derive a formulation of the information-disturbance tradeoff in terms of quantum channels, as well as a continuity estimate for the no-broadcasting theorem. We briefly discuss further implications for quantum cryptography, thermalization processes, and the black hole information loss puzzle.
This mission is the statement-level formalization of The Information-Disturbance Tradeoff and the Continuity of Stinespring's Representation (arXiv:quant-ph/0605009v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Continuity with freely chosen common Stinespring dilations (§I, Eq. (1), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
We introduce various measures of forward classical communication for bipartite quantum channels. Since a point-to-point channel is a special case of a bipartite channel, the measures reduce to measures of classical communication for point-to-point channels. As it turns out, these reduced measures have been reported in prior work of Wang et al. on bounding the classical capacity of a quantum channel. As applications, we show that the measures are upper bounds on the forward classical capacity of a bipartite channel. The reduced measures are upper bounds on the classical capacity of a point-to-point quantum channel assisted by a classical feedback channel. Some of the various measures can be computed by semi-definite programming.
This mission is the statement-level formalization of Bounding the forward classical capacity of bipartite quantum channels (arXiv:2010.01058v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
42 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 21 (main paper result selected by page-1 seed) (Theorem 21 (main paper result selected by page-1 seed), PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
An investor may care about reaching a target, avoiding a loss, or crossing an aspiration level rather than maximizing a concave function of final wealth. A target reward can jump from zero to one at a specified wealth. Such nonconcave utility is a natural model for goal-reaching portfolios, but its discontinuity changes what the associated Hamilton–Jacobi–Bellman equation can say at maturity. Portfolio bounds make the distinction sharper: an investor with finite leverage and short-sale limits cannot instantaneously smooth a jump in the payoff. Dai, Kou, Qian and Wan analyze this combination of nonconcavity, portfolio constraints, and a liquidation floor in their 2022 paper.
The paper proves a comparison principle and identifies the control value as the unique viscosity solution under a special terminal asymptotic condition. These are known mathematical results; this mission asks for their Lean proofs. The source is the authors' accepted manuscript, whose main theorem is Theorem 4.2 on printed page 12. The e-companion supplies boundary and terminal results supporting that theorem.
The market contains one risky stock and one riskless bond. After the paper's forward-wealth normalization, wealth started from follows
Here is the excess stock return, is volatility, is Brownian motion, and is the fraction of wealth invested in the stock. Portfolio weights satisfy , with ; either endpoint may be infinite. Wealth remains above the liquidation floor . For utility , the value function is
Assumption 3.1 permits utility to be nondecreasing and right-continuous without being concave or continuous. For some , it eventually satisfies . At it either has a finite value or, when , has the paper's CRRA form near zero. The second case includes logarithmic utility. These alternatives lead to different liquidation boundary conditions.
The formalized Hamiltonian is
and the HJB equation is for and . Definition A.1 tests upper and lower semicontinuous envelopes of candidate solutions against smooth functions and uses the corresponding envelopes and . It also imposes the liquidation boundary condition and a terminal asymptotic condition. For bounded portfolio weights the terminal condition retains the jump of through the normal distribution function and . For unbounded weights its target is the concave envelope .
The goal is Theorem 4.2: for both bounded and unbounded portfolio intervals, the control value satisfies Definition A.1 and is continuous on . In the growth class used by Theorem 4.1, every other viscosity solution agrees with it:
The goal keeps the actual stochastic-control supremum as and quantifies over competing solutions . It does not select a particular numerical method or a preferred proof. Theorem 4.1 gives comparison in this class. Proposition EC.3.2 gives the liquidation boundary behavior. Proposition EC.3.3 gives two terminal regimes, and Lemma EC.3.3 supplies the power-majorant statement used in the unbounded regime. The milestone list follows these stated results, specialized to the one-stock constant-coefficient model of the main theorem.
The characterization connects a portfolio optimization problem to an HJB equation even when the terminal utility jumps. It specifies the terminal behavior that distinguishes the bounded and unbounded portfolio regimes. In the bounded case a discontinuity can persist in the approach to maturity; in the unbounded case the limiting target is the concave envelope. The comparison statement then makes the characterization unique within the stated growth class. These conclusions are the analytical basis for the paper's later discussion of numerical schemes, although the numerical convergence theorem is outside this mission's scope (Dai et al., 2022, §§4 and EC.3).
A complete formalization would produce reusable definitions of the constrained control value, the extended-real Hamiltonian and its envelopes, and terminal limits for discontinuous payoffs. The paper's results are proved on paper but have no machine-checked proof in this proposal. The declarations here are compiled statements awaiting proofs. Independent work on the comparison theorem, boundary behavior, terminal asymptotics, and supporting real analysis can proceed against the same definition layer.
The usual terminal condition does not describe the limit of as approaches when jumps. Replacing the limit by would erase the singular behavior that the paper studies. The bounded-portfolio condition instead depends on the left limit , the size of the jump, and the scaled quantity . A viscosity comparison argument must handle this terminal profile while the Hamiltonian itself can be infinite or discontinuous in the unbounded portfolio regime. The liquidation boundary has a separate CRRA asymptotic when utility diverges at zero. Each of these clauses is part of the solution concept and must remain compatible with the value function.
The Lean market stores as real numbers and as extended real endpoints. It assumes , , , , and at least one nonzero admissible weight. The last three inequalities include the paper's standing bounds and exclude . Admissible controls are progressively measurable, obey the bounds and liquidation floor, satisfy the integral wealth equation through a Brownian Itô integral, and have integrable terminal utility. The supremum of their expectations is extended real so an infinite value is preserved; the goal explicitly proves finiteness before converting it to a real value. Brownian motions are quantified over filtered probability spaces and have independent future increments relative to their filtration.
The PDE domain is . Semicontinuous envelopes and boundary and terminal limits approach within . Smooth tests are real functions. The Hamiltonian and its envelopes are extended real; finite-width expressions involving are used only under bounded portfolio endpoints. The terminal point is included only for the finite-utility boundary branch, where the source defines . The CRRA formula uses a logarithmic branch at zero power, avoiding division by zero. These commitments rule out a vacuous solution notion or a value function defined as an arbitrary viscosity solution. Proving the control value finite, nontrivial comparison, and both terminal limits remains part of the mission. The e-companion's multivariate statements are included only in the one-stock constant-coefficient specialization used by Theorems 4.1–4.2.
We show that the new quantum extension of Renyi's \alpha-relative entropies, introduced recently by Muller-Lennert, Dupuis, Szehr, Fehr and Tomamichel, J. Math. Phys. 54, 122203, (2013), and Wilde, Winter, Yang, Commun. Math. Phys. 331, (2014), have an operational interpretation in the strong converse problem of quantum hypothesis testing. Together with related results for the direct part of quantum hypothesis testing, known as the quantum Hoeffding bound, our result suggests that the operationally relevant definition of the quantum Renyi relative entropies depends on the parameter \alpha: for \alpha<1, the right choice seems to be the traditional definition, whereas for \alpha>1 the right choice is the newly introduced version. As a sideresult, we show that the new Renyi \alpha-relative entropies are asymptotically attainable by measurements for \alpha>1, and give a new simple proof for their monotonicity under completely positive trace-preserving maps.
This mission is the statement-level formalization of Quantum hypothesis testing and the operational interpretation of the quantum Renyi relative entropies (arXiv:1309.3228v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
35 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact strong converse exponent in quantum hypothesis testing (Theorem IV.10, PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
4 results of the paper are not stated yet, because the library lacks an interface they need:
In this note we study in a finite dimensional Lie algebra the set of all those elements x for which the closed convex hull of the adjoint orbit contains no affine lines; this contains in particular elements whose adjoint orbits generates a pointed convex cone~. Assuming that is admissible, i.e., contains a generating invariant convex subset not containing affine lines, we obtain a natural characterization of such elements, also for non-reductive Lie algebras. Motivated by the concept of standard (Borchers) pairs in QFT, we also study pairs of Lie algebra elements satisfying for which pointed. Given , we show that such elements can be constructed in such a way that defines a -grading, and characterize the cases where we even get a -grading.
This mission is the statement-level formalization of Elements in pointed invariant cones in Lie algebras and corresponding affine pairs (arXiv:2110.07297v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
33 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.20: Characterization Theorem (Theorem 3.20: Characterization Theorem, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
14 results of the paper are not stated yet, because the library lacks an interface they need:
We study the loss of entanglement of bipartite state subjected to discarding or measurement of one qubit. Examining the behavior of different entanglement measures, we find that entanglement of formation, entanglement cost, and logarithmic negativity are lockable measures in that it can decrease arbitrarily after measuring one qubit. We prove that any convex and asymptotically non-continuous measure is lockable. As a consequence, all the convex roof measures can be locked. Relative entropy of entanglement is shown to be a non-lockable measure.
This mission is the statement-level formalization of Locking entanglement measures with a single qubit (arXiv:quant-ph/0404096v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is One-qubit locking of formation, operational cost, and logarithmic negativity (Eqs. (1)–(3), continuation on p.2, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Assume that two distant parties, Alice and Bob, as well as an adversary, Eve, have access to (quantum) systems prepared jointly according to a tripartite state. In addition, Alice and Bob can use local operations and authenticated public classical communication. Their goal is to establish a key which is unknown to Eve. We initiate the study of this scenario as a unification of two standard scenarios: (i) key distillation (agreement) from classical correlations and (ii) key distillation from pure tripartite quantum states. Firstly, we obtain generalisations of fundamental results related to scenarios (i) and (ii), including upper bounds on the key rate. Moreover, based on an embedding of classical distributions into quantum states, we are able to find new connections between protocols and quantities in the standard scenarios (i) and (ii). Secondly, we study specific properties of key distillation protocols. In particular, we show that every protocol that makes use of pre-shared key can be transformed into an equally efficient protocol which needs no pre-shared key. This result is of practical significance as it applies to quantum key distribution (QKD) protocols, but it also implies that the key rate cannot be locked with information on Eve's side. Finally, we exhibit an arbitrarily large separation between the key rate in the standard setting where Eve is equipped with quantum memory and the key rate in a setting where Eve is only given classical memory. This shows that assumptions on the nature of Eve's memory are important in order to determine the correct security threshold in QKD.
This mission is the statement-level formalization of Unifying classical and quantum key distillation (arXiv:quant-ph/0608199v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Pure-state intrinsic information equals twice marginal squashed entanglement (pure-intrinsic-squashed, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
21 results of the paper are not stated yet, because the library lacks an interface they need:
We provide a complete picture of contractivity of trace preserving positive maps with respect to -norms. We show that for contractivity holds in general if and only if the map is unital. When the domain is restricted to the traceless subspace of Hermitian matrices, then contractivity is shown to hold in the case of qubits for arbitrary and in the case of qutrits if and only if . In all non-contractive cases best possible bounds on the -norms are derived.
This mission is the statement-level formalization of Contractivity of positive and trace preserving maps under Lₚ norms (arXiv:math-ph/0601063v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Sharp general Schatten-norm bound and trace-map attainment (Theorem II.1 and following attainment clause, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
The entanglement cost of a quantum channel is the minimal rate at which entanglement (between sender and receiver) is needed in order to simulate many copies of a quantum channel in the presence of free classical communication. In this paper we show how to express this quantity as a regularised optimisation of the entanglement formation over states that can be generated between sender and receiver. Our formula is the channel analog of a well-known formula for the entanglement cost of quantum states in terms of the entanglement of formation; and shares a similar relation to the recently shattered hope for additivity. The entanglement cost of a quantum channel can be seen as the analog of the quantum reverse Shannon theorem in the case where free classical communication is allowed. The techniques used in the proof of our result are then also inspired by a recent proof of the quantum reverse Shannon theorem and feature the one-shot formalism for quantum information theory, the post-selection technique for quantum channels as well as Sion's minimax theorem. We discuss two applications of our result. First, we are able to link the security in the noisy-storage model to a problem of sending quantum rather than classical information through the adversary's storage device. This not only improves the range of parameters where security can be shown, but also allows us to prove security for storage devices for which no results were known before. Second, our result has consequences for the study of the strong converse quantum capacity. Here, we show that any coding scheme that sends quantum information through a quantum channel at a rate larger than the entanglement cost of the channel has an exponentially small fidelity.
This mission is the statement-level formalization of Entanglement Cost of Quantum Channels (arXiv:1108.5357v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Operational channel entanglement cost equals regularized maximum formation (Theorem 12 (Eq.22; paper-result seed), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
11 results of the paper are not stated yet, because the library lacks an interface they need:
We investigate the classical communication over quantum channels when assisted by no-signaling (NS) and positive-partial-transpose-preserving (PPT) codes, for which both the optimal success probability of a given transmission rate and the one-shot -error capacity are formalized as semidefinite programs (SDPs). Based on this, we obtain improved SDP finite blocklength converse bounds of general quantum channels for entanglement-assisted codes and unassisted codes. Furthermore, we derive two SDP strong converse bounds for the classical capacity of general quantum channels: for any code with a rate exceeding either of the two bounds of the channel, the success probability vanishes exponentially fast as the number of channel uses increases. In particular, applying our efficiently computable bounds, we derive an improved upper bound on the classical capacity of the amplitude damping channel. We also establish the strong converse property for the classical and private capacities of a new class of quantum channels. We finally study the zero-error setting and provide efficiently computable upper bounds on the one-shot zero-error capacity of a general quantum channel.
This mission is the statement-level formalization of Semidefinite programming strong converse bounds for classical capacity (arXiv:1610.06381v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 11: β strong converse bound (original seed pinned from abstract) (Theorem 11, PDF p. 16). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Entanglement distillation, an essential quantum information processing task, refers to the conversion from multiple copies of noisy entangled states to a smaller number of highly entangled states. In this work, we study the non-asymptotic fundamental limits for entanglement distillation. We investigate the optimal tradeoff between the distillation rate, the number of prepared states, and the error tolerance. First, we derive the one-shot distillable entanglement under completely positive partial transpose preserving operations as a semidefinite program and demonstrate an exact characterization via the quantum hypothesis testing relative entropy. Second, we establish efficiently computable second-order estimations of the distillation rate for general quantum states. In particular, we provide explicit as well as approximate evaluations for various quantum states of practical interest, including pure states, mixture of Bell states, maximally correlated states and isotropic states.
This mission is the statement-level formalization of Non-asymptotic entanglement distillation (arXiv:1706.06221v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact Hermitian hypothesis-testing characterization (Seed abstract main result pinned to Theorem 4, Eq. (25): exact hypothesis-testing characterization, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum amplifier channels are at the core of several physical processes. Not only do they model the optical process of spontaneous parametric down-conversion, but the transformation corresponding to an amplifier channel also describes the physics of the dynamical Casimir effect in superconducting circuits, the Unruh effect, and Hawking radiation. Here we study the communication capabilities of quantum amplifier channels. Invoking a recently established minimum output-entropy theorem for single-mode phase-insensitive Gaussian channels, we determine capacities of quantum-limited amplifier channels in three different scenarios. First, we establish the capacities of quantum-limited amplifier channels for one of the most general communication tasks, characterized by the trade-off between classical communication, quantum communication, and entanglement generation or consumption. Second, we establish capacities of quantum-limited amplifier channels for the trade-off between public classical communication, private classical communication, and secret key generation. Third, we determine the capacity region for a broadcast channel induced by the quantum-limited amplifier channel, and we also show that a fully quantum strategy outperforms those achieved by classical coherent detection strategies. In all three scenarios, we find that the capacities significantly outperform communication rates achieved with a naive time-sharing strategy.
This mission is the statement-level formalization of Capacities of Quantum Amplifier Channels (arXiv:1605.04922v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Equation (66), Appendix B (B9)–(B10): coherent-detection capacity regions (Equation (66), Appendix B (B9)–(B10): coherent-detection capacity regions, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
10 results of the paper are not stated yet, because the library lacks an interface they need:
Expressions of several capacity regions in quantum information theory involve an optimization over auxiliary quantum registers. Evaluating such expressions requires bounds on the dimension of the Hilbert space of these auxiliary registers, for which no non-trivial technique is known; we lack a quantum analog of the Carath'{e}odory theorem. In this paper, we develop a new non-Carath'{e}odory-type tool for evaluating expressions involving a single quantum auxiliary register and several classical random variables. As we show, such expressions appear in problems of entanglement-assisted Gray-Wyner and entanglement-assisted channel simulation, where the question of whether entanglement helps in these settings is related to that of evaluating expressions with a single quantum auxiliary register. To evaluate such expressions, we argue that developing a quantum analog of the Carath'{e}odory theorem requires a better understanding of a notion which we call ``quantum conditioning." We then proceed by proving a few results about quantum conditioning, one of which is that quantum conditioning is strictly richer than the usual classical conditioning.
This mission is the statement-level formalization of On Dimension Bounds for Auxiliary Quantum Systems (arXiv:1207.3911v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3(b): quantum conditioning is strictly richer than classical conditioning (Theorem 3(b): quantum conditioning is strictly richer than classical conditioning, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
A formula for the capacity of a quantum channel for transmitting private classical information is derived. This is shown to be equal to the capacity of the channel for generating a secret key, and neither capacity is enhanced by forward public classical communication. Motivated by the work of Schumacher and Westmoreland on quantum privacy and quantum coherence, parallels between private classical information and quantum information are exploited to obtain an expression for the capacity of a quantum channel for generating pure bipartite entanglement. The latter implies a new proof of the quantum channel coding theorem and a simple proof of the converse. The coherent information plays a role in all of the above mentioned capacities.
This mission is the statement-level formalization of The private classical capacity and quantum capacity of a quantum channel (arXiv:quant-ph/0304127v6). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Regularized private and key capacities of a cq wiretap channel (Theorem 1 / (6), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Consider an open quantum system with (discrete-time) Markovian dynamics. Our task is to store information in the system in such a way that it can be retrieved perfectly, even after the system is left to evolve for an arbitrarily long time. We show that this is impossible for classical (resp. quantum) information precisely when the dynamics is mixing (resp. asymptotically entanglement breaking). Furthermore, we provide tight universal upper bounds on the minimum time after which any such dynamics 'scrambles' the encoded information beyond the point of perfect retrieval. On the other hand, for dynamics that are not of this kind, we show that information must be encoded inside the peripheral space associated with the dynamics in order for it to be perfectly recoverable at any time in the future. This allows us to derive explicit formulas for the maximum amount of information that can be protected from noise in terms of the structure of the peripheral space of the dynamics.
This mission is the statement-level formalization of Zero-error communication under discrete-time Markovian dynamics (arXiv:2402.18703v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
37 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Eventual scrambling characterizes mixing and asymptotic entanglement breaking (Theorem 1.1, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need: