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?
In the present paper we introduce and study Bosonic Gaussian classical-quantum (c-q) channels; the embedding of the classical input into quantum is always possible and therefore the classical entanglement-assisted capacity C_{ea} under appropriate input constraint is well defined. We prove a general property of entropy increase for weak complementary channel, that implies the equality C_{ea}=C (where C is the unassisted capacity) for certain class of c-q Gaussian channel under appropriate energy-type constraint. On the other hand, we show by explicit example that the inequality C<C_{ea} is not unusual for constrained c-q Gaussian channel.
This mission is the statement-level formalization of Gaussian classical-quantum channels: gain of entanglement-assistance (arXiv:1211.4774v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §3, unnumbered criterion (14): Gaussian c-q iff isotropic K (§3, unnumbered criterion (14): Gaussian c-q iff isotropic K, 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.
3 results of the paper are not stated yet, because the library lacks an interface they need:
Improve the separation exponent between block sensitivity and sensitivity of total Boolean functions. This mission targets ; higher is better.
For every and every integer , the goal asks for a total Boolean function with and . The shared definition SensitivityCampaign.AchievesExponent expresses this requirement. This is an open proof target.
Using a finite certificate. Choose a total Boolean function , an input , and integers . Prove , , and , then apply SensitivityCampaign.finite_certificate. The shared theorem handles normalization and passage to arbitrarily large sensitivity. Direct proofs of the asymptotic goal are equally welcome. Use exact certified bounds; numerical estimates alone do not establish the target.
Background: OpenAI problem 132 and the campaign proposal.
Two natural ways to measure the local instability of a Boolean function can behave differently. One counts individual input bits whose flips change the answer. The other permits several bits to change together, provided the chosen groups are disjoint. Quantifying the largest possible gap is a question in the complexity of total Boolean functions, and the Block Sensitivity vs. Sensitivity campaign tracks concrete lower bounds on its separation exponent.
The task is to establish a specified asymptotic exponent using the campaign's shared definitions. A numerical score for an abstract recurrence is insufficient: the witnesses must be actual total Boolean functions, and the sensitivities must become arbitrarily large. This mission records one completed construction checkpoint and its exact mathematical scope. Earlier accepted results, the original OpenAI construction and the community's intermediate refinements provide the surrounding research history in the campaign references.
A total Boolean function on coordinates is a map defined at every binary input. At an input , a coordinate is sensitive if flipping that bit changes the output. The sensitivity counts these coordinates, and is the maximum over all inputs.
A sensitive block at is a nonempty subset of coordinates whose simultaneous flip changes the output. The block sensitivity is the maximum size of a collection of pairwise disjoint sensitive blocks at that same input. The global value maximizes this quantity over all inputs. Blocks in one witness share an input and must be disjoint as coordinate sets; their sizes need not agree. These conventions are exactly those in the shared foundation mission.
For every real and every integer , establish the existence of a dimension and a total Boolean function such that
The number is an exact finite decimal. The witnesses may depend on both and . This is the campaign proposition , and the main theorem instantiates its template literally.
A supporting finite-family theorem asserts that, for every natural number , there is a finite total Boolean function with
The associated exact logarithmic quotient is approximately . It is a lower bound supplied by this construction, rather than a determination of the optimal separation exponent. The fixed prefactor is independent of , and the lower bound concerns explicit nonempty pairwise disjoint sensitive blocks at the all-zero input.
Any fixed exponent strictly below gives a literal power separation along functions of unbounded sensitivity. Taking increasing thresholds yields an infinite family whose sensitivities tend to infinity. The theorem does not assert a loss-free inequality at the displayed endpoint, an optimality result, or an improved universal upper bound.
The full construction, its actual Boolean functions and the exponent conversion have passed complete local Lean kernel checks with only the standard three axioms. The shared-labeling lemma is separately accepted and publicly Proved. The main theorem currently has a checked reduction on Prove2Me; the larger finite-family dependency still awaits server acceptance after combined submissions exceeded the300-second verification limit. This mission records the exact proved local statement while preserving that server-status distinction.
The reusable content includes the finite-family statement, the unchanged campaign finite-certificate interface, and the exact exponent conversion. Those interfaces permit later constructions to replace the finite witnesses without changing what the campaign's asymptotic goal means. Source attribution to the original OpenAI development, community contributors and Robin Kothari/Codex is retained in the published proof sources. The new contribution is credited to username yousofy with Codex.
A high block-sensitivity value at one input does not by itself control maximum sensitivity over all inputs. Likewise, a finite example with a favorable ratio does not by itself state the required unbounded-sensitivity family. A valid contribution must account for both requirements. Checking only selected inputs, allowing overlapping blocks, or changing the shared complexity definitions would establish a different assertion.
A large part of the formal verification concerns this connection between finite construction data and actual Boolean functions. Exact integer comparisons also matter: rounded decimal scores and floating-point feasibility checks do not prove the target inequality. Independent source and numerical audits supplement the Lean kernel checks; the authoritative server status of each referenced theorem remains visible separately.
The formalization uses Lean4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Finite input coordinates are represented by Fin n, and Boolean outputs by Bool. The shared SensitivitySeparation definitions count single-bit changes and nonempty pairwise disjoint sensitive blocks. The shared SensitivityCampaign definition quantifies over arbitrary positive real exponent loss and integer sensitivity thresholds.
The published goal has no hypothesis assuming the desired construction, separation, or labeling. In particular, zero-dimensional or bounded-sensitivity examples cannot satisfy the threshold quantifier. Standard real powers are used for the final comparison, while construction certificates are checked using exact natural-number arithmetic. The shared finite-certificate theorems and supporting finite-family statements are included as reference items. Corrections to exposition, independently checked proofs of the same goal, reusable supporting lemmas and genuinely stronger constructions are welcome.
yousofy with Codex, Shared local-lemma labelings: exponent2.1303, Prove2Me,2026. Main statement and proof submissions.Two natural ways to measure the local instability of a Boolean function can behave differently. One counts individual input bits whose flips change the answer. The other permits several bits to change together, provided the chosen groups are disjoint. Quantifying the largest possible gap is a question in the complexity of total Boolean functions, and the Block Sensitivity vs. Sensitivity campaign tracks concrete lower bounds on its separation exponent.
The task is to establish a specified asymptotic exponent using the campaign's shared definitions. A numerical score for an abstract recurrence is insufficient: the witnesses must be actual total Boolean functions, and the sensitivities must become arbitrarily large. This mission records one completed construction checkpoint and its exact mathematical scope. Earlier accepted results, the original OpenAI construction and the community's intermediate refinements provide the surrounding research history in the campaign references.
A total Boolean function on coordinates is a map defined at every binary input. At an input , a coordinate is sensitive if flipping that bit changes the output. The sensitivity counts these coordinates, and is the maximum over all inputs.
A sensitive block at is a nonempty subset of coordinates whose simultaneous flip changes the output. The block sensitivity is the maximum size of a collection of pairwise disjoint sensitive blocks at that same input. The global value maximizes this quantity over all inputs. Blocks in one witness share an input and must be disjoint as coordinate sets; their sizes need not agree. These conventions are exactly those in the shared foundation mission.
For every real and every integer , establish the existence of a dimension and a total Boolean function such that
The number is an exact finite decimal. The witnesses may depend on both and . This is the campaign proposition , and the main theorem instantiates its template literally.
A supporting finite-family theorem asserts that, for every natural number , there is a finite total Boolean function with
The natural number indexes distinct finite construction instances; it is not a dimension bound. The fixed prefactor does not depend on . The associated exact logarithmic quotient is a lower bound supplied by this construction, rather than a determination of the optimal separation exponent.
Any fixed exponent strictly below gives a literal power separation along functions of unbounded sensitivity. Taking increasing thresholds yields an infinite family whose sensitivities tend to infinity. The theorem does not assert a loss-free inequality at the displayed endpoint, an optimality result, or an improved universal upper bound.
The main theorem and its reusable finite-family input have accepted proofs and public Proved status. The exact growth-rate lower bound log(201838849)/log(7922), approximately2.13012479519, is also separately accepted. These facts are recorded with source hashes and acceptance receipts in the accompanying proof package.
The reusable content includes the finite-family statement, the unchanged campaign finite-certificate interface, and the exact exponent conversion. Those interfaces permit later constructions to replace the finite witnesses without changing what the campaign's asymptotic goal means. Source attribution to the original OpenAI development, community contributors and Robin Kothari/Codex is retained in the published proof sources. The new contribution is credited to username yousofy with Codex.
A high block-sensitivity value at one input does not by itself control maximum sensitivity over all inputs. Likewise, a finite example with a favorable ratio does not by itself state the required unbounded-sensitivity family. A valid contribution must account for both requirements. Checking only selected inputs, allowing overlapping blocks, or changing the shared complexity definitions would establish a different assertion.
A large part of the formal verification concerns this connection between finite construction data and actual Boolean functions. Exact integer comparisons also matter: rounded decimal scores and floating-point feasibility checks do not prove the target inequality. Independent source and numerical audits supplement the Lean kernel checks; the authoritative server status of each referenced theorem remains visible separately.
The formalization uses Lean4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Finite input coordinates are represented by Fin n, and Boolean outputs by Bool. The shared SensitivitySeparation definitions count single-bit changes and nonempty pairwise disjoint sensitive blocks. The shared SensitivityCampaign definition quantifies over arbitrary positive real exponent loss and integer sensitivity thresholds.
The published goal has no hypothesis assuming the desired construction, separation, or labeling. In particular, zero-dimensional or bounded-sensitivity examples cannot satisfy the threshold quantifier. Standard real powers are used for the final comparison, while construction certificates are checked using exact natural-number arithmetic. The shared finite-certificate theorems and supporting finite-family statements are included as reference items. Corrections to exposition, independently checked proofs of the same goal, reusable supporting lemmas and genuinely stronger constructions are welcome.
yousofy with Codex, Coupled target and guard profiles: exponent2.1301, Prove2Me,2026. Main statement and proof submissions.A rule that assigns an output bit to every input string can respond differently to changing one bit and changing a group of bits. Sensitivity counts individual changes that affect an output. Block sensitivity permits disjoint groups of coordinates to change separately. Understanding the largest possible difference between these measures is a question about the dependence of Boolean functions on their inputs.
Hao Huang's 2019 theorem established a polynomial relation between sensitivity and polynomial degree, resolving the Sensitivity Conjecture. Determining the sharp quantitative relation between sensitivity and block sensitivity remained a separate problem. OpenAI's 2026 result disproved a universal quadratic bound for total Boolean functions. Subsequent accepted results include the 2.075 theorem by Robin Kothari and Codex and the accepted 2.085 certificate developed for yousofy with Codex. This mission records a stronger quantitative target, 2.119.
A total Boolean function is a map
that assigns an output to every length- bit string. For an input and a coordinate set , let denote the string obtained by reversing exactly the bits in .
A coordinate is sensitive at if . Write for the number of such coordinates, and define
A sensitive block at is a nonempty coordinate set with . Let be the largest size of a family of pairwise disjoint sensitive blocks at the same input, and set
Each member of a block family is flipped separately from the original input. The definitions use finite coordinate sets and finite families of blocks.
The main theorem is
Explicitly, for every real and every natural number , there must exist a natural number and a total Boolean function such that
The formal statement is SensitivityCampaign.AchievesExponent (2.119 : ℝ). Both and may depend on and . The decimal denotes the exact rational number displayed above. The claim includes arbitrarily small positive exponent loss and arbitrarily large sensitivity; neither quantifier is optional.
In particular, the statement gives a fixed exponent 2.118 for functions of unbounded sensitivity, strictly above 2.1. The target is a specific checkpoint in the broader problem of determining the optimal separation exponent. It does not assert that the displayed endpoint is attained without exponent loss.
The target extends these earlier quantitative bounds and crosses the campaign's 2.10 checkpoint. It requires the separation to persist beyond every sensitivity threshold, so a favorable comparison confined to bounded sensitivity would not establish the result. It also leaves the exact optimal exponent unresolved.
The new contribution is a certified finite construction and formal proof within the existing nine-predicate framework. The proof retains the generic development and attribution from Kothari and Codex's accepted 2.075 contribution, including its credit to abhishekdpseok's accepted 2.0635 proof and the earlier OpenAI and community work. The new certificate and its assembly were developed for username yousofy with Codex.
The complete self-contained source has passed standalone compilation in Lean 4.33.1, with only the standard axioms propext, Classical.choice, and Quot.sound. Its numerical certificates and source correspondence have also undergone independent checks. Prove2Me accepted the complete proof on 20 October 2026, submission bb3251a4-f00f-4b06-962a-97be2de5db1b. The public theorem and proof record records its verification status. Further work can examine the proof, improve its reusable interfaces, or establish stronger bounds.
The sensitivity bound must hold at every input. A calculation only at an input supporting many sensitive blocks does not control this maximum. Likewise, a collection of output-changing coordinate sets provides the required block bound only when every set is nonempty and the sets are pairwise disjoint.
The asymptotic requirement creates a separate difficulty. Increasing the dimension alone does not force sensitivity to increase, because added coordinates may be ignored. A complete argument must provide witnesses above every prescribed sensitivity threshold. Finally, the exact rational exponent needs rigorous comparisons: an approximate numerical score alone does not prove the stated inequality.
The shared Lean representation is f : (Fin n → Bool) → Bool, using the definitions in SensitivityCampaign and OAI.Paper320. Sensitivity is the finite supremum over all inputs. Block sensitivity takes the finite supremum over all block families at each input, assigning zero to any family that fails the disjointness, nonemptiness, or output-change conditions. The empty family is allowed.
The target imposes no normalization on or a distinguished input, and it includes no promise restricting the function's domain. Dimensions zero and constant functions are permitted by the underlying types, but cannot satisfy . Natural-number complexity measures are cast to real numbers before real exponentiation. Every positive is included, even when is nonpositive.
The complete source imports Mathlib and the unchanged campaign definition. Existing reusable infrastructure includes the complexity measures, coordinate reindexing results, and the finite-certificate interface. Independent verification, clearer reusable statements, and stronger certified bounds are welcome, while preserving totality, global sensitivity, and the unbounded-sensitivity requirement.
A rule that assigns an output bit to every input string can react very differently to changing one bit and changing several bits together. Quantifying that difference is a basic question about Boolean functions in theoretical computer science. Sensitivity measures how many individual bit changes can affect one output; block sensitivity allows disjoint groups of bits to change separately. The question here is how far apart these two measures can grow.
Hao Huang's 2019 theorem established a polynomial relation between sensitivity and polynomial degree, resolving the Sensitivity Conjecture. The sharper question about the exponent remained. OpenAI's 2026 superquadratic separation ruled out a universal quadratic bound. The subsequent accepted exponent-2.075 contribution by Robin Kothari and Codex provides the established comparison point for this mission. The target is the stronger quantitative bound 2.085.
A total Boolean function is a map
that assigns an output to every length- bit string. For an input and a set of coordinate positions, write for the string obtained by reversing exactly the bits in .
A coordinate is sensitive at when . Write for the number of such coordinates and define
A sensitive block at is a nonempty coordinate set with . Define as the largest size of a family of pairwise disjoint sensitive blocks at that same input, and set
Each block is flipped separately from the original input. All functions and coordinate sets in these definitions are finite.
The main theorem is the campaign statement
Its full meaning is
The exact formal target and its proof status are recorded here. Both the dimension and the function may depend on and . The decimal denotes an exact rational number. The statement permits arbitrarily small positive exponent loss and explicitly requires arbitrarily large sensitivity. For example, choosing gives exponent 2.084 at every requested sensitivity threshold. This is a concrete checkpoint within the broader problem of determining the optimal separation exponent.
The target raises the established exponent bound from 2.075 to 2.085, with the quantifiers stated above. In particular, it supplies a fixed exponent strictly above 2.075 for a family whose sensitivities are unbounded. This distinction matters: a favorable comparison for one finite Boolean function, without an appropriate asymptotic conclusion, would not establish the target.
The new contribution is an eight-layer numerical certificate within the existing nine-predicate framework. Its foundation comes from Kothari and Codex's accepted 2.075 proof, which retains credit to abhishekdpseok's accepted 2.0635 development and the earlier OpenAI and community proofs.
The complete self-contained proof has compiled successfully in Lean 4.33.1. The certificate and its assembly have also passed independent checks. Prove2Me has accepted the complete proof, submission c6096517-61e7-4f51-bc68-c1521d61eb65, on 20 October 2026. The target record is the reference for subsequent verification status. The separate proof explanation supplies the construction details and exact arithmetic.
The sensitivity estimate must hold at every input. Checking only the input that supports many sensitive blocks leaves that requirement unresolved. Likewise, a collection of output-changing sets is insufficient unless its members are nonempty and pairwise disjoint.
The asymptotic quantifiers impose a further requirement: witnesses must exist beyond every sensitivity threshold. Merely increasing the dimension does not establish this, since a function can ignore added coordinates. Finally, the exact rational exponent requires rigorous arithmetic bounds; a numerical logarithm estimate alone does not prove the formal statement.
The shared Lean representation uses f : (Fin n → Bool) → Bool and the definitions in SensitivityCampaign and OAI.Paper320. Sensitivity is the finite supremum over all inputs. Block sensitivity takes the finite supremum over all block families at each input, assigning zero to a family that fails the disjointness, nonemptiness, or output-change conditions. The empty family is allowed.
The target imposes no normalization on or on a distinguished input. Dimensions zero and constant functions are permitted by the underlying types, but cannot satisfy the required sensitivity threshold . Real exponentiation is applied after casting the natural-number complexity measures to real numbers.
The development uses Mathlib and the unchanged campaign definitions. Reusable infrastructure includes the complexity-measure definitions and the finite-certificate interface. Independent verification, clearer reusable statements, and stronger rigorously certified bounds are welcome contributions. Any stronger target should preserve totality, global sensitivity, and the unbounded-sensitivity requirement.
819ad4c6-aa25-48ca-82e9-c8df39c182c0. Theorem and proof record.f80a3f37-72fa-4d56-a094-3e4d351764f3. Theorem and proof record.We find a regularized formula for the entanglement-assisted (EA) capacity region for quantum multiple access channels (QMAC). We illustrate the capacity region calculation with the example of the collective phase-flip channel which admits a single-letter characterization. On the way, we provide a first-principles proof of the EA coding theorem based on a packing argument. We observe that the Holevo-Schumacher-Westmoreland theorem may be obtained from a modification of our EA protocol. We remark on the existence of a family hierarchy of protocols for multiparty scenarios with a single receiver, in analogy to the two-party case. In this way, we relate several previous results regarding QMACs.
This mission is the statement-level formalization of Entanglement-Assisted Capacity of Quantum Multiple-Access Channels (arXiv:quant-ph/0511228v2). 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 QMAC capacity region (Theorem 6, (42)–(44), PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
Building on the ideas in L E Labuschagne, Composition Operators on Non-commutative -spaces, \textit{Expo. Math} \textbf{17}(1999), 429--468, we indicate how the concept of a composition operator may be extended to the context of Haagerup -spaces.
This mission is the statement-level formalization of Composition Operators on Haagerup -spaces (arXiv:math/0603612v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Normal states are epsilon-delta absolutely continuous (Lemma 3.2, 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.
21 results of the paper are not stated yet, because the library lacks an interface they need:
This paper is essentially a lecture from the author's course on quantum information theory, which is devoted to the result of C. H. Bennett, P. W. Shor, J. A. Smolin and A. V. Thapliyal (quant-ph/0106052) concerning entanglement-assisted classical capacity of a quantum channel. A modified proof of this result is given and relation between entanglement-assisted and unassisted classical capacities is discussed.
This mission is the statement-level formalization of On entanglement-assisted classical capacity (arXiv:quant-ph/0106075v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is BSST capacity as an attained mutual-information maximum (§II, equation (4): BSST entanglement-assisted classical capacity, 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.
3 results of the paper are not stated yet, because the library lacks an interface they need:
Collins and Popescu realized a powerful analogy between several resources in classical and quantum information theory. The Collins-Popescu analogy states that public classical communication, private classical communication, and secret key interact with one another somewhat similarly to the way that classical communication, quantum communication, and entanglement interact. This paper discusses the information-theoretic treatment of this analogy for the case of noisy quantum channels. We determine a capacity region for a quantum channel interacting with the noiseless resources of public classical communication, private classical communication, and secret key. We then compare this region with the classical-quantum-entanglement region from our prior efforts and explicitly observe the information-theoretic consequences of the strong correlations in entanglement and the lack of a super-dense coding protocol in the public-private-secret-key setting. The region simplifies for several realistic, physically-motivated channels such as entanglement-breaking channels, Hadamard channels, and quantum erasure channels, and we are able to compute and plot the region for several examples of these channels.
This mission is the statement-level formalization of Public and private resource trade-offs for a quantum channel (arXiv:1005.3818v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Private dynamic capacity: operational region equals the regularized entropic region (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 define classical-quantum multiway channels for transmission of classical information, after recent work by Allahverdyan and Saakian. Bounds on the capacity region are derived in a uniform way, which are analogous to the classically known ones, simply replacing Shannon entropy with von Neumann entropy. For the single receiver case (multiple access channel) the exact capacity region is determined. These results are applied to the case of noisy channels, with arbitrary input signal states. A second issue of this work is the presentation of a calculus of quantum information quantities, based on the algebraic formulation of quantum theory.
This mission is the statement-level formalization of The Capacity of the Quantum Multiple Access Channel (arXiv:quant-ph/9807019v3). 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 Exact capacity region of a finite-dimensional quantum multiple-access channel (Theorem 10, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
A firm can sell a product outright or charge customers each time they use it. Selling collects one payment and transfers the asset to the customer. Pay-per-use service (PPU) keeps control of the asset, earns revenue from each use, and incurs a delivery or operating cost each time. These arrangements coexist for equipment, vehicles, and other products whose useful life contains many potential uses. A firm choosing between them needs to know how production cost and delivery cost affect the profit it can earn in competition. Ladas, Kavadias, and Loch study that question in a two-stage game and derive a threshold for which business model earns more in an asymmetric duopoly equilibrium.
The threshold is a result about competitive earnings, not just customer preference. A service provider can attract customers who need few uses, while a seller can attract customers who expect to use the product often. Each firm's price changes the boundary between those groups. The mission focuses on the paper's base model and its Proposition 3: the comparison of the seller's and service provider's equilibrium profits. The paper proves the result in its 2021 SSRN manuscript; this mission asks for a machine-checked account of that known result.
There are two firms. One sells a product for a single price and pays a production cost for each unit sold. The other charges a price per use. Under the paper's strong pooling assumption, one asset supplies its full capacity of uses, so the provider allocates production cost over those uses. Its effective cost per use is , where is delivery cost per use. The willingness to pay for one use is . The base model assumes that all customers have this same value but differ in desired lifetime usage , uniformly distributed over with density . Sections 2.1–2.3 set out these assumptions.
The customer utilities are from buying and from service. A customer belongs to the seller's segment if buying gives nonnegative utility and at least as much utility as service. A customer belongs to the provider's segment if service gives nonnegative utility and at least as much utility as buying. These conditions define the market segments at every price pair, including prices far from equilibrium. The paper writes both comparisons weakly, so a customer at a tie belongs to both segments. In the relevant equilibria, such ties have zero measure.
The seller's profit is its margin times the mass of its segment. The provider's profit is the average over its segment of usage times margin . Both averages use the uniform density . Firms first select business models and then set prices simultaneously. This mission fixes the asymmetric subgame with one seller and one service provider. A price equilibrium is a pair at which neither firm can increase its profit by changing its own price; the provider's price is constrained by . The comparison is made where the provider is admissible, , as the paper specifies before Proposition 3 and when discussing infeasibility in Section 3.2. The model and game timing appear on manuscript pages 7–9.
Write and for the integral-defined profits at an equilibrium. Proposition 3 gives a production-cost-dependent delivery threshold:
The goal asserts that an equilibrium exists and that every price equilibrium has the stated comparison:
For delivery cost above the threshold, the seller's equilibrium profit is strictly larger. The milestone list follows the paper's Appendix A.2.1 profit and equilibrium table and Appendix A.2.4's two threshold regimes. Proposition 3, manuscript page 14 states the comparison.
The result separates two drivers of the business-model choice. Production cost creates a possible pooling advantage for the provider, because many uses can share one asset's cost. Delivery cost erodes that advantage on every use. The threshold states exactly when the provider's equilibrium earnings exceed the seller's, under the base model's assumptions. It also provides a benchmark for the paper's later analyses of usage uncertainty, heterogeneous valuation, and queueing inefficiencies. Those extensions change the model and are outside this mission. Sections 3–6 develop the base result and its extensions.
The result is already proved in the cited manuscript. The formalization would make explicit the price game, its whole strategy spaces, and the passage from the model's utility-defined market segments to equilibrium profits. It would also establish that the comparison is valid at every equilibrium in the admissible region, including boundary parameter values. No machine-checked proof of this model or Proposition 3 is being reused here; the platform search found related duopoly models with different customers, prices, and cost conventions. The definitions of the segments and profit integrals can be reused for later formalizations of this paper's variants.
The paper computes an indifferent customer's usage and then obtains price candidates from an interior first-order condition and a constrained KKT calculation. Those calculations alone do not establish a global equilibrium: a deviation can put all customers on one side of the indifferent point, leave a firm with no customers, or use a nonpositive price. The profit formulas derived for an interior split do not describe those cases. A formal equilibrium statement must compare each firm with every permitted price, rather than treating the stationary equations as a definition of equilibrium.
The boundary also matters. At that point the seller can have several equilibrium prices with the same zero profits, so uniqueness of prices is too strong. The goal concerns profits at every equilibrium. Appendix A.2.4 switches the algebraic profit comparison according to the provider's price regime, while Proposition 3 switches its threshold formula at ; the two switches have to describe the same profit ordering over the whole admissible region.
Lean represents , and customer usage as real numbers. The parameter predicate records , , , , and . The last condition is the paper's service admissibility condition; it implies . Customer mass is real Lebesgue measure restricted to the utility-defined segment and divided by ; service profit integrates over its segment and divides by the same . These segments are bounded and measurable, so their measures and integrals have the intended finite values. The threshold and table formulas only use divisions whose denominators are positive under admissibility.
The paper's weak market inequalities are retained, including their treatment of ties. Seller deviations range over all real prices because no duopoly seller-price bound is imposed in the source. Provider deviations range over all prices at most , matching its stated constraint. The equilibrium predicate requires global profit comparisons. The goal asserts existence before saying what holds at every equilibrium, so an empty equilibrium set cannot satisfy it. Profits in the goal are calculated from customer segments and integrals at an equilibrium; they are not defined by the table. The paper's Appendix A.2.1 table provides a separate milestone proving those values, and the global best-response and equilibrium-profit statements are identified as stronger than the printed calculations.
This mission needs Mathlib's real measure, set integral, and real algebra libraries, plus the paper-specific definitions of utility, market segments, profits, equilibrium, the two pricing regimes, and . Contributions that establish the closed-form integrals, global best responses, equilibrium table, all-equilibrium profit identity, and regime comparisons are within scope. The earlier monopoly benchmark, the full business-model choice game, and the later heterogeneous, uncertain-usage, and queueing models are separate targets.
Product recalls are frequent and costly. A firm that launches an innovation without thorough quality assurance testing gains time on the market but risks a recall, which brings direct costs (repairs, refunds, legal settlements) and lasting damage to the product's reputation. Testing removes the risk but delays the launch, and while a firm tests, a rival can take the market with its own innovation. Kim, Koenigsberg and Ofek (SSRN 3492105, November 2019; published in Management Science, 2022, doi:10.1287/mnsc.2022.4303) model this trade-off as a two-period game and ask when competing firms test and when they rush to market. Their answer for two identical firms, Proposition 2, is the goal of this mission: depending on the failure probability of an untested product, neither firm tests, both test, or exactly one tests.
Two firms each hold an innovation. The mature product has quality and the innovation quality , with . Production costs nothing. There are two periods, .
Before , each firm chooses its testing decision simultaneously. A firm that tests () sells its mature product at and a fail-proof innovation at . A firm that does not test () launches its innovation at . The untested innovation fails during that period with probability , independently across firms. On failure the firm pays a recall cost , where is a fixed cost, a penalty per unit of first-period revenue and the firm's first-period profit, and at it sells a recalled innovation of quality , with reputation damage .
In each period a new unit mass of consumers arrives, with tastes uniform on . A consumer of taste gets utility from a product of quality at price and buys the product of greatest utility if that utility is nonnegative. Given the two products on offer, the firms set prices; the pricing subgame is the one-period price game, and its equilibrium profit for quality against is written . The testing game is the simultaneous game in which a firm choosing against a rival choosing earns the expected two-period payoff , and an equilibrium is a pure Nash equilibrium of it.
With the cutoffs of the paper's appendix,
and , the interval between the two roots of the quadratic in given by (A.3):
and the two symmetric equilibria never coexist.
Proposition 2 is the paper's main result for competition. It shows that competition changes the testing decision in two directions. A rival's early launch makes simultaneous rushing less costly, because identical products earn nothing in the first period and the revenue-based recall penalty then vanishes. Firms also try to differentiate their timing, which produces the asymmetric equilibrium in which one firm tests and the other does not. Comparing the result with the monopoly benchmark (Proposition 1) gives the paper's managerial conclusions: duopolists may skip a test that a monopolist would run (Corollary 2), and both firms test only when the fixed recall cost is large (Corollary 3).
The proofs in the paper are algebraic and partly omitted ("tedious algebra … available from the authors"). A formal development checks every case of the price equilibria, including the global deviations that the first-order conditions do not cover, and the exact boundaries of each equilibrium region. It also settles the boundary behaviour the paper leaves implicit: the regions are disjoint only off their boundaries. No machine-checked proof of any result of this paper is known.
Most of the work is in Lemma 1. The first-order conditions of the price game give the stated prices, but an equilibrium must also survive non-local deviations: the low-quality firm may undercut to take the whole market, and the high-quality firm may price below the region where both firms sell. Demand is piecewise in the prices, with kinks where one firm's market vanishes and a tie-splitting rule at equal qualities, so each best response is a maximization over several branches. The uniqueness half of the Bertrand bullet needs an undercutting argument. The cutoff characterizations then require sign control of a quadratic in whose discriminant can be negative, and of a denominator in that is negative for small .
All quantities are real numbers. The parameters are a structure with fields , and a predicate bundles the standing assumptions , , , , , . The page writes neither nor ; both are implicit and are made explicit here.
Demand is the Lebesgue measure of the set of tastes in that buy the product, with indifferent consumers counted with weight . A price equilibrium allows deviations to every nonnegative price. The period profit is revenue at the prices computed in the proof of Lemma 1, for the higher quality, for the lower and for equal qualities. It is computed from demand, so Lemma 1's profit formulas are theorems. The untested firm's objective of (A.1) is a positive affine transform of revenue and has the same best responses, so the price game is posed on revenue.
Lemma 1 identifies the unique price equilibrium for each of the two differentiated quality pairs as well as for equal qualities. The payoff is built from the recall events, each failing independently with probability , and from the period profits. Testing decisions are Booleans (true = test). Equilibria of the testing game are pure Nash equilibria with weak best responses, using the published agt_games predicate AGT.IsPureNash.
The cutoffs are written exactly as on p. 37. Every statement that uses requires its denominator to be positive, and every statement that uses requires the discriminant to be nonnegative; when these fail, the corresponding region is empty. The paper calls its regions "mutually exclusive", but at the boundaries a symmetric and an asymmetric equilibrium coexist, so the goal asserts exclusivity only between the two symmetric equilibria.
Trivializing formalizations are ruled out. Defining the payoffs by the four closed forms of the paper's proof, or the period profits by Lemma 1's formulas, would make the milestones definitional and the goal pure algebra. Here both are built from consumer choice.
Not in scope: the monopoly benchmark (Proposition 1, Corollary 1), Corollary 2 (proved only in a limit), the comparative statics of Corollary 4, the conditions and of (A.3), and the extensions of §5. Contributions are welcome on any milestone. Lemma 1's analysis of the vertical-differentiation price game with uniform tastes is reusable for other quality-competition models.
An information designer can change what others know without choosing their actions. When several designers disclose information at once, each designer's experiment affects the incentives faced by agents who receive messages from all of them. The resulting strategic problem appears in competing disclosures, advice, and mediated decisions. Koessler, Laclau, and Tomala study this interaction in a finite-state model and ask whether the designers and agents can play consistently at every continuation of the game. Their working paper proves an existence result for this general model before examining special splitting, corporation, and multi-period games.
The existence question has a specific obstacle. After seeing the designers' experiments, agents may have several optimal continuation behaviors. A designer's payoff can jump as those behaviors change with the experiment profile. The paper's Example 5 shows that some ways of selecting an agent equilibrium at each profile yield an induced game between designers with no approximate equilibrium. The continuation behavior must therefore be part of what the equilibrium chooses; a fixed arbitrary rule cannot be presumed adequate. The paper invokes the equilibrium-selection result of Simon and Zame (1990) for this step. The example and the proof are in the working paper, pp. 6–7 and 21–23.
Let be a nonempty finite set of designers and a nonempty finite set of agents. Designer holds a component of the state, drawn with a common prior on . The prior is general: its coordinates may be dependent. Agent chooses an action in a nonempty finite set , and the action profile lies in . Designer and agent receive real payoffs and respectively. The primitive model appears in §2, p. 5.
Designer can send agent a message in a finite set . The designer's full message profile is . A statistical experiment is a rule : at each value of the designer's state component it specifies a lottery on full message profiles. The designers choose their experiments simultaneously from . Each agent observes the whole experiment profile , but later sees only his own messages . The signal , uniformly distributed on , is public to all agents and may coordinate their action lotteries. Nature draws the state from ; conditional on it, each designer's experiment draws a message profile. This sequence is Definition 1 and the game timeline, pp. 5–6.
For fixed , the agents play a Bayesian continuation game . Its equilibrium-outcome correspondence consists of conditional distributions of action profiles given all messages that can arise from Bayes Nash behavior using the public signal. The agents' incentive test is ex ante: each agent may replace his entire private-message-to-action-lottery rule while the others keep theirs. Private messages with zero probability impose no incentive restriction. Public randomization allows convex combinations of equilibrium outcomes. As stated in §2, p. 6, is nonempty and convex and is the set of public correlated equilibrium outcomes.
An equilibrium selection chooses one at every and is Borel measurable. For a selected outcome, designer receives
The designers may themselves mix: designer chooses a Borel probability measure on , and the profile law is the product of these measures. By Definition 2, p. 6, an equilibrium of is a selection together with a mixed Nash equilibrium of the designers' induced game. Selection at every gives the agents equilibrium behavior in every continuation subgame.
The goal is Theorem 1, p. 6: for every finite profile of message sets, the game admits an equilibrium. With and , the statement is
The milestone list follows the assertions used in the paper's proof. It first records the nonemptiness, convexity, and public-correlation characterization of ; then the compact convex values and upper hemicontinuity of and . The final two milestones record a Borel measurable payoff selection whose designers' game has a mixed equilibrium, and a Borel measurable continuation selection that realizes that selected payoff. These statements are on pp. 6–7.
Theorem 1 guarantees that the general finite-message model has at least one consistent profile of information design and agent continuation behavior. It permits multiple designers, arbitrary correlation in the prior, messages sent privately to different agents, and mixed experiment choices. The result supports the paper's later analysis by ensuring that the baseline game has an equilibrium even though an arbitrary continuation selection need not support one. The theorem is proved in the paper; the machine-checked proof and reusable formal infrastructure are the work of this mission.
Formalizing the result adds a precise interface for finite statistical experiments, agent continuation equilibria with public correlation, set-valued payoff maps, measurable selections, and mixed deviations over spaces of experiments. The finite-game lottery predicate from the published agt_games definition and its proved Nash-existence theorem are available as prerequisites. The remaining public-device, continuity, and selection material can serve other Bayesian-game formalizations.
The obvious first step is to choose one equilibrium outcome of the agents' game at each experiment profile and then seek a Nash equilibrium of the designers' game. That step fails because the chosen continuation outcome may change discontinuously with the experiments. In the paper's Example 5, a particular legitimate selection gives an induced zero-sum game with a gap between maxmin and minmax payoffs, so it has no approximate equilibrium. An argument that assumes every measurable selection works would be false. The existence theorem needs a selection compatible with mixed strategic behavior, and it needs that selection realized by actual agent equilibrium outcomes. Both demands are represented in the last two milestones.
The Lean model uses finite nonempty designer, agent, state, action, and message types. Nonempty message sets are an explicit addition to the printed hypotheses: if one such set were empty, that designer would have no experiment and the existence claim would fail. The paper's printed action-product index is read as , the agent index, because actions belong to agents. The common prior is a lottery on the whole state profile, without a product assumption.
Finite lotteries are nonnegative real weight functions summing to one. The experiment spaces inherit the finite-dimensional product topology and Borel sigma algebra. The public signal has Lebesgue probability law on ; its strategy process is measurable and Bayes Nash at almost every signal value. The outcome correspondence is constructed from these processes, with no free outcome variable unrelated to agent incentives. Upper hemicontinuity uses the open-neighborhood definition. Designer mixed profiles are independent Borel probability measures, and deviations range over every such measure. Integrability is required for the mixed payoff and every deviating payoff, avoiding Lean's default value for a nonintegrable Bochner integral.
The target requires an existential Borel selection that belongs to at every . A fixed selection, a nonmeasurable selection, or an unconstrained outcome map would alter the theorem. Contributions that establish compactness, upper hemicontinuity, measurable selection, and the mixed-equilibrium conclusion for these exact definitions are in scope. The separate results on splitting games, corporations, and multi-period play are outside this mission.
Large service systems such as call centres, hospital wards and cloud server farms route several customer classes to several server pools, with each pool trained for only some of the classes. Staffing such a network sits between two failure modes: too few servers make queues explode, and too many waste capacity. In the Halfin–Whitt (quality-and-efficiency-driven) regime, arrival rates and pool sizes grow like and the staffing surplus or deficit of each pool is of order . Whether those surpluses can be scheduled into a stable system is a question about the network as a whole: a surplus in one pool can serve a deficit elsewhere only through the compatibility graph.
Hmedi, Arapostathis and Pang (arXiv:2009.01942, v3, 2021; Operations Research 2023) answer this for networks whose compatibility graph is a tree and that have no abandonment. They introduce one number, the system-wide safety staffing (SWSS) , the value of a small linear program. They prove that its sign decides stability.
Timeline.
There are classes and pools. Write if pool can serve class , and assume the bipartite graph with these edges is a tree. The first-order rates are , and , and the second-order corrections are . Complete resource pooling (CRP) means that the linear program "minimize subject to , on the edges" has a unique solution , with and on every edge. Put and .
For a positive probability vector , the SWSS parameter is the optimal value of
over and supported on the edges.
Let be the unique array on the edges with row sums and column sums (defined when ). Let . The limiting controlled diffusion is
with and a standard Brownian motion. Here is the total queue, the number of idle servers, and the control says how queued customers are split among classes and idle servers among pools. A stationary Markov control is a Borel map , used as .
(a) If , then for every edge , under the constant control , the diffusion has a unique invariant probability measure . Moreover there are , and such that, with ,
(b) If , then under every stationary Markov control almost surely. If , then under every stationary Markov control there is no invariant probability measure.
The theorem turns a stochastic stability question into the sign of a linear-program value computable from the network data. Positive SWSS is the condition under which a staffing rule with safety capacity can be made stable by scheduling, and the proof exhibits a simple stabilizing control. The identity links the LP value to the drift of the diffusion. It extends earlier uniform-stability results from networks with a single non-leaf pool to arbitrary trees.
The results are proved on paper. This mission produces machine-checked statements, and eventually proofs, of the limiting-diffusion half. That requires:
No part of this is formalized elsewhere. The existing platform layers for Halfin–Whitt diffusions concern single-pool networks.
The linear-algebra half is a genuine induction on trees, not an unfolding of definitions. Theorem 2 eliminates leaves class by class. Theorem 3 identifies the gains with the entries of , which forces to be invertible and to be positive. Theorem 4 then rewrites the LP value through the drift.
The probabilistic half is harder:
Classes are Fin I and pools Fin J, and the tree is SimpleGraph.IsTree on Fin I ⊕ Fin J. States are EuclideanSpace ℝ (Fin I), and control values are pairs of vectors in Mathlib's stdSimplex. Strong solutions, standard Brownian motion, invariant measures, the generator and the weighted total-variation norm are the published EthierKurtz, GPhNGIDiffusion.EMError and UnifErgHW.Diffusion definitions. The weighted norm uses the weight , which is equivalent to the paper's -norm up to a factor .
Conventions committed to:
The statement admits trivializations, each ruled out:
For the instability clauses, strong solutions exist and are pathwise unique for every Borel control (a theorem of Veretennikov, 1981, and its locally bounded extensions; the drift is locally bounded with linear growth and the noise is additive and nondegenerate). This is background, not a claim of the mission.
Out of scope: the clauses of Theorem 1 about the diffusion-scaled th systems (Theorems 6 and 8), and the half of Theorem 4. They need a controlled continuous-time Markov chain layer with work-conserving action sets, which does not exist on the platform.
Welcome contributions:
The Pratt–Arrow risk premium is the basic local measure of risk aversion under expected utility (EU): a decision-maker with a twice differentiable utility facing a small zero-mean risk at wealth pays approximately
variance times the index of absolute risk aversion (Pratt 1964; Arrow 1965). It is used throughout portfolio theory, insurance pricing and decision analysis, wherever a risk attitude has to be summarised by one number.
Much of decision theory since the 1980s replaces EU by rank-dependent utility (RDU, Quiggin 1982), which distorts cumulative probabilities by a probability weighting function . Its special case with linear utility is Yaari's dual theory (DT, Yaari 1987). Under these models risk aversion comes from two sources, the curvature of and the curvature of , and the variance alone no longer measures how much a small risk costs. Eeckhoudt and Laeven (arXiv:1612.03347v2, published in Operations Research, 2022) identify the missing measure: the second dual moment, or maxiance, the expected best of two independent draws of the risk. They show that under DT the local risk premium is proportional to the maxiance, and that under RDU it is the sum of a variance term and a maxiance term.
A finite lottery lists outcomes in increasing order with unconditional probability masses . Write and . The masses need not sum to one: the risks below are attached to one branch of a lottery and carry only that branch's mass. An RDU decision-maker with utility and weighting function evaluates a lottery by (4.1):
DT is the case (3.1). The paper assumes that is twice continuously differentiable with , and that is twice continuously differentiable with , , .
For a risk with cumulative distribution and mean , the unconditional variance and maxiance are
and denotes the total unconditional mass. For a probability distribution, (2.1).
Fix , , and initial wealth . Lottery pays with probability and with probability . Lottery takes mass from each branch of and puts the released mass on a middle outcome with . The RDU risk premium is for the that makes the decision-maker indifferent between and , that is, the solution of (4.2). The spread from with to attaches to the middle branch the risk , which takes the values each with unconditional probability . The DT construction with lotteries , , outcomes , premium and risk ( with probability each) is the same with and .
As jointly, with , , the moments of ,
The result. Formula (4.3) shows that, for a small zero-mean risk, an RDU decision-maker's premium splits additively into an EU part (variance times utility risk aversion ) and a DT part (maxiance times probability-weighting risk aversion ). Variance and maxiance appear on an equal footing, so the maxiance is the natural second risk measure for non-EU preferences, as the variance is for EU. The DT index plays the role of the Arrow–Pratt coefficient in the probability plane. The paper builds its global comparative risk aversion result (Proposition 5.1), its examples with Prelec's weighting function and its portfolio application on this local index.
Formalizing it. The result is proved in the paper by Taylor expansion, with "" left informal. This mission fixes the precise asymptotic meaning: a little-o remainder in the joint limit. It also makes definite the claims the paper takes for granted: that the premium exists and is unique, and that the moments of and take the stated values. No part of this development, nor any rank-dependent utility evaluation, is formalized on the platform or, as far as is known, elsewhere.
The obvious argument expands both sides of (4.2) and keeps "the second-order terms". This needs care on two counts. First, the premium is defined only implicitly, so its size has to be controlled before is expanded: the term is negligible only once is known. Second, the two leading terms have different orders, and , and the remainder must be uniformly small relative to their sum in a two-parameter limit. The tempting reading "small variance and small maxiance" (p. 4) with fixed is false: at fixed the dual term carries a relative error of order that does not vanish as . The DT step (3.4) needs the explicit solution (3.3) and the strict positivity of .
All quantities are real. A lottery is a pair of vectors indexed by ; the evaluation (4.1) is the finite rank-dependent sum, with cumulative masses computed from the vector. The sum equals the Stieltjes integral only for outcomes in increasing order, so the premium predicates keep the page's ranges and , which order and . Initial wealth is added to every outcome.
Committed conventions:
A formalization that defined the premium by its Taylor polynomial, replaced by the leading terms, or took the limit in alone would be trivial or false; the goal quantifies over every solution of the indifference and uses the joint limit.
Not formalized: the equivalence of (2.1) with the Stieltjes form, Proposition 5.1 (global comparative risk aversion), the examples of §6, the portfolio application of §7 and the non-binary generalisation of Appendix A.
Needed infrastructure: finite rank-dependent sums, Taylor expansion of functions with little-o remainders (Mathlib's taylor_mean_remainder family and Asymptotics), and the intermediate value theorem. Contributions welcome: proofs of the milestones, and a general Stieltjes-integral version of (4.1) for finitely supported distributions that would let later missions treat non-binary risks.
Mortgage lenders in the United States and Canada can insure a loan against default when it is originated. In the US the guarantee is typically provided by government-sponsored enterprises, in Canada by government-backed mortgage insurers. Such guarantees are usually discussed as risk-sharing devices, or criticized because they weaken lenders' incentives to screen borrowers. Ahnert and Kuncl (Bank of Canada Staff Working Paper 2019-47; published as Government Loan Guarantees, Market Liquidity, and Lending Standards, Management Science, 2024) isolate a different channel. Loans are later sold in a secondary market where buyers cannot tell good loans from bad ones, the lemons problem of Akerlof (1970). Insurance bought at origination changes which loans reach that market, and therefore its price and its liquidity.
The model is deliberately risk-neutral, so insurance has no risk-sharing value. Every effect comes from the interaction of screening incentives, private information at the interim date, and market segmentation between insured and uninsured loans. This mission formalizes the paper's characterization of the liquid equilibrium with loan insurance (Proposition 2, existence and parts 1–2) and the results that the paper's proof uses.
There are dates and a continuum of lenders , each with one loan. A loan pays at with probability , or if the lender screens at , and otherwise. Screening costs lender a private amount , distributed with distribution function supported on . At each lender privately learns the quality of its loan and a liquidity shock , , with . Its utility is , so a shocked lender values interim consumption more.
At a lender may insure its loan for a fee . Insurance guarantees , so an insured loan pays the safe amount . At loans can be sold to competitive outside financiers who do not observe screening, shocks or quality, but do observe insurance. There are therefore two markets, for insured loans at price and for uninsured loans at price .
Write . Lenders use a threshold rule: those with cost screen. The market for uninsured loans is liquid when shocked lenders sell good loans, (condition (2)). A liquid equilibrium (Definition 1) consists of screening and insurance choices, prices and a fee such that:
Without insurance, the break-even price (4) and the marginal lender's indifference (5) characterize the benchmark equilibrium of Lemma 1.
Assume , , and condition (35), which is equivalent to . Then a liquid equilibrium exists in which a share of high-cost lenders insures, with
fee and . Moreover, the price of uninsured loans is higher and the screening threshold lower than in every solution of the no-insurance system (4)–(5):
In attack order:
The result is the paper's positive case for loan guarantees. Insured loans are removed from the uninsured market in two ways. Shocked lenders who insure hold average-quality loans. Unshocked high-cost lenders who insure give up the option to sell their lemons later. Both effects improve the pool of uninsured loans traded, so rises, and the liquid equilibrium survives for smaller liquidity shocks: replaces the benchmark bound . The cost is lower lending standards (). The paper's welfare analysis (Proposition 4) and its regulation results (Proposition 5) start from this trade-off.
On the formal side, the paper's arguments are informal derivative computations and limit arguments in Appendix B. As far as is known, nothing in this model is machine-checked. Formalizing the result requires the equilibrium to be posed as a genuine fixed point: optimality among all screening and insurance choices, with sales chosen optimally, and break-even prices. The closed forms then become theorems, not definitions. The comparative statics in part 3 of Proposition 2 remain open for later work.
The closed forms follow quickly once one assumes the equilibrium structure: screeners do not insure, high-cost lenders are exactly indifferent about insurance, and the marginal screener is indifferent about screening. The work is in deriving that structure from Definition 1 and then exhibiting the equilibrium.
Everything is defined in the namespace LoanInsurance.Liquid, in one definitions file LoanInsurance.Liquid.Model. The conventions are:
Params with fields A, μ, ψ, ν, lam (the paper's ), etaBar () and F. The standing assumptions of §2 form the predicate Standing. The density on is replaced by what the paper uses: is continuous and strictly increasing on , below , and above .A trivializing formalization is ruled out: the equilibrium is never defined by the equations (5), (8) and (33) or by the closed forms. It is optimality among all four choices plus break-even. Neither nor is built into the definition. The goal is an existence statement whose witness must satisfy Definition 1.
A complete development needs elementary real analysis: monotonicity of linear-fractional functions, the intermediate value theorem for the fixed points (6) and (37), and case analysis on . Lemmas about the prices (4) and (33) are reusable across the milestones. Proofs of any milestone, and alternative formulations of Definition 1 that are proved equivalent, are welcome.
Retail chains routinely delegate replenishment decisions to store managers. The manager sees signals the head office does not: local events, weather, the mood of the neighbourhood. The head office (the principal) knows only the probabilities of these demand states. It also cannot observe lost sales directly, because unmet demand leaves no record, so it cannot simply pay the manager (the agent) on the true newsvendor cost. What it can observe is leftover stock and whether the shelf was empty when someone checked.
Alp and Şen (M&SOM 23(1):55–69, 2021) study performance measures built from these observable quantities. Under scheme , the agent is charged for leftover stock and pays a lump-sum penalty if the shelf is empty at the end of the period. One value of aligns the agent's order with the principal's optimal order in every demand state only when all states have the same demand variability (their Corollary 1). The paper's response is early inspection: scheme checks the shelf at an earlier time . Its Proposition 2 shows that with two demand states, a suitable inspection time and one penalty restore perfect alignment, even though the principal does not know the state.
The question belongs to the literature on sales-force and inventory incentives (e.g. F. Chen, Sales-force incentives and inventory management, M&SOM 2(2):186–202, 2000), where the agent's private information about demand is the central obstacle.
There is one period of length and two demand states . The agent knows ; the principal does not. In state , cumulative demand is a Wiener process with drift and standard deviation . So the period demand is and the demand up to time is . Write and for the standard normal distribution function and density, and .
The stock starts at a level and is raised to an order-up-to level . Leftover stock costs per unit and lost demand per unit, so the principal's expected cost is the newsvendor cost
Let be the critical fractile, . The principal's optimal level is .
Under scheme with unit weight on leftover stock, the agent's expected score, eq. (4) of the paper, is
Its derivative in , at , is the function of eq. (9):
In Lean these objects are agentCost, Φ, φ, omega, incentiveM, inspectionLHS and argminFrom in EarlyInspect.Align.Model. The principal's cost is the published InventoryControl.newsboyCost co cu μ σ.
Assume , and . Then there is with
and the penalty
achieves the following with inspection time . For every and both ,
The result shows that when the principal inspects is an incentive instrument in its own right. With end-of-period inspection, one penalty cannot align a manager across states that differ in variability. Moving the inspection earlier changes the stock-out probability differently in each state, and with two states that extra freedom is enough to make the manager's privately optimal order equal the principal's in both. Proposition 2 is the paper's headline claim, stated in the abstract and the conclusion. The paper generalizes its second consequence in Theorem 4: for more than two states, some with yields lower expected cost for the principal than scheme .
The paper states its results without proofs in the journal text; all proofs are in an online appendix. This mission states the goal and the results it rests on as machine-checkable statements. Two of them needed repair. As printed, Proposition 2 is false without a sign condition: in the paper's own case , , with , no exists. Theorem 3's "unique root" holds only on the feasible region . None of these results has been formalized before.
The principal's problem is the convex newsvendor problem. The agent's is not convex. The score adds a decreasing Gaussian tail to a convex function, and its derivative can change sign more than once on the real line. The obvious argument, " by the choice of , hence is the agent's optimum", fails twice. First, a stationary point need not be a minimizer: the agent's choice is the argmin of the score over , and that requires the sign pattern of on all of , which is Lemma 1 and Theorem 3. Second, the same must serve both states, and the condition of §4.2.2 under which the root is unique has to hold at the constructed in each state. The existence of is an intermediate-value argument whose sign condition is exactly the added hypothesis.
All quantities are real. Only the two normal marginals of the demand process are used, so the Wiener process is not formalized. The normal law is the published InventoryControl.newsboyDemand m s (mean , standard deviation ), and is newsboyDemand (t * μ) (Real.sqrt t * σ), with variance . The agent's weight is fixed to , as in Proposition 2. The principal's cost follows the text (leftover , lost demand ), not eq. (1), which prints the coefficients swapped. is characterized by .
The following hypotheses are added and disclosed in the items. appears in Proposition 2 and in milestone 5. and appear in Lemma 1, whose threshold divides by and whose second clause fails for negative . (nonnegative starting stock) appears in Theorem 3 and the goal. Standing hypotheses and appear throughout.
The goal cannot be trivialized by defining the agent's choice as a root of or as . Both choices are stated as sets of minimizers of the expected costs, and these sets are claimed to be singletons, so no vacuous reading is possible. A sorry-free check shows that the goal's hypotheses are satisfiable.
Useful infrastructure includes derivatives of Gaussian expectations of and of Gaussian tails, monotonicity and convexity of and , and the uniqueness of the critical fractile. These are reusable for any newsvendor-type model with normal demand. Proofs of individual milestones are welcome, as are proofs of the remaining results of the paper (Corollary 1, Theorem 3 parts 2–3, Theorem 4) as new statements.
Customers often need several complementary products, such as hardware and software, cars and financing, or jet engines and maintenance, sold by specialist firms that are complementors to one another. A recurring strategic move is for one complementor to launch an integrated system: a single offering that competes with the multi-component system its complementor still helps to supply. The paper's examples are AT&T's bundles of internet and entertainment services after the Time Warner merger, BMW's financing and leasing, Rolls-Royce's "power-by-the-hour" package of engines with maintenance, and Apple's music service competing with Spotify.
Reisinger, Schmidt and Stieglitz (Management Science, 2021) ask when such a move pays, and why it is observed even when the integrated system is neither better than the two-component system nor aimed at a different customer segment. Their answer separates the entrant's incremental profit into a direct effect (market expansion and conversion of customers to the integrated system) and a strategic effect: once an integrated system competes with the two-component system, the rival complementor cuts its component price while the entrant raises its own. The entrant thereby squeezes its complementor's margin. This decomposition follows the direct/strategic-effect analysis of Bulow, Geanakoplos and Klemperer (1985) and Fudenberg and Tirole (1984).
Two complementors and each sell one component of a two-component system with gross utility . Either may launch an integrated system with gross utility by paying an investment . Production costs are zero. The parameter measures substitutability between systems. Inverse demand is linear:
a system that is not offered having quantity zero. The model restricts to an admissible range: if , and if .
The game has two stages. In stage 1 the complementors decide simultaneously whether to launch an integrated system. In stage 2 they set prices. This gives three price subgames: no entry (i), accommodation (ii), in which only enters, and escalation (iii), in which both enter. A price equilibrium of a subgame is a pure Nash equilibrium in which a firm selling two products may change both prices at once. In stage 1, 's benefit of entering when stays out is , and 's benefit of entering when is in is . The thresholds and are the values of at which these vanish.
's incremental profit from entry splits into three parts:
These are the profits from market expansion, from conversion of customers to the integrated system, and from squeezing the complementor.
In the accommodation equilibrium, for every admissible :
Moreover, when there is a threshold such that for every admissible some makes the stage-1 outcome accommodation while
that is, enters although its integrated system loses money. The goal states this existence claim and does not fix the threshold.
The result gives a rationale for entry with an integrated system that is unprofitable on its own terms. The value of entry can lie entirely in the entrant's old business, through the margin it takes from its complementor. This matters for reading platform and ecosystem strategy, where launches of "first-party" hardware or bundles are often judged by their own profitability, and for competition policy, where the same move lowers the rival complementor's price and changes how the gains of the system are divided. Proposition 1, which the goal relies on, also shows that the asymmetric outcome, where one complementor integrates and the other does not, occurs for an intermediate band of entry costs, so the asymmetry arises endogenously between identical firms.
The paper proves these statements with computer-algebra-style calculations on closed forms. As far as is known, none of it is formalized. A complete development checks every equilibrium derivation, including uniqueness of the equilibria under joint deviations, and the inequalities that the paper's appendix treats briefly. The positivity of (Proposition 1 (i)) is argued in the appendix through a monotonicity claim that does not hold as written, and the two displayed formulas listed under Formalization scope contain misprints. The formal record settles these points.
The equilibrium computations are linear algebra, but each is stated as an equivalence: a profile is an equilibrium if and only if it equals the closed form. The "only if" direction needs strict concavity of each firm's two-price profit in both prices jointly. The comparison versus needs the admissible range: the factor is positive only because , and this has to be extracted from a square-root bound. The loss-making-entry claim needs more than 's entry benefit being nonnegative. must also stay out, so has to lie in and above 's integrated-system profit at the same time. That is why the goal depends on Proposition 1 (i), whose central inequality is a polynomial inequality in three variables over a region bounded by a square root. Plugging in boundary values of , as the appendix does, does not by itself establish it.
All objects are over in the namespace SystemSqueeze.Accommodation, in one definition file:
Standing UC UI γ bundles , , and Admissible UC UI γ. Positivity of and are added; the paper uses them without stating them.IsNoEntryEq, IsAccEq and IsEscEq are pure Nash equilibria with joint deviations in a firm's two prices.The equilibrium lemmas are reusable for any linear-demand analysis of this model, including Propositions 2 and 4–8 of the paper, which are not part of this mission. Contributions of proofs for any milestone are welcome, as are alternative proofs of .
Firms reposition their products as consumer tastes drift: car makers redesign models, retailers change assortments, media outlets shift their editorial line. Each move costs money, and competitors respond to it. Ning and Villas-Boas (2020) study when two competing firms should incur a fixed cost to move toward consumers whose preferred position follows a random path. The answer is a pair of repositioning thresholds. The paper characterizes them through a system of two transcendental equations and, for small repositioning costs, derives explicit asymptotic expansions. Those expansions give the paper's comparative statics in volatility, attribute importance and patience.
This mission formalizes that small-cost analysis: Proposition 2 of the paper, together with the chain of identities and limits in its appendix that leads to it.
Consumers have preferences . All consumers share the same position on the repositionable attribute, and they are uniformly spread on the fixed attribute . The position follows a driftless Brownian motion with variance , reflected at and . Two firms sit at the ends of in , and at opposite ends in . A consumer buying from a firm at distance gets utility , so measures how much the repositionable attribute matters. A firm may jump to the other end of the -line at a cost . Firms discount at rate . All these parameters are standing assumptions.
Under price competition, a firm earns the flow profit when both firms are on the same side. When they are on different sides and the firm is at distance from the consumers, it earns
Write . In the symmetric equilibrium, a firm on the far side repositions when its distance reaches a threshold . Firms on the same side reposition at a positive hazard rate on . Value matching and smooth pasting of the value functions
give five conditions (5)–(9). Eliminating leaves the threshold system (14)–(15) in alone. With :
A threshold pair at cost is a solution of (14)–(15) with and . A solution branch is a pair of functions that is a threshold pair for every sufficiently small . The appendix uses the prices and , and their sum .
For every solution branch, as :
The goal fixes no constant. It asserts only the directions and the vanishing relative effect of , so it survives any refinement of the expansions.
In attack order:
The result. Proposition 2 is the paper's main qualitative statement about cheap repositioning. More volatile tastes make firms wait longer before moving: with high the consumers are likely to drift back. A more important repositioning attribute makes them move sooner. In both cases the band , in which same-side firms randomize, widens. Patience, by contrast, drops out to first order. The law also quantifies how strongly repositioning reacts to its cost: a small cost has a large effect on behaviour.
Formalizing it. The result is proved in the paper by an asymptotic computation in its appendix. As far as a search of the Prove2Me catalog shows, none of it is formalized. The mission produces a checked version of every step, in the paper's own notation. Two places need more than transcription. The printed (16)–(17) have right sides that still depend on , so they are restated as two-term expansions. The paper also never states that solutions of (14)–(15) exist for small ; the existence milestone supplies that.
The thresholds are defined only implicitly, as solutions of a transcendental system, and the goal is about every solution branch. Nothing is known in advance about such a branch: not continuity, not uniqueness, not a closed form. The natural first idea, to substitute the expansions (16)–(18) and compare coefficients, assumes what has to be shown. The expansions must be derived from (14)–(15) for an arbitrary branch.
The derivation is delicate because the leading behaviour cancels. The left side of (xii) vanishes to third order at , so the rate of is the cube root of a ratio of small quantities. The gap is of order , one order below the thresholds' own displacement. Clause 4 of the goal needs the leading coefficient to be independent of , and clauses 2–3 need strict inequalities between leading coefficients.
All quantities are real. The parameters are a structure with fields r, σ2 (the variance itself) and δ, and Standing requires all three to be positive. Primes are deriv evaluated at the point, and is the derivative of pid, not a hand-coded formula. Equations (14)–(15) keep the paper's ratio form: since , a vanishing denominator makes them false, not vacuously true. The milestone deriving (14)–(15) from (5)–(9) states the displayed ratios with both denominators nonzero.
Commitments beyond the printed text:
Two readings are ruled out as trivializing. Defining the thresholds by formulas, or assuming (16)–(18) for the branch, would make the goal a computation; the goal instead quantifies over every branch. Stating clause 4 as would be contentless, because both thresholds tend to .
The development needs real asymptotics: Taylor control of near , cube roots as real powers, and filters on . It needs no stochastic calculus, since the value functions enter only through their closed forms. The limit (xviii) and the asymptotic analysis of an implicitly defined branch are reusable beyond this paper. Contributions to any milestone are welcome. Not formalized: the hazard rate (13), the verification that the thresholds form a Markov perfect equilibrium, Propositions 3–6, the asymmetric equilibrium and the limit .
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.