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?
Decision analysts routinely have to rank two risky prospects, with returns and , when nothing is known about them beyond a mean and a standard deviation for each. The classical tools are of two kinds. First-order stochastic dominance (FSD) ranks above for every increasing utility, but it can never be certified from means and variances alone: with only the first two moments fixed, the admissible laws of and include pairs that FSD does not rank. Mean–variance rules such as the Sharpe ratio rank everything, but lack a general expected-utility justification. Müller, Scarsini, Tsetlin and Winkler (Ranking distributions when only means and variances are known, Operations Research 69(3), 2021; SSRN 3440103) close the gap by restricting the utilities: they bound the ratio of marginal utilities, and they ask how strong that bound must be for every pair of laws with the given moments to be ranked.
The relevant order between the two extremes is almost first-order stochastic dominance (AFSD), introduced by Leshno and Levy (Management Science, 2002) to rule out "pathological" utilities that FSD must accommodate. Müller, Scarsini, Tsetlin and Winkler (Management Science, 2017) discuss that this symmetric case of their order is AFSD, i.e. the order generated by utilities whose marginal utilities differ at most by a fixed factor. Leshno and Levy computed the smallest parameter for which one given pair of laws is ranked; the present mission concerns a bound that holds for all pairs with prescribed means and variances.
Fix . The utility class consists of continuously differentiable with
For and real random variables , dominates by -SD, written , if for every . The symmetric case is -AFSD with : gives FSD, and gives the increasing affine utilities, i.e. ranking by means. Increasing shrinks and makes the order easier to satisfy.
Write for the means and for the standard deviations, and
The quantity is a standardized advantage of over ; decreases from at towards as .
The proof works with the piecewise-linear utilities and , with , and with the closed forms
the paper's worst-case values of and given the moments, and the point .
For square-integrable with ,
The goal quantifies over all with the given moments; nothing about their laws is fixed. The upper bound is the domain of the order in Definition 1(b).
PricingRM.DetHeuristic.gallego_bound (the case ).The result. Theorem 7 turns two summary statistics into an expected-utility guarantee: once exceeds the value making , every decision maker whose marginal utility varies by at most the factor prefers , concave or not. It complements the paper's Theorems 3 and 6, which restrict to concave and to convex utilities and give tight bounds in and ; the class contains utilities that are neither, and both standard deviations enter. The paper's Example 8 shows the practical use: with the rule "" settles a project choice for a whole team with heterogeneous, non-concave preferences. The authors note that the bound of Theorem 7 is not tight; the tight constant is open in the paper (Remarks 9–10).
Formalizing it. The result is proved in the paper; none of it is formalized. A formal development produces a reusable definition of the bounded-marginal-utility-ratio class and of AFSD in Mathlib's probability language, distribution-free bounds on expectations of piecewise-linear functions of a square-integrable variable, and a machine-checked version of the threshold. The Scarf/Gallego bound, which the proof uses twice, is already proved on the platform.
The obvious argument fails at the first step: a stochastic dominance relation is usually checked through distribution functions, but nothing about the distribution functions of and is known. For concave utilities (Theorem 3) Jensen's inequality disposes of entirely, which is why that bound ignores ; for the symmetric class no such step is available, both variables must be controlled at once, and the worst case over all laws with given moments must be computed in closed form for a family of utilities rather than for a single one. On the formal side, the normalization step needs the boundedness of to be derived from the ratio condition (there is no supremum hypothesis), the bounds need integrability of for an unbounded , and the threshold computation is real algebra with nested square roots.
Random variables are measurable functions on one probability space , with MemLp X 2 P and MemLp Y 2 P in the goal; only their laws matter. Means are Bochner integrals and with Mathlib's variance, never free reals in the goal. "Continuously differentiable" is ContDiff ℝ 1 and is deriv u. The order SDle carries and integrability of and , because the identity utility is in the class. It compares the expectations for every utility in the class for which both compositions are integrable. This excludes Lean's zero value for a non-integrable integral from a comparison, while keeping the order reflexive when ; every class utility is integrable under the goal's hypotheses. Divisions follow Lean's ; when the paper's is undefined, Lean gives and , and the goal then asserts dominance for increasing affine utilities only, which is true. The worst-case quantities and are stated as the inequalities the proof uses; attainment (the two-point laws) is not formalized.
A trivializing formalization is ruled out: the goal is stated for every in the class, not only for or at a fixed ; for every pair with the moments as hypotheses, not for chosen laws; and with , since for the class contains only constants.
A complete development needs: the mean value inequality for deriv; integrability of Lipschitz functions of an variable; the Gallego bound (available); and elementary real algebra with Real.sqrt. The utility class, the order, and the bounds on , are reusable for Theorems 3 and 6 of the same paper and for other almost-dominance results. Proofs of any milestone, alternative proofs of the goal, and formalizations of Theorems 3 and 6 are welcome.
Energy-efficiency and emission standards for products such as vehicles and appliances are set by regulators whose jurisdictions overlap a single manufacturer's markets. The best-known case is United States fuel-economy regulation. California has long been allowed to set stricter vehicle standards than the federal government, and the 2019 dispute between California and the federal administration over a single "50-state" standard put the question of split versus unified markets on the policy agenda. A manufacturer facing two different standards can sell two product versions (a split market), sell one version that meets the stricter standard everywhere (a unified market), or withdraw from the stricter market.
Han, Hu and Dawande (Curbing Emissions: Environmental Regulations and Product Offerings Across Markets, Manufacturing & Service Operations Management, 2022) model this as a game between an environmentally concerned regulator, an environmentally agnostic regulator, and a monopolist. They ask when the market splits, and whether negotiation between the regulators can unify a split market and lower total emissions. This mission formalizes their answer for one negotiation format, the exact global standard (§4.1.1), together with the base-model results it rests on. Citations refer to the authors' accepted manuscript of 28 July 2022, including its Online Appendices.
A monopolist sells in two markets of sizes . Regulator sets a minimum efficiency standard for products sold in . Consumers' valuations are uniform on . A consumer with valuation who buys a product of efficiency at price receives , where is the efficiency bonus, and buys when this is positive. Producing efficiency costs per unit plus a fixed setup cost per product.
Regulator maximizes consumer utility in minus . Here is a benchmark efficiency, is the perceived per-unit environmental impact, and the sum runs over both markets. Regulator maximizes consumer utility in only and therefore sets . The total emissions are .
Given , the firm chooses among three strategies: (differentiated products at and ), (one unified product at in both markets), and (one product at , sold in only). Each product is priced at . A base-model outcome is a standard together with a profit-maximizing strategy of the firm, such that cannot do better with another standard paired with any profit-maximizing response.
In the exact-standard negotiation, and agree on one standard for both markets and a transfer from to . Their total utility is (eq. (4)). The disagreement point is the pair of utilities at the split-market base outcome, and the negotiated pair maximizes the Nash product over the feasible pairs that split the gain equally.
Assume condition (1) of Lemma A.1, where is the larger root of an auxiliary quadratic:
Then a split-market base outcome exists. For every such outcome, the negotiation has a Nash bargaining solution, and every solution has standard
The regulators' total utility at strictly exceeds , and total emissions at are strictly lower than at the split-market outcome.
The result. Proposition 3 shows that, whenever the base model predicts a split market under the paper's sufficient condition, two regulators who negotiate an exact global standard with side payments always reach agreement. The agreed standard unifies the market and lowers total emissions. The negotiated standard coincides with the standard a neutral arbitrator would choose. This makes the exact global standard the benchmark against which the paper compares its other negotiation formats (a baseline global standard, and vertical negotiation with the firm). It also qualifies the policy debate: unification through an exact standard requires the stricter regulator to give up its power to exceed the common standard.
Formalizing it. The proofs in Online Appendix C are short computations in which several steps are "straightforward" or "easy to show". In particular, the existence and use of , the comparison between strategies at the regime boundaries, and the truncated branch of Proposition 2 are argued only briefly. A machine-checked development fixes the equilibrium notion, including how ties between strategies are treated, and verifies every inequality. To our knowledge none of these results has been formalized before.
The algebra of each step is elementary, but the base equilibrium is a bilevel object. optimizes over against a firm response that switches between three regimes at and , and 's utility is a different concave quadratic in each regime. Showing that the split outcome sits at requires comparing the maximum over the regime with the maxima over the and regimes. Only the third term of condition (1), through the implicitly defined , controls the comparison. Simply substituting the closed forms of Lemma A.1 into the negotiation does not prove the goal: the goal quantifies over every split-market base outcome, so the characterization of the base equilibrium must actually be established. The emissions comparison also needs a strict inequality. At the emissions in are equal and only changes, and the case must be excluded using condition (1).
All quantities are real numbers in one parameter record , and every statement assumes the standing assumptions of §3: , , , and . The formalization departs from or adds to the page in these places:
A trivializing formalization is ruled out: the goal does not take the disagreement point from Lemma A.1's closed form or compare two formulas. It reads the disagreement point off an arbitrary split-market base outcome, asserts that one exists, and characterizes the negotiated standard through the Nash-product maximization. A sorry-free verification file checks that the goal's hypotheses hold together at a concrete parameter point (, , , , , , ).
The development needs only real algebra: quadratics, square roots and case analysis over three strategies. The lemmas on piecewise-quadratic best responses, and on the reduction of a transferable-utility Nash bargaining problem to total-utility maximization, may be reused for other regulator–firm models. Proofs of any milestone are welcome. Propositions 4 and 5 (baseline global standard, vertical negotiation) and the unified half of Proposition 2 are outside this mission.
Securities traders commonly pay for clearing and settlement after a trade is executed. A fee that is the same for every transaction is simple to administer, but processing a transaction between customers of the same broker can cost less than processing one between brokers. Degryse, Van Achter, and Wuyts ask whether charging everyone the same fee, or charging each transaction its processing cost, leads traders to make the trades that create the most total value. Their answer depends on the processing cost and on how traders' choice of limit-order quotes changes the next trader's choice. The October 2016 working paper develops this question in a single-security limit-order market; this mission uses its preprint page and result numbering.
In each period, one risk-neutral trader arrives. She is a buyer with probability and values the security at , or a seller with probability and values it at , where . Each trader belongs to one of brokers, with equal arrival shares. A limit order offers one unit at a quoted bid or ask. It remains available for one period, so only the next trader can accept it. A market order accepts the standing quote immediately. The next trader may instead post her own limit order. Broker affiliations are visible, so a trader can choose a quote that attracts counterparties at every broker, called the all strategy, or only counterparties at her own broker, called the own strategy. The market description and tie rules appear in §3 of the working paper, pp. 8–9.
A trade within one broker is internalized; its processing cost is normalized to zero. A trade across brokers costs the post-trade service provider per leg. The uniform fee structure charges on each leg of every trade, while the trade-specific structure charges zero on an internalized leg and on a cross-broker leg. These are the fee schedules analyzed in §4, pp. 10–13. They alter the gains from accepting a standing quote, and therefore the quotes that traders choose to post. A trader indifferent between a market order and a new limit order chooses the market order; a limit-order trader indifferent between attracting all brokers and only her own chooses all brokers.
The model tracks three possible actions in an order-flow chain: posting a limit order, executing an internalized market order, and executing a non-internalized market order. A stationary distribution gives their long-run frequencies. A trade's price transfers value between buyer and seller, while processing uses real resources. Thus expected welfare per period is
This is the stationary-distribution form of Equation (6) in §5 and the Appendix, pp. 14–15 and Appendix pp. 1–2. It also gives welfare zero if no trade occurs.
The goal is Corollary 3 of the working paper, p. 16. Two cost thresholds divide the outcomes:
For , the all strategy gives strictly higher welfare than own, and both fee structures induce all. For , all gives at least as much welfare; uniform fees induce all, while trade-specific fees induce own. For , own gives strictly higher welfare; trade-specific fees induce own and realize higher welfare than uniform fees. At , all and own have equal welfare. The two fee structures still induce different strategies there. The paper says that only uniform fees achieve the maximum in its middle range; at the equality endpoint, both welfare values attain the same maximum, so the formal statement preserves the equality and the distinct strategy choices.
Seven milestones support this target, in the paper's order. Equation (1) is the indifference system that optimal limit-order quotes satisfy. Proposition 1 classifies the equilibrium strategy under uniform fees, Equation (5) locates the cost at which the limit-order profits of all and own coincide under trade-specific fees, and Proposition 2 classifies the trade-specific equilibrium. Appendix Equation (A3) gives the stationary distributions of the two order-flow chains, Equation (7) their trading rates, internalization rates and welfare, and Equation (8) the cost at which the two welfare levels agree. The proposition milestones also identify the resulting quotes and spreads; the welfare goal retains the paper's comparison of actual equilibrium outcomes.
The distinction between the privately chosen strategy and the socially preferred one is operational: trade-specific fees can steer traders toward broker-only trading before that is best for total welfare, while uniform fees can leave them targeting every broker after broker-only trading becomes preferable. The theorem identifies the exact cost ranges in which each mismatch occurs. Its thresholds depend on the number of brokers and the spread in buyer and seller valuations. These claims, including the fact that neither fee schedule is best for the whole cost range, are stated in Corollary 3 and the discussion following it, pp. 16–17.
The result is proved in the paper. The remaining task here is to formalize its equilibrium classification and stationary welfare comparison in Lean, then give the published mathematical statements machine-checked proofs. The mission reuses a published finite-chain stationary-distribution definition; its three-state welfare accounting can serve related trading models, while the exact fee schedules and quote formulas belong to this paper's setting.
The equilibrium cannot be found by comparing the welfare formulas alone: traders maximize their own expected limit-order profits. Whether a quote is accepted changes discretely when it crosses a counterparty's market-order threshold, and the value of posting the counterparty's new limit order is itself an equilibrium value. A quote attractive to all brokers and a quote attractive only to the same broker may each be optimal in different cost ranges. The analysis must also respect the paper's tie rules at both switching thresholds. Once the strategies are classified, the two three-state chains have different stationary trading frequencies, so a fee comparison at a fixed trade volume would not answer the question.
Lean represents as a natural number with and all money amounts as real numbers. The standing assumptions are and ; the latter expresses that the zero internalized cost is lower than the non-internalized cost. Division in threshold and quote formulas uses the real cast of . A market order is chosen at equality, and an optimal all-broker quote is preferred at an all-versus-own tie. An equilibrium is a stationary pair of buyer and seller continuation values, each an attained greatest expected limit-order profit given the other. Optimal quotes determine the strategy; strategy labels are not defined by the cost thresholds.
The transition matrix has state indices for limit, internalized market, and non-internalized market orders. A stationary distribution uses the published finite-chain definition: it is nonnegative, sums to one, and is a fixed row vector of that matrix. The printed third row of Appendix (A2) is all zeros even though the text calls the matrix stochastic. The formal matrix sends that unreachable state back to state ; this changes no stationary probability in (A3). Welfare is calculated from the stationary distribution and true processing costs, not assigned one of the closed formulas in Equation (7). The goal quantifies over equilibrium continuation values and stationary distributions, while the milestones assert their existence and identify the distributions. Contributions that establish these equilibrium, finite-chain, and threshold results are within scope.
Boards and audit committees use formal controls to limit the resources that an executive can divert. Controls can also change the executive's decision: a CEO who values her future reputation may comply when the remaining opportunity to divert is too small. Penno's diversion model puts these two effects in one decision problem. It asks how much costly control the authority should buy when it does not know in advance which CEO type it will draw. The answer depends on the chance of drawing a reputation-sensitive CEO and on the strength of that CEO's career concerns. Penno calls their product tone at the top.
The source for this mission is the May 2019 revision of Penno's SSRN working paper. Its Proposition 1 gives an explicit optimal control level and the corresponding temptation threshold for the high CEO type. The result belongs to a theoretical accounting model; the mission concerns that model's mathematical assertion, rather than an estimate of actual control costs or misconduct.
An authority chooses a formal control level before a CEO sees a temptation . The temptation is uniform on , where . If the CEO diverts resources, the authority loses ; if the CEO complies, it loses none to diversion. The authority also pays the direct cost , with . The control domain is : full control has infinite cost in the paper.
A CEO has type , with . The high type is drawn with probability and the low type with probability . For a CEO of type , diversion gives utility and compliance gives utility , where and . Define . The high type diverts when exceeds her tipping point ; the low type diverts for any positive temptation. The paper assumes so that the high type can divert under some control levels.
Write for the authority's expected loss: the expected amount diverted, averaged over both CEO types and the uniform temptation, plus . When , both types can divert. At and above that boundary the high type never diverts, so only the low type contributes to expected diversion. The definition of in this mission starts from the CEO's utility comparison and integrates the resulting diverted amount. This preserves the decision mechanism underlying the two closed forms in the paper's appendix.
Under the standing model assumptions and the two conditions of Lemma 1, let . Proposition 1 states that the unique optimal control and its high-type tipping point are
Both branches include equality at ; their values agree there. The formal goal states that the displayed control belongs to and has strictly less expected loss than every other admissible control. The paper's printed formula can be negative for sufficiently large , even when Lemma 1 holds. The goal therefore adds the necessary condition , which ensures that the first branch remains an admissible control.
The milestone list follows the model's tipping point (5), the two expected-loss formulas, the convexity and increasing-loss assertions of Lemma 1, and the appendix's first-order and branch-threshold equations. These are source claims used to identify the optimizer, with their original indices and page provenance.
The result describes when stronger reputational incentives accompany more formal control and when they allow the authority to reduce it. The threshold separates an interior solution, where the high type can still divert at sufficiently large temptations, from a boundary solution that keeps the high type compliant throughout the support of . The accompanying expression for makes the behavioral meaning of each branch explicit. Penno uses the result to discuss the relation between tone at the top and formal control in the basic diversion model.
The paper supplies an analytic proof. This mission seeks machine-checked proofs of the same optimization claim and of its supporting statements. Its definition of expected loss also provides a small reusable example of a two-type decision model with a choice-dependent threshold inside an integral. The mathematical result is known from the paper; its Lean proof remains the work of the mission.
A direct optimization of alone misses the expected diversion term, while treating the high type as always compliant misses the change of behavior at . The loss is piecewise because the high type's tipping point can move past the upper end of the temptation interval. A complete argument must establish the two losses from the utility-based diversion rule, control their behavior on the correct intervals, and compare the candidate in the first interval with their shared boundary. The value also needs separate attention: ordinary real division assigns a value, whereas the paper assigns infinite cost to full control.
Lean uses real parameters bundled in Params, together with the standing inequalities of §3. It represents uniform temptation by an interval integral of the diverted amount with density . The CEO diverts exactly when her diversion utility is strictly greater than her compliance utility. At equality, the formal model takes compliance; that single threshold point has no effect on the integral. The high type's tipping point is the unconstrained value , which can exceed even though realized temptations cannot.
All optimization statements use . This agrees with the source convention and avoids treating Lean's real division by zero as a finite control cost. The added inequality is disclosed in the goal and is needed only to keep the printed interior formula nonnegative. There is no assumption that is nonnegative: the source only requires . The first part of Lemma 1 is strict convexity; its second part is expressed as strict increase, as stated in the appendix proof.
The development needs Mathlib's interval integrals, real square root, and real convexity and monotonicity predicates. Contributions that establish the integral closed forms, the behavior of the two loss regions, and the global optimality claim are within scope. A definition that merely hard-codes the appendix's closed forms as , or a goal about an unconstrained control, would lose the CEO choice and the authority's actual feasible set.
Blockchain platforms and decentralized autonomous organizations take governance decisions by token-weighted voting: an account's influence grows with the governance tokens it stakes. Two problems are associated with this design (Buterin 2021). The first is plutocracy: holders of many tokens control decisions. The second is the Sybil attack (Douceur 2002): accounts are pseudonymous, so one person can split her tokens over many identities. A rule that dampens the influence of large stakes — for example votes proportional to the square root of tokens — invites exactly this splitting, because the dampening is undone by holding many small stakes.
Mohan, Khezr and Berg (SSRN 4259599; Management Science 2024, doi:10.1287/mnsc.2023.01536) set up a model in which votes depend on two resources, staked tokens and time commitment. They characterize Sybil resistance (Theorem 1), show that token weighting alone cannot be both plutocracy- and Sybil-resistant (Theorem 2, the Plutocracy–Sybil dilemma), and propose bond voting, in which votes are bought with voting bonds that lock tokens until maturity. This mission formalizes the paper's main positive result: bond voting is robustly v-implementable (Proposition 2).
A platform fixes a maximal commitment horizon . A vote function turns a stake of tokens locked for units of time into votes, with (Definition 1). It values commitment if , and has non-increasing influence of tokens if and , for all and (Definitions 2, 3).
An agent with budget and payoff function chooses . A Sybil attack with identities assigns stakes and commitments . It is feasible if and every , and profitable if its payoff strictly exceeds what the agent obtains as a single entity (Definition 5). A payoff function is Sybil resistant if no budget admits a feasible and profitable attack (Definition 6), and a mechanism is robustly v-implementable if its vote function values commitment, has non-increasing influence of tokens, and is Sybil resistant (Definition 7).
Bond voting. The platform sets a voting bond rate . A -bond costs tokens, returns them at maturity, and carries one vote, so a budget buys votes. An agent of type — marginal pivotality , value of the policy, outside return on her tokens — receives benefit and bears the opportunity cost , so for
Agent types are admissible when and .
For every rate and horizon ,
The goal quantifies over every admissible agent type and every budget, and leaves and free.
The result. Proposition 2 shows that a second voting resource, time, can be added to token voting without reopening the Sybil problem: bond votes are linear in tokens, so splitting across identities earns nothing, while voters with a low opportunity cost of locking tokens, or a strong stake in the outcome, gain influence through longer commitments. Together with Theorem 2, which shows that token weighting alone cannot dampen large holdings without inviting Sybil attacks, it is the paper's case for bond voting as a governance mechanism.
Formalizing it. The result is proved on paper; it has no machine-checked proof. Formalization adds two things beyond a check. First, it fixes the definitions the paper leaves implicit: the payoff of a multi-identity attack, and which single-entity commitment a profitable attack must beat. Second, it states Proposition 1 precisely: the printed third case of equation (6) ( when ) has no maximizer, because the payoff tends to as but is at . The goal is stated so that it remains true for those agent types.
The mathematics is elementary real analysis; the difficulty is in the definitions. The naive reading of Definition 5(c) compares an attack with the agent's payoff at a fixed commitment . Under that reading the "if" half of Theorem 1 fails: an agent with a suboptimal gains by moving her whole budget to one identity with a better commitment. Comparing with the formula instead fails in the third case of (6). The statement holds when the attack must beat every commitment the agent could choose herself, and proving it then requires handling agent types with no optimal commitment, where Proposition 1 cannot be invoked. Discontinuity of at also rules out arguments that take a maximum over the compact interval .
Everything is real-valued (ℝ), with Real.exp and Real.log. Identities are indexed by Fin M; (no identities) and identities with zero stake are allowed. Derivatives in Definitions 2–3 are encoded with HasDerivAt witnesses, not with deriv, so a non-differentiable function cannot satisfy them by default values. The payoff of an attack is the sum of the identities' payoffs, as computed in the paper's proofs (pp. 16, 25). An attack is profitable only if it beats every single-entity commitment , including (not voting). Bond votes and payoffs are at , as the paper imposes. The hypothesis is added: the paper never states the sign of , and Definition 2 fails without it.
Fixing the single entity's commitment to , or proving Sybil resistance only for agent types covered by Proposition 1 cases 1–2, would be a trivializing formalization of the goal; the goal quantifies over all admissible types and all single-entity commitments.
Theorem 1 is stated "given Assumptions 1 and 2" for mechanisms with non-increasing influence of tokens; milestone 4 drops these hypotheses because its proof uses only linearity and the boundary conditions. Not formalized: Theorem 1's "only if" direction (its proof uses a fixed single-entity commitment and equates nonlinearity with strict concavity), Theorem 2 and Corollaries 1–4, Remarks 1–4, Proposition 3, and the numerical sensitivity analysis of §3.3. All definitions live in one file in the namespace BondVoting.Sybil; the attack and resistance definitions are stated for an arbitrary payoff function and can be reused for other voting rules, such as quadratic voting.
Grothendieck introduced the notion of a motive in a letter to Serre in 1964. Among all the objects he was privileged to discover, he wrote, this one appeared to him the most charged with mystery, and the yoga of motives perhaps the most powerful instrument of discovery he had brought to light. The source — James Milne's expository article "Motives — Grothendieck's Dream" — explains what motives are and why Grothendieck valued them so highly. The many good cohomology theories of algebraic geometry — singular, étale, de Rham, crystalline — cannot come from an algebraically defined Q-valued theory, yet they behave as though they did: traces of regular maps are rational and independent of the theory. Grothendieck's answer is a universal cohomology theory with values in a Q-linear category of motives: every good cohomology theory should factor uniquely through it. The construction passes through algebraic cycles modulo an adequate equivalence relation and correspondences; the category so obtained is additive and pseudo-abelian, carries a tensor product satisfying the Künneth formula, and its first computed decomposition is the motive of the projective line, h(P¹) = 𝟙 ⊕ 𝕃, whose endomorphism ring is as small as possible; the trace of the identity on a motive is the Euler-Poincaré characteristic, and the first zeta computations — the point and the projective line — exhibit the mechanism that the Weil conjectures later vindicated in general. The same trace calculus, however, contains the obstruction that Grothendieck's dream runs against: the trace of the identity on the motive of a curve of genus g is 2 − 2g, which is negative for g ≥ 2, so no fiber functor can exist on the category of effective motives and the category cannot be tannakian.
The mission formalizes the definitions and the proved structural theorems of Sections 4-7 of the source: the algebra of correspondences, the category of effective pure motives with its composition, addition, tensor structure, and pseudo-abelian splitting, Grothendieck's decomposition of the motive of the projective line, the trace of the identity as the Euler characteristic, the zeta functions of a point and of the projective line, and — as the goal — the tannakian obstruction: the category of effective motives admits no fiber functor in the presence of a curve of genus at least 2.
The source is an expository article; the mission formalizes the fragment consisting of the correspondence algebra and the category of effective pure motives (Sections 4-6), the trace calculus (Section 6, page 10), and the first two zeta computations (Section 7), under the following disclosed conventions.
Fourteen conventions deserve disclosure. First, the platform publishes definitions as modules, so the three definition bundles — the correspondence world, the effective motives, and the zeta coefficients — are published as platform definitions (Milne_world, Milne_motives, Milne_zeta) and attached to the proposal as reference items; the theorem drafts import them; and the creation script reads the definition code and the theorem statements directly from the repository modules that the CI has just compiled, so the code posted to the platform is byte-identical to the code whose compilation the CI verified. Second, algebraic geometry is abstract: no varieties, algebraic cycles, Chow groups, or cohomology theories are constructed, since Mathlib has none of this; the primitive datum is a world of correspondences (CorrWorld) — varieties with a product, a designated point, a projective line, and a curve of every genus, and for each pair of varieties a Q-vector space of correspondences carrying a degree function into the integers, composition, diagonals, transposes, exterior products, Künneth idempotents, and trace data — with the moving lemmas and the well-definedness of the products of cycle classes living in the interface fields, so that every theorem carries the world as a hypothesis. Third, correspondences are presented ungraded, with the grading recovered through the degree function: the graded pieces Corr^r(X, Y) are the degree-r elements, and morphisms of motives are the degree-zero correspondences of the source's f ∘ Corr⁰(X, Y)Q ∘ e. Fourth, rational coefficients are baked into the interface: the correspondence spaces are Q-vector spaces, the source's tensoring of cycle groups with Q is not repeated. Fifth, the mission lives in the effective category: the paper's second attempt of Section 5; the twist integer m of h(X, e, m), duals, and the full category M~(k) are out of scope. Sixth, morphisms are rendered as fixed points: the sandwiched image f ∘ Corr(X, Y)_Q ∘ e is the subtype of correspondences γ with f ∘ γ ∘ e = γ and degree zero, which coincides with the image when e and f are idempotent. Seventh, the closure of the sandwiched subspaces under the operations (composition, addition, zero, negation, scalar multiplication, exterior product) is imposed through interface axioms, since these are the stability statements that make the morphism spaces well defined. Eighth, direct sums are stated through the five biproduct identities rather than as an equality with a direct-sum object; the pseudo-abelian splitting is stated through the same identities, with the complement and image summands h(X, e − f) and h(X, f) as the explicit witnesses. Ninth, the tensor structure is defined on objects and morphisms through the exterior product, and the Künneth formula is stated at the level of motives: hX ⊗ hY = h(X × Y). Tenth, the Künneth idempotents of the projective line and of the curves of every genus, the diagonal decompositions Δ = e₀ + e₂ and Δ = π₀ + π₁ + π₂, and the trace values 1, −2g, 1 of the pieces — the signed Betti numbers, so that the trace of the identity is the Euler characteristic — are interface data: the source's computations from the intersection ring of the projective plane and of a curve are thereby carried as hypotheses. Eleventh, the trace of the identity on an idempotent motive is defined through the interface-supplied evaluation and coevaluation correspondences, its additivity over idempotent splits is an interface axiom, and the duality zigzag equations of the source are not stated. Twelfth, the fiber functor is rendered as a concrete structure FibFun — a dimension for each motive, an action on morphisms, preservation of identities and composition, multiplication of dimensions over tensor products, and the identification of the trace of the identity with the dimension of the fiber; exactness and faithfulness are deliberately not hypothesized, because the tannakian obstruction needs only the trace-dimension identity, so the goal theorem is formally stronger than the source's formulation — the strengthening is disclosed — and the fibers are Q-vector spaces, whereas the source allows any field F of characteristic zero. Thirteenth, the zeta function is rendered through its Taylor coefficients via a course-of-values prefix recursion equivalent to the source's logarithmic definition log Z(X, t) = Σ N_m t^m / m; the point counts 1 and 1 + p^m of the point and of the projective line are carried as data, and no finite fields are formalized. Fourteenth, everything is developed against the platform's Mathlib build (0df444a); the read-backs attached to the theorem drafts were authored by the same model that produced the statements (readback_model glm-5-latest-short); they are a self-check, not an independent audit, and human review of every item is required before submission.
Eleven items: three published definition bundles attached as references, seven milestone theorem drafts, and the goal theorem.
The formalized fragment is the additive and tensor skeleton that every theory of motives shares, together with the trace calculus and the first two zeta computations, and it ends with the obstruction that gives the mission its point: as long as the trace of the identity on the motive of a curve is its Euler characteristic, no fiber functor can exist, so the category of effective motives is not tannakian and cannot be the representation category of an affine group scheme — the reason the source gives for passing to larger categories of motives. Formalizing the skeleton with every geometric input isolated as an explicit interface hypothesis produces a reusable shape: the same statements admit any future Mathlib development of algebraic cycles as an instantiation.
The categorical skeleton is pure algebra: associativity, units, biproduct identities, the interchange law, and the splitting of idempotents follow from the interface axioms by equational reasoning; the trace computation is additivity over the Künneth decomposition together with the supplied trace values; the zeta computations are inductions on the coefficient recurrence; the goal is the contradiction between a negative trace and the nonnegativity of a dimension. The difficulty is the discipline of the interface — no statement may silently use a geometric fact that has not been assumed — and the bookkeeping of the course-of-values recursion against the geometric expansion of the reciprocal of (1 − t)(1 − p t).
Every item quantifies only over the objects it needs — worlds, motives, morphisms, idempotents, genera, point-count sequences. The goal carries a genus parameter together with the hypothesis that the genus is at least two; every world contains a curve of every genus by the interface, so the hypothesis is satisfiable, and it states the source of the obstruction — the middle Künneth summand of a curve of genus at least two has negative trace. This binder is disclosed here rather than left unstated. The negation-free statements produce witnesses: biproducts, splittings, and decompositions produce their morphisms; the zeta identities are equalities of coefficients; the goal is a negation, as is proper for an obstruction. The fragment excludes the twist m ∈ ℤ, duals, rigidity, and tannakianity as a positive property (Sections 5-6), the abelian category M_num and its semisimplicity, Conjectures C and D and the standard conjectures (Section 6), the zeta function of a motive via characteristic polynomials of Frobenius and the Hasse-Weil bound (Sections 2, 7-8), motivic L-functions, the big modularity conjecture, and the conjecture of Birch and Swinnerton-Dyer (Sections 8-9), and mixed motives (Section 10) — everything the source conjectures rather than proves, and everything requiring cohomological realization, is out of scope. The mission formalizes what the source proves.
In 1923 Hardy and Littlewood proposed two conjectures about the distribution of primes that have shaped a century of analytic number theory. The first — the prime -tuple conjecture — predicts that every admissible prime constellation occurs with a precise asymptotic density: the number of constellations with base point grows like , where the singular series constant is an explicit Euler product over the residues of the offsets modulo the primes. For the twin offsets this specializes to the twin prime conjecture with the twin-prime constant . The second conjecture asserts that the prime-counting function is subadditive: . Richards proved in 1974 that the two conjectures are incompatible — at most one of them is true. The source file states all three results in Lean 4: the two conjectures as open problems, and the incompatibility as a theorem.
The mission takes the first conjecture — the file's title statement, and the one widely believed — as its goal. It formalizes the conjecture's definitional core (prime constellations, admissibility, counting functions, the singular series), and curates as milestones the structural facts any proof must engage: the translation-invariance of admissibility, its necessity for primality, the vanishing count for inadmissible tuples, the divergence of the logarithmic-integral model, the positivity of the singular series, the infinitude consequences down to the twin prime conjecture, and Richards' incompatibility with the second conjecture.
The arena is the set of prime constellations: tuples of primes with even gaps, encoded by a function of offsets with . A constellation is admissible when its entries do not form a complete set of residue classes modulo any prime; the counting function counts admissible constellations with base point at most ; the singular series is with the number of residues occupied by the offsets modulo ; and the conjecture asserts for tuples with distinct offsets.
Nine conventions deserve disclosure. First, the platform publishes definitions as modules Definitions.Def_<definition_name>, so the three definition bundles — constellations and admissibility, counting functions, and the asymptotic layer with the singular series — are published as platform definitions (HardyLittlewood_constellation, HardyLittlewood_counting, HardyLittlewood_series) and attached to the proposal as reference items; the theorem drafts import them. Second, asymptotic equivalence is phrased through a self-contained definition — f ~ g when the difference is little-o of g — rather than an external asymptotic-equivalence notation; the formulation coincides with the classical ratio limit when the model sequence is eventually positive and unbounded, and it degenerates correctly: for an inadmissible tuple the singular series is zero, the model vanishes identically, and the conjecture asserts exactly that the counting function is eventually zero, which is the true degenerate content. Third, the counting functions are defined as the cardinalities of finite sets of natural numbers (noncomputable, Classical), with counting primes up to and including , matching the source's phrasing. Fourth, admissibility is split: the source's constellation-level condition is kept verbatim, and the parameter-free condition on the doubled offsets (IsAdmissibleTuple) is added beside it; the equivalence — residue coverage is invariant under translation by the base point — is the mission's first milestone, so nothing is assumed that is not proved. Fifth, the residue count is taken on the offsets themselves, exactly as the source's numResidues; at every odd prime this agrees with the count for the doubled offsets , and the product runs over the primes with the source's normalization and prefactor. Sixth, the singular series constant is defined through the unconditional infinite product; its convergence and positivity are not assumed anywhere — they are the content of a milestone, and the hypothesis that makes the product converge (pairwise distinct offsets) is stated there explicitly, since a repeated offset forces every factor to be and the product to diverge. Seventh, a curation decision: the goal is the first conjecture; the second conjecture is deliberately not drafted as a provable item, because Richards' theorem — itself a milestone — shows that the two cannot both hold; the second conjecture appears as a definition and inside the incompatibility milestone. Eighth, the goal is stated for every tuple, with the conjecture's own hypotheses ( and pairwise distinct offsets) inside the predicate, exactly as the source file states it. Ninth, the read-backs attached to the drafts were written by the same model that produced the statements (readback_model glm-5-latest-short), not by an independent auditor; the human item-by-item comparison against the source remains the main defense against an unfaithful formalization.
The goal is the first Hardy–Littlewood conjecture for every tuple. The supporting chain, in attack order, each step a milestone except the last:
The chain assembles: admissibility is the gatekeeper (necessity and vanishing), the model integral and the singular series are the two analytic quantities the conjecture relates, positivity and divergence turn the asymptotic into infinitude, the twin case is the celebrated concrete consequence, and Richards' theorem fences off the second conjecture.
The prime -tuple conjecture is the strongest concrete prediction about the distribution of primes that is consistent with current knowledge: it implies the twin prime conjecture, the Sophie Germain-type infinitudes, and every admissible pattern one can write down, each with a precise constant. It sits at the edge of the circle method — the same machinery that yields the ternary Goldbach theorem for additive patterns — and its obstruction is exactly the correlation between primes that current technology cannot rule in. A Lean formalization of the conjecture's statement, together with the surrounding structural facts, fixes the target unambiguously and gives solvers an attack path whose every waypoint is independently valuable: each milestone is a theorem of lasting interest in the theory of prime constellations, and the Richards incompatibility is a landmark result of 1974 that the community can be proud to carry.
The milestones span elementary number theory (residue coverage, admissibility, the twin-configuration check), real analysis (the divergence of the logarithmic integral), analytic number theory at the research frontier (the convergence and positivity of the singular series, via Mertens-type estimates), and combinatorial asymptotics for Richards' incompatibility. The admissibility lemmas are of moderate difficulty; the divergence of the model integral is a standard exercise in integral comparison; the positivity of the singular series requires the classical estimate that the Euler product converges on distinct offsets; the Richards milestone requires constructing, from the conjectured density of a suitable long admissible constellation, an interval carrying more primes than subadditivity permits — a research-grade formalization. The goal itself is one of the great open problems of number theory; the mission's value lies in the precisely stated target and the independently valuable waypoints, exactly the role of an OpenProblem mission.
Every item quantifies only over the objects it needs — offset tuples, base points, primes, bounds; no item carries a vacuous hypothesis: the twin configuration is admissible, the conjunctions of the conjecture are satisfiable, and the vanishing and incompatibility statements are the intended degenerate truths. The fragment excludes the second Hardy–Littlewood conjecture as a provable target (Richards' theorem makes it a trap), excludes no case of the first conjecture (it is stated for every tuple, exactly as the source), and adds no hypothesis to the conjecture beyond the source's own. Nothing in the mission asserts the truth of the first conjecture or of the twin prime conjecture; it formalizes the statements precisely, together with the implications among them that are known.
Sensitivity and block sensitivity measure how a Boolean function responds to changes in its input. They are central examples of query complexity measures: an algorithm learns an unknown input by querying its individual coordinates, while these measures describe how many changes the function can detect at a single input. Understanding their relationship helps distinguish the complexity caused by individual coordinate changes from the complexity caused by changes to groups of coordinates.
The Block Sensitivity vs. Sensitivity campaign tracks the largest certified separation exponent. Its classical benchmark is a quadratic separation. OpenAI problem 132 supplied a superquadratic construction and a Lean formalization in 2026. Subsequent campaign entries reached 2.0391, 2.05, and 2.0635. This entry establishes the exact exponent using the same definitions and quantifiers.
A total Boolean function assigns an output bit to every input of bits:
For an input and a coordinate set , let denote the input obtained by flipping precisely the coordinates in . The sensitivity at an input counts the individual coordinates whose flips change the output:
The block sensitivity at an input, denoted , is the largest number of pairwise disjoint nonempty coordinate sets such that flipping any one of them changes the output at . The sets are tested separately, always starting from the same input. The corresponding global measures are
The maxima range over all inputs, including inputs on which the output is zero and inputs on which it is one. No monotonicity, symmetry, or restriction on the number of variables is imposed.
For every real and every integer , establish the existence of a dimension and a total Boolean function with
The campaign predicate SensitivityCampaign.AchievesExponent (2.075 : ℝ) states this exact proposition. The decimal is interpreted exactly, as , rather than as an approximate floating-point value. The function and dimension may depend on both the exponent loss and the requested threshold .
The threshold quantifier is essential: the target concerns arbitrarily large sensitivity. A small isolated function, or a collection of functions whose sensitivity stays bounded, does not by itself establish the campaign statement. The use of an arbitrary positive exponent loss agrees with the campaign's other entries and allows their values to be compared directly.
This result increases the certified exponent beyond the campaign's 2.0635 entry. It provides an intermediate achieved bound toward the separate 2.10 research target. It does not assert that 2.10 has been reached or identify the optimal exponent.
The complete Lean proof has compiled successfully, passed local kernel replay, and been accepted by Prove2Me. The verified theorem and full proof establish the stated target. Its supporting development includes nine-predicate sensitivity estimates, bounds on joint changes of nested predicates, finite labeling existence, disjoint sensitive-block witnesses, and an exact integer certificate. The accompanying proof explanation describes how these ingredients establish the stated target. The finite-certificate and logarithmic-score theorems from the campaign foundation remain referenced as reusable milestones.
A construction must have many disjoint sensitive blocks at one input while keeping sensitivity small at every input. A large block family supplies only the lower-bound half of this requirement. An input that makes many individual coordinates sensitive can invalidate the global upper bound even if the intended block-witness input behaves well.
Joint boundary behavior is another constraint: analyzing several related predicates independently can lose information about which changes can occur together. The formal proof therefore needs correct sensitivity estimates for the actual input-coordinate flips throughout the construction. Numerical growth estimates must also account for every fixed overhead before they can certify a finite exponent inequality.
The function type is (Fin n → Bool) → Bool. Sensitivity and block sensitivity use the existing OAI.Paper320 definitions, imported through Definitions.Def_SensitivityCampaign. Both measures are natural numbers defined using maxima over finite collections. The exponent comparison casts them to real numbers and uses real exponentiation. Since every requested witness has sensitivity at least two, the base of that power is positive.
The mission retains the shared campaign definitions without modifications. The two foundation milestones are SensitivityCampaign.finite_certificate, which turns suitable finite sensitivity and block-sensitivity bounds into the asymptotic target, and SensitivityCampaign.finite_certificate_log, which expresses the same interface using a logarithmic score. Their normalization and unbounded-sensitivity conclusions are part of their proved statements.
The supplied proof targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The supporting assertions are proved in the submitted source; no conjectural lemma or numerical approximation is used as an assumption. The general transfer estimates and exact certificate provide material for subsequent improvements, while this mission's goal remains the fixed campaign value 2.075.
f80a3f37-72fa-4d56-a094-3e4d351764f3. The present development reuses its foundation, including its earlier source credits.People receive both informative reports and messages that are unrelated to the truth. A standard question in social learning is whether sharing beliefs helps a population identify the correct state. The question changes when everyone knows misinformation exists but does not know its ideological direction. Mostagir and Siderius study this setting and show that the ranking of two learning rules changes with the amount of misinformation: Bayesian updating can be at least as reliable at low levels, while simple averaging is more reliable at sufficiently high levels under full support. Their result is stated as Theorem 1 of the SSRN working paper, later published in Management Science.
The comparison matters for models of collective decisions because the same population, news quality, and misinformation distribution can lead to different rates of wrong terminal actions solely because the agents process others' beliefs differently. The paper's question is therefore about the behavior of learning rules, not just the accuracy of any one message. The mission covers the paper's regime comparison; its separate results on hazard rates, polarization, and targeting are outside this target.
The unknown state is either or . An organic message matches the state with probability . A fraction of all messages consists of misinformation. Its split is the fraction of misinformation advocating ; has distribution with density . Agents start with heterogeneous prior probabilities of state , distributed according to a continuous law . The paper assumes these priors and the split are independent. All comparisons concern the limit of a large population, where the observed fraction of each message type is determined by and (§2, pp. 4–6).
A DeGroot agent first updates on her own message while treating it as organic, using equations (1) and (2) of the paper. Thereafter agents average one another's beliefs. In the large-population model used by the proof, every agent reaches the same consensus : the -average of the two face-value posteriors, weighted by the fractions of and messages. A Bayesian agent treats misinformation as possible and infers the message shares from the population's beliefs. The same observed share can be explained by the true state and split or by the other state with a different split. The posterior weighs these two narratives according to their densities under and the agent's prior (proofs of Lemmas 1–2, pp. 18–19).
An agent's terminal action favors whichever state has posterior belief at least one half. A society mislearns at when a positive -mass of agents favors the wrong state; for DeGroot agents, who share a consensus, this is a single belief comparison. Write and for the -probabilities of Bayesian and DeGroot mislearning. The paper studies both true states; the formulas for mirror those for .
The main target is Theorem 1, p. 10. For every , set
For every continuous symmetric prior law on and every split law supplied by a density, the goal compares both states separately:
The first comparison is non-strict because both mislearning probabilities can be zero, although the preprint uses the word “lower.” The value of comes from the paper's proof, which states the result with an existential threshold. The five milestones state the DeGroot and Bayesian mislearning cutoffs, the necessary misinformation level for Bayesian mislearning, the cutoff difference, and the resulting full-support probability formulas. Their source text and page numbers accompany the individual items.
The theorem isolates a regime in which adding misinformation changes the relative performance of the two learning rules. Under full support, the high-misinformation conclusion is strict: some split realizations cause Bayesian society to mislearn even while DeGroot society learns. The low-misinformation conclusion gives a uniform comparison over every allowed distribution of the split, without requiring its full support (Theorem 1 and proof, pp. 10, 20). These are statements about society-level mistakes, not a claim that an individual averaging rule is always more accurate.
The result has a published mathematical proof. It does not yet have a machine-checked proof in this development. Formalizing it requires a reusable interface for two-state misinformation models: a law of heterogeneous priors, a density for the split, the two narrative splits, posterior beliefs, and mislearning events. Those objects can also support the paper's later questions about the distributional shape of misinformation and the choice of targeting policy.
The obvious comparison of the two update rules at a fixed message fails to settle the result. DeGroot agents act on an average of face-value posteriors; Bayesian agents act on an agent-specific posterior after considering competing explanations of the same population message share. Thus the two groups can be wrong for different split realizations, and a statement about one representative belief does not give a society-level mislearning probability. The comparison must also distinguish a pointwise mistake at the edge of the split support from an event of positive probability. A second issue is that the converse direction of the printed Lemma 2 assumes agents with beliefs arbitrarily close to the extremes, which requires full prior support on (Lemma 2 and proof, p. 19).
Lean uses the paper's large-population formulas directly: is an integral over , and is a density-weighted posterior over the two narrative splits. The Bayesian terminal belief is its period-two posterior; later observations add no information in this model. is a probability measure concentrated on with no atoms. is given by a measurable nonnegative real density whose integral is one and whose support lies in . Full support on an interval means that the density is bounded below there by a positive constant and is zero outside. Symmetry means invariance of under .
The formalized regime has so the cutoffs involving division by are defined as intended; the paper's misinformation-free case is an example outside this theorem. A belief of exactly counts as wrong, matching the weak cutoff inequalities. Mislearning for Bayesian society requires a positive -mass of wrong agents, and the final probabilities are extended nonnegative real measures of split events. The real posterior's zero-denominator default can arise outside the split support, which carries zero -mass; pointwise Bayesian milestones restrict to the support.
The model defines mislearning from posterior beliefs and the law of , so the main theorem cannot be reduced to a comparison of cutoff formulas by definition. Solver contributions may establish measurability and integrability facts for the model, the cutoff lemmas, and the final comparison. The standing interval-support assumptions in the paper are narrowed to where the theorem needs them; the main comparison does not fix arbitrary smaller support intervals.
An online retailer may buy products from suppliers and resell them, or let suppliers sell directly while collecting a commission. The choice changes who sets retail prices and how a wholesale price change for one product affects the prices of competing products. In the first arrangement, the retailer sets all retail prices; in the second, suppliers set their own prices after the retailer chooses a commission. Hu, Zheng, and Pan study how this cross-brand retail pass-through changes the comparison between those arrangements. Their Proposition 2 identifies a sharp split: nonnegative cross-brand pass-through favors agency selling for the retailer, while negative pass-through can reverse the retail-price ordering. The question matters when a retailer must choose a contract for several competing products rather than evaluate a single supplier in isolation. Hu, Zheng, and Pan, SSRN preprint, §§3–5.
There are symmetric suppliers, each with marginal cost . At a common retail price in an open positive interval , the demand for one product is and falls with price. Its demand sensitivity is
The paper assumes that , that has slope less than one, and that . These are the symmetric-price forms of its demand conditions A1, A3, and A4. The model also uses an aggregate diversion ratio : the fraction of the own-product demand response diverted to other suppliers. Under A1, . Hu, Zheng, and Pan, §§3.1–3.2, pp. 7–9.
Let be own-brand pass-through and for be cross-brand pass-through. The total response is . The suppliers' conduct parameters under wholesale and agency selling are respectively
The wholesale retail price and agency retail price are any solutions, in , of the two equations of Lemma 1 after the retailer's marginal cost is normalized to zero. The corresponding wholesale price is , and the agency commission rate is . The profits come from the respective wholesale and agency contract objectives. Finally, §5 defines
These are the quantities in Proposition 2. Hu, Zheng, and Pan, Lemma 1, p. 11; §5, p. 13.
For every pair of equilibrium prices satisfying Lemma 1's equations, Proposition 2(i) asserts that implies
The milestone list includes Proposition 1's comparison of and , the price ordering, and the auxiliary profit comparisons in the authors' proof. Hu, Zheng, and Pan, Propositions 1–2, pp. 12–13; Appendix B, pp. 26–27.
When , the price part of Proposition 2(ii) gives the exact criterion
The milestone for this case is the authors' rewrite of condition (8) in terms of . The paper also says that wholesale selling can be more profitable for the retailer and agency selling may benefit suppliers; those are existence observations illustrated by its examples and are outside this mission's goal. Hu, Zheng, and Pan, Proposition 2(ii), p. 13; Appendix B, p. 27.
Proposition 2 separates two forces in the contract choice. Agency selling avoids the retailer's wholesale markup, while the sign of cross-brand pass-through changes the relative intensity of supplier competition. Under nonnegative pass-through, the paper obtains simultaneous comparisons of prices and both parties' profits. Under negative pass-through, the threshold gives a precise condition for a reversal in retail prices. These conclusions let the two contracts be compared using measurable pass-through responses and the demand curve, instead of treating the number of competing suppliers alone as decisive. Hu, Zheng, and Pan, §§4–5, pp. 12–13.
The result is proved in the source paper. This mission supplies compiled Lean statements and a common definition layer, but no machine-checked proofs of the theorem or its milestones yet. Completing it would verify the equilibrium comparisons under explicit demand and denominator conditions. The auxiliary monotonicity and profit identities can also be reused when studying the paper's later results on supplier preferences and welfare.
The immediate comparison of the two equilibrium price equations does not determine which price is larger: the conduct parameter differs between contracts, and the agency equation contains a cost term with a squared denominator. The paper's assumptions control the slopes of two demand-sensitivity expressions, while the profit comparisons require different auxiliary curves for suppliers and the retailer. In the negative pass-through case, the condition involving must still be combined with the conduct-parameter ordering. These are substantive inequalities; simply unfolding the profit definitions does not give Proposition 2. Hu, Zheng, and Pan, Appendix B, pp. 26–27.
Lean uses real-valued demand on an open, order-connected interval and a natural-number supplier count , cast to the reals in formulas. Derivatives are ordinary derivatives on . The smoothness assumption is there because A3 differentiates an expression containing . Positive demand is explicit; A1 requires . The strict bound follows from the strict total-demand decrease in A1, although the paper prints the weaker interval . The expressions divide only where their denominators are positive: , , and by A3. The paper uses in its proof, so that bound is also explicit. The retailer's marginal cost is fixed to as on p. 12. Hu, Zheng, and Pan, A1–A4, pp. 7–8; Lemma 1, p. 11; Proposition 2 proof, p. 26.
The n-product demand system and Stackelberg games are represented by their conduct-parameter symmetric equilibrium equations from Lemma 1. Every theorem concerns every pair of prices satisfying those equations in ; no existence or uniqueness of such a pair is presumed. The original game and A5's invariant-conduct assumption are not reconstructed. Profits remain the original contract objectives at symmetric prices, rather than being defined by the reduced forms that the proof seeks to establish. The definition layer, demand calculus, and milestone inequalities are all open to proof contributions; the contract-profit identities must be derived from their objective definitions.
The entanglement-assisted classical capacity of a noisy quantum channel is the amount of information per channel use that can be sent over the channel in the limit of many uses of the channel, assuming that the sender and receiver have access to the resource of shared quantum entanglement, which may be used up by the communication protocol. We show that this capacity is given by an expression parallel to that for the capacity of a purely classical channel: i.e., the maximum, over channel inputs , of the entropy of the channel input plus the entropy of the channel output minus their joint entropy, the latter being defined as the entropy of an entangled purification of after half of it has passed through the channel. We calculate entanglement-assisted capacities for two interesting quantum channels, the qubit amplitude damping channel and the bosonic channel with amplification/attenuation and Gaussian noise. We discuss how many independent parameters are required to completely characterize the asymptotic behavior of a general quantum channel, alone or in the presence of ancillary resources such as prior entanglement. In the classical analog of entanglement assisted communication--communication over a discrete memoryless channel (DMC) between parties who share prior random information--we show that one parameter is sufficient, i.e., that in the presence of prior shared random information, all DMC's of equal capacity can simulate one another with unit asymptotic efficiency.
This mission is the statement-level formalization of Entanglement-assisted capacity of a quantum channel and the reverse Shannon theorem (arXiv:quant-ph/0106052v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: entanglement-assisted classical capacity (Theorem 1: entanglement-assisted classical capacity, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
10 results of the paper are not stated yet, because the library lacks an interface they need:
We give a detailed proof of the conjecture that the asymptotic entanglement cost of preparing a bipartite state \rho is equal to the regularized entanglement of formation of \rho.
This mission is the statement-level formalization of The asymptotic entanglement cost of preparing a quantum state (arXiv:quant-ph/0008134v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entanglement cost equals regularized entanglement of formation (Theorem 1 / Eq.(7), continued on PDF p.3, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We develop entanglement-of-formation potentials for feedback-assisted classical communication and one-way randomness distillation. For a finite-dimensional quantum channel without initial shared entanglement, an exact amortization theorem bounds the increase of message information plus entanglement remaining across the communicating laboratories. This proves a classical-feedback capacity bound using a mixed-convex-roof expression previously studied by Winter and Yang in the context of potential capacities. We determine the capacity of flagged mixtures of noiseless and entanglement-breaking channels, improve a published depolarizing-channel converse, and evaluate the new bound exactly for the amplitude damping channel. A state analogue gives a finite-blocklength upper bound on the net shared randomness obtainable with one-way classical communication. Amplitude-damping Choi states provide exact benchmarks, while a full-rank generalized amplitude-damping Choi state demonstrates a useful improvement where we do not evaluate the operational rate exactly. We also distinguish one-way from two-way randomness distillation: a two-round weak-measurement protocol strictly exceeds the exact one-way rate of every nontrivial qubit isotropic state. The protocol preserves quantum side information during its first decoding and extracts additional randomness in the reverse direction. This shows why the one-way state potential is not a general two-way converse. Together, these results establish a common entanglement-based approach to sharper communication and randomness bounds, while revealing how retained quantum correlations enable two-way distillation to surpass one-way limits. △ Less
This mission is the statement-level formalization of Entanglement-of-formation potentials for feedback-assisted classical communication and randomness distillation (arXiv:2610.04831v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2.1: cardinality and attainment (Proposition 2.1: cardinality and attainment, 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.
26 results of the paper are not stated yet, because the library lacks an interface they need:
A new protocol for quantum broadcast channels based on the fully quantum Slepian-Wolf protocol is presented. The protocol yields an achievable rate region for entanglement-assisted transmission of quantum information through a quantum broadcast channel that can be considered the quantum analogue of Marton's region for classical broadcast channels. The protocol can be adapted to yield achievable rate regions for unassisted quantum communication and for entanglement-assisted classical communication; in the case of unassisted transmission, the region we obtain has no independent constraint on the sum rate, only on the individual transmission rates. Regularized versions of all three rate regions are provably optimal.
This mission is the statement-level formalization of A father protocol for quantum broadcast channels (arXiv:quant-ph/0612155v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entanglement-assisted broadcast father inner region (Theorem 2 / Eq. (9), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum error correction (QEC) is an essential element of physical quantum information processing systems. Most QEC efforts focus on extending classical error correction schemes to the quantum regime. The input to a noisy system is embedded in a coded subspace, and error recovery is performed via an operation designed to perfectly correct for a set of errors, presumably a large subset of the physical noise process. In this paper, we examine the choice of recovery operation. Rather than seeking perfect correction on a subset of errors, we seek a recovery operation to maximize the entanglement fidelity for a given input state and noise model. In this way, the recovery operation is optimum for the given encoding and noise process. This optimization is shown to be calculable via a semidefinite program (SDP), a well-established form of convex optimization with efficient algorithms for its solution. The error recovery operation may also be interpreted as a combining operation following a quantum spreading channel, thus providing a quantum analogy to the classical diversity combining operation.
This mission is the statement-level formalization of Optimum Quantum Error Recovery using Semidefinite Programming (arXiv:quant-ph/0606035v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimum recovery is an attained semidefinite program (Abstract; IV, Eq. (22): optimum entanglement-fidelity recovery is an attained SDP, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Many quantum information tasks use inputs of the form , which naturally induce permutation and unitary symmetries. We classify all quantum channels that respect both symmetries - i.e. unitary-equivariant and permutation-invariant quantum channels from to - via their extremal points. Operationally, each extremal quantum channel factors as unitary Schur sampling an irrep-level unitary-equivariant quantum channel the adjoint unitary Schur sampling. We give a streaming implementation ansatz that uses an efficient streaming implementation of unitary Schur sampling together with a resource-state primitive, and we apply it to state symmetrization, symmetric cloning, and purity amplification. In these applications we obtain polynomial-time algorithms with exponential memory improvements in . Further, for symmetric cloning we present, to our knowledge, the first efficient (polynomial-time) algorithm with explicit memory and gate bounds.
This mission is the statement-level formalization of Classification and implementation of unitary-equivariant and permutation-invariant quantum channels (arXiv:2510.08154v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Choi commutants characterize both channel symmetries (Proposition 4, PDF p. 16). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
20 results of the paper are not stated yet, because the library lacks an interface they need:
A robo-advisor is an automated portfolio manager. It invests a client's wealth according to a model of the client's risk preferences, and it learns those preferences by interacting with the client: questionnaires, check-ins, requests to confirm or revise a risk profile. The design question of how often such a system should query its client is practical: each interaction updates the advisor's view of a preference that drifts over time, but each interaction is also exposed to the client's momentary reaction to recent market moves.
Capponi, Ólafsson and Zariphopoulou (Management Science 68(4), 2022; read here as arXiv:1911.01391v2) model this trade-off. Their Proposition 5.1 gives a closed-form approximation of how well the portfolio tracks the client's true risk aversion as a function of the time between interactions, and shows that this approximation has a unique optimal interaction time whose position responds monotonically to the model's parameters. This mission formalizes part (ii) of that proposition and the comparative statics (5.6).
Time is discrete. The client's true risk aversion evolves over the investment horizon; in each period it receives, with probability , an idiosyncratic shock with standard Gaussian and , and no shock otherwise (p. 17). The robo-advisor and client interact every periods. At an interaction the client communicates a risk-aversion parameter that is distorted by a behavioral bias: it is the true value multiplied by , where the coefficient measures the strength of the bias (eq. (5.2), pp. 17–18). Between interactions the advisor keeps using the last communicated value. Market returns have volatility in economic state , and is the volatility in the initial state.
The personalization measure (5.4) is the expected time-average relative error between the advisor's risk tolerance and the client's ,
Lower is better. Proposition 5.1(i) shows that is, up to error terms, a multiple of the approximate personalization measure
The first term is the bias cost, which shrinks as interactions become rarer (the bias averages returns over a longer window); the second is the staleness cost, which grows with the number of shocks missed between interactions. The mission is about , as Proposition 5.1(ii) is. In Lean the parameters are a structure Params with fields sig0 (), pe (), se (), β, and is Rtilde P φ.
Assume , , , and . Then
and is increasing in and and decreasing in and (5.6). "" means that no is a minimizer, decreases strictly on and tends to its infimum .
The proof (Appendix C, p. 46) works with the bracket and an auxiliary function with . The milestones are its displayed claims, in order: ; the two degenerate cases and ; the factorization of ; the value of and the criterion ; the sufficient condition of p. 22; the lower bound , which settles the corner case ; and the interior case , where is strictly convex, tends to , and has a unique zero at which is minimized.
The result gives the model's two qualitative predictions in exact form. Without behavioral bias the advisor should interact at every period; without idiosyncratic shocks it should never interact; when both are present there is a single best interaction frequency, and it moves in the economically expected direction: more bias or more volatile markets call for rarer interaction, more frequent or larger preference shocks call for more frequent interaction. The p. 22 criterion gives a checkable condition, in terms of against , under which interacting at every period is not optimal.
The proof in the paper is a sketch. The convexity of in the interior case is asserted ("it can be shown"), and the comparative statics (5.6) are stated as following from "the form of the function ". As printed, (5.6) asserts strict signs of partial derivatives of , which fail on the open parameter region where the minimizer sits at the corner (there is locally constant). A machine-checked proof therefore supplies the missing convexity argument and the corrected comparative statics. No part of the proposition is known to be formalized.
The function mixes , and a square root of . The sign of its derivative is not visible from the formula, and the paper's sign analysis passes through ; the paper's claim that is strictly convex has no written proof. The comparative statics are not a differentiable implicit-function computation either: the minimizer switches between the corner and an interior root of , and the monotonicity must hold across that switch. The obvious move of differentiating the first-order condition in the parameters covers only the interior region and says nothing at the corner.
All quantities are real. The time between interactions is a real variable on : the model uses integer , but Proposition 5.1 differentiates in and places in . The standing ranges , , , are bundled in Params.Standing. " minimizes " is the predicate IsOptInteraction P φ: and for all ; there is no argmin function, so no junk value can satisfy the goal. Square roots are Real.sqrt, is , and every statement restricts so that no radicand is negative and no denominator vanishes. Derivatives are stated with HasDerivAt and an explicit value. Rtilde P φ takes last, while the page writes both and .
Two readings are fixed. The case "" is: no minimizer exists, is strictly decreasing on , and . The comparative statics (5.6) are stated as monotone comparative statics: if a parameter increases (keeping ), the minimizer moves weakly in the stated direction, and strictly whenever the original minimizer exceeds . The monotonicity clauses quantify over minimizers for both parameter sets, and the existence clause of the goal ensures both exist, so they are not vacuous. Stating the goal about alone, or defining by sInf or by a formula, would trivialize the claim; the goal is about and its minimizers.
Part (i) of Proposition 5.1, which relates to with unquantified error terms, is not formalized; neither is the optimal investment strategy of Proposition 4.1. The development needs one-variable real calculus from Mathlib, including square-root and quotient derivatives, monotonicity and convexity on intervals, and limits at infinity. Proofs of the milestones, of the convexity of on all of (which appears to hold without the hypothesis ), and of the derivative form of (5.6) on the interior region are all welcome.
This mission formalizes the question whether the group of interval exchange transformations is amenable, Question 1.6 of Juschenko, Matte Bon, Monod and de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219, p. 4 (doi:10.1017/etds.2016.32), together with the landmark results of the literature on the question.
An interval exchange transformation cuts the circle into finitely many arcs and puts them back in a different order. These maps model the dynamics of polygonal billiards with rational angles, and since Katok–Stepin (1967) and Keane (1975) they have been a central object of ergodic theory. Under composition they form a group, . Two questions about this group are open: whether it contains a non-abelian free subgroup (Katok's question), and whether it is amenable, that is, whether it carries a finitely additive, translation-invariant probability measure on all of its subsets. Amenability would answer Katok's question in the negative, since an amenable group has no non-abelian free subgroup.
Timeline.
Write for the circle (UnitAddCircle). A permutation of is an interval exchange transformation (IntervalExchange.IsIntervalExchange g) when it is right-continuous, has finitely many points of discontinuity, and has finitely many angles . Equivalently, cuts the circle into finitely many half-open arcs and translates each of them. The group (IntervalExchange.IET) is the subgroup of permutations of that they generate; a milestone states that it consists of the interval exchange transformations themselves. For a subgroup , the angle group (angleGroup G) is the subgroup of generated by all angles of elements of , and the rational rank (rationalRank) of a subgroup of is the supremum of the such that embeds in it. For a subgroup of , (IETOf Λ) consists of the elements of all of whose angles lie in .
A mean on a set is a function from the subsets of to with , for disjoint , and . A group is amenable (Garrido.IsAmenable G) when it carries a mean with for all and . An action of on a set is amenable (IsAmenableAction G X) when carries a -invariant mean, and extensively amenable (IsExtensivelyAmenable G X) when the finite subsets of carry a -invariant mean that, for each finite , gives full weight to the finite sets containing .
The milestones use further notions, defined precisely in the definitions item and in their own statements:
IsRecurrentAction) when for every symmetric such and every , the induced walk returns to with probability .extend F X) is its extension to an arbitrary set by direct limits, and an action of on gives the semidirect product (FunctorProduct F G X) acting on . The lamplighter case is (Lamplighter G X).wobbling X) of a metric space consists of the permutations of with .The question is open. A proof settles it positively and, through von Neumann's theorem, answers Katok's question in the negative; a disproof shows that is not amenable.
The milestones are results from the literature, stated as their sources state them. From Juschenko–Matte Bon–Monod–de la Salle: is a group (p. 4); Lemmas 2.1 and 2.2 on extensive amenability; Theorem 1.3 and Corollary 1.4, the functorial criterion; Proposition 5.3, that a subgroup of is amenable if and only if its action on is extensively amenable; Proposition 4.1 and Lemma 4.3, the inverted-orbit reformulations; Theorem 4.2, recurrence implies extensive amenability; Lemma 5.2 and Theorems 5.1 and 1.9, amenability in rational rank at most ; and Theorem 1.10, the Liouville dichotomy, with the steps of its proof: Lemma 5.10, Proposition 5.11 with Lemma 5.13 (realizing as the topological full group of a minimal subshift of polynomial complexity), and Matte Bon's theorem for virtually cyclic groups. The external results these proofs cite are milestones too: Kesten's criterion for a graph (Woess, Theorem 10.6), Lyons–Peres Theorem 2.17 on rough embeddings, Pólya's theorem (already proved on the platform as MarkovMixing.polya_recurrence), the Baldi–Lohoué–Peyrière comparison lemma, and Matte Bon's Theorem 1.2 on topological full groups of subshifts of slow complexity. From Juschenko–de la Salle: Theorem 1.4 on the wobbling group, with coarse embeddings defined by non-decreasing control functions.
Garban's question, whether is extensively amenable for every , and Question 1.11 of Juschenko–Matte Bon–Monod–de la Salle, whether a polynomially growing Schreier graph forces extensive amenability, are stated as open milestones. Each comes with a milestone stating that a positive answer implies the goal.
The result. A proof would make a natural amenable group containing, by Juschenko–Monod and Juschenko–Matte Bon–Monod–de la Salle, finitely generated infinite simple amenable groups, and would answer Katok's question. A disproof would give the first non-amenable finitely generated group of interval exchange transformations; by Theorem 1.9 it would have rational rank at least .
Formalizing it. The definitions of extensive amenability, of the functorial semidirect products , of inverted orbits and recurrent actions, and of wobbling groups are reusable beyond this mission, as are the external probabilistic results (Kesten's criterion, rough embeddings and recurrence). Pólya's theorem is already formalized and proved on the platform (MarkovMixing.polya_recurrence). None of the other landmarks is formalized.
Every known amenability proof for subgroups of passes through Proposition 5.3 and then needs extensive amenability of the action on the circle. The available criterion for extensive amenability is recurrence of the Schreier graphs, which embed into lattices with the rational rank; for these graphs can be transient, so recurrence is unavailable. Garban's theorem shows that the natural strengthening of extensive amenability fails for all transient wobbling actions, and Theorem 1.10 shows that the Liouville route fails in rank at least .
is UnitAddCircle, and permutations act on it by evaluation. is defined as the subgroup generated by the interval exchange transformations, so that its group structure needs no proof inside the definitions; a milestone states that nothing else lies in it. The source's precise definition (“a right-continuous permutation of such that the set , called the set of angles of , is finite”) is read together with its opening phrase, “cutting this circle into finitely many intervals”, so the definition also requires finitely many points of discontinuity: without that requirement a right-continuous permutation with two angles can have infinitely many discontinuities, and the cocycle of Proposition 5.3 would not be finitely supported. Means take values in and are normalized to total mass . Random walks have finitely supported step distributions where the sources say “finitely supported”, and probabilities of events of a walk are finite sums over the step sequences. Recurrence of a Markov chain is return to the starting point with probability , expressed through first-return probabilities. Functors are Mathlib functors from the wide subcategory of FintypeCat on the injective maps to GrpCat with amenable values, extended to a set by the filtered colimit over its finite subsets.
The goal admits no trivializing reading: contains the irrational rotations and the non-rotation exchanges, and Garrido.IsAmenable is the standard notion. The external milestones (Kesten, Lyons–Peres, Baldi–Lohoué–Peyrière) are cited results, stated in the form the sources apply; proofs of them are welcome contributions in their own right.
The problem of converting noisy quantum correlations between two parties into noiseless classical ones using a limited amount of one-way classical communication is addressed. A single-letter formula for the optimal trade-off between the extracted common randomness and classical communication rate is obtained for the special case of classical-quantum correlations. The resulting curve is intimately related to the quantum compression with classical side information trade-off curve of Hayden, Jozsa and Winter. For a general initial state we obtain a similar result, with a single-letter formula, when we impose a tensor product restriction on the measurements performed by the sender; without this restriction the trade-off is given by the regularization of this function. Of particular interest is a quantity we call ``distillable common randomness'' of a state: the maximum overhead of the common randomness over the one-way classical communication if the latter is unbounded. It is an operational measure of (total) correlation in a quantum state. For classical-quantum correlations it is given by the Holevo mutual information of its associated ensemble, for pure states it is the entropy of entanglement. In general, it is given by an optimization problem over measurements and regularization; for the case of separable states we show that this can be single-letterized.
This mission is the statement-level formalization of Distilling common randomness from bipartite quantum states (arXiv:quant-ph/0304196v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
22 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Regularization of the one-way common-randomness trade-off (Abstract and §3: regularized one-way common-randomness trade-off, PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum communications promises reliable transmission of quantum information, efficient distribution of entanglement and generation of completely secure keys. For all these tasks, we need to determine the optimal point-to-point rates that are achievable by two remote parties at the ends of a quantum channel, without restrictions on their local operations and classical communication, which can be unlimited and two-way. These two-way assisted capacities represent the ultimate rates that are reachable without quantum repeaters. By constructing an upperbound based on the relative entropy of entanglement and devising a dimension-independent technique dubbed "teleportation stretching", we establish these capacities for many fundamental channels, namely bosonic lossy channels, quantum-limited amplifiers, dephasing and erasure channels in arbitrary dimension. In particular, we determine the fundamental rate-loss trade-off affecting any protocol of quantum key distribution. Our findings set the ultimate limits of point-to-point quantum communications and provide the most precise and general benchmarks for quantum repeaters.
This mission is the statement-level formalization of Fundamental Limits of Repeaterless Quantum Communications (arXiv:1510.08863v8). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-dimensional teleportation covariance and the Choi commutator (Eqs.(79)–(80), PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
52 results of the paper are not stated yet, because the library lacks an interface they need:
We ask when qubit controls can produce an effective generator that drives every initial state to the same pure state. Lie-algebra closure alone cannot answer this question because it loses the distinction between reversible control and irreversible dissipation. Lie wedges retain this distinction by enforcing nonnegative strengths for dissipative generators. For drift-free qubits with Hamiltonian controls available with either sign and at most one independently actuated dissipator generated by a traceless jump operator, we classify all nontrivial systems into thirteen structural types, or strata. Explicit tests assign each system to a stratum, and necessary and sufficient conditions determine whether its Lie wedge contains a stabilizing generator. These criteria distinguish stabilizable and non-stabilizable systems even when they share the same generated Lie algebra and stratum. In one exceptional stratum, a single dissipative orientation cannot stabilize a pure state even with the available Hamiltonian controls. Averaging two orientations of the same dissipative channel, related by those controls, produces a stabilizing generator. △ Less
This mission is the statement-level formalization of Lie-Wedge Stratification and Pure-State Stabilizability in Single-Channel Qubit Control (arXiv:2610.00046v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 2.7: Dissipation functional with basis normalization (Lemma 2.7, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
33 results of the paper are not stated yet, because the library lacks an interface they need:
The use of quantum resources in the work extraction from a quantum system is an emerging research topic. Recently, [arXiv:2602.22893] established the necessity of measurement coherence for obtaining advantage in work extraction from an unknown isolated quantum system. However, a quantitative relation between the magnitude of this advantage and established measures of measurement coherence is missing. Here, we establish such a connection by introducing a faithful operational quantifier of the work advantage provided by a measurement. We show that measurement coherence is necessary and sufficient for a positive advantage, and derive upper and lower bounds in terms of the robustness of measurement coherence and an norm based coherence measure respectively. Finally, we examine this quantifier of advantage from the resource theoretic perspective. Our results provide an operational characterisation of measurement coherence as a resource for work extraction and reveal a nontrivial relation between its resource content and thermodynamic value. △ Less
This mission is the statement-level formalization of All coherent measurements provide observational ergotropic advantage (arXiv:2609.18735v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (Theorem 1, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We investigate the relaxation dynamics and steady state of a qubit interacting with a coherent environment through an energy-conserving flip-flop interaction within the Markovian repeated-interaction framework. We derive an exact analytical solution for the evolving and stationary state, nonperturbative in the environmental coherence. We show that environmental coherence provides a resource for dissipative state preparation by expanding the set of accessible steady states. In particular, coherent ancillas can increase the system ground- state population beyond that of the bath, corresponding to an effective temperature below the bath temperature, and enhance its steady-state purity, with these effects controlled by the interplay between the system energy scale and the system-ancilla coupling. Nevertheless, we prove that the purity of the system can never exceed the purity of the ancilla. We further analyze the thermodynamics of the protocol and show that environmental coherence can modify and even reverse the natural direction of heat transfer, giving rise to anomalous heat flow. Remarkably, for fixed interaction parameters, the direction of the coherence-induced heat transfer is governed by the relative phase between the system and ancilla coherence, whereas their magnitudes determine the amount of heat exchanged. Our results establish environmental coherence as a resource for controlling steady-state preparation and energy transfer in repeated-interaction dynamics. △ Less
This mission is the statement-level formalization of Coherence-assisted quantum state preparation and thermal control through repeated interactions (arXiv:2610.10794v1). 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 Stationary purity is capped by ancilla purity (Abstract; §III B Eq.(26); Appendix D: ancilla purity cap, PDF p. 19). 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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
Can entangled noise erase entanglement more efficiently than separable noise? Standard robustness restricts the added noise to separable states; generalized robustness allows any state. We prove that the two costs coincide for every two-qubit state and give an explicit full-rank qubit--qutrit state with a strict gap. Positivity under partial transpose (PPT) characterizes separability in both dimensions, so the boundary is not caused by a failure of the PPT criterion. Instead, product-vector geometry permits a rank-one bridge between the two-qubit dual optimizations and supplies a two-dimensional completely entangled subspace for the qubit--qutrit separation. Local isometric embeddings complete the finite-dimensional bipartite classification, also for any fixed multipartite cut. Combined with known three-qubit separation, the result classifies universal equality relative to full separability in all finite multipartite systems. △ Less
This mission is the statement-level formalization of The Minimal Dimension of Entangled-Noise Advantage (arXiv:2609.28367v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
45 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main-text Theorem 1; seed announced in abstract (Main-text Theorem 1; seed announced in abstract, 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.
Randomized measurement protocols give experimental access to low-degree polynomial invariants of a quantum state rather than to the state itself, which raises the question of what the best entanglement criterion is that can be built from finitely many such invariants. In this work we answer this question through convex duality. For each degree we introduce the cone of local unitary trace inequalities that are valid for separable bipartite states in all local dimensions, together with its one-matrix counterparts for Hermitian and positive semidefinite matrices. Each cone is the polar dual of a moment cone; we also determine the minimal combinatorial parametrization of the separable cone. The framework organizes the known moment criteria: the PPT criterion using the first three moments of the partial transposition is the image under an embedding of a Hankel determinant from the positive semidefinite cone to the bipartite cone, which we show to be an extremal ray, and we determine the first nontrivial separable cone completely, finding exactly four extremal rays. The framework allows us to analyze the realignment criterion and its centered (or enhanced) variant. We prove that the even singular value moments of the (centered) realignment matrix are trace invariants, associated with explicit fixed-point-free involutions. Extracting the optimal trace-norm bound from such moments thus becomes a dimension-free truncated moment problem, which we solve in closed form for and relax to a semidefinite program of size for arbitrary . The dual solutions are polynomial minorants of on , and two explicit families, binomial and -weighted, yield hierarchies of separability inequalities. Finally, we compare the criteria against one another and on PPT entangled states. △ Less
This mission is the statement-level formalization of Optimal entanglement criteria from trace invariants (arXiv:2609.29471v1). 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 Abstract / §4.1: separable trace inequalities and their moment polar (Abstract / §4.1: separable trace inequalities and their moment polar, 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.
4 results of the paper are not stated yet, because the library lacks an interface they need: