Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In this paper we study the problem of calculating the convex hull of certain affine algebraic varieties. As we explain, the motivation for considering this problem is that certain pure-state measures of quantum entanglement, which we call polynomial entanglement measures, can be represented as affine algebraic varieties. We consider the evaluation of certain mixed-state extensions of these polynomial entanglement measures, namely convex and concave roofs. We show that the evaluation of a roof-based mixed-state extension is equivalent to calculating a hyperplane which is multiply tangent to the variety in a number of places equal to the number of terms in an optimal decomposition for the measure. In this way we provide an implicit representation of optimal decompositions for mixed-state entanglement measures based on the roof construction.
This mission is the statement-level formalization of Convex Hulls of Varieties and Entanglement Measures Based on the Roof Construction (arXiv:quant-ph/0402055v2). 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 Both roofs are graph-hull fiber extrema (Lemma 2.2: roofs are graph-hull fiber extrema, 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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
The class of -compact sets can be considered as a natural extension of the class of compact metrizable subsets of locally convex spaces, to which the particular results well known for compact sets can be generalized. This class contains all compact sets as well as many noncompact sets widely used in applications. In this paper we give a characterization of a convex -compact set in terms of properties of functions defined on this set. Namely, we prove that the class of convex -compact sets can be characterized by continuity of the operation of convex closure of a function (= the double Fenchel transform) with respect to monotonic pointwise converging sequences of continuous bounded and of lower semicontinuous lower bounded functions.
This mission is the statement-level formalization of Characterization of convex -compact sets (arXiv:1004.3792v1). 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 Monotone continuity characterizes convex µ-compact sets (Theorem, 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.
A class of problems in quantum information theory, having an elementary formulation but still resisting solution, concerns the additivity properties of various quantities characterizing quantum channels, notably the "classical capacity", and the "maximal output purity". All known results, including extensive numerical work, are consistent with the conjecture that these quantities are indeed additive (resp. multiplicative) with respect to tensor products of channels. A proof of this conjecture would have important consequences in quantum information theory. In particular, according to this conjecture, the classical capacity or the maximal purity of outputs cannot be increased by using entangled inputs of the channel. In this paper we state the additivity/multiplicativity problems, give some relations between them, and prove some new partial results, which also support the conjecture.
This mission is the statement-level formalization of On some additivity problems in quantum information theory (arXiv:math-ph/0003002v2). 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 Depolarizing products: multiplicativity and explicit purities (§5, Theorem (i)-(iii): multiplicativity and explicit depolarizing purities, PDF p. 11). 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 address the question of the multiplicativity of the maximal p-norm output purities of bosonic Gaussian channels under Gaussian inputs. We focus on general Gaussian channels resulting from the reduction of unitary dynamics in larger Hilbert spaces. It is shown that the maximal output purity of tensor products of single-mode channels under Gaussian inputs is multiplicative for any p>1 for products of arbitrary identical channels as well as for a large class of products of different channels. In the case of p=2 multiplicativity is shown to be true for arbitrary products of generic channels acting on any number of modes.
This mission is the statement-level formalization of Multiplicativity of maximal output purities of Gaussian channels under Gaussian inputs (arXiv:quant-ph/0406065v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract/main result: Gaussian maximal-output-purity multiplicativity (Abstract/main result: Gaussian maximal-output-purity multiplicativity, 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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum information characteristics, such as quantum mutual information, loss, noise and coherent information are explicitly calculated for Bosonic attenuation/amplification channel with input Gaussian state. The coherent information is shown to be negative for the values of the attenuation coefficient .
This mission is the statement-level formalization of Sending Quantum Information with Gaussian States (arXiv:quant-ph/9809022v1). 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 Thermal output and the three entropies (§4, unnumbered main result: thermal output and all three entropies, PDF p. 9). 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:
The existing unconditional security definitions of quantum key distribution (QKD) do not apply to joint attacks over QKD and the subsequent use of the resulting key. In this paper, we close this potential security gap by using a universal composability theorem for the quantum setting. We first derive a composable security definition for QKD. We then prove that the usual security definition of QKD still implies the composable security definition. Thus, a key produced in any QKD protocol that is unconditionally secure in the usual definition can indeed be safely used, a property of QKD that is hitherto unproven. We propose two other useful sufficient conditions for composability. As a simple application of our result, we show that keys generated by repeated runs of QKD degrade slowly.
This mission is the statement-level formalization of The Universal Composable Security of Quantum Key Distribution (arXiv:quant-ph/0409078v1). 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 §4.2: ideal KD has perfect equality, uniformity and privacy (§4.2: ideal KD has perfect equality, uniformity and privacy, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
8 results of the paper are not stated yet, because the library lacks an interface they need:
The classical asymptotic equipartition property is the statement that, in the limit of a large number of identical repetitions of a random experiment, the output sequence is virtually certain to come from the typical set, each member of which is almost equally likely. In this paper, we prove a fully quantum generalization of this property, where both the output of the experiment and side information are quantum. We give an explicit bound on the convergence, which is independent of the dimensionality of the side information. This naturally leads to a family of Renyi-like quantum conditional entropies, for which the von Neumann entropy emerges as a special case.
This mission is the statement-level formalization of A Fully Quantum Asymptotic Equipartition Property (arXiv:0811.1221v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Fully quantum asymptotic equipartition property (Theorem 1 (AEP), equations (6)-(7); original paper-level seed, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We report a deterministic and exact protocol to reverse any unknown qubit-unitary operation, which simulates the time inversion of a closed qubit system. To avoid known no-go results on universal deterministic exact unitary inversion, we consider the most general class of protocols transforming unknown unitary operations within the quantum circuit model, where the input unitary operation is called multiple times in sequence and fixed quantum circuits are inserted between the calls. In the proposed protocol, the input qubit-unitary operation is called 4 times to achieve the inverse operation, and the output state in an auxiliary system can be reused as a catalyst state in another run of the unitary inversion. We also present the simplification of the semidefinite programming for searching the optimal deterministic unitary inversion protocol for an arbitrary dimension presented by M. T. Quintino and D. Ebler [Quantum , 679 (2022)]. We show a method to reduce the large search space representing all possible protocols, which provides a useful tool for analyzing higher-order quantum transformations for unitary operations.
This mission is the statement-level formalization of Reversing Unknown Qubit-Unitary Operation, Deterministically and Exactly (arXiv:2209.02907v5). 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 Theorem 1: deterministic exact four-call inversion (Theorem 1: deterministic exact four-call qubit-unitary inversion, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
5 results of the paper are not stated yet, because the library lacks an interface they need:
Two new relative entropy quantities, called the min- and max-relative entropies, are introduced and their properties are investigated. The well-known min- and max- entropies, introduced by Renner, are obtained from these. We define a new entanglement monotone, which we refer to as the max-relative entropy of entanglement, and which is an upper bound to the relative entropy of entanglement. We also generalize the min- and max-relative entropies to obtain smooth min- and max- relative entropies. These act as parent quantities for the smooth Renyi entropies, and allow us to define the analogues of the mutual information, in the Smooth Renyi Entropy framework. Further, the spectral divergence rates of the Information Spectrum approach are shown to be obtained from the smooth min- and max-relative entropies in the asymptotic limit.
This mission is the statement-level formalization of Min-and Max-Relative Entropies and a New Entanglement Monotone (arXiv:0803.2770v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
22 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (§V): max-relative entropy of entanglement is an entanglement monotone (Theorem 1 (§V): max-relative entropy of entanglement is an entanglement monotone, 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.
We propose a general method for studying properties of quantum channels acting on an n-partite system, whose action is invariant under permutations of the subsystems. Our main result is that, in order to prove that a certain property holds for any arbitrary input, it is sufficient to consider the special case where the input is a particular de Finetti-type state, i.e., a state which consists of n identical and independent copies of an (unknown) state on a single subsystem. A similar statement holds for more general channels which are covariant with respect to the action of an arbitrary finite or locally compact group. Our technique can be applied to the analysis of information-theoretic problems. For example, in quantum cryptography, we get a simple proof for the fact that security of a discrete-variable quantum key distribution protocol against collective attacks implies security of the protocol against the most general attacks. The resulting security bounds are tighter than previously known bounds obtained by proofs relying on the exponential de Finetti theorem [Renner, Nature Physics 3,645(2007)].
This mission is the statement-level formalization of Post-selection technique for quantum channels with applications to quantum cryptography (arXiv:0809.3019v1). 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 1: postselection bound (Theorem 1: Post-Selection Theorem (seed paper result), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
A strong converse theorem for the classical capacity of a quantum channel states that the probability of correctly decoding a classical message converges exponentially fast to zero in the limit of many channel uses if the rate of communication exceeds the classical capacity of the channel. Along with a corresponding achievability statement for rates below the capacity, such a strong converse theorem enhances our understanding of the capacity as a very sharp dividing line between achievable and unachievable rates of communication. Here, we show that such a strong converse theorem holds for the classical capacity of all entanglement-breaking channels and all Hadamard channels (the complementary channels of the former). These results follow by bounding the success probability in terms of a "sandwiched" Renyi relative entropy, by showing that this quantity is subadditive for all entanglement-breaking and Hadamard channels, and by relating this quantity to the Holevo capacity. Prior results regarding strong converse theorems for particular covariant channels emerge as a special case of our results.
This mission is the statement-level formalization of Strong converse for the classical capacity of entanglement-breaking and Hadamard channels via a sandwiched Renyi relative entropy (arXiv:1306.1586v4). 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 Exponential strong converse for entanglement-breaking and Hadamard channels (seed, 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.
We describe a modification of the Alicki-Fannes-Winter method which allows to prove uniform continuity on the set of quantum states with bounded energy of any locally almost affine function having limited growth with increasing energy. Some applications in quantum information theory are considered. The asymptotic continuity of the relative entropy of entanglement and of its regularization under the energy constraint on one subsystem is proved. Channel-independent continuity bounds for the quantum mutual information at the output of a local channel and for the output Holevo quantity under the input energy constraint are obtained.
This mission is the statement-level formalization of Adaptation of the Alicki-Fannes-Winter method for the set of states with bounded energy and its use (arXiv:1609.07044v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 2: logarithmic-power spectral threshold (Lemma 2, 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.
15 results of the paper are not stated yet, because the library lacks an interface they need:
We are interested in the properties and relations of entanglement measures. Especially, we focus on the squashed entanglement and relative entropy of entanglement, as well as their analogues and variants. Our first result is a monogamy-like inequality involving the relative entropy of entanglement and its one-way LOCC variant. The proof is accomplished by exploring the properties of relative entropy in the context of hypothesis testing via one-way LOCC operations, and by making use of an argument resembling that by Piani on the faithfulness of regularized relative entropy of entanglement. Following this, we obtain a commensurate and faithful lower bound for squashed entanglement, in the form of one-way LOCC relative entropy of entanglement. This gives a strengthening to the strong subadditivity of von Neumann entropy. Our result improves the trace-distance-type bound derived in [Comm. Math. Phys., 306:805-830, 2011], where faithfulness of squashed entanglement was first proved. Applying Pinsker's inequality, we are able to recover the trace-distance-type bound, even with slightly better constant factor. However, the main improvement is that our new lower bound can be much larger than the old one and it is almost a genuine entanglement measure. We evaluate exactly the various relative entropy of entanglement under restricted measurement classes, for maximally entangled states. Then, by proving asymptotic continuity, we extend the exact evaluation to their regularized versions for all pure states. Finally, we consider comparisons and separations between some important entanglement measures and obtain several new results on these, too.
This mission is the statement-level formalization of Relative entropy and squashed entanglement (arXiv:1210.3181v2). 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 Theorem 2, Eq. (8): commensurate lower bound for squashed entanglement (Theorem 2, Eq. (8): commensurate lower bound for squashed entanglement, 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.
Quantum f-divergences are a quantum generalization of the classical notion of f-divergences, and are a special case of Petz' quasi-entropies. Many well known distinguishability measures of quantum states are given by, or derived from, f-divergences; special examples include the quantum relative entropy, the Renyi relative entropies, and the Chernoff and Hoeffding measures. Here we show that the quantum f-divergences are monotonic under the dual of Schwarz maps whenever the defining function is operator convex. This extends and unifies all previously known monotonicity results. We also analyze the case where the monotonicity inequality holds with equality, and extend Petz' reversibility theorem for a large class of f-divergences and other distinguishability measures. We apply our findings to the problem of quantum error correction, and show that if a stochastic map preserves the pairwise distinguishability on a set of states, as measured by a suitable f-divergence, then its action can be reversed on that set by another stochastic map that can be constructed from the original one in a canonical way. We also provide an integral representation for operator convex functions on the positive half-line, which is the main ingredient in extending previously known results on the monotonicity inequality and the case of equality. We also consider some special cases where the convexity of f is sufficient for the monotonicity, and obtain the inverse Holder inequality for operators as an application. The presentation is completely self-contained and requires only standard knowledge of matrix analysis.
This mission is the statement-level formalization of Quantum f-divergences and error correction (arXiv:1008.2529v6). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
53 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract main result (p.1), pinned to Theorem 7.1 (Theorem 7.1 (abstract main result), PDF p. 33). 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:
We prove a lower bound on the relative entropy between two finite-dimensional states in terms of their entropy difference and the dimension of the underlying space. The inequality is tight in the sense that equality can be attained for any prescribed value of the entropy difference, both for quantum and classical systems. We outline implications for information theory and thermodynamics, such as a necessary condition for a process to be close to thermodynamic reversibility, or an easily computable lower bound on the classical channel capacity. Furthermore, we derive a tight upper bound, uniform for all states of a given dimension, on the variance of the surprisal, whose thermodynamic meaning is that of heat capacity.
This mission is the statement-level formalization of Tight bound on relative entropy by entropy difference (arXiv:1304.0036v3). 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 Tight relative entropy bound and explicit equality witnesses (theorem1, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
We derive one-shot upper bounds for quantum noisy channel codes. We do so by regarding a channel code as a bipartite operation with an encoder belonging to the sender and a decoder belonging to the receiver, and imposing constraints on the bipartite operation. We investigate the power of codes whose bipartite operation is non-signalling from Alice to Bob, positive-partial transpose (PPT) preserving, or both, and derive a simple semidefinite program for the achievable entanglement fidelity. Using the semidefinite program, we show that the non-signalling assisted quantum capacity for memoryless channels is equal to the entanglement-assisted capacity. We also relate our PPT-preserving codes and the PPT-preserving entanglement distillation protocols studied by Rains. Applying these results to a concrete example, the 3-dimensional Werner-Holevo channel, we find that codes that are non-signalling and PPT-preserving can be strictly less powerful than codes satisfying either one of the constraints, and therefore provide a tighter bound for unassisted codes. Furthermore, PPT-preserving non-signalling codes can send one qubit perfectly over two uses of the channel, which has no quantum capacity. We discuss whether this can be interpreted as a form of superactivation of quantum capacity.
This mission is the statement-level formalization of On the power of PPT-preserving and non-signalling codes (arXiv:1406.7142v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract main result; §V (49): non-signalling and entanglement-assisted quantum capacities coincide (Abstract main result; §V (49): non-signalling and entanglement-assisted quantum capacities coincide, 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.
4 results of the paper are not stated yet, because the library lacks an interface they need:
We study a protocol in which many parties use quantum communication to transfer a shared state to a receiver without communicating with each other. This protocol is a multiparty version of the fully quantum Slepian-Wolf protocol for two senders and arises through the repeated application of the two-sender protocol. We describe bounds on the achievable rate region for the distributed compression problem. The inner bound arises by expressing the achievable rate region for our protocol in terms of its vertices and extreme rays and, equivalently, in terms of facet inequalities. We also prove an outer bound on all possible rates for distributed compression based on the multiparty squashed entanglement, a measure of multiparty entanglement.
This mission is the statement-level formalization of Distributed Compression and Multiparty Squashed Entanglement (arXiv:0707.2792v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem II.1: multiparty distributed compression inner bound (seed paper result) (Theorem II.1: multiparty distributed compression inner bound (seed paper result), 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.
The quantum capacity of a memoryless channel is often used as a single figure of merit to characterize its ability to transmit quantum information coherently. The capacity determines the maximal rate at which we can code reliably over asymptotically many uses of the channel. We argue that this asymptotic treatment is insufficient to the point of being irrelevant in the quantum setting where decoherence severely limits our ability to manipulate large quantum systems in the encoder and decoder. For all practical purposes we should instead focus on the trade-off between three parameters: the rate of the code, the number of coherent uses of the channel, and the fidelity of the transmission. The aim is then to specify the region determined by allowed combinations of these parameters. Towards this goal, we find approximate and exact characterizations of the region of allowed triplets for the qubit dephasing channel and for the erasure channel with classical post-processing assistance. In each case the region is parametrized by a second channel parameter, the quantum channel dispersion. In the process we also develop several general inner (achievable) and outer (converse) bounds on the coding region that are valid for all finite-dimensional quantum channels and can be computed efficiently. Applied to the depolarizing channel, this allows us to determine a lower bound on the number of coherent uses of the channel necessary to witness super-additivity of the coherent information.
This mission is the statement-level formalization of Quantum Coding with Finite Resources (arXiv:1504.04617v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Qubit dephasing: third-order boundary (Result 1, Eq. (6), 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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
Many problems in signal processing, statistics and compressed sensing ask for a sparse solution of an underdetermined, possibly noisy linear system: a vector with as few nonzero entries as possible such that is close to . The direct formulation, minimizing the number of nonzeros , is combinatorial and NP-hard in general. A standard surrogate replaces by the quasi-norm power with , which tends to as and is continuous in . Practitioners use small because it is observed to produce sparser solutions than the convex choice .
The question this mission formalizes is whether that observation is a theorem: does minimizing for a sufficiently small actually return a sparsest feasible point, and does it do so without recovery conditions on such as the restricted isometry property or the null space property? Yang, Chen and Xiang (arXiv:1907.00880, Mathematics of Operations Research, 2022) answer yes for the -constrained problem. In the noiseless case , where the constraint is , the first half of the answer had also been discussed by Peng, Yue and Li (IEEE Transactions on Information Theory, 2015, Theorem 1), as the paper notes on p. 9; the paper extends it to noisy constraints and adds the stabilization of the solution set.
Fix a matrix , a vector , a noise level , an exponent and a norm index . The objective is
The feasible set is , where is the usual norm on . The constrained - problem (1.1) is
and denotes its set of global minimizers. Problem (1.4) is the case . Throughout, the paper's blanket assumptions hold: , , and (so that is not a solution).
Two auxiliary objects appear in the milestones. The closed orthants of are the sets of vectors with a prescribed sign ( or ) in each coordinate (2.2). For with the same number of nonzero entries, the log-moment differences are
Under the blanket assumptions with , there is such that
and for this there is such that
The thresholds and depend on and are only asserted to exist; no explicit value is part of the goal.
The first clause of Theorem 2.2 justifies a common computational practice: the sparsest-solution problem, which is combinatorial, can be replaced by a continuous (though nonconvex) problem with a small exponent, and every optimal solution of the latter is optimal for the former. Unlike classical recovery guarantees, it requires nothing of the sensing matrix , and it covers noisy data through the constraint. The second clause says that below some threshold the choice of no longer matters at all, so there is a well-defined "small- limit" solution set. The paper's Theorem 2.3 builds on this by giving an explicit , and its smoothing penalty method (§3) targets exactly the problems covered here.
The result is proved in the paper; nothing here is open. To the best of the platform's search, none of these statements has been formalized: no machine-checked version of Theorem 2.2, Proposition 2.1 or Lemmas 2.2–2.4 exists on the platform or in Mathlib. A formal proof would also produce reusable pieces: the description of the ball as an intersection of half-spaces, finiteness of optimal sets of concave separable objectives over polyhedra without lines, and the fact that power sums of orders determine a sorted real vector.
The obvious argument is a limit: as , so minimizers for small "should" approach minimizers of . This fails as stated: minimizers for different need not converge, is discontinuous, and a limit of near-minimizers need not be a minimizer of the limit problem. What replaces compactness is a finiteness statement: all optimal solutions for all lie in one finite set (Proposition 2.1), which in turn rests on the extreme-point property of minimizers of a concave separable objective on each orthant piece of a polyhedron. The second clause is harder still: two candidate solutions of equal sparsity can exchange order infinitely often as unless one shows that the sign of is eventually constant, which requires the expansion in the log-moments and the identification, via power sums, of the case where all of them vanish.
Vectors are functions Fin n → ℝ (indices ), is a Matrix (Fin m) (Fin n) ℝ, and is A *ᵥ x. The norm is the PiLp q norm with an extended nonnegative real ( is ⊤). The objective lpObj p x is for and the support size for . is the set of global minimizers over , not an infimum value. Orthants are indexed by sign patterns Fin n → Bool, extreme points are Mathlib's Set.extremePoints ℝ, and is written as a sum over the supports (the paper sorts the entries first; a sum is order-independent). The blanket assumptions are explicit hypotheses of each statement about problem (1.1) or (1.4).
Three trivializing formalizations are ruled out: computing as (in Lean 0 ^ 0 = 1, which would make the whole feasible set and the goal's first clause trivial); writing the constraint with the default norm on Fin m → ℝ, which is the sup norm and gives the problem; and an empty feasible set, excluded by hypothesis.
A complete development needs: the norm as a maximum over sign vectors; finiteness of extreme points of a line-free polyhedron (not in the pinned Mathlib in this form); existence of minimizers of a coercive continuous function on a closed set; Newton's identities (Mathlib's MvPolynomial.psum_eq_mul_esymm_sub_sum and relatives) to pass from power sums to elementary symmetric polynomials; and a first-order expansion of near . Proofs of any milestone are welcome, as are alternative proofs of Lemma 2.3 and the polyhedral finiteness facts as standalone results.
Stochastic evolutionary game dynamics model a population of agents who occasionally revise their actions by a noisy best-response rule with noise level . As , the population spends long periods near Nash equilibria and occasionally transits between them; the exponential rates of these transitions, and hence which equilibrium is stochastically stable, are given by path-cost minimization problems (Freidlin–Wentzell 1984; Catoni 1999). Sandholm and Staudigl (2016) showed that in the small-noise double limit these discrete problems converge to continuous optimal control problems on the probability simplex, with a running cost that is linear in each orthant of the control (semilinear) and a state constraint: the population state must stay in the simplex.
Such problems could in principle be solved by optimal control methods, but the available Hamilton–Jacobi theory did not cover them. Soner (1986) treats discounted state-constrained problems, and Capuzzo-Dolcetta and Lions (1990) treat Hamiltonians with superlinear growth; here there is no discounting and the Hamiltonian grows only linearly. Sandholm, Tran and Arigapudi characterize the value functions of these problems and give a verification theorem that certifies explicitly computed solutions, including solutions along which the state constraint binds. This mission formalizes that characterization, following the authors' manuscript of July 4, 2018.
Let be a polytope of dimension : the convex hull of finitely many points. Its tangent space is the direction of its affine hull, is its relative interior, and is its tangent cone at . The norm is the norm, and for a speed bound .
Fix a Lipschitz continuous . The running cost (3.1) of moving from in direction is
A path is a Lipschitz map , , with cost . For compact sets , the source problem and target problem have value functions
the infima running over all and . The Hamiltonian is , and .
A function is a viscosity subsolution of the state-constrained system (4.1) if it is continuous, vanishes on , and whenever is smooth and has a local maximum at ; a supersolution if at local minima ; a viscosity solution if both; and a maximal one if it dominates every viscosity solution on .
If is Lipschitz, on ,
and every admits a time and a path from into with , then is the value function of the target problem on .
The goal is stated for every polytope, every , every and every compact .
The system (4.1) has infinitely many viscosity solutions ( is one, and so is for ), so the value function cannot be identified as "the" solution. Theorems 3.2–3.3 identify it as the largest one, and require the subsolution inequality only almost everywhere: a candidate is checked at points of differentiability, without test functions or superdifferentials. Theorem 3.4 turns this into a constructive tool: a candidate function with paths attaining its values is certified optimal. The paper uses it in §6 to compute exit and transition costs, and hence stochastically stable states, in evolutionary games where the optimal paths run along the boundary of the simplex.
The results are proved in the paper; none is formalized. A complete development would give a machine-checked state-constrained verification theorem for a non-coercive, linearly growing Hamiltonian, together with reusable infrastructure: Lipschitz path costs as lower integrals, value functions with values in , almost-everywhere conditions on lower-dimensional convex sets, and first-order viscosity solutions relative to a constraint set.
Verification is easy in one direction: the attainability hypothesis immediately gives the value function. The other inequality is the content of Theorem 3.3: an arbitrary Lipschitz almost-everywhere subsolution must lie below the value function. The obvious argument integrates along an optimal path, but a Lipschitz need not be differentiable at any point of a given path, and paths along the relative boundary of meet the set where nothing is assumed. Closing this gap needs analysis that is not packaged for this setting: Rademacher's theorem relative to an affine subspace, regularization of almost-everywhere subsolutions on relatively open convex sets, stability of viscosity subsolutions, approximation of boundary paths by interior paths with converging costs, and the relation between the source and target problems under time reversal.
The ambient space is EuclideanSpace ℝ (Fin n). A polytope is the convex hull of a finite nonempty set; its dimension is not fixed, so the simplex () is included. is vectorSpan ℝ X, is intrinsicInterior ℝ X, and is a separate function. Costs and value functions take values in (ℝ≥0∞), so an empty infimum is ; a statement that calls a value function real asserts its finiteness on first. is the derivative within and the cost is a lower Lebesgue integral. "Almost all " is with respect to -dimensional Hausdorff measure restricted to , and is the derivative of relative to , represented by a vector of . Viscosity tests are smooth functions on and local extrema relative to .
Using Lebesgue measure on for "almost all" would make the subsolution conditions vacuous on lower-dimensional polytopes such as the simplex; the formalization avoids this, and the statements must not be weakened to full-dimensional .
One disclosed correction: Theorems 3.2, 4.2 and Propositions 4.3, 4.4 assume , and Theorem 3.3 assumes ; with an empty set the value function is identically and every constant satisfies the conditions. The goal needs no correction.
Contributions are welcome at every milestone, and in particular in reusable lemmas: relative Rademacher theorem on convex sets, mollification on relatively open convex sets, and additivity and approximation of Lipschitz path costs.
A Markov branching process with immigration (MBI) models a population in continuous time: each individual independently dies, splits or is removed at affine rates, and batches of immigrants arrive at a constant rate. Such processes appear in population biology, queueing (infinite-server systems with batch arrivals), epidemics and the analysis of branching algorithms. They were introduced by Sevast'yanov, and the classical references are Harris, The Theory of Branching Processes, and Athreya and Ney, Branching Processes.
For questions about when the population first exceeds a level, first drops to a level, or leaves an interval, the classical literature gave little: only the downward first passage time, the one that crosses levels continuously, had been characterised through its Laplace transform (Avram, Patie and Wang, 2019; Vidmar, arXiv:1908.04714; and, for continuous-state branching processes, Duhalde, Foucart and Ma, 2014). Loeffen, Patie and Wang (arXiv:2208.14425, 2022; Mathematics of Operations Research, 2025) develop a potential theory for general continuous-time Markov chains that are skip-free downward (they can only move down one unit at a time). In that theory every hitting and exit probability is expressed through three fundamental excessive functions. They then apply it to MBIs and obtain a complete set of fluctuation identities. Most of these identities are new.
Let with in . A Q-matrix on is a matrix with for and ; the defect is a killing rate to a cemetery state . The chain generated by waits at an exponential time of rate , then jumps to with probability or to ; after an explosion it is sent to . Its transition function is and its resolvent is . The chain is skip-free downward when (2.1) holds: for and for . For a set , is the first hitting time of , is the lifetime, is the first entrance time into , and is the resolvent of the chain killed on entering .
The MBI with parameters lives on with Q-matrix (5.1):
Here , is an offspring law with and , is a law on , and . The killing rate is . With it is a Markov branching process (MBP). The branching and immigration mechanisms are and , where , and . Lemma 5.1 defines sequences , , , , by explicit recursions, and Theorem 5.4 defines
For every MBI, every identity of Theorem 5.4 (pp. 15–16), as one conjunction:
together with the probability of leaving and the probability of ever reaching .
Theorem 3.1(1) and (3) (the fundamental functions and the resolvent density formula (3.2)); Theorem 3.3(1)–(4) (point hitting, two-sided exit, exit from an interval, upward first passage, for a general skip-free chain); Lemma 5.1 (generating functions of ); Lemma 5.2 (the generating function of ); Lemma 5.3 (stationarity of ).
Theorem 5.4 gives closed forms, in terms of explicit recursively defined sequences, for the resolvent, the probability of hitting a level from above or below, the two-sided exit probabilities and the probability of ever exceeding a level. These quantities are needed in extinction and explosion analyses of branching populations and in ruin-type questions for population-driven systems. Without the theorem they can be computed only by solving infinite systems of linear equations. The general results of Section 3 apply to any skip-free downward chain, including chains with state-dependent killing; the paper also applies them to compound Poisson processes.
All results are proved in the paper. None of them has a machine-checked proof. This mission's development produces a formal theory of continuous-time Markov chains with killing and explosion (minimal transition function, resolvent, killed and dual chains, hitting and exit probabilities). It also produces formal versions of the general fluctuation identities and of the generating-function calculus for MBIs.
The transition function of a chain with unbounded rates is the minimal solution of the backward equations. Other solutions exist when the chain explodes, so no argument may treat as "the" solution of a linear system. Section 3 rests on the strong Markov property at hitting times, on duality with respect to an excessive measure, and on limits of resolvent ratios, which need not be monotone. For the MBI, the generating-function identities require solving the ODEs (5.7)–(5.8) on and relating power series to integrals whose integrand blows up at . The recurrent and MBP regimes are not covered by the transient formulas. They require a separate passage to the limit in an auxiliary killing parameter.
.toReal together with explicit finiteness clauses (, ).Finding a nonzero nonnegative point in a linear subspace is the feasibility core of linear optimization. For a subspace with orthogonal complement , the pair of problems
subsumes every polyhedral feasibility problem and every linear program through standard homogenization. A maximum support solution of the pair, a point of each cone with as many positive coordinates as possible, always exists, and identifies which coordinates can be positive at all. Rescaling algorithms solve such problems with elementary steps (a simple "basic procedure" interleaved with a reconditioning step) and with running-time bounds in terms of a condition measure of the input.
Timeline of the results this mission builds on, as described in the source (arXiv:2003.08911v3, pp. 1–3):
Let be a linear subspace and its orthogonal complement. The support of is . The maximum support index set is
and a maximum support point is an whose support is . For each coordinate , , and the condition measure is , with when .
For let be the vectors vanishing off , , and, for a positive diagonal matrix , the orthogonal projection onto .
Algorithm 1 (partial support) takes with a guess of . It starts from , and repeatedly calls a basic procedure, which returns either with , in which case the algorithm halts with and ; or with , in which case it doubles for a maximizer of (a rescaling step), drops from if , and halts with , if becomes empty. Its output is written .
Algorithm 2 (maximum support) starts with and in each main iteration computes and ; it halts if and otherwise replaces by .
With and , for every , every subspace and every admissible behaviour of the basic procedure: Algorithm 2 never gets stuck, has no infinite execution, never starts main iteration , performs at most
rescaling steps, and upon termination returns , and points , with , .
The result. Theorem 1 gives an algorithm for the maximum support problem whose cost depends only on , without knowing either quantity: guessing rounds and rescaling steps, each of which is a call of the basic procedure on a projected problem. Because the pair of problems subsumes polyhedral feasibility and linear programming, a maximum support solution is a certificate of which inequalities of a homogenized system can hold strictly. The duality behind the stopping test, that and partition the coordinates, is a theorem of the alternative for subspaces of the Goldman–Tucker type.
Formalizing it. The result is proved in the source; nothing here is open. No part of it is machine-checked: there is no formal development of projection-and-rescaling algorithms, of condition measures for subspaces, or of the subspace form of the strict-complementarity partition. Checking the source against the formal statements already found that the printed bounds (5), (6) and (7) are false for some subspaces (counterexamples are recorded in the corresponding items); the targets above carry the minimal corrections, so a complete proof certifies the corrected bounds.
The correctness part reduces to the partition claim and to Corollary 1. The partition requires a theorem of the alternative for the pair and the nonnegative orthant, which is not literally the LP form of Farkas' lemma available in libraries.
The counting part is where the printed argument breaks. The proof of Proposition 1 asserts "throughout the algorithm", by applying Lemma 1 to each rescaling step. But the basic procedure certifies only the subspace , not . As long as the two cones and coincide and the identity holds. Once an index of has been trimmed, which can happen when , it does not. The count of rescalings must also use doublings per trimmed index rather than , which matters precisely because Algorithm 2 uses guesses for which is a power of . The obvious induction on steps therefore has to carry the invariant and works only under . For larger guesses, which Algorithm 2 makes in its early iterations, only the coarse count is available.
is EuclideanSpace ℝ (Fin n) and a Submodule; is Mathlib's orthogonal complement. The Euclidean norm is never used for the paper's norms: and are written coordinatewise, and maximizes over the unit box, not the Euclidean ball. Index sets are Finset (Fin n). is stored as its diagonal. is the orthogonal projection of onto , which agrees with the paper's map on . when , as in the source. Proposition 1 and Theorem 1 assume , since Algorithm 1 cannot run on .
Both algorithms are transition relations whose states carry the rescaling and iteration counters, and the basic procedure is nondeterministic: every admissible answer and every maximizer is a possible step, and both branches may be available at once. Every statement quantifies over all executions. Progress (no reachable non-halted state is stuck) and the absence of infinite executions are stated explicitly. This rules out the trivializing formalizations: a relation with no transitions (which would make "upon termination" vacuous), a fixed deterministic basic procedure, over the Euclidean ball, bounds for a single execution, and termination as "some execution halts". A sorry-free check exhibits, for and , a reachable halted state of Algorithm 2 after two rescaling steps, which also witnesses that the printed (7) fails.
A complete development needs the theorem of the alternative for subspaces, orthogonal projections onto intersections of subspaces, a variant/measure argument for termination of nondeterministic relations, and logarithm and floor arithmetic for the schedule . The partition claim and the condition-measure lemmas are reusable for other rescaling and condition-number analyses. Proofs of the milestones, alternative arguments for the partition, and the sharper count of Proposition 1 are all welcome.
A bipartite quantum state shared by Alice and Bob is -extendible if there is a state on copies of Alice's system and copies of Bob's system whose reduced state on every pair (one Alice copy, one Bob copy) is . Extendibility (also called shareability) measures how much the correlations of can be shared among many parties. Only separable states are extendible for all , so the extendibility numbers of an entangled state quantify its entanglement. The notion appears in the characterization of entanglement and non-locality, in quantum de Finetti theorems, in quantum key distribution, and in entanglement measures such as the squashed entanglement, for which it gives lower bounds (Doherty, Parrilo, Spedalieri 2004; Brandão, Christandl, Yard 2011).
Computing extendibility is in general a semidefinite program whose size grows exponentially, and analytic answers are known only for a few families. Werner states, the states invariant under all , are the standard test family. The one-sided case was solved earlier; for the two-sided case only a few extension sizes were known (Johnson, Viola 2013). D. Jakab, A. Solymos and Z. Zimborás (arXiv:2208.13743v2, 2022) map the two-sided problem for Werner states to the ground state problem of a permutation-symmetric spin Hamiltonian and solve it with the representation theory of .
Fix a local dimension and extension sizes . Let be the flip on , . For the Werner state is
the unique -invariant state with . A state on is an -extension of if its partial trace onto Alice's -th and Bob's -th copy equals for every and . The extendible Werner parameters form an interval .
A -partition is a sequence of integers with sum (a Young diagram with boxes and at most rows). Dominance order is iff for every . The Casimir value is
For and , the minimum product diagram is , the rows of reversed, added to those of and sorted decreasingly. The energy of the pair is
The Hamiltonian sums the flips of every Alice copy with every Bob copy .
for every , and . This is the characterization the paper derives in Eq. (12) and the first expression of Eq. (13). It fixes no closed form for the minimum.
The goal reduces a semidefinite feasibility problem on a space of dimension to a minimization over pairs of Young diagrams, a finite set of size polynomial in for fixed . It decides the two-sided extendibility of every Werner state, for every local dimension and every pair of extension sizes, and shows a non-trivial trade-off between and . The milestones on the minimum product diagram are statements about Littlewood–Richardson coefficients of independent interest in algebraic combinatorics.
Status. The paper also states a closed formula, Eq. (16), and it is false as printed. Eq. (15) has a sign slip: at , exact diagonalization of gives while Eq. (16) gives . Eq. (13)'s claim that a minimizing pair can be taken of a special non-overlapping shape is also false: at , the pair gives (confirmed by Lanczos diagonalization), below the best special pair, . The mission therefore poses the characterization by the minimum over all pairs, which every check confirms, and no closed form. The printed middle equalities of Eq. (10) are also off: for a box moved from row to row the difference is ; the inequality and the refinement claim of Eq. (10) are true. None of these results has a machine-checked proof.
The reduction to is elementary; the obstacle is the spectrum. , , commute, so the eigenvalues of are labelled by triples , but only the triples with inside occur. Minimizing over this Littlewood–Richardson support is not a local computation: the obvious candidate, adding the rows of and in the same order, gives the dominance-maximal constituent and the largest Casimir value. The paper's answer goes through a theorem of Azenhas on skew Littlewood–Richardson tableaux and a duality of multiplicities. On the analytic side, Schur–Weyl duality and the Casimir value on each isotypic component are needed, neither of which is in Mathlib in this form. Finally, the minimum of itself has no known closed form; the natural guess of non-overlapping shapes fails.
All objects are explicit finite matrices over . The joint system is indexed by (Fin nA → Fin d) × (Fin nB → Fin d); sites and rows are 0-based. Extendibility requires a positive semidefinite, trace-one extension whose marginal on every pair is the given state, and the marginal sums each traced configuration exactly once. -partitions are weakly decreasing maps Fin d → ℕ with the right sum, so rows of length zero are allowed and there are at most rows. The Casimir value keeps its shift, since compares at three sizes. "" is written as the existence of an eigenvalue, or of a pair, below ; the sets are finite and nonempty. Standing hypotheses: , , (for , is not a state).
Restricting the marginal condition to some pairs, dropping positivity or the trace, rescaling the marginal, or bounding the number of rows differently would each change the theorem; the definitions exclude all of these. The goal is not trivially true at the edges: for , it says that every Werner state is -extendible, and the minimum of is .
The development reuses two published definitions: the -isotypic projector on (QAlgorithms.Schur.isotypicProjector) and the polynomial Littlewood–Richardson coefficient counted by LR tableaux (lrCoefficient). Needed infrastructure: Schur–Weyl duality for the isotypic projectors, the Casimir eigenvalue on each component, the Littlewood–Richardson rule for the tensor product of two Schur modules, and Azenhas's theorem. Proofs of the combinatorial milestones (dominance, duals, Azenhas, the minimum product diagram) are reusable in algebraic combinatorics; the Casimir and Schur–Weyl results are reusable in quantum information. Contributions to any milestone, or alternative proofs of the minimum product diagram, are welcome.
The stability number of a graph, the largest number of pairwise non-adjacent vertices, is one of the basic parameters of combinatorial optimization: computing it is NP-hard, and random graphs are the standard test bed for what typical instances look like. For the Erdős–Rényi–Gilbert graph , in which every edge is present independently, the behaviour of is known to first order in the dense regime (Grimmett–McDiarmid 1975) and in the sparse regime (Frieze 1990). Independence of the edges is what all these arguments use, and it is also the feature that real networks most obviously lack.
A. Gupte and Y. Zhu (arXiv:2207.04514, Mathematics of Operations Research, 2025) introduce a random graph in which the edges at a vertex are dependent through a Markov chain, and ask which classical properties survive. Their first main result is a lower bound on of order that holds with high probability. This mission formalizes that result, read in the arXiv version v4 (24 May 2024).
Fix an initial probability and a decay parameter , and write . The recursive Markov random graph (Definition 1 of the paper) has vertices and is generated vertex by vertex. When arrives, its edges to the earlier vertices form a row of Bernoulli variables , with when the edge is present. Rows of different vertices are independent. Within a row:
So each row is a non-homogeneous Markov chain whose transition matrix (display (2) of the paper) depends on the marginal of the previous edge. The marginals then obey the recursion with , and a present edge lowers the chance of the next one by the factor . At the model is ; the paper assumes throughout.
The average degree is . A property holds with high probability (w.h.p.) if its probability tends to as , and concentrates to if for every . The logarithm is natural.
For every , and ,
The constant is the paper's, and the statement is required for every and every admissible , .
In attack order:
The theorem shows that the dependence between consecutive edges does not destroy the scale of the stability number. Combined with the paper's upper bound (Theorem 2.4) and its analysis of the greedy algorithm (Proposition 2.3), it places between the dense and the sparse regimes of . Theorem 2.2, a milestone here, is of independent interest: the graph has average degree , and Corollaries 2.5–2.7 of the paper derive from it bounds on the minimum degree and the chromatic number and the existence of large clique minors.
The formalization adds a checked account of a proof whose printed version has gaps. Several printed lemmas are false as stated: Lemmas 4.2 and 4.3 lose a scaling factor, Lemma 6.2 has a wrong upper bound, Lemmas 10.1 and 10.4 are stated in a setting where they fail and Lemma 10.1 has a wrong constant, Theorem 4.4 is false without a Markov hypothesis, and the stochastic-dominance step (5) in the printed proof of Theorem 2.2 is false. Each affected milestone is stated in a minimally corrected form. Theorem 2.1 and Theorem 2.2 themselves are true. None of these results has a machine-checked proof.
A first idea is to transfer arguments directly. For with the bound comes from Turán's theorem plus concentration of the edge count, and the edge count is a sum of independent indicators. In the edges at a vertex are strongly dependent: the edge count of a row is the partial sum of a non-homogeneous Markov chain whose marginals decay like , so its mean grows only like . Standard laws of large numbers do not apply, and concentration of a row sum around needs a second-moment bound that uses the Markov structure; the marginal recursion alone does not suffice (a comonotone coupling with the same marginals has row sums that stay bounded). The heart of the mission is therefore Corollary 4.6, a law of large numbers for this chain, built from the recursion estimates of Lemmas 4.2–4.3 and the second-moment bound of Lemma 10.1, and its transfer to the average degree through the independence of the rows.
The vertex set is Fin n, the paper's being k − 1, and the edge is G.Adj (j−1) (i−1). The law of is an explicit finite weight rmrgWeight n p r G on SimpleGraph (Fin n). It is a product over rows, each row's weight being the Markov chain above with the transition out of edge using the -th iterate of from . Probabilities are rmrgProb n p r E, the sum of the weights of the graphs in . Definition 1's phrase "independent of all other edges" cannot hold for the next edge of the same row; it is read through the paper's generation process (rows independent, each row a Markov chain with transition matrix (2)). Lemma 3.1 is the milestone certifying that the marginals of this weight obey the recursion. A sanity file checks that the weights sum to for and that the first two edge marginals are and .
The decay chain is IsDecayChain P Y β on a probability space: -valued measurable variables, the Markov property, and the two transition rules, with conditional probabilities written multiplicatively. Expectations are Bochner integrals, and "w.h.p." and concentration are limits of probabilities of the events , as defined on p. 4 of the paper. Variances in Lemma 10.2 come with square integrability for all large , so the hypothesis is not met by the junk value .
A trivializing formalization is ruled out: the weight is exactly the law of Definition 1, not one favouring sparse graphs, and no hypothesis of the goal pins the graph or the probability.
The corrections, each with a counterexample satisfying the paper's hypotheses, are declared on the items:
Theorem 4.4 is false as stated and is not an item; Corollary 4.6, which the proof of Theorem 2.2 cites, replaces it. Displays (5)–(10), Proposition 2.3, Theorem 2.4 and Corollaries 2.5–2.7, 4.5, 4.7 and 5.2 are out of scope.
A complete development needs:
rmrgProb: marginals, independence of rows, the row-to-chain identification;SimpleGraph.indepNum, which Mathlib does not yet have.The last two are reusable beyond this mission. Contributions to any milestone are welcome, as are alternative proofs of Theorem 2.2 that avoid the printed stochastic-dominance step.
Centralized platforms that assign work to independent service providers, such as ride-hailing and freelance marketplaces, sales organisations distributing leads, and firms sourcing from several suppliers, are often asked to give their providers guarantees: a minimum income, a max-min fair share of the work, or another fairness criterion. A guarantee shrinks the set of allocations the system may use, so it can lower the total value the system generates. The question is how much value can be lost.
Many settings of this kind have no bound at all on the price of fairness or the price of anarchy (Bertsimas, Farias and Trichakis 2011; Koutsoupias and Papadimitriou 2009). Gur, Iancu and Warnes (SSRN 3351509, published in Management Science in 2020) identify a broad class of job-allocation systems and guarantees for which the relative loss is bounded by a quantity that depends only on the number of providers and on how different they are. This mission formalizes that bound, Theorem 1 of the paper, and the steps of its proof.
A job in a finite set has an intrinsic value . Values may be negative. A set of jobs has value . There are providers . An allocation is a tuple of subsets of , where is the set of jobs given to provider . Provider turns its jobs into value . The heterogeneity profile lies in with , and the degree of heterogeneity is
The feasible allocations form a set that satisfies Assumption 1:
The allocations with guarantees form a non-empty subset that satisfies Assumption 2 (Pareto efficiency): if , and for every , then . Income guarantees under monotone payments, max-min fairness and α-fairness are of this kind (§2.3 of the paper). The value loss under provider guarantees is
For every and all , satisfying Assumptions 1 and 2,
The statement fixes nothing beyond the paper's model: every finite job set, every real-valued , every number of providers and every profile in the box.
These are the steps of the proof in Appendix A, in attack order:
The result. With homogeneous providers () any Pareto-efficient guarantee costs less than half of the optimal value, since . For every fixed the loss stays below . A system designer may therefore choose among income guarantees, max-min fairness and similar rules knowing that none of them can destroy more than a fixed fraction of value. Theorem 2 of the paper shows that the bound is tight. Theorem 1 is the paper's main result.
Formalizing it. The result is proved in the paper; nothing in this mission is open mathematically. The work is the formal proof. On the way it produces reusable pieces:
Two printed gaps get settled:
The obvious attempt is to compare an optimal unrestricted allocation with an optimal guaranteed one job by job. This gives no bound, because and are arbitrary sets subject only to the axioms: there is no explicit allocation rule to compare against. The paper's route has several steps that each need care.
Everything lives in the namespace ProviderGuarantee.Bound. The definitions are in the single file ProviderGuarantee.Bound.Model:
Fintype, and carries no sign condition. An allocation is a function Fin n → Finset D, so provider of the paper is the index .fun i => A (σ i)), and monotonicity and provider independence use Function.update. Assumption 2 includes .sSup. Every set of allocations is finite, so this is a true maximum on non-empty sets, and is a hypothesis of the goal.sSup and the dual value is a real sInf over (15). (15) is (16) with explicit. The milestones state feasibility, boundedness and attainment, so neither value is a default.The goal is about the value loss of the allocation model over all admissible , and . A formalization stating Theorem 1 about the LP value, at a single vertex, at , with , or with a weakened Assumption 1 or 2 would prove a different and easier statement, and is ruled out.
A complete development needs:
Finset.biUnion);LinearOptimization.lp_strong_duality) is a possible tool;Contributions are welcome for any milestone, and for the invariance of (14) under permutation and positive scaling of , which the goal's proof needs and the paper uses tacitly.