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?
Product development is often organized as a search over prototypes: several candidate designs exist, each must be built or tested at a cost before its quality is known, and the firm wants to end up launching the best one without spending too much on testing. When each test reveals the true quality of a prototype, this is Pandora's box problem, solved by Weitzman (Weitzman 1979): attach to every box an index, its reservation price, open boxes in decreasing order of the index, and stop as soon as the best value found exceeds every remaining index.
In practice, tests are rarely perfect. Simulations, virtual prototypes, consumer panels and outsourced test platforms return a noisy measurement of a prototype's value, not the value itself. Bhaskaran and Erat (Bhaskaran and Erat 2025) ask what the optimal sequential testing policy is when each evaluation only yields a signal correlated with the true value. Extensions of Weitzman's model are known to be fragile: with learning across alternatives (Erat and Kavadias 2008) or with the option to select an alternative without inspecting it (Doval 2018), index policies stop being optimal. Theorem 1 of the paper shows that measurement noise is not such a perturbation: an index policy remains optimal once the indices are computed from the right distributions.
There are prototypes, . Prototype has a true value and, when evaluated, yields a measurement . The pair has a joint density on with , and different prototypes are independent. Evaluating prototype costs , paid once.
The firm sees only measurements. It evaluates prototypes one at a time, in any order and adaptively; it may stop at any time, including before any evaluation. On stopping it launches one of the evaluated prototypes, receiving its true value, or launches nothing and receives the outside option . Its net payoff is the value received minus the evaluation costs paid, and a policy is judged by its expected net payoff.
The paper's objects are:
the expected true value of prototype given the measurement ;
In the Lean development these are Model, Policy, run, netPayoff, Admissible, value, Q, g, V, B and fidelityPolicy in the namespace NoisyPrototyping.ReservationPolicy.
The fidelity-adjusted reservation price policy evaluates the prototypes in the order and, after the -th evaluation (), stops and accepts if (always at ), and otherwise evaluates prototype . The goal states that is admissible and that, for every admissible adaptive policy ,
Theorem 1 says that the qualitative structure of Weitzman's solution survives imperfect evaluation. The evaluation order is fixed in advance, by indices that depend only on each prototype's cost and on the joint law of its value and measurement; the stopping rule is a threshold rule applied to a monotone transform of the measurements. Everything the paper does afterwards rests on it: the Gaussian closed form of Theorem 2, the comparative statics of Propositions 1–3 in the fidelity of the test, the choice of fidelity in Propositions 4–6, and the pricing of an outside test platform in Propositions 7–8.
The result is proved on paper by reduction to Weitzman's theorem. Weitzman's theorem itself is neither proved nor posed on the platform (searched October 2026), so the formalization produces two things: a formal proof of optimality of Pandora's rule, in the version with recall, any order, free stopping and an outside option; and a formal account of the reduction from noisy to perfect evaluation, which the paper presents as two short claims.
The natural first idea is to declare that "the firm only cares about " and apply Weitzman directly. Two steps of that argument need work. First, the policies of the noisy problem see the measurements , which may carry more information than when is not injective, so the class of policies in is richer than in ; showing that this extra information is useless requires the independence of prototypes and a conditioning argument for adaptive, history-dependent stopping. Second, the replacement of by in the payoff must be justified for an adaptive launching decision, not for a fixed prototype. Weitzman's theorem itself is not in Mathlib, and its optimality claim ranges over every adaptive policy, so it cannot be checked by comparing finitely many candidate rules.
Prototypes are indexed by Fin N from ; the paper's reordering is a bijection σ : Fin N ≃ Fin N along which the prices are non-increasing (ties in any order), and the paper's is R (σ n). The law of is a probability measure on ; the outcome of all prototypes has the product law, which encodes independence. The goal and Claims 1–2 assume this law has a measurable density . A history records evaluated prototypes and their measurements only; a policy maps histories to evaluate , launch or stop with nothing; each prototype is evaluated at most once, and illegal decisions end the run with nothing. A policy is admissible when the evaluation order and the final decision are measurable events and the net payoff is integrable; values are Bochner integrals of the net payoff.
Disclosed readings: independence across prototypes; ; ; formula (1) with in the denominator (the page prints , which would not give a conditional expectation); as the law of (formula (2) as printed lacks a Jacobian factor). The proof's simplifying assumption that is increasing onto is not made.
The statement admits trivializing encodings, and they are excluded: policies cannot see true values (that would make the problem full-information, where is not optimal); is the explicit formula (1), not a conditional expectation by definition; enters as the hypothesis that it is the least root, never through a choice function; and competitors are compared only when admissible, while the admissibility of is part of the conclusion.
A complete development needs: the conditional expectation of a coordinate under a joint density; conditioning arguments for adaptive policies on a product space; and Weitzman's theorem. The last two are reusable beyond this mission, for any search or bandit model with independent alternatives. Proofs of the milestones in any order are welcome, and a proof of the Weitzman milestone is the most reusable contribution.
Products with positive network effects (messaging apps, online games, social platforms) are known to support higher profits: a buyer's utility grows with the number of other buyers, and a seller can monetize that complementarity (Katz and Shapiro 1986; Candogan, Bimpikis and Ozdaglar 2012). Ajorlou and Jadbabaie ask whether a seller of a product without such an effect can create one artificially, by announcing a sales-based rebate: every buyer pays the market price and later receives a reward that depends on the realized sales volume (arXiv:1902.09646v4, Management Science, 2023).
Because consumers are uncertain about a common quality component and about each other's valuations, the purchase decision becomes a global game with correlated private valuations, in the sense of Carlsson and van Damme (1993) and Morris and Shin (1998). A natural first guess is that a rebate increasing in sales volume, which imitates a positive network effect, should help the seller. The paper's Theorem 2 says the opposite: when the price is already optimal, no increasing sales-based reward program is profitable. This mission formalizes that result and the identities on which it rests.
A firm sells one product at a market price to a unit mass of consumers. Consumer values the product at , where the common quality has the Gaussian prior and the taste is idiosyncratic. Write
A consumer who observes holds the posterior . Valuations are ex ante , with density , where and are the standard normal density and distribution function.
If consumers buy exactly when (a threshold strategy with cutoff ), the sales volume at quality is . A reward program is a function of the sales volume; at cutoff it induces the reward as a function of the quality. The cutoff is an equilibrium for when
The firm's expected profit is
With no reward the cutoff is and the profit is . Assumption 1 says that maximizes the no-reward profit . A reward program is profitable at an equilibrium cutoff if (2) strictly exceeds the no-reward profit at .
Under Assumption 1, for every weakly increasing reward program and every equilibrium cutoff of (1) for ,
The result. Theorem 2 separates two effects that are easy to conflate: an inherent network effect raises profit, but an induced one, paid for through a rebate increasing in sales, lowers the expected net price exactly at high valuations and so cannot beat the optimal plain price. It is the negative half of the paper's design question; the positive half (optimal programs are decreasing in sales volume, "full refund or nothing", §III–§IV) is built on the same representation (9) of the profit by valuations, which is a milestone here. Lemma 1 is the paper's general criterion for when any reward program beats the equivalent plain price, and applies beyond monotone programs.
Formalizing it. The results are proved in the paper (body p. 16, appendix p. 29); no machine-checked version is known. The formal work consists of the Gaussian conditioning identity behind (9), the Gaussian integral of on p. 7, the shift argument for Lemma 5, and the assembly into Theorem 2 with every hypothesis made explicit. The model layer (Gaussian prior, posterior, threshold equilibria) is reusable for the paper's other results and for related global-game pricing models.
The paper treats (9) as a change of conditioning, but it is where the posterior formula of p. 9 must be shown to be the actual conditional law of the quality given a valuation, inside an integral restricted to valuations above the cutoff: the profit (2) integrates over qualities, the right side of (9) over valuations, and connecting them requires Fubini over the joint Gaussian law of together with the factorization of the joint density into times the posterior density. The strict part of Lemma 5 needs more than "a shift of an increasing function is larger": the increase must happen on a set of positive Gaussian measure, which uses that a monotone non-constant function differs between two shifted Gaussian laws. Theorem 2 also uses that the equilibrium cutoff lies in , which is where the bound and Assumption 1 interact.
The model is a structure with fields and a validity predicate , , which every statement assumes (implicit on the page). Laws are Mathlib's gaussianReal, with variances passed through Real.toNNReal; expectations are Bochner integrals of bounded measurable integrands. and are the published BlackScholesModel.stdNormalCDF and stdNormalPDF. The reward program is a function ℝ → ℝ constrained to on , "increasing" means weakly increasing on , and is defined from and the same cutoff used in (1) and (2). In milestones 2–5 the reward is a general measurable function with values in , the paper's . Lemma 5 is posed on with " non-constant": non-constancy of on does not survive composition with , whose range is . Assumption 1 enters only through its maximization clause over prices ; its first-order characterization is not posed. Integrals are over the open half-line.
Three formalizations would trivialize or alter the goal and are excluded: restricting to strictly increasing programs (which drops constant rebates), decoupling from the equilibrium cutoff, and comparing the profit with the price- profit instead of the no-reward profit at the market price .
Contributions welcome: proofs of the milestones in any order, in particular the Gaussian identities (milestones 1 and 2), which are of independent use for Gaussian signal models, and general lemmas on Gaussian shifts of monotone functions.
Forecasting competitions ask many forecasters to report probabilities for many future binary events and award a single prize to one of them. They are used to identify and reward accurate forecasters: the Good Judgment Project gave "superforecaster" status to the top 2% by quadratic score, and data-science platforms run similar leaderboards. The usual rule ranks forecasters by the average of a proper scoring rule and pays the top scorer. A proper scoring rule makes truthful reporting optimal for a forecaster paid in proportion to their score, but a winner-take-all prize changes the incentives: a forecaster who is behind gains by reporting more extreme probabilities, because the competition rewards variance as well as accuracy.
Witkowski, Freeman, Wortman Vaughan, Pennock and Krause (arXiv:2101.01816; Management Science, 2023) design single-prize mechanisms that are strictly incentive compatible (truthful reporting is the unique optimum, whatever the forecaster believes about the others) and that select the most accurate forecaster. Their first mechanism, ELF, borrows a lottery from the competitive scoring rule of Kilgour and Gerchak (2004) and is truthful for arbitrarily correlated events, but it cannot select the best forecaster with probability above . Their second mechanism, I-ELF, is the subject of this mission: it is both truthful under a natural independence assumption and accurate as the number of events grows. The paper also proves that no deterministic mechanism is strictly incentive compatible and that no mechanism can be accurate in the limit for every joint law of the events, so both restrictions in the main theorem are needed.
There are forecasters and events with outcomes . Forecaster holds beliefs and reports . A scoring rule scores a report against an outcome ; it is strictly proper if whenever , and we write when its values lie in .
The ELF lottery on one event gives forecaster the winning probability
The Independent-Event Lotteries mechanism runs one ELF lottery per event, producing an event winner with , and then selects the forecaster who won the most events, breaking ties uniformly at random. The mechanism requires when and (values strictly below on reports in ) when .
Accuracy is measured by the expected score under a joint law of the outcomes. A joint law of the outcomes and the other forecasters' reports is belief independent if the per-event pairs are independent across ; within an event, reports and outcome may be correlated arbitrarily.
For strictly proper and measurable in the report:
The goal fixes no constants: it asserts the shape of the guarantee, not the rate.
Theorem 6 rests on Theorem 2 (single-event ELF is strictly incentive compatible for arbitrary correlation between reports and outcome) and on four steps of its proof (p. 34): the factorisation of I-ELF's selection probability under belief independence, the uniform transfer of expected event-winning probabilities, and the weak and strict monotonicity of the most-wins rule under such a transfer. Theorem 7 rests on Proposition 2, the one-sided Hoeffding inequality as stated on p. 35, eq. (9), the bound , and the explicit lower bound
Theorems 6 and 7 are also milestones on their own.
The theorem gives a single-prize competition that forecasters cannot profitably game, under any beliefs about others that respect independence across events, and that selects the most accurate forecaster with probability tending to one. The explicit rate in the proof of Theorem 7 tells a competition designer how many events are needed for a given accuracy gap and confidence. The incentive guarantee holds in dominant strategies and without risk neutrality, since forecasters care only about the probability of being selected.
The results are proved in the paper. None of them has a machine-checked proof that we know of, and the platform has no formal model of forecasting competitions, scoring-rule lotteries, or selection by most wins with random tie-breaking. A formal development would provide reusable definitions of strictly proper binary scoring rules and of lottery-based selection, and a checked version of an argument (pivotality of an event under uniform tie-breaking) whose case analysis is easy to get wrong.
The incentive half is not linear. Under ELF, a forecaster's selection probability is an expectation of a lottery that is affine in their score, so properness transfers directly. Under I-ELF the selection depends on the whole vector of event winners through an arg max with ties, and correlation between others' reports and outcomes could make an event's lottery depend on the rest. Belief independence removes the correlation across events. Strictness then needs an event to be pivotal with positive probability, and that fails when a scoring rule can reach : a forecaster sure to win two events can make a third irrelevant (the paper's footnote 10). The accuracy half needs concentration of the number of events won, with the constants tracked through the of the lottery.
Forecasters are Fin n with , events Fin m, outcomes Fin m → Bool (true means occurred), reports real numbers constrained to by hypotheses. A scoring rule is R : ℝ → Bool → ℝ; it is assumed measurable in the report so that selection probabilities under a law of the reports are well-defined expectations. I-ELF's selection probability is an explicit finite sum over event-winner vectors with uniform tie-breaking. A belief-independent law is the product (Measure.pi) of per-event joint laws of the outcome and all reports on that event; the selecting forecaster's own coordinate is overwritten by their report. Independent outcome laws are parametrised by their marginals . Limit accuracy is stated for the selection probability of an arbitrary mechanism, with the threshold chosen before , , the reports and the forecaster. Theorem 7 and its lemmas assume only , not strict properness, which the proof does not use.
Trivialising readings are excluded: incentive compatibility is strict (weak compatibility holds even for rules reaching ); others' reports are random and may correlate with the outcome within an event, not fixed; the limit-accuracy threshold may not depend on or the reports; and the selection rule is "most event wins", not the event-lottery average of multi-event ELF.
A complete development needs finite product measures and integrals of products, sub-Gaussian concentration for bounded independent variables (available in Mathlib), and a combinatorial analysis of the arg max under one changed coordinate. The definitions of scoring rules and lottery mechanisms are reusable for other elicitation and competition results. Proofs of any milestone are welcome, as are alternative arguments for the pivotality step.
Assembly projects such as aircraft programs or large software releases split work among several contractors, each responsible for one component. The finished product can only be as advanced as its least-developed component, so the contractors play a minimum-effort game (also called a weakest-link game): the project's value depends on the minimum of the efforts, while each contractor pays for its own effort. Such games have a continuum of Nash equilibria, ranked by payoff, and laboratory evidence since Van Huyck, Battalio and Beil (1990) shows that groups often settle on low-effort equilibria, with larger groups faring worse.
An original-equipment manufacturer (OEM) can affect coordination through the information it shares. Zhang, Shokoohyar, Qi and Katok, Coordination for Assembly (Manufacturing & Service Operations Management, doi:10.1287/msom.2023.0342), study a periodic information-feedback mechanism: the project runs over periods, and at the start of each period every contractor sees every contractor's progress. Their theoretical prediction, tested in the laboratory, is that the number of feedback periods relative to the number of contractors decides whether coordination succeeds. This mission formalizes the negative half of that prediction: with too few feedback periods, the selected equilibrium is the worst one.
There are contractors and periods. Each contractor's total effort lies in and its effort in each period lies in , with , where is the OEM's target level. All contractors start at zero effort. In period each contractor observes all efforts so far and then all simultaneously choose ; the effort level of contractor after period is .
The project level is , the OEM's payoff is , and contractor receives the share of it and pays per unit of effort:
The parameters satisfy .
A history is the list of effort profiles played so far; a strategy maps each history to the current period's effort. A subgame-perfect equilibrium (SPE) is a strategy profile from which no contractor gains by deviating after any history. For a history , write for the set of final level vectors reached by continuing some SPE from .
A subgame-perfect secure equilibrium (SPSE) (Definition 2 of the paper's Online Appendix) is an SPE such that, at the start of every period along its own path, each contractor's own final level maximizes its worst-case profit
among the levels that contractor attains in some SPE continuation. This is the paper's condition (24): among equilibria, contractors favour the one that protects them against the other contractors' least favourable equilibrium behaviour.
If , then an SPSE exists in which every contractor exerts the minimum effort in every period, every SPSE has this property along its path, and the project level is minimal:
The result says that frequent progress reports are not enough by themselves: when there are fewer feedback periods than contractors minus one, the secure refinement of subgame perfection selects the lowest project level, the same outcome as without feedback. It is the theoretical half of the paper's comparison between feedback regimes, which the laboratory experiment then tests with groups of two and four contractors and 1 to 6 feedback periods.
The result has a printed proof in the paper's Online Appendix. No machine-checked version exists. Formalizing it pins down a solution concept (an SPE refined by a maxmin criterion over the set of equilibrium outcomes of each subgame) whose verbal definition admits several inequivalent readings, and fixes which one the proposition holds for.
The companion part (ii) of Proposition 2, for , is false as printed and is not part of this mission: with , , , , , , , the profile with path is an SPE with project level , and no SPSE reaches , although part (ii) predicts that level at . Corollary 2 and Proposition 3, which rest on part (ii), are omitted for the same reason.
The existence half is a statement about whole strategy profiles, including play after every history off the equilibrium path. The constant profile that plays after every history is not an SPE when : after a history that leaves one contractor strictly behind with one period to go, that contractor gains by catching up. An SPE with the all-minimum path must therefore prescribe different, history-dependent behaviour off the path, and the count of tied contractors is what keeps a single deviation from breaking the tie at the bottom.
The SPSE condition quantifies over the set of all SPE outcomes of each subgame, so neither half can be checked by looking at one profile: both existence and uniqueness require knowing that the all-minimum outcome lies in that set at the relevant histories.
All quantities are real numbers; there is no probability. Contractors are indexed by Fin M and periods are 0-based (pathHist σ n is the history before the paper's period ). A history is a List (Fin M → ℝ) and strategies are arbitrary functions of the history: under feedback every past effort is observed, and restricting to state-dependent or open-loop strategies would change the set of SPEs that the definition compares against.
Committed conventions:
N + 1 ≤ M;Trivializing encodings are ruled out: the SPSE carries the SPE clause, the condition is neither dropped nor imposed at every history (under which no SPSE would exist), and the goal includes an existence conjunct, so it cannot hold vacuously.
The development needs the game, its SPE and SPSE (one definition file in the mission), and arguments about backward induction in a finite-horizon game with continuous actions. Proofs of the milestones, of the goal, and reusable lemmas about cumulative-effort games are all welcome.
Min-max problems model two-player zero-sum games and appear across machine learning and operations research: adversarial training of classifiers, generative adversarial networks, and robust optimization against an adversarial perturbation. When is convex in and concave in , von Neumann's minimax theorem gives a saddle point, and first-order methods find approximate ones. In the nonconvex–nonconcave case, which is the case of every neural-network objective, a global min-max point is intractable to find, and local notions such as local min-max points or local Nash equilibria need not exist at all (Jin, Netrapalli and Jordan, ICML 2020; Daskalakis, Skoulakis and Zampetakis, STOC 2021). Without existence there is nothing for an algorithm to converge to.
Mangoubi and Vishnoi propose an equilibrium notion that exists for every smooth bounded objective and can be computed in time polynomial in the dimension and the accuracy (arXiv:2006.12363). The max-player is modelled as an adversary that can only improve by local, "greedy" moves, and the min-player minimizes the value the adversary can reach this way.
Write for each player's strategy space, with the Euclidean norm, and give the norm . Throughout, is , -bounded () and has an -Lipschitz Hessian, .
A point is an -approximate local maximum of if and .
An -greedy path for is a continuous path , differentiable at all but finitely many points, travelling at unit speed, along which and, at every point, either increases at rate more than or its second derivative in the direction of travel exceeds . Let be the set of endpoints of -greedy paths starting at . The greedy max is
The greedy max is in general discontinuous in , so the min-player's stationarity is defined after truncation and Gaussian smoothing. For a bounded , a point is an -approximate local minimum of if
satisfies and .
A pair is an -greedy adversarial equilibrium if is an -approximate local maximum of and is an -approximate local minimum of .
For every , with , and every as above,
The accuracy is not fixed in advance; the theorem asserts that some accuracy at least as fine as is attained.
The theorem gives the first equilibrium notion for nonconvex–nonconcave min-max optimization that is both guaranteed to exist for every bounded objective with Lipschitz Hessian and computable with polynomially many gradient, Hessian and function evaluations. It requires no convexity, monotonicity, bilinearity or initialization near an equilibrium. At an equilibrium, neither player can improve by a local move of the kind second-order methods make: the max-player cannot climb by a greedy path, and the min-player cannot decrease the value the adversary will reach. Appendix A of the paper shows that in the strongly convex–strongly concave case the duality gap at such a point is small, so the notion refines the classical saddle point.
The result is proved on paper and has not been machine-checked. A formalization adds three things beyond the paper. First, a verified calculus of second-order approximate stationarity for discontinuous functions through truncated Gaussian smoothing, reusable for other nonsmooth objectives. Second, a precise account of the paper's conventions: Definition 2.1's second derivative has to be read directionally, (25) holds only with an added , and Lemma 7.3 holds only for , as its proof requires. Third, it settles whether the existence statement holds for every , including , which the printed proof does not cover.
The obvious approach is to minimize , but that function is intractable to evaluate and need not have approximate local minima reachable by local moves. The greedy max replaces it, but is a supremum over an uncountable family of paths, cannot be computed exactly, and jumps as moves: Example 2.4 shows a smooth whose greedy max is discontinuous. Convolution with a Gaussian restores smoothness but moves local minima (Example 5.5), which is why the definition truncates at before smoothing. The central difficulty is to obtain second-order information about the smoothed truncated while only ever evaluating a computable lower bound ; Lemma 7.3 is the step that transfers stationarity from one to the other, and its constants are tight enough that the transfer fails if any hypothesis is weakened.
is EuclideanSpace ℝ (Fin d) and the joint variable lives in WithLp 2 (ℝᵈ × ℝᵈ), so that the Lipschitz-Hessian condition uses the paper's Euclidean norm rather than Lean's sup norm on products. Eigenvalue bounds are quadratic-form bounds on the second Fréchet derivative. Expectations over are integrals against stdGaussian, and Gaussian smoothing is the published definition RandomGradFree.Shared.smoothing.
Conventions and readings, each disclosed in the item it affects:
The goal cannot be satisfied through Lean's junk values: a non-integrable truncated greedy max would make , and fderiv of a non-differentiable function is , so Definition 2.3 demands integrability and asserted derivatives, and the supremum defining ranges over a set that contains and is bounded by .
Not formalized: the algorithmic sentences of Theorem 3.1 (success probability , polynomial oracle complexity), Algorithm 2 and the milestones about its randomized run (Lemma 7.1, Lemma 7.2 (26)–(27), Propositions 7.6, 7.8–7.10), Lemma 5.1, Corollary 5.2, Appendix A and Appendix B. Algorithm 2 and Propositions 7.8–7.10 are natural follow-up contributions, as is the strongly convex–strongly concave duality-gap bound (Theorem A.1), which reuses this mission's definitions. A complete development needs Gaussian integration by parts in , differentiation under the integral for Gaussian convolutions of bounded measurable functions, and concentration of for ; all three are reusable beyond this mission.
Online marketplaces such as Zalando, Amazon or Farfetch let brands sell through the platform's storefront in addition to their own stores. One common arrangement is inventory sharing: the brand keeps ownership of its stock, but makes it visible to the platform's customers, and pays the platform a commission on every unit the platform sells. For a supplier with a fixed stock and a finite selling season, this creates a timing question. Sharing brings more customers, but each platform sale earns less than a direct one. Early in the season there is plenty of time to sell the stock at full margin; late in the season unsold units are worth nothing.
Martínez-de-Albéniz, Pinto and Amorim (SSRN 3643261, 2020; published in Manufacturing & Service Operations Management, 2022) model this problem as a continuous-time optimal control problem with Poisson demand, solve the supplier's problem, and use the solution to study how the platform should set its commission. The supplier's problem is a binary-control relative of the dynamic pricing problem of Gallego and van Ryzin (Management Science 1994): sharing switches the effective price and the demand rate between two values. Its solution is the building block for the paper's platform-pricing results.
A supplier sells a single item during a season. Time is measured as the time-to-go until the end of the season ( at the end). The item sells at the price . Customers of the supplier's own (direct) channel arrive as a Poisson process of rate ; customers of the platform arrive at rate . On a direct sale the supplier earns ; on a platform sale it keeps , where is the commission. Revenue is discounted at rate , and leftover units are worth nothing.
At every moment the supplier chooses : shares the inventory with the platform, does not. Write for the revenue-to-go with units left and time-to-go , and for the marginal revenue-to-go of the -th unit. The revenue-to-go solves the Hamilton–Jacobi–Bellman equation (3)
with and . A decision is optimal for unit at time if it attains this supremum. The threshold of unit is
which is when never exceeds the platform margin . In Lean these objects are Params, hamiltonian, hjbRHS, IsRevenueToGo, marginal, IsOptimalDecision and threshold in the namespace MarketplaceSharing.Threshold.
For every revenue-to-go and every :
and on each interval , , and on , there are constants with
The coefficients are existential, as on the page; their recursions are not part of the goal.
In attack order: well-posedness of (3) (a solution exists and is unique on ); the sharing condition of p. 8, optimal ; Lemma 1, ; Lemma 2, ; Lemma 3, nondecreasing in ; Lemma 4, nondecreasing in ; the explicit of footnote 4 (at ); the first bullet of Theorem 1; and Corollary 1, .
Theorem 1 reduces the supplier's policy, a function of time and stock, to one number per unit: share the -th remaining unit exactly when the time-to-go is at most . Corollary 1 orders these numbers, so the season splits into an early period of direct-only sales and a late period of sharing, which begins earlier the more stock is left. The closed form (4) makes and the thresholds computable. The paper's analysis of the platform's commission (Theorems 2 and 3) takes this policy as the supplier's best response.
The results are proved in the paper, by an induction on that runs through Lemmas 1–4. None of it has a machine-checked proof. A formalization produces a checked proof of a threshold structure for a two-mode Poisson control problem, a checked statement of where the printed text needs correcting (see below), and reusable pieces: well-posedness of a recursive system of Lipschitz ODEs and comparison arguments for HJB equations of this type.
The HJB system (3) is a recursive family of ODEs whose right-hand side switches between two affine laws according to the sign of . The monotonicity statements are comparison results for such switched systems: the obvious argument (differentiate and read off the sign) gives an equation for that involves and the switching times of both units, so monotonicity in and in have to be established together, unit by unit. The closed form (4) then needs the switching times of all lower units to be ordered (Corollary 1) before the ODE on each interval has constant decisions, and the polynomial factors come from repeated resonance of the exponential across units.
The paper defines by a stochastic control problem (2) over Poisson sales processes and derives (3) informally. The mission works with (3) only: the revenue-to-go is any family satisfying IsRevenueToGo ( on , , and the HJB equation for as a derivative within , one-sided at ), and every theorem takes this as a hypothesis. The well-posedness milestone shows such a family exists and is unique on , so no theorem is vacuous. Values at are unconstrained. Decisions are Booleans (true = share).
Conventions and added hypotheses: , , and are standing hypotheses (with or the two decisions tie everywhere and the threshold statement fails); is printed. The paper's range is read as , since does not depend on . The threshold lives in the extended reals with when has no solution (p. 10); the literal "there is an unique " fails for instance at . Three printed formulas are corrected and disclosed: the exponents of (4) carry , as the proof on p. 30 does (the printed form is exact only at ); Lemma 4 is stated in the direction of its words and proof, for (the printed display is reversed); and the formula of footnote 4 is stated at (with ), the only case in which it is exact.
The encoding rules out the trivializing readings: "optimal" is attainment of the supremum in (3), not membership in ; is the supremum of a sublevel set that always contains , not a solution of that could make uniqueness definitional; monotonicity of is a conclusion of the goal, never a hypothesis; and the hypothesis IsRevenueToGo is satisfiable by the well-posedness milestone.
Not formalized: the stochastic formulation (2) and its identification with (3); the recursions for , , (pp. 31–32); the numerical study of §3.3; and the platform-pricing results (Theorems 2 and 3, §4) and §5. A complete development needs one-dimensional ODE existence and uniqueness (Picard–Lindelöf and Grönwall, available in Mathlib), comparison of solutions of scalar ODEs, and calculus with . Proofs of any milestone, and reusable comparison lemmas for switched affine ODEs, are welcome.
Rental platforms, cloud computing, hotel and car-rental systems, and on-demand services all sell access to reusable resources: a unit that is rented comes back after a random rental duration and can be rented again. When such a platform displays a menu of products (an assortment) to each arriving customer, it faces an online decision problem: offering a product now earns a fee, but ties up a unit that a later, more valuable customer might have wanted. Feng, Niazadeh and Saberi study this problem in a Bayesian setting, where customer types are drawn from known distributions, and give an algorithm whose expected revenue is within a factor of an LP upper bound on any online policy (arXiv:2512.06997; Operations Research, 2024). The factor tends to as the smallest inventory grows and never drops below .
Earlier work on online assortment of reusable resources (Gong, Goyal, Iyengar, Simchi-Levi, Udwani and Wang, Management Science 2021; Goyal, Iyengar and Udwani, arXiv:2002.02430) studied the prior-free, adversarial setting, in which fees and rental-duration distributions are type-independent and identical across time. The Bayesian model here lets both depend on the customer type.
There are products; product has identical units, and . Customers arrive at times . Customer has a type , drawn independently from a known distribution on a finite set. A type fixes
Assortments come from a family that is downward closed (Assumption 2), and choice models are weakly substitutable (Assumption 1): , and adding a product to an assortment never increases the choice probability of another. A rented unit with duration is unavailable at times ; a product with no unit on hand cannot be offered.
The benchmark is the Bayesian expected LP Expected-LP: with the probability of offering to type at time , maximize subject to each product's inventory holding in expectation at every time, , and . Let be an optimal solution with , and
All algorithms of the paper follow one template: at time , sample ; for each , discard if it has no unit on hand and otherwise according to a per-product discarding rule; then offer a random subset of the survivors drawn by sub-assortment sampling (Procedure 1). Algorithm 2 discards at random with probability . Algorithm 3 keeps only if its fee exceeds a threshold computed from an optimistic per-unit dynamic program (equation (3)). Sim+Hybrid(i) chooses, product by product, between the two rules by comparing with .
For every instance and every optimal normalized ,
The result gives a single polynomial-time policy that is simultaneously -competitive, which is optimal for small inventories (a two-period example on p. 17 shows no online policy does better against this LP), and asymptotically optimal as inventories grow. Its analysis is modular: each product is treated separately, which is what allows mixing two discarding rules in one algorithm. Sub-assortment sampling is of independent use whenever an assortment must be thinned without distorting the choice probabilities of the remaining products.
The paper's proofs are on paper only; the per-product decoupling, which the paper invokes in a few lines for Theorem 3, is exactly the kind of step a formal proof makes explicit. A complete development produces a reusable finite model of a Bayesian online rental process (types, simulated assortments, discarding, choices and durations), a verified sub-assortment sampler, and an LP-duality certificate for the optimistic DP. None of these results is formalized elsewhere.
The obvious argument fails at the first step: whether product is available at time depends on all earlier rentals, and the offer probabilities of different products are correlated through the shared assortment and through substitution, so rental indicators are neither independent nor product-separable. Two ingredients are needed. Sub-assortment sampling must make each product's selection probability exactly its LP target, whatever happened to the other products; only then can the rentals of product be coupled with an independent sequence for a concentration bound (EC.2). For small inventories, a concentration bound is too weak, and the analysis instead compares the true process with the optimistic DP by backward induction over inventory states (Lemma EC.3), then bounds the DP against the LP with an explicit dual solution (Part (ii)).
Everything is finite: products are Fin n (the paper's product is index ), times are , types range over one finite type space (the paper's as subsets), and durations lie in . The online process is a product of explicit per-step kernels over finite sample paths; probabilities and expectations are finite sums, with no measure theory. Conventions committed to:
The process is not allowed to rent a unit that is not on hand, the post-processing targets are (not , which would make sub-assortment sampling the identity), and the path law uses the same as the benchmark; any formalization that drops one of these makes the goal a statement about a different process. Milestones 3, 4, 7 and 8 are stated for any feasible normalized and arbitrary rules for the other products, which is the generality Theorem 3's proof needs.
Contributions welcome: lemmas on the process (normalization of the path law, the marginal law of one product's rentals), the Chernoff bound, and analytic facts about .
A qubit stored or transmitted in the presence of noise loses purity. If many copies of the same unknown pure state have each passed through the same noisy channel, one may try to undo the noise collectively: feed the noisy copies into a quantum device and ask for output qubits that are as close as possible to perfect copies . The noise map itself is invertible as a linear map, but its inverse is not completely positive, so this purification problem is a genuine optimization over physical devices, closely related to optimal quantum cloning (Werner 1998, Keyl–Werner 1999).
Cirac, Ekert and Macchiavello (1999) found the optimal device for a single output qubit. Keyl and Werner (arXiv:quant-ph/9910124, 1999) solved the problem for an arbitrary number of outputs and two figures of merit, and computed the trade-off between output number and quality. For the figure of merit that tests all outputs jointly, the best fidelity is a function of the output rate alone in the limit, and that function is explicit. This mission formalizes that rate formula.
A qubit is with basis ; qubits are , with basis indexed by words . Fix a noise parameter with . The depolarizing channel acts on a one-qubit density matrix by
A device from to qubits is a quantum channel , i.e. a trace-preserving completely positive linear map from to complex matrices. Its all-qubit fidelity is the worst case over pure inputs:
The optimal all-qubit fidelity is , the supremum over all channels from to qubits. Finally, the rate function is
The proof works with the parametrization , , and with the decomposition of into spin- blocks, . Each block carries a weight (eq. (14)), an explicit probability vector built from , and binomial coefficients, and a state on the symmetric subspace of qubits.
For every sequence and every sequence with ,
The result. Formula (10) says that for every : in the all-qubit sense no purification procedure with a positive output rate approaches perfect fidelity, so optimal purification "works with zero rate". At the same time every fidelity level below one is achieved at a positive rate, and gives the exact trade-off. This contrasts with the one-qubit figure of merit treated in the same paper, where the fidelity of each output tends to one at any rate. Theorem 5.1 reduces an optimization over all channels between exponentially large spaces to a sum of explicit terms.
Formalizing it. The results are proved in the paper; none of them, to our knowledge, has a machine-checked proof. The paper's statement of Proposition 4.2 contains printing errors (swapped cases, a missing normalization factor, for ), and Lemmas 6.1 and 6.2 are stated with an incorrect domain and range; the milestones state the corrected versions, which were checked numerically against a semidefinite program for small . A formal proof would certify the corrected formulas. Related platform items, not posed again here: uniqueness of the optimal cloner (Support21.P16.unique_optimal_cloner, open) and covariance averaging for cloners (Renew46.P45.symmetrization, open), both used in the optimality argument of Theorem 5.1.
The obvious route to the goal is to evaluate the fidelity of one good device. That gives only a lower bound: the goal is about the supremum over all channels, and the upper bound requires the optimality theorem (Theorem 5.1), whose proof needs a reduction to covariant, permutation-symmetric channels, the decomposition of tensor-power representations of , and the optimality and uniqueness of the cloning maps on each spin block. The asymptotic part is also not a direct substitution: the weights must be shown to concentrate at , and on the side the dominant blocks need the binomial-sum branch of , whose limit is Lemma 6.2. Near the two branches meet, and the limit must be controlled uniformly in the block index.
Fin n → Fin 2; tensor powers are QAlgorithms.piKron; a pure state is QAlgorithms.pureDensity φ with ‖φ‖ = 1; a channel is a superoperator with a finite normalized Kraus family (QAlgorithms.IsChannel), which in finite dimension is exactly a CPTP map. The infimum and supremum are sInf/sSup on ℝ over sets that are nonempty and contained in .boseProjector) and the optimal cloner (canonicalCloner), the decomposition of with multiplicities, and concentration of the weights . The binomial-sum limit (Lemma 6.2) and the weight concentration (Lemma 6.1) are reusable outside this mission. Contributions of any milestone, or of lemmas toward the decomposition, are welcome.In contextual stochastic optimization a decision is chosen after observing features , and the ideal policy solves, for each feature value,
for a cost and an uncertain outcome (inventory demand, asset returns). Kallus and Mao (arXiv:2008.07473, Management Science 2023, doi:10.1287/mnsc.2022.4458) estimate such policies with stochastic optimization forests: random forests whose trees are grown to minimize the downstream decision cost rather than the prediction error of .
The bottleneck is choosing a split. The natural rule, the oracle criterion, re-solves an optimization problem for every candidate split of every node, which is too expensive inside a forest. The paper replaces it by an approximate risk criterion that needs only a gradient per child and one Hessian per parent, and justifies the replacement by a second-order perturbation analysis. This mission formalizes that justification.
Let be the law of on and let be the regression cost. For a region with write
A node of a tree is a region ; a candidate split is a partition into disjoint measurable pieces. Abbreviate , for ; note . Let be the unique minimizer of , the gradient and the Hessian in , and the diameter of .
The oracle criterion (eq. (8)) is the optimal cost after the split,
and the approximate risk criterion (eq. (13)) is
For the norm (70) is , and .
Assume is for every ; , , are -Lipschitz in uniformly in ; and at an anchor point the function has a unique, nondegenerate, level-bounded minimizer. Then for every there is such that every split of a region satisfying the paper's conditions 1–3 for obeys
Since does not depend on the split, the two criteria rank splits of a small node alike.
Theorem 2 is the guarantee behind the paper's algorithm: the criterion that is cheap to evaluate agrees with the expensive oracle criterion to second order in the node size, so a forest grown with it splits nodes the way a forest grown with the oracle would, while inverting only one Hessian per node. The same perturbation analysis drives the approximate solution criterion (Theorem 3) and, with constraints, Theorems 4 and 6; the unconstrained milestones here (Corollary 1, Theorem 9) are the reusable core.
The result is proved in the paper; nothing here is open. No part of it has a machine-checked proof. The mission produces a formal model of region-averaged costs, a quantitative second-order perturbation theory for unconstrained minimization (Corollary 1 and Theorem 9, which are standard in the Bonnans–Shapiro theory but absent from Mathlib), and a version of Theorem 2 with its limit, uniformity and error scale made explicit.
The expansions are about global minima, and Taylor's theorem only controls local behaviour. The obvious argument expands around and minimizes the quadratic model; it fails when the perturbation creates a competing minimum far from , which a small does not rule out when is flat at infinity. Theorem 9 is true only because the minimizer is unique along the whole path , , which keeps it from jumping.
The second obstacle is uniformity. Theorem 9 is stated for a fixed , but in Theorem 2 the base function is the average over and moves as shrinks. The little- must hold uniformly over base functions near the limit ; Milestone 7 isolates this step.
Finally, a literal reading of the printed bound is weak: both and are , so the printed bound holds without any second-order cancellation whenever . The content is the factor .
Features are EuclideanSpace ℝ (Fin p), decisions EuclideanSpace ℝ (Fin d) (unconstrained, §2). The law is a probability measure. The regression cost is the primitive; and enter only through it (tower property). Gradients are Mathlib's gradient; the Hessian is the derivative of the gradient, and the inverse Hessian is ContinuousLinearMap.inverse, always paired with a positive-definiteness hypothesis so that it is a true inverse. Minima are real infima, and every statement assumes or derives attainment. Little- claims are – statements; "" bounds the value, the gradient and the Hessian pointwise, with the Hessian in operator norm (weaker than the paper's Frobenius norm, so the statements are stronger).
Choices made where the page is silent or misprinted, all disclosed in the items:
The bound without the factor , a reading of condition 3 that forces at the optimum, a sup-norm defined by a supremum that is for unbounded functions, and a radius chosen after the regions would each make the goal trivial; the statements exclude all four.
Infrastructure needed: differentiation of set integrals with integrands (Mathlib's dominated-derivative lemmas suffice), consistency of minimizers under uniform perturbation, local strong convexity from a positive definite Hessian, and the second-order Taylor bound with remainder. The perturbation results (Milestones 4–7) are reusable for any unconstrained parametric minimization. Proofs of any milestone, and of the goal from Milestones 1, 3 and 7, are welcome.
Retail inventory records are often wrong. A store's system may report units on the shelf that are not there (phantom inventory), so the replenishment system never reorders and the product silently stops selling. Audits fix such errors but are expensive, so a retailer wants to decide which store–SKU pairs to audit from sales data alone. The classical way, studying each pair's sales history over a long period, needs time-homogeneous data that rarely exists.
Farias, Li and Peng (arXiv:2006.13126v3, Manufacturing & Service Operations Management, 2024) instead use a single cross-sectional snapshot of sales across stores and SKUs. Expected demand is modelled as a low-rank matrix, anomalies corrupt a random subset of entries, and only some entries are observed. The paper proposes the entrywise (EW) algorithm and proves that its expected decision cost approaches that of an oracle knowing the model, at rate . A matching lower bound (Proposition 1) is also proved. The paper evaluates the method on synthetic data and on real data from a consumer goods retailer.
An instance has an expected-demand matrix with , rank and SVD with singular values and . It also has an anomaly model , which is a family of laws on indexed by a parameter and a mean level . The remaining data are a true parameter , an anomaly probability , an observation probability , and costs (flagging a normal entry) and (missing an anomaly). Independently for every entry:
Assumptions (§2):
The oracle knows and . It computes the posterior , where and . It flags iff . The EW algorithm runs four steps:
The cost of decisions is
The constants and and the sparsity constant depend only on , , and the regularity constant . The statement asserts the paper's rate with polynomial dependence on the model parameters. It does not fix the polynomial, so a sharper analysis still proves it.
Theorem 1 says that the value of cross-sectional data grows with the number of stores and SKUs. A retailer that can only see one snapshot does nearly as well as one that knows the demand matrix and the anomaly law exactly. With Proposition 1, the rate is optimal up to the logarithmic factor. Theorem 2 is, per the authors, the first entrywise guarantee for matrix completion under Poisson (more generally sub-exponential) noise, and it is reusable outside inventory problems.
The results are proved on paper: Theorem 1 by a proof sketch in §5.1 plus Appendix B, and Theorem 2 in Appendix A, which builds on a cited entrywise eigenvector perturbation theorem of Abbe et al. None of this is formalized. A machine-checked proof would also settle the constants and conventions that the paper leaves implicit. These include the dimension restriction in Lemma 17, the unspecified constant in Lemma 3, the form of the sparsity assumption used in the proof of Theorem 2, and the closed range of in .
The obvious argument plugs consistent estimates of and into the Bayes rule. It breaks at the first step: a Frobenius-norm bound for , which is what standard matrix completion gives, does not control any single . An entrywise bound is needed, under heavy-tailed (sub-exponential, not sub-Gaussian) noise, and with the anomalies corrupting the mean by the unknown factor . The second step inverts the moment map . Closeness of moments yields closeness of parameters only through a quantitative inverse-function argument, which needs the regularity conditions of Lemma 1. A third subtlety is that is a ratio whose denominator can be tiny. The error bound of Lemma 3 therefore degrades on rare sales values, and Theorem 1 averages this over the law of .
One definitions module, InventoryAnomaly.EW.Model, holds the instance, the product sampling law over observedanomalous per entry, the estimators, the costs and four predicates:
Model: §2's assumptions;SparsityMax: the sparsity condition as read in the proof of Theorem 2, p. 41;Regular: Lemma 1's conditions;CostBound: costs in .The sub-exponential norm is the published HighDimProb.Concentration.subexponentialNorm.
Conventions:
The algorithm's selections are universally quantified together with their defining properties. Neither may be replaced by unconstrained functions. The cost of must use , not . The goal must keep the explicit rate and the full probability model, without assuming Theorem 2's event.
Not formalized: Proposition 1 (the lower bound), Appendix E (the TPR/FPR-constrained variant), the cited Lemmas 6–7, and the internal Lemmas 9–13 and Propositions 2–3 of Appendix A.
Useful infrastructure includes entrywise singular-subspace perturbation bounds, Bernstein's inequality for bounded independent sums, and Orlicz-norm bounds for Poisson variables. All three are reusable beyond this mission. Proofs of individual milestones are welcome, especially Lemmas 8, 14, 17 and 19 and Step 4, which are self-contained.
A Gelfand–Tsetlin basis of a representation of the last group in a tower is a basis adapted to every restriction at once: each basis vector spans a line that is cut out by the isotypic decompositions at all levels . When every restriction is multiplicity-free, these lines are canonical, and the basis vectors are indexed by paths in the branching graph. For the symmetric groups, Young's orthogonal form gives such a basis with completely explicit matrices for the simple transpositions (Young, 1932; see Headley, 1996, Theorem 2.1), and the Vershik–Okounkov approach (arXiv:math/0503040) builds the representation theory of around it.
The alternating groups also form a multiplicity-free tower, so their irreducible representations have Gelfand–Tsetlin bases too. Geetha and Prasad (arXiv:1606.04424) write these bases down explicitly inside Young's orthogonal form, so that the Gelfand–Tsetlin bases of and can be compared vector by vector. The branching rules of were known before (Ruff, Algebra Colloquium 2008, Theorem 6.1); the new ingredient is a sign normalisation of the associator that identifies the two halves of a self-conjugate consistently along the whole tower.
For a partition of , is the complex vector space with basis indexed by the standard Young tableaux of shape . Tableaux are written inline row by row, e.g. . The simple transposition acts by Young's formulas (2): if lies in row , column of and in row , column , and , then is (same row), (same column), and otherwise . For (one box fewer), embeds in by , with written in the new box (4).
For self-conjugate , the associator is the operator
where is the transposed tableau, the number of diagonal boxes, and the sign of the permutation carrying a fixed reference tableau to . The reference tableau is chosen through self-conjugate covers (, both self-conjugate): the smaller partition gets the row superstandard tableau, and the larger one the same tableau with added on the diagonal. are the eigenspaces of .
Labels are non-self-conjugate partitions , with , and symbols for self-conjugate , with . Conjugate non-self-conjugate labels are equivalent, . A path has each obtained from by removing one box, with equal signs whenever both are self-conjugate. Definition 2 builds a vector recursively from and . At each step the previous vector is embedded by (4), and when the path passes from a non-self-conjugate shape to it is replaced by .
For and :
and for any set of paths ending at containing one path from each equivalence class,
The theorem gives closed-form Gelfand–Tsetlin bases for every irreducible representation of every alternating group. Each vector is a combination of Young's orthogonal basis vectors with Gaussian-integer coefficients; Example 2 of the paper shows one with four terms and coefficients . The matrices of in this basis then follow directly from Young's formulas. It also shows exactly how the two Gelfand–Tsetlin bases compare: on non-self-conjugate shapes they coincide, and on self-conjugate shapes the -vectors are the -symmetrisations under the associator.
The result is proved in the paper; nothing about it is formalized. Lean's Mathlib has Young diagrams and the platform has standard tableaux, but there is no Young orthogonal form, no associator, no representation of built from partitions, and no Gelfand–Tsetlin basis for any group. A complete development would give the first machine-checked Gelfand–Tsetlin basis for . Along the way it would give a machine-checked Young orthogonal form with its sign calculus, which is reusable for any later work on symmetric-group representations.
The Gelfand–Tsetlin property is a statement about isotypic components at every level. Checking it needs, at each level, the branching rule and an argument that the recursively built vector lands in the right isotypic component. For non-self-conjugate shapes this is inherited from . The difficulty is the self-conjugate case. A path through two consecutive self-conjugate shapes keeps the sign only if restricts exactly to on , so the bare existence of an associator for each , unique up to scalar by Schur's lemma, is not enough. The sign of each has to be fixed coherently along self-conjugate covers, and this is what the choice of and the factor do. The basis half needs, in addition, the count of how many paths share a geodesic (Theorem 3) and the fact that distinct classes give distinct lines.
YoungTableau of QAlgorithms_Papers_Independent_Renew46_P26. Labels are (the paper's entry is label ) and boxes are 0-based (row, column).Ruled out. The Gelfand–Tsetlin predicate is defined intrinsically through isotypic components. It is never defined as membership in a span of the vectors that Definition 2 produces, and is never replaced by a formula that makes Theorem 4 hold by definition.
Not formalized. Corollary 1, the completeness clause of Theorem 1, the bijection clause of Theorem 3, Examples 1–3 and Remarks 1–4.
Solvers will need several pieces of infrastructure:
The Coxeter relations and the sign calculus are reusable beyond this mission. Contributions proving any milestone, or proving that Young's operators define a representation, are welcome.
Large online marketplaces are hybrid platforms: they host third-party sellers and also sell their own products. Running the marketplace gives the platform access to sellers' sales data, and it can use that data to identify successful products and launch imitations of its own. The practice is colloquially called "Sherlocking". It has drawn regulatory attention: the European Commission's case against Amazon over the use of non-public seller data, and proposals to ban platforms from using such data or from competing with their own sellers at all.
Choi, Kim and Mukherjee (CESifo WP 10769 / SSRN 4643950, 2023; Management Science, 2025, doi:10.1287/mnsc.2024.05215) study the problem as a tension between the platform's fee, its entry decision and its information policy. The threat of imitation discourages sellers from joining, so a platform would like to commit not to imitate too aggressively. Commitment to an entry policy is rarely credible, but commitment to a data policy (what the product division is allowed to learn about a seller) is something a platform can build into its organization. The paper asks when the second kind of commitment is as good as the first.
A seller decides whether to join a marketplace run by a platform. Time has two periods of lengths and . The platform posts a referral fee , a share of the seller's profit. The seller's type , his profit per unit time as a monopolist, is uniform on and known only to him; entry costs him . Assumption 1 is .
If the seller enters, the platform collects in the first period. At the start of the second period it may imitate at cost , taking the whole second-period profit ; otherwise it collects . If the platform enters with probability , the entering seller's expected payoff is . Two cutoffs organize the analysis:
The seller enters against a platform that never imitates iff ; the platform gains from imitating type iff .
Full commitment. If the platform could commit to an entry probability for each type, its optimal policy is to stay out on and to enter on with the largest probability that keeps the seller willing to enter,
Its value is , and denotes a fee maximizing on . The resulting entry pattern is the full commitment outcome.
Information policy. Without commitment, the platform chooses an information policy: a set of realizations and a signal , a probability distribution on for each type. Its product division sees only the realization and then decides whether to imitate, in its own interest. The seller anticipates this. The solution concept is weak perfect Bayesian equilibrium. The full commitment outcome is implementable by an information policy if some signal has an equilibrium in which exactly the types in enter and the platform imitates type with probability on and below.
Under the binary signal (3), which reports with probability for and otherwise, the platform obeys the recommendation "stay out" iff
For a maximizer of on , the full commitment outcome at is implementable by an information policy if and only if (OC0) holds at , which is equivalent to
Proposition 3 gives a checkable condition under which information design substitutes for commitment to entry. When (4) holds, the platform obtains its full-commitment profit by restricting what its product division learns, and the seller faces the same entry threat as under full commitment. When (4) fails, the paper's Proposition 4 shows the platform must distort the outcome by excluding an interval of types. The comparison underlies the paper's policy conclusions about bans on data use and on imitation.
The result is proved in the paper; nothing in this mission is open mathematically. What the mission adds is a machine-checked development of a small information-design model: a formal revelation principle for this game (Lemma 1), with an equilibrium notion that handles a continuum of signal realizations, and a formal check that the integral conditions are equivalent. No part of the paper has been formalized before, to our knowledge.
The sufficiency direction is a computation with signal (3). The necessity direction is not: implementability quantifies over every signal space and every equilibrium, so (OC0), which is a property of one specific binary signal, has to be derived from an arbitrary equilibrium. The naive route of conditioning on each realization fails for a continuum of realizations, where conditional expectations are defined only almost everywhere and off-path behaviour is unconstrained. Separately, the goal is stated at the maximizer , and nothing in the hypotheses says directly that lies in the non-degenerate range , where some type enters.
Everything is real-valued, in the namespace Sherlocking.InfoPolicy, with a single definitions module.
X : Type with a σ-algebra. Platform strategies are measurable maps , the probability of imitating after each realization.Implementability is never defined through (OC0) or through signal (3). It quantifies over all realization spaces, signals, strategies and entry sets, under the full equilibrium predicate; a definition that fixed the signal would make the necessity direction trivial.
A complete development needs interval and set integrals of bounded functions, measurability of kernels and parametric integrals, and the Giry monad on Bool, all available in Mathlib. The binary revelation argument is reusable for other sender–receiver models with a binary action. Proofs of any milestone are welcome, as are alternative proofs of Lemma 1.
Many decision problems in operations research end in a linear optimization over a finite set of alternatives whose objective coefficients are random: the longest path in a project network with random activity durations, a maximum-weight assignment or spanning tree with random weights, the best item in a ranking with random utilities. The quantity of interest is the expected optimal value , where . In practice the one-dimensional distributions of the coefficients can be estimated, while their dependence structure usually cannot. The marginal distribution model therefore asks for the largest expected optimal value over all joint distributions consistent with the given marginals, a distributionally robust bound that does not assume independence.
Chen, Ma, Natarajan, Simchi-Levi and Yan (Operations Research, 2022) study this bound for an arbitrary finite feasible set and arbitrary marginals.
Timeline. Meilijson and Nádas (1979) gave a convex formulation of the tight upper bound on the expected completion time of a PERT network when only the marginal distributions of the activity times are known. Bertsimas, Natarajan and Teo (2004) studied the analogous bound for 0–1 problems under marginal moment information. Natarajan, Song and Teo (Management Science 55(3), 2009) gave a concave maximization formula for the marginal distribution model when consists of integer points and the marginals are absolutely continuous. The paper of this mission removes both restrictions: is any finite point set, the marginals are arbitrary (discrete marginals allowed), and the bound is cast in Lagrangian primal and dual forms.
Fix , a nonempty finite set , and probability measures on . Write for the coordinate projections of .
The value to be computed is
The Lean development names these objects proj, Z, frechetClass, couplings, margMeasure (), conj (the inner maximum of ), lagrangian, quantile and quantileForm (the objective of (8)), all in MarginalDRO.Lagrange.
For marginals with finite variance and a nonempty finite , with every optimum attained,
The result. Theorem 2 turns an optimization over joint distributions on , an infinite-dimensional problem, into a saddle problem over probability vectors on and univariate functions on the finite sets . The dual form gives upper bounds on from any choice of prices , and the primal form gives a worst-case joint distribution. The paper builds on it a compact reformulation (its §4) whenever has a tractable description, and applications to appointment scheduling, robust maximum flow, ranking and project scheduling. Theorem 3 makes the primal side explicit as a concave program in the quantile functions, which holds for discrete marginals as well as continuous ones.
Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. The development needs pieces that are of independent use: Kantorovich duality for a signed, unbounded cost that is linear in one variable, the monotone (comonotone) coupling lemma, gluing of couplings along a common marginal, measurable selection of maximizers over a finite set, and a minimax exchange for a Lagrangian that is affine on a simplex and convex in an infinite family of functions. The ≥ step of the printed proof uses a product of couplings that does not give the inequality in general; a formal proof has to replace it by a gluing argument.
The obvious route to the first equality bounds from both sides by a joint law of . From above this needs a measurable optimal selection; from below it needs a joint law under which is a point of and each pair has a prescribed coupling. Independent products of the couplings fail here, because their -coordinates no longer form a point of . The Lagrangian equalities need duality for a cost that is neither bounded nor of one sign, with supported on all of , and attainment of the dual infimum over an unbounded family of potentials, which is invariant under the shifts by arbitrary constants and so has no compactness for free.
Finset (Fin n → ℝ); is its coordinate projection; is stdSimplex ℝ 𝒳, whose topology for finite is the weak-* one.Measure ℝ with IsProbabilityMeasure. Finite variance is MemLp id 2. Lemma 1 and Theorem 3, which print no moment condition, assume a finite mean (Integrable id) so that every expectation is finite.IsGreatest, IsLeast); inner inf/sup are IsGLB/IsLUB. The quantile is a real infimum that takes the value outside , a null set for the integrals.The following formalizations would trivialize the goal and are excluded: as a maximum over or ; a class that fixes only some marginals; couplings without the second marginal ; a conjugate taken over instead of ; equalities decided by the default value of a real sSup/sInf; an empty .
Welcome contributions: the monotone coupling lemma for general supermodular costs, Kantorovich duality on for finite , gluing of couplings, and proofs of any milestone.
Markets in which goods pass through intermediaries (supply chains, interbank lending, procurement networks) do not fit the two-sided buyer–seller models of matching theory: one firm can buy inputs on some trades and sell outputs on others. Trading networks model such markets as a directed graph of possible bilateral trades. Hatfield, Kominers, Nichifor, Ostrovsky and Westkamp (J. Polit. Econ. 2013) showed that when every agent's preferences are fully substitutable, competitive equilibria exist and several notions of stability coincide with competitive equilibrium. Stability notions describe outcomes that agents cannot undo by renegotiating, and competitive equilibrium describes outcomes supported by prices. Knowing that the two coincide matters for market design: a decentralised market that only has to rule out simple deviations already achieves a price-supported, efficient allocation.
Candogan, Epitropou and Vohra (Operations Research, 2021; working paper version IHS Economics Series 323, 2016) rederived these results from the theory of M-convex submodular flows (Murota, Discrete Convex Analysis, SIAM 2003). Full substitutability is equivalent to M♮-concavity of the valuations, and efficient outcomes correspond to optimal flows.
Timeline:
A trading network is a finite directed multigraph . Each vertex is an agent, each arc a possible trade, with seller and buyer . Write for the trades sells, for the trades buys, and . An outcome is a set of trades , and a price vector is . Agent has a valuation and utility
For , the demand restricted to is ; with it is the ordinary demand .
If is chain stable, then there is with
Theorem 5.8 closes the hierarchy of solution concepts in trading networks. Combined with Theorem 5.7 (competitive equilibria are strongly stable, hence chain stable), every notion between chain stability and competitive equilibrium describes the same outcomes. Since chain stability is the weakest of them, it is enough to check deviations along chains to certify an outcome as price supported and, by the first welfare theorem, efficient. The result is also the basis of the paper's algorithmic section, which finds blocking chains as negative cycles.
The theorem is proved, in Hatfield et al. (2013) and again in this paper. No part of it is formalized on the platform. The mission produces a machine-checked trading-network model with M♮-concave valuations, the existence and second welfare theorems for it, and the chain-stability equivalence. The M♮-concavity definition reused here comes from the platform's formalization of Murota's book.
The lifting steps (milestones 6 and 7) are bookkeeping. The substance is in two places. First, Theorems 4.1 and 4.3 and Lemma 5.5 are where substitutability is used: existence of equilibrium prices is a duality statement for a nonlinear integer program, and Lemma 5.5 asserts that an improvement over no trade can always be found with the special shape of a chain. Neither follows from finite enumeration. Without substitutability both fail: with complementary valuations an inefficient no-trade outcome can need a non-chain set of trades to improve on it, and equilibria need not exist. Second, milestone 1 requires closure of M♮-concavity under adding a linear function and maximizing out a group of coordinates (projection). This closure is standard in Murota's book but is not on the platform.
Finset E, evaluated only on subsets of . Prices are functions E → ℝ.DiscreteConvex.EconomicEquilibrium.MNaturalConcave (values in , exchange axiom on the effective domain), applied to the signed representation sold, bought, off the box . The paper's printed axiom on PDF p. 8 has in its last term, a typo for , which is what the definition uses.{e // e ∉ X}.Liquid democracy lets each voter either vote directly or delegate the vote to another voter, who may delegate it further. It has been used in practice, for example by the German Pirate Party on the LiquidFeedback platform and in the Google Votes experiment, and has been studied in computational social choice as a way to give more weight to better-informed voters. A natural worry is that delegation concentrates power: if too many votes flow to a few voters, the outcome rests on those few judgements and the "wisdom of the crowd" of independent votes is lost. Kahng, Mackenzie and Procaccia (Journal of Artificial Intelligence Research, 2021) showed that no local delegation mechanism can guarantee, for every instance, that liquid democracy is never worse than direct voting and sometimes strictly better.
Berinsky, Halpern, Halpern, Jadbabaie, Mossel, Procaccia and Revel (arXiv:2107.11868v3; Management Science, 2025) replace the worst-case requirement by a probabilistic one: competencies and delegations are random, and the comparison is made with high probability as the number of voters grows. Their first main result, Theorem 1, concerns the simplest model in which delegation goes only upward in competence. It is the goal of this mission.
There are voters deciding a binary question with a correct answer. Voter has a competence , the probability that its own vote is correct; given , the votes are independent, with law .
A delegation graph is a directed graph on in which every voter has at most one outgoing edge, the voter it delegates to. A voter who votes directly has weight (the number of voters whose delegation chain ends at ); a delegating voter has weight ; voters on a delegation cycle, or delegating into one, are not counted. is the largest weight. Direct democracy gets correct votes and liquid democracy . The gain of the instance is
A model consists of and . Competencies are drawn i.i.d. from a distribution supported in ; then each voter independently keeps its vote with probability and otherwise delegates to some with probability proportional to (and keeps its vote if all these weights vanish). This defines the law of the random instance.
The Upward Delegation Model has and : each voter delegates with probability , to a strictly more competent voter chosen uniformly. is the class of continuous distributions on .
The proof runs through the infinite Pólya urn with attachment probability : at time there is one ball in one bin; each new ball opens a new bin with probability and otherwise joins an existing bin with probability proportional to its size. is the largest bin size at time .
For every ,
The milestones are the statements the paper's proof uses, in attack order:
then satisfies probabilistic do no harm. If moreover some satisfies with probability , it satisfies probabilistic positive gain.
Theorem 1 shows that the impossibility result of Kahng et al. is an artefact of worst-case analysis: under a simple and natural random model, liquid democracy is asymptotically no worse than majority vote for every continuous competence distribution, and strictly better for some. Lemma 1 is the paper's general tool: it reduces both properties to two checkable conditions, a sub-linear largest weight and a linear increase of the expected number of correct votes, and is reused for the paper's two other models (Theorems 2 and 3). Lemma 2, a sub-linear bound on the largest bin of the infinite Pólya urn (the Simon–Yule preferential-attachment process), is of independent interest in random-structure theory.
The results are proved in the paper. None of them is formalized; Prove2Me has no liquid-democracy, delegation-graph or infinite-urn item. A formal development adds a checked version of the core lemma for arbitrary models, and a formal treatment of the urn that the later models' arguments can be compared with. Several steps of the paper are terse (the late-bin bound rests on a cited convergence rate; the arithmetic of Appendix B.3 is loose), so a checked proof adds more than a transcription.
The obvious argument — liquid democracy moves votes to better voters, so it should do at least as well — fails because concentration is lost when weights become large: if one voter carries a constant fraction of the votes, no longer concentrates, and the majority can be wrong with constant probability even though the expected number of correct votes rises. The heart of Theorem 1 is therefore Lemma 2, a bound with on the largest bin of an infinite Pólya urn. A first-moment bound on each bin handles the bins born before time , but the union bound over the remaining bins needs each to exceed with probability , which first moments do not give. The coupling between the urn and needs the competencies to be distinct, which is where continuity of enters.
All declarations live in the namespace LiquidDemocracy.Upward, in two definition files (Setting, Urn) and one file per theorem, against the platform's default Mathlib.
Fin n; a delegation graph is a map g : Fin n → Fin n with g i = i meaning "votes directly". A voter's weight counts the voters whose chain, followed steps, ends at it; chains running into a cycle reach no direct voter, which implements the cycle convention.Measure.bind; bins are numbered from , time means balls, and the step into time divides by .=o[atTop]; Definitions 1–2 keep the paper's form. In Lemma 1 the model is assumed typed as on p. 10 and measurable.A trivializing formalization is excluded: the instance law is a probability measure for and is nonempty (the uniform distribution on belongs to it), both checked sorry-free, so neither property holds vacuously or fails for a degenerate reason.
A complete development needs Hoeffding's and Chebyshev's inequalities (in Mathlib), Gautschi's inequality for Gamma ratios, a coupling argument for stochastic domination of Markov chains, and the conditional-independence structure of the instance law. The urn results and Lemma 1 are reusable beyond this mission. Contributions to any milestone are welcome, including alternative proofs of the late-bin bound (for instance by second-moment recursions instead of the cited Beta-limit rate).
A pure Nash equilibrium (PNE) of a game is a strategy profile from which no player gains by a unilateral deviation. Unlike mixed equilibria, pure equilibria need not exist, and even when they do they can be hard to find: computing an equilibrium is PPAD-complete in general (Daskalakis, Goldberg & Papadimitriou 2009). The simplest learning procedure that searches for a PNE is best-response dynamics (BRD): repeatedly let some player who can strictly improve switch strategy. BRD is guaranteed to stop at a PNE only for special classes such as potential games (Monderer & Shapley 1996); in general it can wander forever inside a trap, the "sink equilibrium" of Goemans, Mirrokni & Vetta 2005.
A way to measure how often these failures occur is to draw the payoffs at random. The classical line of work, from Goldman (1957) and Goldberg, Goldman & Newman (1968) to Powers (1990) and Rinott & Scarsini 2000, studies the number of PNE when the payoffs are i.i.d. with a continuous law, so that ties have probability zero. The number of PNE then has mean one and is asymptotically Poisson. Amiet, Collevecchio, Scarsini & Zhong (2021) drop the continuity assumption. They show that the single parameter governing the asymptotics is the tie probability , and they relate the game to bond percolation on the hypercube. Their headline result is that, for binary players and small positive , BRD started from a fixed profile reaches a PNE with a failure probability that is summable in .
There are players , each with strategies . A profile is , and . In the random game the payoff of player at profile is , and the family is i.i.d. with a law on that may have atoms. With i.i.d. of law ,
Two profiles that differ only in coordinate are joined by an edge of the hypercube . The edge is oriented from to when , and is unoriented when the two payoffs tie; this gives the random partially oriented hypercube . The set of strictly profitable deviations consists of the heads of the arrows leaving , and is a PNE iff . BRD, , starts at and at each step moves to a uniformly random element of of the current profile. It converges to a PNE if for all large .
A profile is accessible from if an oriented path leads to it, and is the set of profiles accessible from . A trap is a set of at least two profiles that is strongly connected and that no oriented path leaves. In bond percolation each edge of is open independently with probability . Its giant component is the largest open cluster, and its fragment is the set of vertices outside the giant component.
If and (equivalently ), then
The theorem shows that the failure of BRD described in the game-theory literature, cycling in a trap, is asymptotically rare when payoffs tie with small positive probability. By Borel–Cantelli there is then a finite random beyond which BRD always reaches a PNE. The threshold is where the expected number of trapping 4-cycles stops being summable. The percolation coupling (Proposition 4.1) is the paper's new tool: it turns questions about accessibility under BRD into questions about clusters of the hypercube, where the results of McDiarmid, Scott & Withers apply. The same coupling yields the paper's phase transition at for the accessibility of all PNE (Theorem 3.3, not part of this mission).
The paper results are proved on paper, except for one gap. The paper derives (5.8), and through it Theorem 2.3, from the claim that the number of PNE has the same law as the number of isolated vertices of the percolation. That identity is false: the two laws already differ at . Statement (5.8) and Theorem 2.3 are nevertheless true; (5.8) follows from the Chen–Stein method (Arratia, Goldstein & Gordon 1989). Both are posed here as printed, and a correct proof of them is a contribution in its own right. None of these results has a machine-checked proof.
The obvious argument is a first-moment bound: count expected traps and sum over . The 4-cycles that are traps alone have expected number of order , summable exactly when , but traps can have any size up to , and the number of candidate vertex sets grows far faster than any single-shape first moment decays. Controlling traps of every size requires global information about which profiles BRD can reach from , and about how the exponentially many PNE sit relative to that set. That information comes from the component structure of percolation on the hypercube at a fixed edge probability, a deep theory (McDiarmid–Scott–Withers) of which nothing is in Mathlib.
Players are Fin N and profiles are Fin N → Bool; the payoffs of live on Fin N → Profile N → ℝ with the product law gameMeasure μ N. Each has its own probability space; every target is a per- bound or a sum over of per- probabilities, so no coupling across is needed. Sums of probabilities are ∑' in ℝ≥0∞ and are required to be ≠ ⊤. The BRD chain is built from the PMF iterates of its one-step kernel. At a PNE, where the page leaves the step undefined, the chain stays put. The probability of non-convergence is then , averaged with a lower Lebesgue integral. Percolation configurations are Edge N → Bool under a product of Bernoulli laws. " is not in the giant component" is read conservatively: on a tie for the largest cluster, counts as outside. Theorem 2.3 and (5.8) assume , as the page's does (both fail at ). Their constants are uniform over all payoff laws with the given . Lemma 4.3's is two-sided.
Trivializing encodings are excluded: no probability is a Bochner integral of a possibly non-measurable integrand, convergence is not defined by fiat, and a trap needs at least two vertices and closedness, so a single PNE is not a trap. The hypothesis (3.8) is kept literally. At it holds through Lean's , but the goal is then true for a genuine reason (every profile is a PNE).
A complete development needs the theory of finite Markov chains (absorption), Poisson approximation by Chen–Stein, a Berry–Esseen bound, and the component structure of percolation on the hypercube. The last of these is reusable well beyond this mission. Contributions of independent pieces, such as the trap reduction or the first-moment bounds, are welcome.
A chance constraint asks that a random inequality system hold with at least a prescribed probability . Such constraints appear throughout engineering and energy optimization: reservoir and power-system management, network design, and any decision that must stay feasible against uncertain demand or inflow with high reliability. The function is called a probability function. It is in general neither convex nor smooth, even when the underlying random inequality is convex in the random vector, and this is what makes chance-constrained problems hard to solve with standard nonlinear-programming methods.
One remedy is to replace the probability function by a regular approximation and to solve a sequence of approximate problems. van Ackooij, Pérez-Aros, Soto and Vilches (arXiv:2301.09803, Mathematics of Operations Research, 2024) propose an inner regularization built from the Moreau envelope of a scalarized constraint function, for conic constraints in infinite-dimensional decision spaces. The approximate feasible sets contain the original one, and the approximate problems have smooth data. A regularization is useful only if solving the approximate problems recovers the original problem in the limit. This mission formalizes that consistency statement, Theorem 5.4 of the paper.
Let be a separable real Hilbert space (the decision space), a real Banach space with dual , and a random vector on a probability space whose law has a density with respect to Lebesgue measure. A continuous map and a nonempty closed convex cone define the probability function
The conic constraint is scalarized by a convex, weak-compact set whose generated cone has weak closure equal to the positive polar cone . A convex, continuously differentiable is assumed to make every scalarization , , jointly convex. The supremum function is .
For and , the Moreau envelope is . The inner regularization of is
the envelope being taken on with the Hilbert norm. For put and . Given a proper, convex, lower semicontinuous objective , problem (P) minimizes over and the regularized problem (Pλ) minimizes over , with optimal values and .
If is moreover coercive and , then
and for and optimal solutions of with , the point is optimal for (P). If moreover and is Fréchet differentiable on , then in norm.
Theorem 5.4 justifies the regularization as a solution method: optimal values converge, and weak limits of regularized optimal solutions solve the original problem, with strong convergence under a smoothness condition on . Combined with the paper's differentiability results for (§4, not part of this mission), it reduces a nonsmooth chance-constrained problem to a sequence of problems with smooth data whose solutions approximate the true ones. The intermediate results (monotone convergence of , the limsup estimate, convergence of feasible sets) are reusable for any analysis of envelope-based approximations of probability functions.
All statements are proved in the paper. None of them, and none of the general facts used (monotone and lower epi-convergence of Moreau envelopes in Hilbert space, Painlevé–Kuratowski and Mosco convergence), has a machine-checked proof on the platform at the time of writing. The mission produces a formal account of the conic scalarization, of the inner regularization, and of the consistency argument.
The obvious approach, "the regularized feasible sets converge, the regularized objectives converge, hence the minima converge", fails in two places. First, the decision space is infinite-dimensional, so bounded minimizing sequences only converge weakly, and the probability function must be controlled along weakly convergent sequences. This requires weak upper semicontinuity of and a limsup estimate for along weakly convergent , which do not follow from continuity of . Second, convergence of values needs a liminf inequality for along weakly convergent sequences together with Mosco, not merely Painlevé–Kuratowski, convergence of the feasible sets. The probability function is not convex, so the usual convex-analytic route to Mosco convergence is unavailable.
The Lean development uses H with [InnerProductSpace ℝ H] [CompleteSpace H] [SeparableSpace H], Y a real Banach space with dual StrongDual ℝ Y, and weak notions through WeakDual ℝ Y. Extended-valued functions (, , , , , ) are EReal-valued, and infima and suprema are taken there, so no default value enters. Probabilities are ℝ≥0∞-valued. The product carries the ℓ² norm (WithLp 2), as the paper requires. Weak convergence is defined through inner products. The limit is the filter of right neighbourhoods of for values and positive sequences for solutions and feasible sets.
The definitions file contains , , coercivity, conjugate, subdifferential, Fréchet differentiability of an extended-valued function, weak convergence, sequential weak continuity, Painlevé–Kuratowski and Mosco convergence, the conic setting (9)–(10), , , , , , , and optimality for (P) and (Pλ).
Two hypotheses are added to the printed statements, each used by the paper's own proofs: is closed (the bipolar step of Proposition 2.6), and is sequentially weakly continuous in Theorem 3.1 d) and throughout Theorem 5.4. The second is automatic when is finite-dimensional. Both are disclosed in the statements.
Trivializing readings are excluded: the feasible set meets ; is proper; the envelope uses the Hilbert, not the sup, norm on the product; is an extended-real supremum over a nonempty set, not a real supremum with a default value; every is positive. Item b) of the goal is vacuous only when some regularized problem has no optimal solution, exactly as in the paper.
Contributions welcome: Moreau-envelope convergence in Hilbert space, the bipolar theorem for closed convex cones in Banach spaces, measure-theoretic continuity arguments for , and the existence argument for optimal solutions of (P).
In a contextual bandit a learner plays rounds; in round it observes a context , pulls one of arms and receives the reward of that arm in that context. In many applications the learner also learns what the pulled arm would have paid in other contexts. The motivating example of Balseiro, Golrezaei, Mahdian, Mirrokni and Schneider (arXiv:1809.09582) is a bidder in repeated first-price auctions: the context is the bidder's private value, the arm is the bid, and after the auction the bidder can compute the utility the same bid would have earned at every other value. Similar cross-learning structure appears in dynamic pricing with variable costs and in multi-armed bandits with side information about contexts.
Treating each context as a separate bandit problem costs regret of order , which is useless when the number of contexts is large or continuous. The paper shows that cross-learning removes, or reduces, this dependence on . For stochastic rewards it analyses UCB1.CL, a version of UCB1 that updates its statistics in every context it learns about, and bounds its regret by a graph quantity, the clique covering number of the cross-learning graphs. The authors describe this analysis as the main technical contribution of the paper (p. 5).
There are arms and contexts . On a probability space, the reward of arm in context at round is random; the reward vectors of different rounds are independent (rewards may be correlated within a round), and has the same law , with mean , in every round. The best mean in context is and the gap of arm is . The contexts form an arbitrary sequence fixed before the game (adversarial, oblivious contexts).
For each arm a directed cross-learning (CL) graph on the contexts is known: an edge means that pulling arm in context reveals . Every contains all self-loops. The clique covering number is the least number of subcliques (sets with an edge between any two members) that partition the contexts; .
UCB1.CL keeps, for every arm and context , the number of rewards of arm in context observed before round and their sum . In round it pulls an arm maximising
breaking ties arbitrarily. The pseudo-regret is .
For every , every context sequence and every UCB1.CL arm process,
These are the paper's and with the constants of its proof.
With complete cross-learning () Theorem 1 gives regret , independent of the number of contexts; with no cross-learning () it recovers the of independent UCB1 instances; in between, the clique covering number interpolates. The bound applies to bidding in first-price auctions with discretised values and bids, and the paper's lower bounds (Theorems 5–6) show that a dependence on graph invariants of the CL graphs cannot be removed in general.
The result is proved in the paper; nothing about it is formalized. A machine-checked proof would add to the platform its first contextual bandit with cross-learning, its first regret bound in terms of a clique cover, and a Hoeffding inequality for rewards sampled at rounds chosen adaptively by an algorithm, which is reusable in every UCB-type analysis. The formal statements also record corrected versions of four printed slips in the proof (listed under Formalization scope).
The standard UCB1 analysis counts, per arm and context, the pulls made before the arm has been observed times, and pays for each context. Summed over contexts this gives a bound linear in , which is exactly what cross-learning should avoid. The difficulty is that an observation of arm in context may come from a pull in another context, so the per-context counts are coupled through the CL graph and do not decrease independently. Lemma 3 handles this through a linear system over the cliques of a minimum clique cover, and Lemma 4 needs concentration for samples collected at random times determined by the algorithm itself.
Arms and contexts are Fin K and Fin C with . The reward process R t ω i c is defined for all ; the hypotheses are measurability, independence of the round vectors (iIndepFun), values in , and identical distribution of each coordinate across rounds. Contexts are a deterministic sequence ctx : ℕ → Fin C. G i c c' is the edge of , with all self-loops assumed. Rounds are 0-based in Lean (Lean's round is the paper's round ). The UCB index is EReal-valued, at ; the logarithm is natural and the algorithm knows .
The selection rule is a property of the arm sequence: in every round the pulled arm maximises the index, which reads only the rewards observed before round ; ties are arbitrary. The arm of round must be a measurable function of the rewards of earlier rounds. The regret is the expected pseudo-regret of p. 17, summed over all rounds.
Repairs relative to the page: is a positive lower bound on the positive gaps (as printed it is ); the gap-dependent constant is Lemma 3's , without the extra factor of (5); (4) carries on each right-hand side; throughout; Lemma 3 is pathwise for any arm sequence; the Hoeffding step is restricted to the event that the -th observation occurs within the horizon. Lean's , so every statement using restricts to positive gaps.
The formalization rules out the trivializing readings: the index cannot read the means, the gaps or unobserved rewards; the selection property is satisfiable (an explicit sequence exists); is a minimum over labellings whose classes are cliques, so it equals without cross-learning and with complete cross-learning; all constants are absolute.
Not part of the mission: Lemmas 1–2 (comparisons of graph invariants), Theorems 2–3 (EXP3.CL and EXP3.CL-U for adversarial rewards), Theorems 4–10 (lower bounds and the learning-to-bid applications) and the conjecture of Appendix D. Contributions of the optional-skipping Hoeffding inequality as a general lemma, and of clique-cover combinatorics on Fin C, are welcome and reusable.
Nonlinear conic programming covers nonlinear programming (NLP), nonlinear semidefinite programming (NLSDP) and nonlinear second-order cone programming (NSOCP) in one model: minimize a smooth objective subject to the requirement that a smooth map takes values in a closed convex cone. The classical first-order necessary condition, the Karush–Kuhn–Tucker (KKT) condition, holds at a local minimizer only under a constraint qualification such as Robinson's, and for conic constraints such qualifications are restrictive and hard to check.
Sequential optimality conditions avoid this. They require only that approximate KKT points exist along a sequence converging to the candidate, and they hold at every local minimizer with no constraint qualification. They are also what practical algorithms actually produce, since an algorithm only ever stops at an approximate point. For NLP, AGP was introduced by Martínez and Svaiter (2003) and CAKKT by Andreani, Martínez and Svaiter (2010); Andreani, Haeser and Martínez (2011) compare the sequential conditions. R. Andreani, W. Gómez, G. Haeser, L. M. Mito and A. Ramos (Mathematics of Operations Research, 2022) extend AGP and CAKKT to general conic programs, by means of projections onto the cone and its polar. They then show that a safeguarded augmented Lagrangian method generates sequences satisfying them. This mission formalizes that convergence theory (Section 4 of the paper).
Let and be continuously differentiable, where is a finite-dimensional real inner product space. Let be a nonempty closed convex cone, and consider
A point is feasible if . The polar cone is . For a closed convex set , denotes the orthogonal projection of onto (its nearest point). is the adjoint of the derivative of at .
A feasible satisfies AGP (Approximate Gradient Projection) if there are sequences and with
It satisfies CAKKT (Complementary Approximate KKT) if moreover, on the same sequences, .
The augmented Lagrangian is for . Algorithm 1 takes positive tolerances , a nonempty convex compact safeguarding set , and constants , , . At step it:
A point and a function satisfy the generalized Łojasiewicz inequality if, for some and some continuous on with as ,
If is a feasible limit point of a sequence generated by Algorithm 1, and satisfies (28) for , then
Theorem 4.1 shows that the augmented Lagrangian method, with no constraint qualification at all, produces AGP points. AGP was previously the condition behind inexact restoration methods, so this puts the two method families on a common footing. Theorem 4.2 adds the complementarity limit (18) under the generalized Łojasiewicz inequality. Every analytic function satisfies that inequality. For NLSDP the theorem refines the earlier guarantee that such methods generate TAKKT sequences. Combined with the paper's result that every local minimizer is a CAKKT point, it says the algorithm's limit points pass a necessary optimality test that is sharper than AGP. The theory allows cones with empty interior or without self-duality, such as the cone of Euclidean distance matrices.
The results are proved on paper. No machine-checked version is known. Formalizing them needs a working theory of projections onto closed convex cones in finite-dimensional inner product spaces: existence, nonexpansiveness, Moreau's decomposition, and the differentiability of the squared distance. It also needs derivative calculus for the augmented Lagrangian. These are reusable well beyond this paper, by any later formalization of conic optimization algorithms.
The algorithm is stated with free choices at every step, so nothing about it can be computed. Everything has to come from the inequalities that define a run. The main obstacle is the case of an unbounded penalty parameter in Theorem 4.2. In that case the multipliers may diverge, and it is not clear why should vanish. Without (28) it need not: the paper points to a counterexample in which the method produces sequences that are not CAKKT. The bounded case needs instead the observation that the Step 4 test forces once the penalty stops growing. The calculus milestones depend on the differentiability of , which is not in Mathlib in this form.
EuclideanSpace ℝ (Fin n), and is any finite-dimensional real inner product space.ContDiff ℝ 1.MoreauProx.Decomposition.Cones. The polar uses the sign .fderiv ℝ G x, and is Mathlib's gradient.IsALRun on the produced sequences . Every free choice of the page stays free. The convention is encoded as . The initial point plays no role and is omitted.MapClusterPt). In (28), is the open ball and is the operator norm of the derivative.Contributions are welcome on the convex-projection layer: existence and uniqueness of , nonexpansiveness, Moreau's decomposition (posed separately on the platform as MoreauProx.Decomposition.cone_decomposition), and the gradient of the squared distance. They are also welcome on the two case analyses of the convergence proofs.
Learning-augmented algorithms use a machine-learned prediction to perform better when the prediction is accurate, while keeping a worst-case guarantee when it is not. The two guarantees are called consistency (performance under a correct prediction) and robustness (performance under an arbitrary prediction). Agrawal, Balkanski, Gkatzelis, Ou and Tan (arXiv:2204.01120v1; Mathematics of Operations Research, 2024) brought this framework to mechanism design, where the input is reported by strategic agents and the designer must also keep reports truthful.
Their test case is facility location in the plane. Agents report preferred locations and a mechanism places one facility. Without predictions, the coordinatewise median achieves a -approximation for the average distance (Meir, 2019), which the paper reports as optimal among deterministic strategyproof mechanisms; the strategyproof mechanisms in the plane were characterized by Peters, van der Stel and Storcken (1993). A prediction of the optimal location can be used to beat , but only by giving up robustness. This mission targets the paper's exact description of that trade-off.
Timeline.
There are agents. Agent has a preferred location ; the profile is . The plane carries the Euclidean distance . Placing the facility at costs
the utilitarian social cost. An optimal location is any point minimizing (a geometric median of ).
The lower median of real numbers is the -th smallest of them. The Coordinatewise Median with Predictions takes a prediction and a confidence such that is an integer. It adds copies of to the agents' points and returns , the point whose -coordinate is the lower median of the -coordinates and whose -coordinate is the lower median of the -coordinates. At this is the coordinatewise median.
A mechanism is -consistent if for every profile, and -robust if for every profile and every prediction . The approximation ratio of CMP on an instance is .
For every , every with , every profile , every optimal location of and every prediction ,
The constants are exact: Lemma 8 shows both are attained, so no weaker goal would be the paper's theorem.
The paper's proof reduces every instance to a one-parameter family. The milestones follow it:
The COA classes contain the instances with , CMP output , and all points in for one .
The result. Theorem 9 gives a one-parameter menu of guarantees. At both bounds equal Meir's . As consistency tends to while robustness grows without bound. The paper's Theorem 10 shows that no deterministic, strategyproof, anonymous mechanism improves on this menu (Pareto optimality), and its Theorem 12 refines the bound as a function of the prediction error, building on Theorem 9. It is one of the first exact consistency–robustness trade-offs for a mechanism design problem.
Formalizing it. The theorem is proved in the paper; nothing about it is machine-checked. A formal proof would check a reduction argument that runs over several pages and many cases (Lemmas 15–25, Appendix A). It would also check two delicate conventions on which the bounds rest: the lower median of values, and the Euclidean metric. The model layer (Euclidean utilitarian cost, the geometric median as a minimizer, coordinatewise medians with phantom points) is reusable for other planar facility-location mechanisms.
The cost is not a convex or even continuous function of the profile, because the median jumps. So the worst case cannot be found by local optimization over the profile, and the geometric median has no closed form. The paper instead transforms an arbitrary instance into a structured one step by step. Each step must keep three things under control at once: CMP's output, the optimal location (which can move when points move), and a ratio that may only increase. Several steps change the number of agents or regroup clusters (the four-fold copying after Lemma 7, the instances invoked in the proofs of Lemmas 21 and 22), so the argument is not an induction over a fixed . The obvious approach, the triangle inequality agent by agent, needs a bound on in terms of ; but the median is controlled by counts of points, not by distances, and bridging the two is exactly what the reduction does.
All declarations live in the namespace LearnAugFL.CMP, in one definitions module and one module per theorem.
EuclideanSpace ℝ (Fin 2), with the Euclidean dist. Profiles are P : Fin n → Pt; CMP depends only on the multiset of points.cmp P ô k: each coordinate is the lower median of the agents' coordinates together with k copies of the prediction's. Admissible c n k states and , so the constants are functions of the same that fixes .IsOpt P o (a minimizer of ), not a chosen function. Every statement quantifies over every optimal location; geometric medians of collinear profiles need not be unique.ratio P ô o k appear only in the reduction lemmas. There, the families force a positive optimal cost, so no ratio is a junk .Trivializing encodings are ruled out explicitly:
ℝ × ℝ carries the sup metric, under which the bounds are a different statement.Contributions welcome: proofs of the milestones in any order; facts about the lower median of a multiset under insertion of phantom values; and first-order optimality of the geometric median (a subgradient characterization), which Lemma 26 and the instances of Lemma 8 need and Mathlib does not have.
This paper is devoted to systematic study of properties of the quantum entropy and of the Holevo capacity considered as a function of a set of quantum states. The properties of restriction of the quantum entropy to arbitrary set of states are discussed. For some types of sets necessary and sufficient conditions of boundedness and of continuity of restriction of the quantum entropy as well as necessary and sufficient conditions of existence of the Gibbs state are obtained. The Holevo capacity of an arbitrary set of states and its general properties as a function of a set are considered. The notion of the optimal average state of an arbitrary set of states with finite Holevo capacity is introduced. The condition of existence of optimal measure for a set of states is obtained. The general results concerning the quantum entropy and the Holevo capacity are illustrated by considering the several examples of sets of states.
This mission is the statement-level formalization of Entropic characteristics of subsets of states (arXiv:quant-ph/0510073v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
41 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (Theorem 1, PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
30 results of the paper are not stated yet, because the library lacks an interface they need:
Degradable quantum channels are among the only channels whose quantum and private classical capacities are known. As such, determining the structure of these channels is a pressing open question in quantum information theory. We give a comprehensive review of what is currently known about the structure of degradable quantum channels, including a number of new results as well as alternate proofs of some known results. In the case of qubits, we provide a complete characterization of all degradable channels with two dimensional output, give a new proof that a qubit channel with two Kraus operators is either degradable or anti-degradable and present a complete description of anti-degradable unital qubit channels with a new proof. For higher output dimensions we explore the relationship between the output and environment dimensions ( and respectively) of degradable channels. For several broad classes of channels we show that they can be modeled with a environment that is "small" in the sense . Perhaps surprisingly, we also present examples of degradable channels with ``large'' environments, in the sense that the minimal dimension . Indeed, one can have . In the case of channels with diagonal Kraus operators, we describe the subclass which are complements of entanglement breaking channels. We also obtain a number of results for channels in the convex hull of conjugations with generalized Pauli matrices. However, a number of open questions remain about these channels and the more general case of random unitary channels.
This mission is the statement-level formalization of The structure of degradable quantum channels (arXiv:0802.1360v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
37 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4: complete degradable qubit-output structure (original paper seed) (Theorem 4: complete degradable qubit-output structure (original paper seed), PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
Channel capacity describes the size of the nearly ideal channels, which can be obtained from many uses of a given channel, using an optimal error correcting code. In this paper we collect and compare minor and major variations in the mathematically precise statements of this idea which have been put forward in the literature. We show that all the variations considered lead to equivalent capacity definitions. In particular, it makes no difference whether one requires mean or maximal errors to go to zero, and it makes no difference whether errors are required to vanish for any sequence of block sizes compatible with the rate, or only for one infinite sequence.
This mission is the statement-level formalization of Tema Con Variazioni: Quantum Channel Capacity (arXiv:quant-ph/0311037v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
35 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract and Sections 2–7: equivalent quantum capacity definitions (Abstract and Sections 2–7: equivalent quantum capacity definitions, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Coding theorems in quantum Shannon theory express the ultimate rates at which a sender can transmit information over a noisy quantum channel. More often than not, the known formulas expressing these transmission rates are intractable, requiring an optimization over an infinite number of uses of the channel. Researchers have rarely found quantum channels with a tractable classical or quantum capacity, but when such a finding occurs, it demonstrates a complete understanding of that channel's capabilities for transmitting classical or quantum information. Here, we show that the three-dimensional capacity region for entanglement-assisted transmission of classical and quantum information is tractable for the Hadamard class of channels. Examples of Hadamard channels include generalized dephasing channels, cloning channels, and the Unruh channel. The generalized dephasing channels and the cloning channels are natural processes that occur in quantum systems through the loss of quantum coherence or stimulated emission, respectively. The Unruh channel is a noisy process that occurs in relativistic quantum information theory as a result of the Unruh effect and bears a strong relationship to the cloning channels. We give exact formulas for the entanglement-assisted classical and quantum communication capacity regions of these channels. The coding strategy for each of these examples is superior to a naive time-sharing strategy, and we introduce a measure to determine this improvement.
This mission is the statement-level formalization of Trade-off capacities of the quantum Hadamard channels (arXiv:1001.1732v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Unnumbered main result: Hadamard CQE single-letterization (Unnumbered main result: Hadamard CQE single-letterization, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
We give here a self contained and elementary introduction to the Conley-Zehnder index for a path of symplectic matrices. We start from the definition of the index as the degree of a map into the circle for a path starting at the identity and ending at a matrix for which 1 is not an eigenvalue. We prove some properties which characterize this index using normal forms for symplectic matrices obtained from geometrical considerations. We explore the relations to Robbin-Salamon index for paths of Lagrangians. We give an axiomatic characterization of the generalization of the Conley-Zehnder index for any continuous path of symplectic matrices defined by Robbin and Salamon.
This mission is the statement-level formalization of The Conley-Zehnder index for a path of symplectic matrices (arXiv:1201.3728v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
43 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Classical integer Conley–Zehnder index: degree construction, independence and determinant parity (Classical integer Conley–Zehnder index: degree construction, independence and determinant parity, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
8 results of the paper are not stated yet, because the library lacks an interface they need: