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?
The information capacities and ``distillability'' of a quantum channel are studied in the presence of auxiliary resources. These include prior entanglement shared between the sender and receiver and free classical bits of forward and backward communication. Inequalities and trade-off curves are derived. In particular an alternative proof is given that in the absence of feedback and shared entanglement, forward classical communication does not increase the quantum capacity of a channel.
This mission is the statement-level formalization of Inequalities for quantum channels assisted by limited resources (arXiv:quant-ph/0406111v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is A dephasing side channel cannot increase unassisted quantum capacity (§II B Eq.(16): a dephasing side channel cannot increase quantum capacity, 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.
27 results of the paper are not stated yet, because the library lacks an interface they need:
We show how to compute or at least to estimate various capacity-related quantities for Bosonic Gaussian channels. Among these are the coherent information, the entanglement assisted classical capacity, the one-shot classical capacity, and a new quantity involving the transpose operation, shown to be a general upper bound on the quantum capacity, even allowing for finite errors. All bounds are explicitly evaluated for the case of a one-mode channel with attenuation/amplification and classical noise.
This mission is the statement-level formalization of Evaluating Capacities of Bosonic Gaussian Channels (arXiv:quant-ph/9912067v1). 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 II.B, Eq.(2.9): finite-error transpose capacity bound (II.B, Eq.(2.9): finite-error transpose capacity bound, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
22 results of the paper are not stated yet, because the library lacks an interface they need:
We present a simplified framework for proving sequential composability in the quantum setting. In particular, we give a new, simulation-based, definition for security in the bounded-quantum-storage model, and show that this definition allows for sequential composition of protocols. Damgard et al. (FOCS '05, CRYPTO '07) showed how to securely implement bit commitment and oblivious transfer in the bounded-quantum-storage model, where the adversary is only allowed to store a limited number of qubits. However, their security definitions did only apply to the standalone setting, and it was not clear if their protocols could be composed. Indeed, we first give a simple attack that shows that these protocols are not composable without a small refinement of the model. Finally, we prove the security of their randomized oblivious transfer protocol in our refined model. Secure implementations of oblivious transfer and bit commitment then follow easily by a (classical) reduction to randomized oblivious transfer.
This mission is the statement-level formalization of Composable Security in the Bounded-Quantum-Storage Model (arXiv:0709.0492v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Measured BB84 uncertainty with explicit smoothing and positivity (Lemma 2.3, 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.
14 results of the paper are not stated yet, because the library lacks an interface they need:
By combining the Minkowski inequality and the quantum Chernoff bound, we derive easy-to-compute upper bounds for the error probability affecting the optimal discrimination of Gaussian states. In particular, these bounds are useful when the Gaussian states are unitarily inequivalent, i.e., they differ in their symplectic invariants.
This mission is the statement-level formalization of Computable bounds for the discrimination of Gaussian states (arXiv:0806.1625v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Minkowski spectral bound for Gaussian-state discrimination (Theorem 4, Eqs. (60)–(62), 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.
After proving a general no-cloning theorem for black boxes, we derive the optimal universal cloning of unitary transformations, from one to two copies. The optimal cloner is realized by quantum channels with memory, and greately outperforms the optimal measure-and-reprepare cloning strategy. Applications are outlined, including two-way quantum cryptographic protocols.
This mission is the statement-level formalization of Optimal cloning of unitary transformations (arXiv:0804.0129v2). 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 Optimal universal one-to-two unitary cloning, with attaining channels (Theorem 1; Eqs. (8)–(10), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper we develop two types of tools to deal with differentiability properties of vectors in continuous representations of an infinite dimensional Lie group on a locally convex space . The first class of results concerns the space of smooth vectors. If is a Banach--Lie group, we define a topology on the space of smooth vectors for which the action of on this space is smooth. If is a Banach space, then is a Fr'echet space. This applies in particular to -dynamical systems , where is a Banach--Lie group. For unitary representations we show that a vector is smooth if the corresponding positive definite function is smooth. The second class of results concerns criteria for -vectors in terms of operators of the derived representation for a Banach--Lie group acting on a Banach space . In particular, we provide for each examples of continuous unitary representations for which the space of -vectors is trivial and the space of -vectors is dense.
This mission is the statement-level formalization of On Differentiable Vectors for Representations of Infinite Dimensional Lie Groups (arXiv:1002.1602v3). 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 Hilbert-valued smoothness and the inner-product kernel (Theorem 7.1, PDF p. 21). 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.
42 results of the paper are not stated yet, because the library lacks an interface they need:
We address the problem of the information-disturbance trade-off associated to the estimation of a quantum transformation, and show how the extraction of information about the a black box causes a perturbation of the corresponding input-output evolution. In the case of a black box performing a unitary transformation, randomly distributed according to the invariant measure, we give a complete solution of the problem, deriving the optimal trade-off curve and presenting an explicit construction of the optimal quantum network.
This mission is the statement-level formalization of Information - Disturbance Tradeoff in the Estimation of a Unitary Transformation (arXiv:1006.5665v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Attained optimal information–disturbance frontier (§IV C, Eqs.(30)–(34); abstract on PDF p.1, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
We analyze quantum algorithms for cloning of a quantum measurement. Our aim is to mimic two uses of a device performing an unknown von Neumann measurement with a single use of the device. When the unknown device has to be used before the bipartite state to be measured is available we talk about 1 -> 2 learning of the measurement, otherwise the task is called 1 -> 2 cloning of a measurement. We perform the optimization for both learning and cloning for arbitrary dimension of the Hilbert space. For 1 -> 2 cloning we also propose a simple quantum network that realizes the optimal strategy.
This mission is the statement-level formalization of Cloning of a quantum measurement (arXiv:1103.5709v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal one-to-two measurement cloning fidelity (§V, Eq.(61): optimal one-to-two cloning fidelity (seed announced in abstract), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
We study quantum learning algorithms for quantum measurements. The optimal learning algorithm is derived for arbitrary von Neumann measurements in the case of training with one or two examples. The analysis of the case of three examples reveals that, differently from the learning of unitary gates, the optimal algorithm for learning of quantum measurements cannot be parallelized, and requires quantum memories for the storage of information.
This mission is the statement-level formalization of Quantum learning algorithms for quantum measurements (arXiv:1103.0480v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Three-example qubit learning requires adaptation (Abstract; §V.C and Remark 1: optimal three-example qubit learning requires adaptation, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
7 results of the paper are not stated yet, because the library lacks an interface they need:
A consistent functional calculus approach to the spectral theorem for strongly commuting normal operators on Hilbert spaces is presented. In contrast to the common approaches using projection-valued measures or multiplication operators, here the functional calculus is not treated as a subordinate but as the central concept. Based on five simple axioms for a "measurable functional calculus", the theory of such calculi is developed in detail, including spectral theory, uniqueness results and construction principles. Finally, the functional calculus form of the spectral theorem is stated and proved, with some proof variants being discussed.
This mission is the statement-level formalization of The Functional Calculus Approach to the Spectral Theorem (arXiv:2003.06130v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
49 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 7.6 (Spectral Theorem: General Case) (Theorem 7.6 (Spectral Theorem: General Case), PDF p. 35). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
We consider three different communication tasks for quantum broadcast channels, and we determine the capacity region of a Hadamard broadcast channel for these various tasks. We define a Hadamard broadcast channel to be such that the channel from the sender to one of the receivers is entanglement-breaking and the channel from the sender to the other receiver is complementary to this one. As such, this channel is a quantum generalization of a degraded broadcast channel, which is well known in classical information theory. The first communication task we consider is classical communication to both receivers, the second is quantum communication to the stronger receiver and classical communication to other, and the third is entanglement-assisted classical communication to the stronger receiver and unassisted classical communication to the other. The structure of a Hadamard broadcast channel plays a critical role in our analysis: the channel to the weaker receiver can be simulated by performing a measurement channel on the stronger receiver's system, followed by a preparation channel. As such, we can incorporate the classical output of the measurement channel as an auxiliary variable and solve all three of the above capacities for Hadamard broadcast channels, in this way avoiding known difficulties associated with quantum auxiliary variables.
This mission is the statement-level formalization of Hadamard quantum broadcast channels (arXiv:1611.07651v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2: exact classical capacity of a Hadamard broadcast channel (Theorem 2, §3.3: classical capacity of a Hadamard broadcast channel (seed paper result), 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.
We prove the existence of a universal recovery channel that approximately recovers states on a v. Neumann subalgebra when the change in relative entropy, with respect to a fixed reference state, is small. Our result is a generalization of previous results that applied to type-I v. Neumann algebras by Junge at al. [arXiv:1509.07127]. We broadly follow their proof strategy but consider here arbitrary v. Neumann algebras, where qualitatively new issues arise. Our results hinge on the construction of certain analytic vectors and computations/estimations of their Araki-Masuda norms. We comment on applications to the quantum null energy condition.
This mission is the statement-level formalization of Approximate recovery and relative entropy I. general von Neumann subalgebras (arXiv:2006.08002v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is A support-dominating state in a closed convex family (Lemma 2: support-dominating state in a closed convex set, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
31 results of the paper are not stated yet, because the library lacks an interface they need:
We present an efficient machine learning (ML) algorithm for predicting any unknown quantum process over qubits. For a wide range of distributions on arbitrary -qubit states, we show that this ML algorithm can learn to predict any local property of the output from the unknown process~, with a small average error over input states drawn from . The ML algorithm is computationally efficient even when the unknown process is a quantum circuit with exponentially many gates. Our algorithm combines efficient procedures for learning properties of an unknown state and for learning a low-degree approximation to an unknown observable. The analysis hinges on proving new norm inequalities, including a quantum analogue of the classical Bohnenblust-Hille inequality, which we derive by giving an improved algorithm for optimizing local Hamiltonians. Numerical experiments on predicting quantum dynamics with evolution time up to and system size up to qubits corroborate our proof. Overall, our results highlight the potential for ML models to predict the output of complex quantum dynamics much faster than the time needed to run the process itself.
This mission is the statement-level formalization of Learning to predict arbitrary quantum processes (arXiv:2210.14894v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
37 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Corollary 3 (Norm inequality for general 𝑘-local Hamiltonian) (Corollary 3 (Norm inequality for general 𝑘-local Hamiltonian), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
17 results of the paper are not stated yet, because the library lacks an interface they need:
Let be a real finite-dimensional Lie algebra containing pointed generating invariant closed convex cones. We determine those derivations of which induce a 3-grading of the form on such that the -eigenspaces of are generated by the intersections with generating cones of the form , where is the coadjoint orbit of a linear functional and is the dual cone of . In particular, we show that, if is solvable, no such derivation except the trivial one exists. This continues our classification of Lie algebras generated by Lie wedges of endomorphism semigroups of standard subspaces. The classification is motivated by the relation of nets of standard subspaces to Haag-Kastler nets of von Neumann algebras in Algebraic Quantum Field Theory.
This mission is the statement-level formalization of Lie wedges of endomorphism semigroups of standard subspaces in admissible Lie algebras (arXiv:2007.13445v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
25 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.17 (Non-degeneration Theorem); precise result selected for the seed (Theorem 3.17 (Non-degeneration Theorem); precise result selected for the seed, PDF p. 23). 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.
23 results of the paper are not stated yet, because the library lacks an interface they need:
The quantum Schur transform maps the computational basis of a system of qudits onto a \textit{Schur basis}, which spans the minimal invariant subspaces of the representations of the unitary and the symmetric groups acting on the state space of -level systems. We introduce a new algorithm for the task of weak Schur sampling. Our algorithm efficiently determines both the Young label which indexes the irreducible representations and the multiplicity label of the symmetric group. There are two major advantages of our algorithm for weak Schur sampling when compared to existing approaches which proceed via quantum Schur transform algorithm or Generalized Phase Estimation algorithm. First, our algorihtm is suitable for streaming applications and second it is exponentially more efficient in its memory usage. We show that an instance of our weak Schur sampling algorithm on qubits to accuracy requires only qubits of memory and gates from the Clifford+T set. Further, we show that our weak Schur sampling algorithm on qudits decomposes into gates from an arbitrary fault-tolerant qudit universal set, for , and requires a memory of qudits to implement.
This mission is the statement-level formalization of Weak Schur sampling with logarithmic quantum memory (arXiv:2309.11947v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Streaming weak Schur sampling with logarithmic quantum memory at fixed local dimension (Abstract; III and III.A, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
Intertemporal choice compares outcomes received at different times. A familiar model assigns each instantaneous outcome a utility and aggregates those utilities with a time weight. That model is useful in economics and operations research, but its meaning depends on what choices are feasible and how a preference over one stretch of time relates to a preference over another. When outcomes must vary continuously, an agent cannot freely paste two trajectories together at a chosen instant. Pivato's 2018 preprint asks which observable properties of preferences still force an integral representation under that constraint. The resulting theorem concerns a finite horizon; the paper also develops distinct infinite-horizon representations, which are outside this mission.
Earlier discounted-utility models often begin with an integral or a discounted sum and then study its implications. Here the integral is the conclusion. This changes the formalization problem: the preference structure, the permitted trajectories, and the relation between preferences on overlapping time regions must be defined independently of any utility or discount function. Theorem 1 on p. 13 is the paper's finite-horizon characterization. The Appendix A and B results selected as milestones connect its structural axioms to a content-based representation and then to an integral.
Time is the compact interval , with . The outcome space is connected, and a trajectory is a continuous map from to . A set of feasible trajectories includes every constant trajectory , which gives outcome at every time. Feasibility is substantive: a trajectory obtained by pasting arbitrary continuous pieces may fail to be continuous at the join.
A time interval is relatively open in . It includes when and when , but excludes any interior endpoints. A time span is a finite union of disjoint such intervals with distinct endpoints. The empty span is allowed. Relative interior and closure give the Boolean operations and . These operations can bridge omitted boundary instants.
For every time interval , a primitive preference order compares restrictions of members of to . Each such order is complete, transitive and nontrivial. The order on the whole horizon is ; its comparison of constant trajectories induces the synchronic preference on outcomes. Preferences on general spans are induced through the paper's limited-separability construction: representatives agree with the compared trajectories on , are indifferent on each component of , and are then compared on the full horizon. The representatives must belong to .
The axioms constrain this primitive structure. Richness (R) permits preference-preserving insertion of a middle trajectory between fixed outer restrictions. Minimal equicontinuity (MinEqn) requires interiors of synchronic contour preimages to be time spans. The eight characterization axioms are interval separability (ISep), limited separability (LSep), static equivalence (StEq), continuity of synchronic preferences (C), dominance (Dom), continuity of intertemporal preferences (CIP), tradeoff consistency (TC), and ephemerality (Eph). Their definitions refer only to preferences and feasible trajectories.
A discounted utility integral representation consists of a continuous utility and a continuous, strictly increasing map with and . For every time span and feasible restricted trajectories , it satisfies
The goal is Theorem 1 of the preprint: under the standing preference assumptions, (R), and (MinEqn), the eight axioms hold if and only if such a representation exists. The theorem also says that the normalized is unique and that any two representing utility functions differ by for some and . The milestone list includes the structural equivalences of Lemmas A1, A3 and A4; the compatibility and separability results of Lemma A5 and Proposition A6; the richness result of Lemma A9; the comeasurability claim of Lemma B1; and the content-utility characterization in Theorem B2(b).
The characterization identifies when local comparisons, continuity, and consistency of tradeoffs across regions of time determine one common utility scale and one normalized time weight. The uniqueness clauses prevent two different discount profiles from representing the same structure, while allowing the expected positive affine freedom in utility. Without the characterization, an integral can be used as an example of a preference rule, but the stated axioms would not certify that every admissible rule has that form.
The paper gives a mathematical proof, but this mission records open Lean statements rather than verified proofs. A completed development would make the time-span algebra, the induced intermittent order, and the content integrator reusable for related representation results. It would also expose precisely where the finite-horizon assumption is used before adapting the framework to the paper's later infinite-horizon theorems. The cited preprint relies in part on companion results about contents and their measure representations; formal proofs of those results are welcome groundwork.
Continuous trajectories cannot generally be pasted at a time boundary while remaining feasible. This blocks the immediate finite-product argument often used for separable preferences. The paper's richness conditions replace that maneuver with preference-equivalent trajectories whose restrictions can be coordinated across component intervals. A second difficulty is that a finitely additive content on regular-open spans is not automatically a Borel measure: the representation needs a way to account for boundary behavior before the integral formula follows. The source treats this in its appendices and invokes companion work.
Lean uses the subtype with its relative topology, continuous maps for feasible trajectories, and sets of subtype times for spans. A member of is represented by a full member of , so comparisons never range over arbitrary functions on . The intermittent order is existentially induced from whole-horizon comparisons; a universally quantified extension rule could be vacuous when no extension exists. The axioms are stated directly on preferences, without mentioning or .
The integral is represented by integration against the Lebesgue–Stieltjes measure of a continuous StieltjesFunction. This is the paper's Riemann–Stieltjes expression on bounded continuous integrands, using its equation (B12). Integrals are restricted to the image of the span in . The representing function is normalized at both horizon endpoints; uniqueness compares its values on . Both the final integral representation and the intermediate content representation require agreement with primitive interval orders, in accordance with their identification with induced orders in Lemma A5. The intermediate utility also represents synchronic preference.
The strict clauses of (Dom), (TC), and (CIP) range over nonempty spans; at the empty span their literal unqualified forms become contradictory. Condition (R) is stated for a nonempty middle interval, : with as printed, continuity would force the two outer trajectories to agree at , which no set containing two distinct constant trajectories in a Hausdorff outcome space can satisfy. These domain choices and the specialization of Appendix B's Theorem B2 to are recorded in the moderation notes. Definitions of time spans, preference orders, contents, simple-function integration, and the measure connection are reusable contributions. Machine-checked proofs of the listed milestones and of the final equivalence are the intended contributions.
Islands, remote villages and mining sites that are not connected to a power grid have traditionally run on diesel generators. Solar panels can replace part of that fuel, but the sun shines only during the day, and demand continues at night. Pairing solar capacity with energy storage lets daytime surplus serve nighttime demand, at the price of an additional investment and of energy lost in each charge–discharge cycle. Many storage technologies compete for this market (lithium-ion and sodium batteries, pumped hydro, hydrogen), each with its own capital cost and cycle efficiency. A planner therefore faces two coupled questions: how much solar and storage capacity to install, and which storage technology to install at all.
Kaps, Marinesi and Netessine (SSRN 3761397; Management Science, 2023, doi:10.1287/mnsc.2021.04129) study these questions in a stochastic capacity-investment model. Their answer to the second question is a closed-form rule: technologies are ranked by a single number, the storage-cost-to-efficiency ratio , and a technology pays off exactly when this ratio is below an explicit function of the solar cost and the fuel cost.
A firm serves periods. Each period has a day with deterministic demand and a night with deterministic demand . The firm installs solar capacity at per-period unit cost , and storage able to discharge units at per-period unit cost , where and is the cycle efficiency. Day generation is uniform on , independently across periods; nothing is generated at night. Any demand not covered by solar or storage is met by a fossil backup at marginal cost , with . Every unit of renewable energy served therefore saves . Write .
The tracking model follows the stored charge , starting from :
and its expected profit is
The full-discharge model assumes all stored energy is used within the period:
A plan is optimal if it maximizes the model's profit over all . For a technology , is the set of market parameters at which the optimal tracking storage is positive. Technology is preferred to when (Definition 1). The threshold is
The goal concerns the tracking model, the paper's primary object, and not its approximation.
A supporting item, with no paper counterpart, asserts that an optimal tracking plan exists.
The theorem reduces the comparison of storage technologies, each described by two parameters, to a one-dimensional ranking that holds uniformly over all demand levels, solar costs and backup costs. It also gives a profitability test that uses only , and . Neither statement involves , or . Lemma 1 locates the transition from "no storage" to "some storage" in the tracking model exactly, although that model has no closed-form solution. The intermediate results establish when the tractable full-discharge model is an exact surrogate for the tracking model.
The results are proved in the paper, by first-order conditions of the full-discharge model and a comparison argument. No machine-checked proof exists. This mission produces one: a Lean formalization of a multi-period storage recursion with uniform generation, its expected profit, and the threshold structure of its optimizers. Several printed statements are corrected along the way (see Formalization scope), so the formal versions also serve as an erratum.
The tracking model couples periods through the stored charge, so its expected profit has no closed form, and optimal plans cannot be computed. Everything about has to be derived indirectly, by sandwiching the tracking profit between quantities of the one-period full-discharge model. The sandwich rests on two facts: everywhere, and for .
The obvious first idea, first-order conditions of the closed form (20), needs care: (20) equals only where , and plans outside that region must be handled too. Theorem 3's printed optimal capacity ignores and is wrong whenever no storage is optimal. Optimal plans need not be unique: at with a whole segment of plans is optimal. A proof must therefore argue about optimality, not about the uniqueness of a stationary point. The existence of a tracking optimum also needs an argument when , because the profit is then not coercive in .
Parameters form a structure with and , constrained by a predicate Standing. The paper states , and . Three conditions are added, and each is disclosed: and (unit costs; with the problem is unbounded) and (with every profit vanishes). Storage starts empty (footnote 3, p. 15). Generation is encoded as with uniform on , which is Lebesgue measure restricted to the unit cube. Expectations are Bochner integrals of bounded continuous functions. Everything is real-valued.
"" is formalized as an optimal tracking plan exists and every optimal tracking plan has . The existence clause rules out the vacuous reading. Definition 1's is read as a proper superset, without which the "only if" direction of Theorem 2(a) fails for equal ratios. ranges over tuples with and , for a fixed .
One printed statement is restated. Theorem 4's first bullet asserts that is optimal in both models, not that optima are unique, and uses from eq. (25) rather than Theorem 3's formula. Eqs. (20) and (25) are per period in the paper and carry the factor here.
The tracking profit is the -period expectation of the charge recursion. Defining it through the closed form (20), through , or defining or optimality through , would make the goal a statement about the full-discharge model or a restatement of milestone 9, and is excluded.
Not in scope: Theorem 1 (strategic complements), Theorem 3's closed-form optimal decisions, Theorem 4's second and third bullets (), the partial-discharge model (Theorems 5–6), the capacitated generator (Theorem 7) and the numerical study. The recursion and the unit-cube encoding of i.i.d. uniform generation are reusable for related storage and inventory models. Contributions are welcome for any milestone and for the existence of an optimal tracking plan.
A manager's voluntary report can change more than investors' estimate of a firm. It can change what a controlling shareholder does to the firm. Jia and Menon study a shareholder who privately knows the value of an alternative strategy and may replace the current strategy. Investors observe intervention but do not observe that private value. A shareholder who expects to sell soon therefore weighs the market price after intervention along with the eventual liquidation value. The manager can influence that choice by disclosing or withholding the value of the current strategy. The question matters for accounting and corporate governance because withholding information can improve the firm's eventual value even when the manager has no direct preference for a higher short-term stock price. Jia and Menon, authors' manuscript, §§1–2.
The paper's Proposition 1 identifies a change in the form of equilibrium disclosure as the shareholder puts more weight on the interim price. The same model gives full disclosure when that weight is zero, disclosure of both low and high values at moderate weight, and disclosure only of high values at greater weight. This mission targets that proposition, with its intervention and Bayes equations as intermediate statements. Jia and Menon, Proposition 1, p. 18 of the authors' manuscript.
The current firm value is uniformly distributed on . With probability , the manager privately learns its realization. An informed manager may truthfully disclose or remain silent; an uninformed manager cannot disclose or reveal that he is uninformed. A controlling shareholder privately observes an alternative value , uniformly distributed on , then chooses whether to intervene. Intervention makes the liquidation value equal to ; otherwise . Investors see the manager's disclosure decision and the shareholder's intervention decision , and set a competitive price . Jia and Menon, §2, pp. 6–8.
The shareholder's utility is , where measures the weight on the interim stock price. The manager in the main model maximizes . The paper writes for shareholder short-termism. Assumption 1 requires , so intervention is a live option at every current value. Jia and Menon, §2 and Assumption 1, pp. 7–8.
An equilibrium specifies the informed manager's disclosure set , the belief after no disclosure, and a shareholder intervention threshold after each disclosure decision. Here . Truthful disclosure reveals , so the intervention threshold after that announcement uses belief . After silence, investors and the shareholder account for both informed managers who withheld and uninformed managers who could not disclose. The shareholder best responds to either belief. The informed manager compares expected liquidation values under the resulting interventions and discloses when indifferent. Jia and Menon, §§2–4, pp. 7–18.
The goal is Proposition 1. There is a , fixed by the model parameters before is chosen, for which an equilibrium exists for every . Every equilibrium has the corresponding disclosure region:
In the two-tailed regime, and . In the upper-tailed regime, . The common belief and shareholder intervention threshold are
The supporting targets are the paper's Lemma 1 for the shareholder threshold, equations (7)–(8) for the manager's expected value, the zero-short-termism benchmark, equation (14) for the disclosure decision, and equations (15), (18), and (19) for the two Bayes fixed points and the lower threshold. The milestone list retains the source's labels and text. Jia and Menon, Proposition 1, pp. 18–20, and Appendix, pp. 36–39.
The proposition separates two reasons to disclose: a low current value can prompt beneficial intervention, while a high current value can deter intervention that would destroy value. As the shareholder cares more about the price effect of intervention, the low-value disclosure region disappears. The result therefore gives a precise condition under which voluntary silence can protect liquidation value, despite the manager's exclusive concern for that value. The paper also uses the equilibrium in its later analysis of market reactions and comparative statics. Jia and Menon, §§4–5.
The result is proved in the cited paper; the remaining task here is a machine-checked Lean proof of the stated model, its best-response and Bayes identities, and Proposition 1. The proposal contains proof targets with sorry, not completed machine-checked proofs. Definitions of threshold responses and Bayes beliefs should remain reusable for other disclosure games, provided their priors and tie conventions are checked against those games.
The manager's choice cannot be inferred from the current value alone. Disclosure changes the shareholder's belief, the probability of intervention, and the conditional alternative value revealed to investors by intervention. Comparing only the chance of intervention misses the price effect that makes the shareholder act too often. Comparing only the two conditional means misses how often each action occurs. Jia and Menon, §§3–4.
The equilibrium also imposes a fixed-point condition: the withholding interval determines the belief after silence, while that belief determines which values a manager withholds. The form of the interval changes at . At the boundary, the low endpoint is a manager indifference point and remains disclosed. The challenge is to establish existence in each regime and characterize every equilibrium with those endpoint conventions, including the extreme shareholder weight . Jia and Menon, Proposition 1 and Appendix proof, pp. 18, 36–39.
Lean uses real values and interval integrals against the two uniform laws. The lower support endpoint of is zero, as in the paper. The Standing predicate includes Assumption 1 and the explicit added restriction : the source says "with probability " but does not give strict bounds, while its Bayes formulas and nondisclosure regions need a nondegenerate informed population. The shareholder weight is quantified over ; is derived from it. Set integrals on a withholding region are used only when equilibrium makes the region measurable and contained in the bounded support. The conditional mean at the zero-probability endpoint is assigned its limiting value so total real functions do not introduce a zero-over-zero artifact.
The shareholder's best-response condition is weak at indifference, while the manager's tie-break requires disclosure. Equation (14) prints a strict inequality even though the paper says an indifferent manager discloses; the Lean decision condition uses . The target requires an equilibrium for every admissible and describes every equilibrium, so its universal characterization cannot hold vacuously. The shareholder threshold and manager payoff are defined from utility and integrals, rather than by the closed formulas being posed as milestones. The goal covers the paper's long-term manager case ; Proposition 3 and the later comparative statics are outside this mission.
Impulse control models a decision maker who acts on a system by discrete interventions rather than continuously: a central bank adjusting a rate, a firm switching production capacity, a portfolio manager rebalancing with fixed transaction costs. Each intervention has a fixed cost, so the controller chooses both when to act and how much. In many applications an order is not executed the moment it is given: there is an execution delay between the decision and its effect, during which the controller cannot revise it.
Djehiche, Hamadène, Hdhiri and Zaatra (arXiv:1904.11924v2, published in Mathematics of Operations Research, 2022) study the infinite-horizon version of this problem with random coefficients: the state process and the reward are only assumed progressively measurable with respect to a Brownian filtration, not Markovian. Without a Markov structure the usual route through quasi-variational inequalities is unavailable, and the authors work instead with optimal stopping and (reflected) backward stochastic differential equations.
Execution delay in impulse control goes back to Robin (1976) for diffusions. It was treated for inventory problems with delivery lags by Bar-Ilan and Sulem (1995), for delayed reaction by Øksendal and Sulem (2008), and on a finite horizon by Bruder and Pham (2009), all in Markovian settings. Non-Markovian impulse control without delay was studied by Djehiche, Hamadène and Hdhiri (2010), and with execution delay by Hdhiri and Karouf (2018). The paper under formalization treats delay, random coefficients and an infinite horizon together; its stated main issue is the continuity of the value process.
Let carry a standard -dimensional Brownian motion , and let be its natural filtration augmented by the -null sets. The data are:
A strategy is a sequence of stopping times and -measurable -valued impulses. It is admissible, , if almost surely. The impulse decided at takes effect at :
The value is built by an iterated optimal stopping scheme. For an index , a stopping time and a finitely-valued -measurable , set , and for define the obstacle
and the Snell envelope
The sequence increases to a limit , with obstacle given by the same formula with in place of .
Define , , and let be an -measurable -valued maximiser in the obstacle. Then is optimal:
The formal goal asserts that the scheme and its obstacle exist, that a strategy satisfying the recursion exists, and that every such is admissible, attains , and dominates every admissible strategy.
In the order the proof uses them: Proposition 4.1 (the scheme is well-posed, , ); Remark 4.2 (gluing over the values of ); Proposition 4.2 i) (monotone convergence, càdlàg limit, the Snell identity for ) and ii) (independence of the starting time after ); the measurable maximiser of the proof of Proposition 5.3; the bound (6.27) on ; Proposition 6.4 (continuity of ); the full optimal-stopping identity at the first hitting time, Appendix (8.54), including the essential supremum after a random starting time; and the two halves of the proof of Theorem 6.1, and for every .
Theorem 6.1 reduces a control problem over sequences of stopping times and impulses, with delayed effect, to a countable family of single optimal stopping problems, and identifies an optimal strategy explicitly from the value process. It gives existence of an optimal strategy in a non-Markovian infinite-horizon setting where no verification theorem for a quasi-variational inequality is available.
The result is proved on paper. As far as is known it has no machine-checked proof. Formalizing it would add a continuous-time optimal stopping layer (Snell envelopes with values at , first hitting times after random times) that the current libraries lack, and a precise record of the conventions the paper leaves implicit: values at , versions of optional projections, and the index shift between Sections 3 and 6.
The obvious argument is a dynamic programming verification: show the value satisfies a fixed-point equation, then check the candidate strategy attains it. Here the candidate strategy stops at the first time meets its obstacle , and that time is optimal only if the Snell envelope is continuous. The limit of increasing continuous supermartingales is only càdlàg, and the obstacle involves at the shifted time , so a jump of propagates to a jump of and back. Ruling out these jumps (Proposition 6.4) is the main technical step of the paper; it uses that the Brownian filtration is quasi-left continuous, and fails for general filtrations. The remainder needs a continuous-time Snell envelope theory over stopping times that may be infinite, which Mathlib does not provide.
Fin l → ℝ; is a nonempty Finset. Time is ℝ≥0; stopping times take values in WithTop ℝ≥0. The filtration is the published ReflectedBSDE.Existence.augmentedFiltration of a standard Brownian motion (Peng1990.SMP.IsStdBrownian). It is never an arbitrary filtration. The essential supremum is the published ReflectedBSDE.Existence.IsEssSupOver.The bibliographic data are those of the paper's reference list (arXiv:1904.11924v2, pp. 28–29).
Rank aggregation turns many local comparisons into one global ordering. In a sequential setting, the experimenter chooses which two items to compare next, sees a noisy binary answer, and decides when enough evidence has been collected. More comparisons can improve the ranking, but each comparison has a cost. This tradeoff appears in preference elicitation and pairwise choice studies, where comparisons are easier to obtain than an entire ranking. Chen, Chen, and Li study how to make that tradeoff when comparison outcomes follow a parametric probability model and the per-comparison cost tends to zero (preprint, §§1–3).
The paper states a lower bound on the minimum Bayes risk among all sequential ranking policies, upper bounds for two explicit policies, and a corollary that the policies attain the minimum asymptotically. The central question is therefore precise: can a comparison rule that learns which pairs are informative achieve the same leading Bayes risk as a policy that may use any admissible adaptive selection, stopping, and ranking procedure? This mission targets that corollary in the arXiv version 1710.06056v1, including the supplemental proofs (paper and supplement).
There are items. Their latent scores are ; fixing the first score removes the otherwise unidentifiable common shift. The parameter has a prior density on , with support . Each available arm is a pair with . A comparison of that pair produces with probability mass function ; favors item . The Bradley–Terry–Luce model is one example, but the result allows a broader family of positive comparison mass functions (§2, pp. 5–6).
A sequential ranking policy consists of an adaptive randomized pair-selection rule , a stopping time for the observed comparison history, and a terminal permutation . The permutation induces pair decisions when item is ranked ahead of item . Its Kendall loss counts pairwise errors against the strict ordering of the latent scores. A comparison costs , so the policy's Bayes risk is
The infimum covers every adaptive randomized pair selector, stopping time, and ranking measurable at stopping. A policy that never stops pays infinite comparison cost. These are the objects of equations (2.2)–(2.5) (§2, pp. 6–7).
For each candidate parameter, the comparison log likelihood sums the log probabilities of the first observed outcomes. The two proposed generalized likelihood ratio stopping times compare the best log likelihoods on opposite sides of each pair-ordering boundary. Both use the threshold , , and start checking after the first comparison. At stopping, ranks a maximum likelihood estimate (§3.1, pp. 8–10).
The pair-selection rule uses the max–min information value : among probability distributions on comparison pairs, it maximizes the minimum weighted KL divergence to a parameter that induces a different ranking. It mixes a maximizing allocation evaluated at the current MLE with uniform exploration. The mixing probability is asymptotically, where and (§3.1–3.2, pp. 8–13).
The goal is Corollary 4: for each , the concrete policy exists and its risk satisfies
The mission's milestones state the paper's information bound for the least distinguishable alternative (Lemma 13), the maximal Azuma–Hoeffding inequality (Lemma 8), a level-crossing bound for Lipschitz random fields (Lemma 9, stated with a guard that the printed version omits and without which it is false), the unrestricted Bayes-risk lower bound (Theorem 1), the stopped likelihood-ratio tail estimate (Lemma 11), the bound for of order (Lemma 10), the expected Kendall-loss bound (Theorem 2), the within-ranking regularity of (Lemma 14), the expected sample-size bound (Theorem 3), and the paper's claim that the ε-greedy selection rule satisfies the exploration and allocation conditions A6 and A8. Theorems 1–3 separate the lower benchmark, error cost, and sampling cost; the corollary combines them as a statement about the true policy risk and the true unrestricted infimum (pp. 12–13, 22–23, 25, 38, 42).
The result identifies a pairwise-comparison procedure whose Bayes risk has the best possible leading order when comparisons become cheap. A lower bound alone does not identify a usable procedure; an upper bound for the two proposed rules alone does not show that a better adaptive policy cannot improve the leading risk. Together they explain the value of balancing uniform exploration against information-directed pair selection in this model (Theorems 1–3 and Corollary 4).
The analytic results are proved in the paper; they are not yet machine checked in this mission. The published Lean bandit definitions already supply a reusable randomized interaction law, natural filtration, and stopping-time notion. A complete formalization would add the paper-specific ranking loss, KL allocation problem, GLR procedures, and asymptotic analysis on top of that substrate. The probability and decision-theoretic pieces can also be reused for other sequential identification problems.
The likelihood-maximizing parameter and information-maximizing allocation both depend on observed data, while the pairs selected next depend on those estimates. This feedback prevents replacing the adaptive experiment with a fixed independent sample sequence. The stopping rules also inspect likelihood maxima over sets of parameters with opposing pair orders, so a pointwise likelihood estimate does not by itself control the stopping event uniformly over those sets. Finally, comparing the policy risk with is insufficient: the corollary must compare it with the infimum over all admissible policies (§6 and supplemental Appendices A–I).
Parameters are functions Fin m → ℝ, with item 1 fixed at score zero; Lean's item index is one less than the paper's. Pair arms use the published StochasticBandit, BanditPolicy, and BanditTrajectory definitions. Binary comparison outcomes are rewards and . The norm on the finite parameter space is the sup norm, and A2's balls are centered in . A maximum likelihood estimate and a max–min allocation are represented by arbitrary measurable selectors satisfying the page's maximizing properties. Their existence is a mathematical obligation; the goal also asserts existence of the resulting exact policy family, so an empty policy class cannot make it true.
The Bayes risk, expected loss, expected stopping time, and optimal risk use . This retains the infinite cost of nontermination and avoids turning a nonintegrable expectation into zero. The supremum and infimum defining range over exactly the probability simplex and the set of rank alternatives in , and the likelihood suprema over the nonempty compact sets , so no default value of an empty or unbounded real supremum enters. Limits are from positive ; the exploration probability is clipped at away from zero. Ties in estimated scores are resolved by item index, and terminal rankings are required to be permutations. A4 is a uniform positive KL separation of differently ranked parameters of and, as the page's remark on A4 requires, contains no parameter with two tied scores. A6's exponent is existential, as printed; A8 is read uniformly over finite histories after the first uniformly sampled comparison. The prior is required to be a measurable probability density, and each binary comparison probability is positive so its logarithm is defined.
Contributions to the ten milestones, proofs of selector existence, a complete nonvacuity example, and reusable facts about stopped likelihoods and finite max–min KL problems are in scope. Lemmas 5, 6, 7 and 12 remain available as supporting work; the proposal lists only the source results whose statements have been pinned down here. The proposed goal is the explicit Corollary 4 ratio, never mere existence of a value function or a ratio against its own constructed benchmark.
Manufacturers that depend on a component often fund a new supplier whose technology could replace the incumbent one, while keeping the incumbent as a backup. Apple's 2013 prepayment to GT Advanced Technologies for sapphire production, which ended in the supplier's bankruptcy, and Intel's 2012 equity stake in ASML to accelerate extreme-ultraviolet lithography are the two cases that motivate Zhang and Lee (SSRN 3269249; Management Science, 2021, doi:10.1287/mnsc.2021.4078). Such a funder chooses between two instruments: a loan, repaid only up to what a failed supplier still holds, and an equity stake, which shares the supplier's value. The question the paper answers is which instrument induces the higher probability of technical success (PTS), once the existing supplier's reaction is taken into account.
The comparison sits between two literatures. Corporate finance knows the cost-shifting effect of debt under limited liability: a borrower who does not bear the cost of failure takes more risk (Brander and Lewis, 1986). Supply-chain work on collaborative development studies cost and effort sharing with a single supplier (Bhaskaran and Krishnan, 2009). The paper adds the incumbent supplier, whose cost reduction changes how much the manufacturer values the new technology.
Three firms play. The new supplier has no wealth. Reaching a PTS requires the verifiable investment and the unverifiable effort , with capabilities ; a larger means a more mature technology. The manufacturer sells units of an end product at price and offers a contract: an upfront investment , a cap on effort expenses, and an expected procurement payment , plus an equity share under equity. The supplier chooses and a filed effort expense subject to
Under equity the supplier's value is , it earns , and the share is the fair valuation . Under a loan (interest normalized to ) it earns . The manufacturer maximizes its payoff over contracts subject to incentive compatibility (the supplier's choice maximizes its payoff) and participation.
If the new technology fails, the manufacturer buys from the existing supplier, which can lower its unit cost from to at cost and keeps the share of the surplus ; is the manufacturer's bargaining power. It maximizes . The manufacturer and the existing supplier play a static game, and , denote the PTS of its Nash equilibria under equity and under a loan. Two quantities drive the equilibrium:
and the paper assumes .
For equilibria with an uncertain R&D ():
The goal asserts only the threshold shape; it does not fix the thresholds' values, so it is stated about the equilibria of the two games, not about formulas.
The result locates the boundary between two effects. Under a loan, limited liability makes the supplier invest more (cost shifting), but the incentive fades as success becomes likely. Under equity the manufacturer shares the supplier's value and is willing to pay more for success (profit sharing). Proposition 1 says profit sharing wins when the technology is mature enough, and that the incumbent's bargaining position acts non-monotonically: equity wins when the existing supplier is either weak or strong. The second part has no analogue when the incumbent's cost is exogenous, which is why the backup supplier matters. Proposition 2 of the paper, on the manufacturer's payoff, is stated in terms of the threshold .
The paper's proofs are pen-and-paper and partly informal: the contract analysis (pp. Appendix-18–23) proceeds by first-order conditions across case regions, and the comparison squares an inequality without treating the case where one side is negative. A machine-checked development would certify that the closed forms are the equilibria of the game as stated, including the participation and incentive constraints, and that the threshold structure holds without gaps. None of these results has a machine-checked proof on the platform.
The obstacle is Lemma A.1, not the algebra of Proposition 1. The manufacturer's problem is a moral-hazard contract design problem with a non-smooth agent: the supplier's choice of switches between the expense cap and the budget, the constraint set (3) has two caps, and under a loan the repayment is a minimum. Each candidate contract induces a best response that must be computed globally, not only from a first-order condition, and the optimal contract must be compared against every incentive-compatible alternative, including those with slack caps. Under equity the share is itself pinned by a fixed point with the induced PTS. A proof that only checks first-order conditions in the region where the paper's contract lives does not establish optimality.
A second difficulty is the equilibrium layer: the manufacturer's optimum depends on , and on the PTS, so the equilibrium PTS solves a fixed-point equation, and boundary equilibria ( or ) must be excluded by the hypotheses and .
All quantities are real numbers. The parameters form a record with the standing assumptions , , and, added, . The loan's interest is dropped, following the paper's normalization . An outcome of each game is a contract together with the supplier's response; it is admissible when the response maximizes the supplier's payoff over (3) (the maximizer is chosen with the contract, the standard principal–agent tie-break), participation holds, , and, under equity, with . The equilibrium is the platform's generic pure Nash equilibrium with feasible sets (CarbonDoubleCount.Planner.IsPureNash), instantiated with the manufacturer (admissible outcomes) and the existing supplier ().
The goal quantifies over all equilibria with ; the Lemma 1 milestones assert that such equilibria exist when , so the goal is not vacuous. Substituting the closed forms (6), (7) for the equilibrium PTS in the goal would trivialize it into the proof-of-Proposition-1 milestones and is ruled out. In (i) only varies, with fixed; the paper's remark that is not imposed. In (ii) the thresholds are real numbers. The printed proposition puts them in , while its proof explicitly allows them to lie outside that interval when a region disappears; the formal statement follows the proof. The derivative claims of Lemma 1, Proposition 2 and the benchmark models of §5 are out of scope.
A complete development needs a global analysis of the agent's best response under (3), optimization of a concave function over , and real-algebra lemmas about square roots. Contributions on any milestone are welcome; milestones 1 and 5 are independent of the contract analysis.
Firms increasingly source design work (logos, packaging, product sketches) through crowdsourcing contests: a seeker posts a problem statement and an award, independent designers submit entries, and the best entry wins. The problem statement is the seeker's main lever. It can list conceptual objectives (what the design should convey) and execution guidelines (fonts, colours, shapes to use). Practitioners disagree on how much to specify: more detail tells designers what the seeker values, but also raises the effort needed to take part.
Jiang, Huang and Beil (SSRN 3260862, 2018; Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2020.0873) model this trade-off and test it on data from a design-contest platform. Their theory builds on the contest model of Terwiesch and Xu (Management Science 54(9):1529–1543, 2008), in which designers generate several trials with Gumbel-distributed quality shocks and free entry fixes the number of participants. The new ingredient is the problem statement: the number of disclosed objectives and the number of execution guidelines enter designers' costs and the quality of their designs. Theorem 1 of the paper describes how designers respond. This mission formalizes that theorem.
A seeker offers an award and discloses conceptual objectives and execution guidelines. A designer who takes part chooses the number of objectives to incorporate and the number of design trials to generate. Objectives beyond the disclosed must be guessed.
Here are the unit costs of guessing and of understanding an objective, is the probability that a sampled concept meets one objective (so attempts are expected, each costing ), and is decreasing.
and a participant's expected utility is . Not taking part yields the outside option .
The win probability (A.1) from Gumbel shocks; the marginal winning chance; the trial-effort condition (A.3); ; the equilibrium characterization (A.2)–(A.3) at fixed ; and an entry utility free of ; the closed forms (A.5) and (A.6) ; the rise of the entry utility with in Region 0; and the decrease of and in .
Theorem 1 is the paper's theoretical core. It predicts an inverted-U relation between disclosed objectives and participation, and no effect of execution guidelines on participation, only on effort. Section 4 turns these predictions into hypotheses, and §5 tests them on contest data. The seeker's optimal disclosure (Proposition 1) is derived from the same characterization.
The theorem is published with a proof in the appendix, but nothing in it has been machine-checked. A formal development makes three of the paper's choices explicit. It separates the parts of the proof that are first-order algebra from the parts that need a global argument. It states the free-entry level as a condition, not as a root of a formula. And it isolates the claims the proof does not support (see Formalization scope). The contest model (logit win probability, cost (1), free entry) is shared with other crowdsourcing models built on Terwiesch and Xu (2008), and its definitions can be reused for them.
The payoff is not concave in the designer's choices. The win probability (A.1) is a logistic function of , convex while , so first-order conditions do not identify best responses. A newcomer's first idea, "solve the first-order conditions and invoke concavity", fails. Uniqueness survives because any equilibrium must satisfy the first-order conditions, but at the kink only one-sided conditions are available, and they must be combined into the three regions of (A.2).
The monotonicity of is a second difficulty. The entry utility is not monotone in , so can have several roots and can jump as varies. The region-0 formula (A.4) is implicit, because depends on . Comparing at two values of therefore needs the largest-root description of free entry, not a closed form.
Everything is real-valued, as the paper allows (p. 9). The namespace is ProblemSpec.Equilibrium. A single definition file holds the parameters, the standing assumptions, , , (A.1), the expected utility, the symmetric equilibrium, , , , , the entry utility, the free-entry condition and the closed forms , . The win probability is (A.1) itself, for real , as in the paper. The milestone (A.1) connects it to i.i.d. Gumbel shocks for integer trial counts, using the published Gumbel law of AssortSearch.Cannibal.Model.
The formalization commits to the following conventions and additions:
Two claims of the page are not stated. Existence is false. Theorem 1 says is the symmetric equilibrium. At , , , , , , , , , , , the free-entry level is , with , , and equilibrium utility . A designer who deviates to , earns about . The goal therefore states uniqueness only. The "first … then" ordering is stated region by region. Monotonicity holds on the points where designers guess and on the points where they do not, but the guessing points need not form an initial segment of values, because can jump. "Decreases" is weak, since with , is constant.
Not in scope: Lemma 1, Proposition 1 and Lemmas 2–8 (the seeker's problem and extensions), and the empirical sections.
Welcome contributions: proofs of the milestones, especially the uniqueness argument at the kink , the Gumbel computation (A.1), and the comparison of free-entry levels in the goal's part 3.
Load balancing asks for an assignment of jobs to machines that keeps the largest machine load, the makespan, small. On unrelated machines the processing time of a job may depend arbitrarily on the machine; the deterministic problem has the classical -approximation of Lenstra, Shmoys and Tardos (1990). In many applications (virtual-circuit routing, assigning customers to warehouses, cloud jobs) the processing times are not known when the assignment is made, only their distributions are. The assignment is fixed up front, the sizes are then revealed, and the quantity to control is the expected makespan.
Timeline:
There are machines and jobs . On a probability space, the random variable is the size of job on machine . Jobs are independent: the vectors for different are independent, while the sizes of one job on different machines may be correlated. An assignment puts the jobs on machine , and its expected makespan is
Every size splits into a truncated part and an exceptional part . The effective size of a random variable at an integer is
The algorithm works at a scale on the sizes . With , the LP with parameter asks for with
The class loop starts with ; while it gives the machines the class and removes them. The class defines a generalized assignment instance with processing times and costs , which the Shmoys–Tardos algorithm rounds to an assignment with
There is an absolute constant such that for every instance and every :
For , taking , (A)–(C) give an assignment of expected makespan at most ; a binary search over loses a factor . The constant is left unspecified so that the goal survives any improvement of the lower-bound constants.
In attack order: Lemma 1 (exceptional items lower bound) and Lemma 4 (truncated items lower bound); Lemma 5 (valid inequalities) and Proposition 1 (LP lower bound), which give (A); Observation 1 (the class loop terminates; at most machines of class ) and Observation 2 (the GAP rounding), which give (B); Lemma 2 (effective-size Chernoff bound), the effective-size facts and , Observation 3 (tail ), Lemma 7 (union bound over classes) and Lemma 6 (expected makespan ), which give (C).
Theorem 1 shows that the expected makespan on unrelated machines, a quantity that is #P-hard even to evaluate for a fixed assignment (Theorem 4 of the paper), can be approximated within a constant factor by a polynomial-size certificate: an LP with one effective-size constraint per subset of machines, measured at the parameter . The same LP technique underlies the budgeted variant in the same paper and enters the later -norm results (Molinaro 2019). Lemma 6 is a converse of the valid inequalities that needs only one constraint per machine, which is what makes the rounding through the generalized assignment problem possible.
All results here are proved on paper; none is formalized. A formalization produces a reusable effective-size calculus (Lemma 2, Jensen-type bounds) in Mathlib's probability library, an expected-maximum lower bound for independent variables (Lemma 1), and a Lean version of the Shmoys–Tardos rounding with costs. It also records two corrections found while pinning the statements: Lemma 5's inequality (3) fails under the threshold as printed (a -machine instance with expected makespan has ), so the threshold is an absolute constant ; and Lemma 1 requires independence, which the page omits.
The obvious approach maps every random size to one deterministic number and balances those. The paper shows (p. 7) that every such approach loses a factor on unrelated machines: the right effective size of a job depends on how many machines it competes for, which is not known in advance. The LP sidesteps this with exponentially many constraints, one per subset of machines, and the rounding cannot satisfy them all. The upper bound therefore rests on the class loop picking, for each machine, one parameter such that few machines have small classes and machines of large class have tails decaying like . On the lower-bound side, Lemma 4 rests on the Kleinberg–Rabani–Tardos analysis of Bernoulli variables, which the paper only cites, and Observation 2 rests on the Shmoys–Tardos rounding, also only cited.
Machines are Fin m with and jobs Fin n, both 0-based. The probability space is (Ω, P) with Ω : Type and IsProbabilityMeasure P; sizes are X : Fin m → Fin n → Ω → ℝ, each measurable, nonnegative and integrable (integrability keeps and the expected makespan from collapsing to the Bochner junk value ). Job independence is iIndepFun (fun j ω i => X i j ω) P, independence of the per-job vectors, not of all variables. Logarithms are natural. The makespan is the supremum over the finite set Fin m. Truncation keeps , the exceptional part keeps . is a junk value , never used.
The LP's are functions of , fixed by (6). The class loop is a recursion with fuel that recomputes each round; an unclassified machine gets the junk class , which Observation 1 rules out for feasible . The Shmoys–Tardos algorithm is represented by its guarantee: an output of the rounding is any assignment satisfying (13)–(14). The goal bounds every such assignment, which is stronger than bounding the one the algorithm returns, and (B) asserts that one exists. Running time, the ellipsoid separation oracle and the binary search over are not modelled.
None of the definitions mentions an optimal assignment or its value. A goal of the form "there exists with expected makespan at most " is ruled out: it is true with , because a minimizer exists among the assignments.
Corrected statements: Lemma 1 adds independence (and drops "discrete"); Lemma 5 and Proposition 1 replace the threshold by an absolute constant , with the of (4) equal to ; Lemma 4's is an absolute constant . Welcome contributions: the effective-size Chernoff bound, the Jensen facts, Observation 1 (pure combinatorics of the class loop), the union-bound and tail-integral steps of Lemmas 6–7, and a cost-preserving Shmoys–Tardos rounding.
Related platform results: UnrelatedSched.TwoApprox.rounding_load_bound and MatousekLP.Scheduling.rounding_makespan_le (Proved) carry out the Lenstra–Shmoys–Tardos rounding for deterministic sizes without costs; WilliamsonShmoys.generalized_assignment_cost_preserving_rounding (Open) is a cost-preserving GAP rounding with load at most . None of them states Observation 2.
A manager can influence a project's output through effort, but the owner observes output rather than effort. When the manager can also trade privately in a financial market, a contract based on output and market returns changes both effort incentives and the manager's ability to hedge risk. The owner must decide what the contract pays, how sensitive it is to output, and how much market exposure it gives the manager. Huang, Ju and Xing formulate these choices as a continuous-time control problem in Optimal Contracting with Unobservable Managerial Hedging, the November 2017 working paper underlying the later Management Science article. This mission uses the working paper's equations and numbering.
The question is operational: given an initial promise to the manager, which admissible contract maximizes the owner's discounted cash flow? The paper's Proposition 2.3 answers with a payment boundary, a liquidation boundary, and sensitivities chosen from a two-dimensional control box. Formalizing that proposition requires the value to come from the control problem itself. The free-boundary equation alone does not identify a contract or prove its optimality.
The state is the manager's contract value, with initial promise . The owner controls the contract sensitivity , gross market exposure , and a nondecreasing cumulative payment process . The two shocks and are independent standard Brownian motions. The project is liquidated at . Time-zero payment is permitted and is charged to the owner.
Effort lies in and costs . The manager's effort response is the minimizer of over that interval. The regular controls lie in and . With and , the state dynamics of equation (21) are
The principal's value is the least upper bound of expected payoffs over admissible contracts from . Equation (24) includes the discounted output and effort flow, the discounted payment measure, and the liquidation payoff , all scaled by . Admissibility includes the paper's transversality condition (57). The value is a control value, not an arbitrary solution of a differential equation.
The first target is the value characterization of Proposition 6.4. On the continuation interval , is twice continuously differentiable and satisfies
Here and . At and above , ; at the boundary, and . Proposition 6.4 also states concavity on and strict concavity on .
The mission goal is the stronger Proposition 2.3: for each initial promise, a reflected contract attains . It pays immediately, makes further payments only when the contract value is at , and liquidates when the value reaches zero. Before liquidation its sensitivities come from maximizers of the displayed Hamiltonian's control-dependent terms. The market sensitivity is recovered from and by .
Proposition 2.3 connects a value function to an implementable payment and risk-sharing rule. The upper boundary describes when the owner returns part of the manager's contract value as cash; the lower boundary describes termination. Concavity records the owner's endogenous aversion to leaving value exposed to the manager's future actions. Without the attainment statement, a smooth solution of the HJB could remain only a candidate and would not determine an optimal contract.
The working paper gives an argument for these conclusions; the statements here are open Lean targets. A complete development would check the stochastic control value, the regularity and comparison steps, and the existence of the reflected contract against the same definitions. The finite-horizon Itô integral and independent Brownian coordinates come from the published Peng1990.SMP.Stochastic definition. The effort clamp and the model-specific contract are new definitions for this mission.
The control has both regular choices and a singular payment process . If one optimizes an unconstrained payment rate as though it were an ordinary bounded control, the Hamiltonian is unbounded whenever . The correct value therefore has a gradient constraint and a free payment boundary. Showing that the resulting boundary rule actually attains the value also requires a reflected stochastic equation up to the liquidation time. The two Brownian shocks must remain separate: merging them changes the information available to the controls.
Lean represents as time-indexed real processes on an underlying probability space. Brownian coordinate zero is the market shock; coordinate one is the idiosyncratic shock. The filtration is the Brownian filtration supplied by Peng1990.SMP.Stochastic, and Itô integral conditions hold on every finite horizon. This is the reduced principal's problem (24). The manager's separate optimization in Lemma 2.2 and the original output and market processes are outside the model; incentive compatibility enters through .
The formalization uses real-valued payoffs and an explicit least-upper-bound condition for every , so empty or unbounded feasible payoff sets cannot silently produce Lean's default real supremum. The control box is compact under the standing interval assumptions. Its Hamiltonian and net-contribution suprema are therefore genuine finite suprema. The convention for an empty set in the definition of is , matching the degenerate zero-continuation case. Derivatives at zero use one-sided, within-set derivatives.
The paper's formulas use and the proof uses a diffusion coefficient bounded away from zero. The model explicitly assumes and in addition to the paper's stated interval and cost bounds. Admissible contracts have integrable drift and payoff and finite expected discounted payments, so a nonintegrable real integral cannot become zero by Lean's total-function convention. Payments use the Stieltjes measure of , extended by zero before time zero; this charges an immediate lump sum. The transversality limit is taken along deterministic times as in the proof of Lemma 6.3. The value is the supremum of admissible contract payoffs, not a function postulated to solve the HJB. Contributions formalizing the comparison theorem, the singular-control dynamic programming step, or the reflected equation are directly useful to the goal.
Most employment relationships rely on incentives that no court enforces. A relational contract is a self-enforcing promise: the employer pays a discretionary bonus after observing effort, and keeps the promise because reneging would destroy the value of the future relationship (Bull 1987; MacLeod and Malcomson 1989; Levin 2003). This mechanism has a well-known weakness. When the relationship has a known last period, no bonus is credible in that period, and backward induction removes it from every earlier period as well.
A second source of incentives is reciprocity. Workers respond to a generous upfront wage with higher effort, the "gift exchange" of Akerlof (1982), a pattern documented in many laboratory and field studies. Fahn (Reciprocity in Dynamic Employment Relationships, Management Science 2023, doi:10.1287/mnsc.2022.4657; working paper CRC TRR 190 Discussion Paper No. 198, 2019) combines the two in a finite-horizon principal–agent model. In this model the agent's reciprocity is tied to the relational contract and vanishes if the principal reneges. Because reciprocity is valuable even in the last period, the employer has something to lose by reneging at every date, so bonuses stay credible despite the known end date.
The paper's main dynamic result, Proposition 1, describes how the two incentive instruments evolve over the relationship. This mission formalizes that result, together with the lemmas its proof uses, in the reduced optimization problem the paper derives. All page references are to the 2019 working paper.
There is one principal and one agent, both risk neutral, over periods with . Effort costs the agent and yields output to the principal, with productivity . The reciprocity parameter measures how strongly the agent responds to an upfront wage, and the two parties share a discount factor .
In each period the principal pays an upfront wage before effort is chosen and may pay a bonus afterwards. An agent who reacts only to the wage chooses the deviation effort . The paper reduces the equilibrium analysis (its Lemma 2) to the following per-period problem. To implement effort at wage , the principal must pay the bonus
and her per-period profit is . A promised bonus is credible only if it does not exceed what the principal would lose by reneging. This is the dynamic enforcement constraint
where denotes the principal's continuation profit from period on, and . A profit-maximizing path is one in which, for every , the pair maximizes over subject to (DE), and . The bonus paid in period is . In the last period the bound is , so the problem becomes the reciprocity spot contract, in which no bonus is paid.
The first-best levels maximize without (DE). (DE) is said to bind in period when no first-best pair satisfies it. Two reciprocity thresholds appear in the results: , and, for a (DE) multiplier , .
Along every profit-maximizing path, for :
Moreover, whenever , strict changes propagate forward and equalities propagate backward:
The goal is stated for every , , and , and contains no closed-form expression.
These follow the paper's proof order:
Proposition 1 predicts the shape of incentive pay over a finite employment spell. Effort, wage and bonus are flat early on, while the future is valuable enough that (DE) does not bind. Once it binds, the bonus falls and the upfront wage rises in every remaining period, and effort declines because the substitution is incomplete. Relational and reciprocity-based incentives are therefore dynamic substitutes. The paper relates this to observed effort patterns near the end of employment relationships and to the experimental evidence of Boosey and Goerg (2018).
The result is proved in the paper, with an argument that mixes first-order conditions, the implicit function theorem, and an induction on continuation profits. To our knowledge none of it has been machine-checked. A formal proof would check the case split between zero and positive wages and between slack and binding periods, which the paper's proof treats in prose. It would also establish the uniqueness and existence facts that the phrase "the equilibrium" presupposes. The milestones are reusable on their own: they give the explicit optimizers of a one-period contracting problem with a cubic cost and a square-root reciprocity term.
The obvious approach is comparative statics. Treat each period's problem as a parametric program in the bound , show that its solution moves monotonically in , and combine this with decreasing in . Two steps of this approach fail as stated.
First, the profit is not jointly concave on the feasible set: the term and the cross term make the Hessian indefinite where . In addition, the wage has a corner at that is active for some parameters and not for others. Uniqueness of the optimum, and the regularity needed to differentiate it, have to be obtained rather than assumed.
Second, the bound is not exogenous. It is the discounted value of the next period's problem, so monotonicity in requires an induction that runs backward through the value functions (Lemma 5). The step from monotone bounds to monotone wages and bonuses must also handle the switch between the zero-wage and positive-wage branches.
The strict-propagation clauses are sharper than plain monotonicity: they also require that the solution responds strictly to whenever (DE) binds.
The Lean development formalizes the reduced problem of p. 17, not the paper's game. Histories, strategies, the norm function and subgame norm-perfect equilibrium do not appear, and Lemma 2's reduction from the game to the per-period problem is not part of the mission. The conventions are as follows:
A formalization that fixes the path by closed forms in a given multiplier sequence, or that assumes (DE) slack or binding throughout, would make the goal a computation. The goal therefore quantifies over every profit-maximizing path, and a separate milestone shows that such a path exists.
A complete development needs elementary real analysis (one-variable calculus, monotonicity from derivatives, and existence of maximizers of continuous coercive functions) and an induction over the finite horizon. All of this is available in Mathlib. Proofs of any milestone are welcome, as are alternative routes to the goal that avoid multipliers.