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?
We present a general dilation scheme for quantum instruments with continuous outcome space in finite dimensions, in terms of an indirect POVM measurement performed on a finite dimensional ancilla. The general result is then applied to a large class of instruments generated by operator frames, which contains group-covariant instruments as a particular case, and allows to construct dilation schemes based on a measurement on the ancilla followed by a conditional feed-forward operation on the output. In the case of tight operator frames our construction generalizes quantum teleportation and telecloning, producing a whole family of generalized teleportation schemes in which the instrument is realized via a joint POVM at the sender combined with a conditional feed-forward operation at the receiver.
This mission is the statement-level formalization of Realization schemes for quantum instruments in finite dimensions (arXiv:0810.3211v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Equivalent left-tight frame identities (Definition 4 and Eq.(85), PDF p. 17). 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.
18 results of the paper are not stated yet, because the library lacks an interface they need:
We study analogues of Jucys-Murphy elements in cellular algebras arising from repeated Jones basic constructions. Examples include Brauer and BMW algebras and their cyclotomic analogues.
This mission is the statement-level formalization of On Cellular Algebras with Jucys Murphy Elements (arXiv:0907.3459v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 6.10 (see [4], Lemma 2.3) — degenerate affine skein power identity (Lemma 6.10 (see [4], Lemma 2.3), PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
37 results of the paper are not stated yet, because the library lacks an interface they need:
Lie's Third Theorem, asserting that each finite-dimensional Lie algebra is the Lie algebra of a Lie group, fails in infinite dimensions. The modern account on this phenomenon is the integration problem for central extensions of infinite-dimensional Lie algebras, which in turn is phrased in terms of an integration procedure for Lie algebra cocycles. This paper remedies the obstructions for integrating cocycles and central extensions from Lie algebras to Lie groups by generalising the integrating objects. Those objects obey the maximal coherence that one can expect. Moreover, we show that they are the universal ones for the integration problem. The main application of this result is that a Mackey-complete locally exponential Lie algebra (e.g., a Banach-Lie algebra) integrates to a Lie 2-group in the sense that there is a natural Lie functor from certain Lie 2-groups to Lie algebras, sending the integrating Lie 2-group to an isomorphic Lie algebra.
This mission is the statement-level formalization of Categorified central extensions, 'etale Lie 2-groups and Lie's Third Theorem for locally exponential Lie algebras (arXiv:0812.1673v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is A discrete generalized cocycle gives the explicit loop prolongation (Lemma II.3: discrete cocycle loop prolongation, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
42 results of the paper are not stated yet, because the library lacks an interface they need:
A simple unifying view of the exceptional Lie algebras is presented. The underlying Jordan pair content and role are exhibited. Each algebra contains three Jordan pairs sharing the same Lie algebra of automorphisms and the same external su(3) symmetry. Eventual physical applications and implications of the theory are outlined.
This mission is the statement-level formalization of Exceptional Lie Algebras, SU(3) and Jordan Pairs (arXiv:1112.1258v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is G2: the external A2 hexagon and two weight triangles (§4 opening, Fig. 2: the g2 prototype, 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.
10 results of the paper are not stated yet, because the library lacks an interface they need:
We study the product formula in the framework of (unbounded) functional calculus of sectorial operators . We give an abstract result, and, as corollaries, we obtain new product formulas for the holomorphic functional calculus, an extended Stieltjes functional calculus and an extended Hille-Phillips functional calculus. Our results generalise previous work of Hirsch, Martinez and Sanz, and Schilling.
This mission is the statement-level formalization of Product formulas in functional calculi for sectorial operators (arXiv:1309.0318v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract regularised calculus product formula (Theorem 2.5, 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.
23 results of the paper are not stated yet, because the library lacks an interface they need:
We describe a new method for approximating an arbitrary qubit unitary with precision using a Clifford and T circuit with gates. The method is based on rounding off a unitary to a unitary over the ring and employing exact synthesis. We also show that any qubit unitary over the ring with entries of the form can be exactly synthesized using Clifford and T gates using two ancillary qubits. This new exact synthesis algorithm is an improvement over the best known exact synthesis method by B. Giles and P. Selinger requiring elementary gates.
This mission is the statement-level formalization of Synthesis of unitaries with Clifford+T circuits (arXiv:1306.3200v1). 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 Approximate Clifford+T synthesis with two ancillas (Theorem 1, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
These lecture notes provide an elementary introduction, within the framework of finite quantum systems, to recent developments in the theory of entropic fluctuations.
This mission is the statement-level formalization of Entropic Fluctuations in Quantum Statistical Mechanics. An Introduction (arXiv:1106.3786v1). 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 Paper seed: finite-time quantum Evans–Searles symmetry (Proposition 3.3(7)) (Paper seed: finite-time quantum Evans–Searles symmetry (Proposition 3.3(7)), PDF p. 74). 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.
73 results of the paper are not stated yet, because the library lacks an interface they need:
We present a generalized version of classical geometric invariant theory `a la Mumford where we consider an affine algebraic group acting on a specific affine algebraic variety . We define the notions of linearly reductive and of unipotent action in terms of the fixed point functor in the category of --modules. In the case that we recuperate the concept of lineraly reductive and of unipotent group. We prove in our "relative" context some of the classical results of GIT such as: existence of quotients, finite generation of invariants, Kostant--Rosenlicht's theorem and Matsushima's criterion. We also present a partial description of the geometry of such linearly reductive actions.
This mission is the statement-level formalization of Reductive and unipotent actions of affine groups (arXiv:1406.4446v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Extensions of subgroup translation actions and normalized twisted cocycles (Observation 5.4, equations (4)–(7), PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
45 results of the paper are not stated yet, because the library lacks an interface they need:
In this note we collect several characterizations of unitary representations of a finite dimensional Lie group which are trace class, i.e., for each compactly supported smooth function on , the operator is trace class. In particular we derive the new result that, for some , all operators , , are trace class. As a consequence the corresponding distribution character is of finite order. We further show is trace class if and only if every operator , which is smoothing in the sense that , is trace class and that this in turn is equivalent to the Fr'echet space being nuclear, which in turn is equivalent to the realizability of the Gaussian measure of on the space of distribution vectors. Finally we show that, even for infinite dimensional Fr'echet-Lie groups, and are smoothing if and only if is a Schwartz operator, i.e., all products of with operators from the derived representation are bounded.
This mission is the statement-level formalization of On the characterization of trace class representations and Schwartz operators (arXiv:1512.02451v1). 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 Lemma 1.1: integrated operators preserve smooth vectors (Lemma 1.1, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
20 results of the paper are not stated yet, because the library lacks an interface they need:
We give a fresh account of the astonishing interplay between abelian von Neumann algebras, L^\infty-spaces and measure algebras, including an exposition of Maharam's theorem from the von Neumann algebra perspective.
This mission is the statement-level formalization of Abelian von Neumann algebras, measure algebras and L^\infty-spaces (arXiv:2108.06406v2). 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 Lemma 4.1: Existence of measure support (Lemma 4.1, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
55 results of the paper are not stated yet, because the library lacks an interface they need:
The quantum Schur transform is a fundamental building block that maps the computational basis to a coupled basis consisting of irreducible representations of the unitary and symmetric groups. Equivalently, it may be regarded as a change of basis from the computational basis to a simultaneous spin eigenbasis of Permutational Quantum Computing (PQC) [Quantum Inf. Comput., 10, 470-497 (2010)]. By adopting the latter perspective, we present a transparent algorithm for implementing the qubit quantum Schur transform which uses ancillas and can be decomposed into a sequence of Clifford + T gates, where is the accuracy of the algorithm in terms of the trace norm. We discuss the necessity for some applications of implementing this operation as a unitary rather than an isometry, as is often presented. By studying the associated Schur states, which consist of qubits coupled via Clebsch-Gordan coefficients, we introduce the notion of generally coupled quantum states. We present six conditions, which in different combinations ensure the efficient preparation of these states on a quantum computer or their classical simulability (in the sense of computational tractability). It is shown that Wigner 6-j symbols and SU(N) Clebsch-Gordan coefficients naturally fit our framework. Finally, we investigate unitary transformations which preserve the class of computationally tractable states.
This mission is the statement-level formalization of Generalised Coupling and An Elementary Algorithm for the Quantum Schur Transform (arXiv:2305.04069v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is General coupling preserves normalization and orthogonality in M (§IV.A, unnumbered: generally coupled states are normalized and M-orthogonal, PDF p. 13). 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:
We give an efficient randomized algorithm for approximating an arbitrary element of by a product of Clifford+ operators, up to any given error threshold . Under a mild hypothesis on the distribution of primes, the algorithm's expected runtime is polynomial in . If the operator to be approximated is a -rotation, the resulting gate sequence has -count , where is approximately equal to . We also prove a worst-case lower bound of , where , so that our algorithm is within an additive constant of optimal for certain -rotations. For an arbitrary member of , we achieve approximations with -count . By contrast, the Solovay-Kitaev algorithm achieves -count , where is approximately .
This mission is the statement-level formalization of Efficient Clifford+T approximation of single-qubit operators (arXiv:1212.6253v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Units and totally nonnegative unit squares (Lemma 10: units and totally nonnegative unit squares, 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.
9 results of the paper are not stated yet, because the library lacks an interface they need:
The celebrated Evans-Searles, respectively Gallavotti-Cohen, fluctuation theorem concerns certain universal statistical features of the entropy production rate of a classical system in a transient, respectively steady, state. In this paper, we consider and compare several possible extensions of these fluctuation theorems to quantum systems. In addition to the direct two-time measurement approach whose discussion is based on (LMP 114:32 (2024)), we discuss a variant where measurements are performed indirectly on an auxiliary system called ancilla, and which allows to retrieve non-trivial statistical information using ancilla state tomography. We also show that modular theory provides a way to extend the classical notion of phase space contraction rate to the quantum domain, which leads to a third extension of the fluctuation theorems. We further discuss the quantum version of the principle of regular entropic fluctuations, introduced in the classical context in (Nonlinearity 24, 699 (2011)). Finally, we relate the statistical properties of these various notions of entropy production to spectral resonances of quantum transfer operators. The obtained results shed a new light on the nature of entropic fluctuations in quantum statistical mechanics.
This mission is the statement-level formalization of Entropic Fluctuations in Statistical Mechanics II. Quantum Dynamical Systems (arXiv:2409.15485v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite ancilla tomography recovers the entropic functional (finite-ancilla-tomography, PDF p. 13). 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.
28 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper we consider the -function (the Holevo capacity of constrained channel) and the convex closure of the output entropy for arbitrary infinite dimensional channel. It is shown that the -function of an arbitrary channel is a concave lower semicontinuous function on the whole state space, having continuous restriction to any set of continuity of the output entropy. The explicit representation for the convex closure of the output entropy is obtained and its properties are explored. It is shown that the convex closure of the output entropy coincides with the convex hull of the output entropy on the convex set of states with finite output entropy. Similarly to the case of the -function, it is proved that the convex closure of the output entropy has continuous restriction to any set of continuity of output entropy. Some applications of these results to the theory of entanglement are discussed. The obtained properties of the convex closure of the output entropy make it possible to generalize to the infinite dimensional case the convex duality approach to the additivity problem.
This mission is the statement-level formalization of On entropic quantities related to the classical capacity of infinite dimensional quantum channels (arXiv:quant-ph/0411091v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §6, unnumbered Theorem: convex-duality additivity equivalence and consequences (§6, unnumbered Theorem: convex-duality additivity equivalence and consequences, PDF p. 19). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We show that for a fixed amount of entanglement, two-mode squeezed states are those that maximize Einstein-Podolsky-Rosen-like correlations. We use this fact to determine the entanglement of formation for all symmetric Gaussian states corresponding to two modes. This is the first instance in which this measure has been determined for genuine continuous variable systems.
This mission is the statement-level formalization of Entanglement of formation for symmetric Gaussian states (arXiv:quant-ph/0304042v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symmetric Gaussian entanglement of formation (Proposition 2: entanglement of formation of symmetric two-mode Gaussian states, 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.
This paper attempts to develop a theory of sufficiency in the setting of non-commutative algebras parallel to the ideas in classical mathematical statistics. Sufficiency of a coarse-graining means that all information is extracted about the mutual relation of a given family of states. In the paper sufficient coarse-grainings are characterized in several equivalent ways and the non-commutative analogue of the factorization theorem is obtained. Among the applications the equality case for the strong subadditivity of the von Neumann entropy, the Imoto-Koashi theorem and exponential families are treated. The setting of the paper allows the underlying Hilbert space to be infinite dimensional.
This mission is the statement-level formalization of Sufficiency in quantum statistical inference (arXiv:math-ph/0412093v1). 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 Lemma 1: countable common-null-set subfamily (Lemma 1: countable common-null-set subfamily, 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.
29 results of the paper are not stated yet, because the library lacks an interface they need:
Previous work on the classical information capacities of bosonic channels has established the capacity of the single-user pure-loss channel, bounded the capacity of the single-user thermal-noise channel, and bounded the capacity region of the multiple-access channel. The latter is a multi-user scenario in which several transmitters seek to simultaneously and independently communicate to a single receiver. We study the capacity region of the bosonic broadcast channel, in which a single transmitter seeks to simultaneously and independently communicate to two different receivers. It is known that the tightest available lower bound on the capacity of the single-user thermal-noise channel is that channel's capacity if, as conjectured, the minimum von Neumann entropy at the output of a bosonic channel with additive thermal noise occurs for coherent-state inputs. Evidence in support of this minimum output entropy conjecture has been accumulated, but a rigorous proof has not been obtained. In this paper, we propose a new minimum output entropy conjecture that, if proved to be correct, will establish that the capacity region of the bosonic broadcast channel equals the inner bound achieved using a coherent-state encoding and optimum detection. We provide some evidence that supports this new conjecture, but again a full proof is not available.
This mission is the statement-level formalization of Classical capacity of bosonic broadcast communication and a new minimum output entropy conjecture (arXiv:0706.3416v1). 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 Conditional coherent-state capacity region (Section IV, Eqs. (1), (16)-(17); PDF pp.1,3-5, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We introduce a new form for the bosonic channel minimal output entropy conjecture, namely that among states with equal input entropy, the thermal states are the ones that have slightest increase in entropy when sent through a infinitesimal thermalizing channel. We then detail a strategy to prove the conjecture through variational techniques. This would lead to the calculation of the classical capacity of a communication channel subject to thermal noise. Our strategy detects input thermal ensembles as possible solutions for the optimal encoding of the channel, lending support to the conjecture. However, it does not seem to be able to exclude the possibility that other input ensembles can attain the channel capacity.
This mission is the statement-level formalization of The bosonic minimum output entropy conjecture and Lagrangian minimization (arXiv:0906.2758v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal and displaced thermal stationary witnesses and local output-entropy minima (Unnumbered main result: thermal stationarity and local output-entropy minima, 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.
11 results of the paper are not stated yet, because the library lacks an interface they need:
We present a phase space formulation of quantum mechanics in the Schr"odinger representation and derive the associated Weyl pseudo-differential calculus. We prove that the resulting theory is unitarily equivalent to the standard "configuration space" formulation and show that it allows for a uniform treatment of both pure and mixed quantum states. In the second part of the paper we determine the unitary transformation (and its infinitesimal generator) that maps the phase space Schr"odinger representation into another (called Moyal) representation, where the wave function is the cross-Wigner function familiar from deformation quantization. Some features of this representation are studied, namely the associated pseudo-differential calculus and the main spectral and dynamical results. Finally, the relation with deformation quantization is discussed.
This mission is the statement-level formalization of Quantum mechanics in phase space: The Schr"odinger and the Moyal representations (arXiv:1209.1850v1). 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 Unitary equivalence with the window subspace (Abstract main result: unitary equivalence with configuration space, 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.
9 results of the paper are not stated yet, because the library lacks an interface they need:
Paired-comparison data (which of two items a user clicked, which of two players won a game, which of two products a respondent preferred) are summarised by ranking scores, one real number per item. The Bradley–Terry model (Bradley and Terry, 1952) is the standard statistical model for such scores, and its parameters are estimated by maximum likelihood or by maximum a posteriori (MAP) estimation. The workhorse for both is the MM algorithm (minorize–maximize), systematised for the Bradley–Terry family by Hunter (2004); the MAP version with a Gamma prior is due to Caron and Doucet (2012).
Vojnović, Yun and Zhou (arXiv:1901.00150v3) give the first rate-of-convergence analysis of these algorithms that depends on the structure of the comparison data. They find that the classic MAP iteration can be arbitrarily slow when the prior is weak, and that a simple rescaling of each iterate removes the slowdown. This mission formalizes the rate of the rescaled MM algorithm, the paper's Corollary 4.2.
There are items. For , is the number of comparisons in which item beat item . The co-occurrence matrix has entries for and . Three quantities of enter the rate:
The parameter is , with item strengths , and item beats item with probability . The log-likelihood and the log-prior of independent priors on the are
The log-a posteriori function is , and the MAP estimate maximizes it. The MM algorithm maximizes, at each step, the surrogate , where
lies below and touches it at . The rescaling is with . It shifts all scores by a common constant so that . The rescaled MM algorithm (Algorithm 1) is with a maximizer of . Finally and .
If the MAP point , the iterate (an output of ) and the virtual gradient point all lie in , then
The milestones follow the structure of the paper:
Without rescaling, the MAP rate of MM (the paper's Corollary 3.4) is , and the paper shows this is tight on two items. For a weak prior, which is the usual choice in practice, convergence is therefore arbitrarily slow. The rescaled rate replaces by . It thus recovers, as , the maximum-likelihood rate governed by the algebraic connectivity of the comparison graph, at the cost of one normalisation per step. This explains the many-orders-of-magnitude speed-ups that the paper reports on real datasets.
The framework of §4.1 is stated for any objective, any surrogate and any map satisfying (F1), (F2), (P1), (P2). It applies to other generalized Bradley–Terry models (Rao–Kupper, Luce, Plackett–Luce) and to gradient descent. The results are proved on paper; none of them, and none of the Bradley–Terry objects, has a machine-checked proof that we know of. A formalization would also settle the points the printed statements leave implicit (see below).
The objective is not strongly convex with a useful constant on all of : its curvature in the direction comes only from the prior and is of order . The natural argument (strong convexity of gives a PL inequality, and the PL inequality gives a linear rate) therefore yields only the slow -dependent rate. The faster rate needs a PL inequality that holds only on the points where (Lemma 4.1). This uses the fact that the Hessian bound does not couple with its orthogonal complement. The rescaling must then keep every iterate in that set without decreasing .
All curvature bounds hold only on the box , because is unbounded. The MM step is compared with a virtual gradient step, and that step must stay in the box.
Parameters live in EuclideanSpace ℝ (Fin n) (items are 0-based); is the Euclidean norm and uses the sup norm. Counts are natural numbers and every sum runs over . Eigenvalues come from Mathlib's eigenvalues₀, and is by convention for . Gradients are Mathlib's gradient; the Hessian forms are second iterated Fréchet derivatives. The framework minimizes , exactly as the paper does.
The goal fixes these points, relative to the printed statement:
Theorem 4.2 is stated with rate ; the page prints , which does not match its own proof or Corollary 4.2.
The goal does not assume (F1), (F2), (P1) or the surrogate bound for . Those are milestones about the concrete model. Stating Corollary 4.2 with any of them as a hypothesis, or with or the MM step replaced by an abstract map, would be a different and weaker theorem.
A complete development needs, besides the model file, a descent lemma for functions with Lipschitz gradient on a convex set and the variational characterisation of of a symmetric matrix. It also needs Gershgorin's theorem and second-order calculus for log-sum-exp functions; these are reusable well beyond this mission. Proofs of any milestone, including the general Lemma 4.1 and Theorem 4.2 independently of the Bradley–Terry model, are welcome.
During an epidemic a government knows more about the severity of the disease than the public, and what it chooses to say changes how many people stay at home. Isolation is cheap for some and expensive for others. A person who cannot work from home loses income, and people facing different costs answer the same message in different ways. de Véricourt, Gurkan and Wang (ESMT Working Paper 20-03, 2020; published in Management Science, 2021, doi:10.1287/mnsc.2021.4016) model this as a problem of information design (Bayesian persuasion, Kamenica and Gentzkow 2011). The receivers are a continuum of individuals who play a game among themselves, because each active person raises everyone else's infection risk.
The paper's main finding links economic inequality to misinformation. As the spread of isolation costs grows, the optimal policy exaggerates the severity of the epidemic less often and less strongly, and downplays it more. This mission formalizes that result, Theorem 2, together with the chain of statements on which its proof rests.
A unit mass of individuals each choose : isolate () or interact (). An isolated individual pays an economic cost , uniformly distributed on with mean and standard deviation , where . Write for the width of . An active individual pays the health risk . Here is the perceived infectiousness, the mass of active individuals and the healthcare cost of an infection.
A profile is a Bayesian Nash equilibrium (BNE) if, for every and every type , minimizes , where is the active population the profile induces.
The infectiousness is with ; it is high with prior probability , and the prior mean is . The paper also assumes . The government commits to an information policy , a law of messages given the state. Message moves the public to the posterior mean by Bayes' rule. For a weight on the economy, the government's cost is
An optimal policy minimizes over all policies and all their BNE profiles. On the binary message space the paper names four kinds of policy:
In equilibrium (Proposition 1), every type below the threshold isolates. The reduced cost at posterior mean is , and is its lower convex envelope on . The functions of (equations (23)–(25)) define thresholds for the ratio . Explicit rational functions of the parameters, and ((13)–(16)), are the second posteriors of the optimal exaggerating and downplaying policies.
Let , every other parameter fixed and admissible at both levels. Then
When exaggerating is optimal at both levels (, ), the exaggeration probabilities of optimal exaggerating policies satisfy
When downplaying is optimal at both levels (, ), the downplaying probabilities satisfy
The probabilities belong to policies that are optimal for the government's problem over all finite-message policies and BNE profiles.
Theorem 2 is the paper's answer to its question. Inequality in the economic cost of isolation pushes the government's message toward downplaying the epidemic, whatever weight the government puts on health. Theorem 1, the full characterization of the optimal policy, is a complete solution of a persuasion problem whose receivers play a congestion-type game, and Theorem 2 is a comparative-statics statement about that solution.
To our knowledge none of these results has a machine-checked proof. The mission produces:
The proofs in the paper are calculus on explicit functions, but they are long and contain sign slips. The proofs of Lemma 3 Parts C and D swap "convex" and "concave". The proof of Theorem 2 attaches the downplaying and exaggerating probabilities to the wrong -intervals. A closed form printed for in the proof of Lemma 2 does not equal its definition . A formal proof settles these points.
The obvious argument goes through the closed forms (17)–(18) of the optimal probabilities and differentiates them in . That argument needs, first, that the optimal policies are those forms. This rests on Theorem 1, the convex-envelope reduction and the curvature analysis of . The reduced cost is neither convex nor concave, and its shape changes across seven parameter regimes. Second, the derivatives of and in are rational expressions whose signs follow only from the regime bounds and . These bounds involve square roots. Third, the step from the equilibrium game to the reduced problem must handle the indifferent type and arbitrary BNE profiles, not only the threshold profile.
Params holds . The predicate Standing collects the assumptions of §2: , , , , and .Fin 2 (0 ). Message spaces are finite types; with a binary state, two messages suffice for the optimum.BiconvexProg.BranchBound.convexEnvelope.Theorem 2 must not be stated about the closed forms (17)–(18). It quantifies over policies that are optimal for (6), so a proof has to go through Theorem 1. The government's cost must also not be defined as , which would skip Proposition 1. A sorry-free check in the workspace exhibits two parameter pairs (one exaggerating, one downplaying) that satisfy the regime hypotheses of the goal at both inequality levels.
Contributions to every milestone are welcome. The general pieces are reusable beyond this paper:
Banks that can sell loans after origination may face different incentives to screen them before lending. A buyer that has invested in screening can inspect a seller's loan and buy it when its quality is high. That opportunity can make screening more valuable and reduce the equity a buyer needs to commit. At the same time, a seller may prefer to avoid the screening cost and rely on a later sale. Song and Thakor study when these two choices coexist in an interbank market, even though banks begin with the same opportunities and information (Song and Thakor, SSRN 3667175). The resulting question concerns the capital structure of banks and whether a trading market opens a region of heterogeneous behavior between two homogeneous regimes.
The paper's Proposition 2 is a result about this transition as the chance of a boom changes. It also compares the width of the heterogeneous region across market efficiencies. The mission formalizes that result from the authors' specified model and their preprint's assumptions. The preprint describes the paper as forthcoming in Management Science; the DOI record identifies the associated journal work.
A good loan pays at its final date. A medium loan pays in a boom and zero in a recession. Both require an initial investment . The probability of a boom is , with , so a medium loan is not creditworthy on its own. Before a bank screens, each type has probability one half. Screening costs and reveals the type. A bank can finance the loan with deposits and equity; supplying one unit of equity costs insiders per unit. Default also loses the bank its charter value . The paper restricts , and by Assumptions 1–4 and fixes the matching technology by Assumption 5 (preprint, pp. 7–12); is increasing and concave.
Without loan trading, the minimum screening equity is , the profit from screening is , and the profit without screening is . Their difference, , is the screening advantage. The paper writes each quantity as an explicit real-valued function of in equations (8)–(11). A cutoff separates the choices when the loan market is closed (Proposition 1, p. 15).
With trading, some banks can be buyers that screen, while others are sellers that do not. If buyers have mass and sellers mass , market tightness is . A seller meets a buyer with probability ; a buyer meets a seller with probability . Here measures matching efficiency. The buyer's bargaining weight is , and the price for a verified good loan is . Trading reduces the buyer's required equity to (Assumption 5, equation (13), and Lemma 1; the matching function follows Kiyotaki and Wright (1993)).
The main target is Proposition 2, p. 21. Under the paper's assumptions and its endpoint conditions, there are cutoffs . Every bank screens below ; none screens above ; between them, buyers and sellers coexist. In the interior the buyer/seller ratio is determined by
The two cutoffs solve the paper's equations (A4) and (A7). The mission also targets uniqueness of the equilibrium in every regime, expansion of the heterogeneous region when a larger feasible is used, and falling and as rises within that region. The milestone list covers the matching identities of Assumption 5, the Nash price (13), Lemma 1's equity threshold, the monotonicity of (footnote 19), the sign form of the cost condition (A1), the strict concavity of , the closed-market cutoff of Proposition 1, the two trading cutoffs (A4) and (A7), the interior indifference equation (A9)/(15), and the monotonicity in of the left side of (15) (Appendix A, pp. 34–37).
The result identifies a region in which banks that started alike choose different capital structures and screening decisions. A loan-trading market changes the relative payoffs of screening and not screening, and the boom probability determines which choice can survive a unilateral switch. The cutoffs show precisely where the market moves from all-screening to mixed behavior and then to no-screening. The market-efficiency comparison says when the mixed region widens. These distinctions matter for the paper's subsequent welfare comparison and its discussion of capital requirements (Song and Thakor, §§3–4).
The result is proved in the source paper. The remaining work is a machine-checked proof of the model-specific statements and their consequences, including the bargaining maximum, incentive threshold, cutoff existence and uniqueness, and comparative statics. The definitions are reusable for further formal work on the paper's welfare and capital-requirement results; this mission does not assert that those extensions have been formalized.
The equilibrium claim joins several regimes in one statement. The homogeneous corners are governed by whether a single bank would gain by changing its behavior, whereas the interior is governed by equality of buyer and seller profits. A root of the displayed equation alone does not establish an equilibrium: the cutoff and no-switch conditions must also hold, and the root must be unique. Moreover, the source's claimed global negative derivative for is not implied by its assumptions. The cutoff argument must therefore use a valid shape condition without importing that false assertion. The charter-value function is concave but otherwise general, so reasoning cannot rely on a particular polynomial example.
Lean represents all expectations by the closed-form real expressions in equations (7)–(15); there is no probability space. The parameter structure fixes , and . All five numbered assumptions remain explicit, including Assumption 4. The formalization reads screening cost and equity cost as positive, reads the paper's smooth as differentiable on , and requires for an open market. The bargaining price is optimized over . The buyer meeting probability uses its continuous value at . Proposition 1 uses a reduced closed-market outcome that records screening and equity; at its profit tie, footnote 21 selects no screening. The open-market equilibrium variable is the buyer share , with only in the interior; the all-buyer corner uses the sole-seller limit instead. Price and buyer equity are constructed from the paper's equations, and are never arbitrary choices. The cutoffs are required to satisfy , so all three regimes are nonempty; a version in which the equilibrium is any root of (15), or in which price or buyer equity are free variables, would be a different and weaker statement and is excluded. The hypotheses are jointly satisfiable, but only for small market efficiency (numerical searches find ); an explicit rational instance is checked in Lean.
The preprint prints a plus sign in (A6) where its preceding deviation inequality requires a minus sign; the Lean condition uses the latter. The paper also claims that the absolute sensitivity of to falls with , but that claim is false under its hypotheses, so the mission does not include either sensitivity clause of Proposition 2. The paper's unsupported global first-derivative bound for is excluded. The milestone from the proof of Proposition 5 states its displayed second-derivative identity wherever exists, and states strict concavity throughout the interval. Any further result should keep these corrections explicit. Contributions to the bargaining, real-analysis, and equilibrium lemmas are welcome; proofs of the milestone statements can then support the capstone theorem.
Rooftop solar changes both a household's electricity bill and the utility's cost of serving its customers. A tariff that encourages an aggregate amount of solar generation can still leave one customer tier paying more than before. Regulators therefore face a joint design question: can they induce a chosen adoption pattern while meeting the solar supplier's and utility's profit requirements and protecting every customer tier? Singh and Scheller-Wolf formulate this question for a solar company that sells generation through a power purchase agreement, a regulated utility, and households grouped into tiers. Their SSRN paper studies several tariff families; Proposition 5 identifies a tiered tariff that can implement the selected outcome and, when the customers' aggregate financial gain is nonnegative, avoid cross-subsidization.
The selected outcome is assumed to have been chosen for social welfare reasons. The result concerns the next task: implementing it through the tariff while customers decide whether to adopt and the solar company chooses its price. That distinction matters because a tariff that appears to allocate enough money to all parties may change the solar company's preferred price, and therefore change which households adopt.
There are finitely many customer tiers . Tier contains households. Each household has annual electricity demand , potential solar generation , and excess generation . If it adopts solar, it draws from the grid and sells back. The target adopting set identifies the tiers whose households install solar. Let be baseline utility demand, the target rooftop generation, and net utility demand. The paper restricts attention to outcomes with at least one adopting tier and (§3, pp. 10–11).
The regulator sets a tariff , a customer's utility bill based on grid draw , electricity sold to the grid , and adoption indicator . For tier , the two relevant bills are and . A solar company chooses a single price per unit generated by adopting households and pays unit cost when its sales volume is . Each customer adopts when its adopter bill plus is no larger than its nonadopter bill. With ties favoring adoption, this is , where . Thus the solar company's price determines both its sales volume and its unit cost (§§3–4, pp. 10–13).
The regulator's P2 objective is the largest increase in a tier household's cash outflow relative to the baseline rate . A nonpositive objective means no tier is financially worse off, which the paper calls cross-subsidization free. P2 also requires a specified solar-company profit and utility profit change . Write for the financial welfare improvement of the whole system and for customers' aggregate financial gain (§4, pp. 12–15).
Tariffs of type charge nonadopters and adopters , where is a common rate and a tier-specific adopter charge. The paper constructs one such tariff, , from the target outcome. At its prescribed price , the target tiers adopt, the solar company earns and earns strictly less at every other price, and the utility receives its specified profit change :
This is the feasibility claim of Proposition 5(a), p. 18.
When the aggregate customer gain is nonnegative, has a nonpositive P2 objective:
If a tier with the smallest demand does not adopt, Proposition 5(b) further says minimizes this objective among feasible tariffs. Both clauses belong to the combined goal theorem. The milestone list also includes the customer threshold, the welfare identity, the threshold formula, Proposition 5(a), Lemma 1, the retail-rate identity for , and the cross-subsidization clause (p. 18 and proof on p. S.3).
Proposition 5 gives a tariff implementation for any admissible target adoption set without relying on control of the solar company's price. Its equity guarantee has a clear limit: it requires nonnegative aggregate customer gain. Within the paper's family, the additional lowest-demand condition gives an exact minimax result for customers' bill changes (Proposition 5, p. 18). This distinguishes the existence of an implementing tariff from its distributional performance.
The mathematical result is already proved in the paper; this mission asks for a machine-checked development of its model, construction, and claims. The reusable pieces include finite-tier induced-adoption sets, price-dependent sales volume, and the accounting identities between company profits and customer outflows. The statements in this proposal are proof targets and do not claim an existing Lean proof.
Setting each customer's adoption threshold to produce is insufficient by itself. The solar company chooses to maximize profit, and a change in price can change both the adopting set and the unit cost . The prescribed price must beat every alternative real price strictly. The utility's required profit change constrains the same tier fees used to set thresholds. Finally, a nonnegative total customer gain does not by itself imply that every tier benefits; P2 asks about the largest individual tier increase. These coupled requirements are visible in the paper's P2 formulation and in the proof of Proposition 5 (pp. 13–14, 18, S.3).
Lean represents tiers by a finite type and outcomes by finite sets of tiers. All demands, prices, bills, costs, volumes, and profit changes are real. The tier type is unordered: the paper relabels tiers during 's construction. A tariff is represented by its two bills per tier, the evaluations P2 uses. For , fees are indexed by tier, consistent with the paper's statement that the utility can infer a solar customer's tier from grid draw (p. 17). Adoption ties go to adoption, and the solar company's price ranges over all real numbers. P2 feasibility includes the induced adopter set, the firm's unique best response, and the utility constraint.
The standing assumptions state , , nonincreasing , and . Positivity of is implicit in the paper and makes the displayed volume and price divisions valid. The target set is nonempty and satisfies . The utility's total generation cost is outside the household sum in its accounting constraint; this is the reading consistent with the paper's welfare identity. The printed indexing slips in (17) and (19) are avoided by expressing the induced equilibrium directly. Customer aggregate gain is computed from , rather than defined from the desired conclusion. The optimality quantifier covers feasible tariffs, the family studied in §4.3. Contributions may develop the equilibrium argument, the accounting lemmas, the rate identity, or the complete optimality proof.
A standard-essential patent is a patent that an implementer must use to make a product compliant with a technical standard. Its owner may demand a royalty from firms using the standard. Whether a patent is truly essential can be disputed, yet licensing offers and investment decisions are made before a court resolves that dispute. Standard-setting organizations can commission essentiality checks that certify patents before licensing. Better checks identify more patents that are not essential, but they also change what an implementer believes about a patent that passes the check. Schuett and Wipusanawan study how those two effects interact with litigation and research investment in their TILEC discussion paper, §§2–5.
A common policy intuition is that a more accurate check should save litigation costs by excluding weak patent claims. The paper identifies a countervailing effect in a model where an innovator chooses research effort before it knows whether its patent will be essential. The question here is local: when a small increase in check accuracy leaves each state's licensing regime unchanged, how does equilibrium welfare change if the patent owner faces no effective cap on royalties? The paper's Proposition 1 answers this question, building on its licensing, investment, and welfare formulas Schuett and Wipusanawan, pp. 16–25.
An upstream firm chooses research effort at cost . Research succeeds with probability . Following success, the standard uses the firm's technology, its patent is essential, and the commercial value is one of finitely many values with probabilities . Following failure, the standard uses a status-quo technology, the patent is not essential, and value occurs with probability . The separate distribution for the unsuccessful upstream technology enters the paper's assumption that the status quo has higher expected value than that technology. The model requires Assumption 1, p. 10.
An essentiality check certifies an essential patent correctly. It also certifies a non-essential patent in error with probability , where is accuracy. After observing certification and value, the upstream firm offers a royalty fraction bounded by . The downstream firm can accept or litigate. Litigation costs each firm ; the court determines essentiality correctly. A non-certified patent earns the upstream firm no licensing revenue in this model. The paper assumes Assumption 2, p. 12.
A certified patent can produce a hybrid licensing outcome, in which the unsuccessful firm sometimes offers a low royalty and the downstream firm sometimes litigates a high offer, or a pooling outcome, in which both types offer the maximum royalty. Write and for the sets of states with those outcomes. The implementer's belief that a certified patent is essential, , depends on expected effort , accuracy , and the value distributions. In equilibrium, . The paper derives a private investment wedge from the difference between expected licensing revenues after success and failure, and a social wedge from expected value less both parties' litigation costs equations (1)–(7), pp. 16–22.
The main target is Proposition 1. With an ineffective royalty cap, , fix where no positive-probability state lies exactly at the hybrid–pooling boundary. Along a continuous path of nearby equilibrium efforts , the right derivative of welfare satisfies
The inequality is weak because the paper concludes Proposition 1 and its proof, pp. 24–25. The target concerns a marginal increase that preserves the licensing regimes; it makes no claim about a large change that moves states between and .
The milestone statements cover the regime condition (4), the private revenue wedge (5), the welfare identity (6), Lemma 2's positive response of research effort to accuracy, and Lemma 3's comparison of private and social investment incentives. Their order exposes the quantities the goal uses without replacing Proposition 1 with a narrower fixed-regime statement.
Within this model, the result says that improved screening can lower welfare when unconstrained licensing already induces too much research investment. It identifies a limit on an intervention aimed at reducing disputes over essentiality: even a check that detects more non-essential patents may change the incentives of firms whose patents pass. This is a statement about the model's local equilibrium, not a claim that every real-world checking program lowers welfare. The paper separately examines changes large enough to alter licensing regimes and the case of an effective royalty cap Schuett and Wipusanawan, §§5–6.
The economic theorem is proved in the cited paper. This mission asks for a machine-checked account of its finite-state model and the local welfare claim; the displayed Lean statements are open proof targets. The shared definitions of certification beliefs, licensing outcomes, revenue, and welfare are useful for checking later variants of the model, including alternative certification errors or royalty caps. No machine-checked proof of this paper's proposition is claimed here.
The local comparison crosses three choices. Accuracy changes the chance that a failed innovator is certified. Certification changes the downstream firm's belief when it sees a high royalty. The resulting licensing outcome affects the innovator's incentive to invest, and effort feeds back into the belief. Simply holding effort fixed misses the welfare effect in Proposition 1. Treating the hybrid and pooling sets as fixed for all accuracy levels is also too broad: the paper restricts the result to a neighborhood where the regime condition does not meet equality. At a boundary, the relevant formulas can switch and the local derivative need not have the same form pp. 20, 24–25.
The Lean model uses real values and probabilities on a finite state type Fin n. Each of , , and is a nonnegative probability vector. Assumptions 1 and 2, , and the paper's increasing convex research cost with and as are explicit standing conditions. The cost is represented by a real function twice continuously differentiable on , which covers the effort domain below one. Equilibrium effort is interior and satisfies the private first-order condition with the implementer's belief equal to effort.
Three premises used in the paper's argument are made explicit. Litigation costs satisfy . The second derivative at the equilibrium effort satisfies , as required by the displayed denominator in Lemma 2; convexity alone gives only nonnegativity. A right-continuous equilibrium-effort path supplies nearby equilibria for the local comparison. The derivative is one-sided because the target concerns an increase from , including . Strictness of the regime condition is demanded only for states with positive probability under or ; an absent state cannot affect welfare or investment.
The belief formula is the paper's ratio when its denominator is positive. Its value at a zero-probability state is immaterial to the weighted outcome; the regime milestone also gives a cross-multiplied condition there. Uncertified patents give the upstream firm zero revenue, and the downstream firm retains value without litigation. Welfare is assembled from the two firms' payoffs in every certification and licensing outcome, then related to equation (6). Defining welfare directly by (6), fixing in the goal, or assuming the derivative of would remove the main work of the proposition. Contributions to the finite-state payoff model, the regime and welfare identities, and the local derivative and wedge comparison are all within scope.
Bundle methods minimize a convex objective while using local supporting affine functions to represent a component that may be nonsmooth. Their iterations can spend time improving the model without moving the current proximal center, so a bound on useful center changes alone does not bound the total work. Liang and Monteiro study a common generic proximal bundle (GPB) framework for several model update rules and give one explicit iteration bound that covers every rule admitted by its bundle update blackbox. The result is a proved theorem in their paper, rather than an open complexity conjecture.
The framework matters when a convex objective combines a component supplied through subgradients with another component whose proximal subproblems can be handled directly. One-cut, two-cut, and multiple-cut bundle updates fit the same abstract requirements in the paper. A common statement makes their guarantees comparable without identifying a specific update formula as canonical.
The problem is to minimize hybrid convex composite objective over . The effective domain is nonempty and contained in the domain of . The function is lower semicontinuous and -convex, for : its convexity inequality gains the quadratic term . For each , a chosen subgradient defines a supporting affine cut
The hybrid oracle condition allows both a constant and a distance-dependent part:
where . For tolerance , the pair minimizes among all nonnegative pairs satisfying the same condition. An optimal point nearest the initial point exists under the paper's assumptions, and .
A GPB run is an infinite sequence of points , best-so-far points , centers , and convex bundle models . At a serious update, the next center is the current point and the next model lies between and . At a null update, the center stays fixed and a bundle update blackbox selects the next model. Its output must dominate a mixture of a fresh cut and an auxiliary model that agrees with the previous model at and has as its proximal minimizer. Every new minimizes its model plus the squared distance to its center divided by . The best-so-far point minimizes the observed objective values. The gap compares with the proximal model value; a step is serious when .
The goal is Proposition 4.9, an explicit total iteration bound for every run admitted by GPB when is set by equation (38). Put and
There is an index with and
Here is the minimum of the two serious-iteration expressions in (61), with the paper's limiting convention at . The milestones follow the two quantities in this product: Corollary B.2 and Lemma 4.2 yield the serious-iteration estimate; Proposition 4.3 packages it. Equation (7), Lemmas 4.6, A.3, and 4.7 bound the behavior within each cycle; Proposition 4.8 bounds the cycle length. The goal combines the two bounds without selecting one concrete bundle update.
The theorem gives a finite tolerance certificate with a numerical bound on all iterations, including those that only improve the bundle model. The bound depends on the oracle parameters, curvature, initial distance to the solution set, tolerance, and proximal stepsize. It therefore states what an implementation gains by satisfying the BU conditions even when its internal model construction differs from another implementation. The broader paper also analyzes particular update schemes and an adaptive method, but the target here is the common GPB result Liang and Monteiro, §3–4.
The mathematical result is already proved in the source. This mission asks for machine-checked definitions and proofs of its explicit bound and the selected supporting statements. No machine-checked proof is supplied by these open theorem items. The definitions of the hybrid oracle, proximal model, and abstract GPB run can be reused to formalize the paper's concrete update schemes later.
Counting serious steps does not count intervening null steps. A null step can leave the center fixed while the model changes, and the BU condition permits many such models. The main obstacle is to obtain a uniform bound for a complete cycle from conditions that are local to one model update. The separate analytic obstacle is the hybrid descent estimate (7): the oracle bound contains both a constant term and a term proportional to distance, and the needed quadratic coefficient is , not the easier . The source's auxiliary proximal displacement estimate also depends on lower semicontinuity so that its minimizers exist.
The Lean space is EuclideanSpace ℝ (Fin n), with its usual norm and real inner product. The function domain stands for ; , , and each bundle model are real-valued on , with an extended value off when lower semicontinuity is stated. All model inequalities and proximal minimizations are over . This represents the paper's extended-valued functions without ambiguous arithmetic at . The selected subgradient inequality is also required only on . The source's lower semicontinuity of and of the BU auxiliary model is omitted, which strengthens the resulting claims; lower semicontinuity of and of each generated model remains. The abstract serious-iterate sequences explicitly keep their auxiliary points in .
Index zero is initialization and counts as serious because ; subsequent indices are natural numbers. The GPB run predicate retains the existential auxiliary model in every null update, so it covers every admissible variant. The goal concludes existence of a successful bounded index. It assumes so equation (38) defines . For , the serious-step formula uses the limiting value rather than real division by zero. The printed cycle and total bounds omit an integer rounding and can be too small; the formal targets use a ceiling and a nonnegative logarithm. Lemma 4.2(c), Lemma A.3, and Lemma 4.7 carry the additional qualifications needed by their printed proofs, disclosed beside their statements.
The development needs Mathlib's finite-dimensional Euclidean spaces, convexity, lower semicontinuity, and real logarithm, plus real-sequence and finite-index estimates. Contributions proving the milestones, the goal, or reusable facts about the GPB model are within scope. A proof for one fixed update formula alone does not establish the goal over the BU blackbox.