Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In the present paper we study abelian extensions of connected Lie groups modeled on locally convex spaces by smooth -modules . We parametrize the extension classes by a suitable cohomology group defined by locally smooth cochains and construct an exact sequence that describes the difference between and the corresponding continuous Lie algebra cohomology space . The obstructions for the integrability of a Lie algebra extensions to a Lie group extension are described in terms of period and flux homomorphisms. We also characterize the extensions with global smooth sections resp. those given by global smooth cocycles. Finally we apply the general theory to extensions of several types of diffeomorphism groups.
This mission is the statement-level formalization of Abelian extensions of infinite-dimensional Lie groups (arXiv:math/0402303v1). 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 The group defined by a normalized two-cocycle (Lemma II.1, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
94 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper we study non-abelian extensions of a Lie group modeled on a locally convex space by a Lie group . The equivalence classes of such extension are grouped into those corresponding to a class of so-called smooth outer actions of on . If is given, we show that the corresponding set of extension classes is a principal homogeneous space of the locally smooth cohomology group . To each a locally smooth obstruction class in a suitably defined cohomology group is defined. It vanishes if and only if there is a corresponding extension of by . A central point is that we reduce many problems concerning extensions by non-abelian groups to questions on extensions by abelian groups, which have been dealt with in previous work. An important tool is a Lie theoretic concept of a smooth crossed module , which we view as a central extension of a normal subgroup of .
This mission is the statement-level formalization of Non-abelian extensions of infinite-dimensional Lie groups (arXiv:math/0504295v1). 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 Normalized factor systems: group criterion, inversion and conjugation (Lemma II.7 (continues on PDF p. 16), PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
46 results of the paper are not stated yet, because the library lacks an interface they need:
We study the twisted Weyl symbol of metaplectic operators; this requires the definition of an index for symplectic paths related to the Conley-Zehnder index. We thereafter define a metaplectically covariant algebra of pseudo-differential operators acting on functions on symplectic space.
This mission is the statement-level formalization of A Weyl Calculus on Symplectic Phase Space (arXiv:math-ph/0508024v2). 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 Symplectic Cayley bijection, product and inverse (Lemma 6: symplectic Cayley bijection, product and inverse, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
23 results of the paper are not stated yet, because the library lacks an interface they need:
This paper attempts to give an overview about sufficiency in the setting of quantum statistics. The basic concepts are treated paralelly to the the measure theoretic case. It turns out that several classical examples and results have a non-commutative analogue. Some of the results are presented without proof (but with exact references) and the presentation is intended to be self-contained. The main examples discussed in the paper are related the Weyl algebra and to the exponential family of states. The characterization of sufficiency in terms of quantum Fisher information is a new result.
This mission is the statement-level formalization of Sufficiency in quantum statistical inference. A survey with examples (arXiv:quant-ph/0604091v1). 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 The Bernoulli sample mean is sufficient (Introduction: Bernoulli sample mean is sufficient, 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.
35 results of the paper are not stated yet, because the library lacks an interface they need:
We show that the eigenvalues and eigenfunctions of the stargenvalue equation can be completely expressed in terms of the corresponding eigenvalue problem for the quantum Hamiltonian. Our method makes use of a Weyl-type representation of the star-product and of the properties of the cross-Wigner transform, which appears as an intertwining operator.
This mission is the statement-level formalization of A new approach to the star-genvalue equation (arXiv:0808.0489v1). 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 Phase displacement multiplication and commutation (§3, (10)–(11), 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:
Work of Clifford, Munn and Ponizovski{\u\i} parameterized the irreducible representations of a finite semigroup in terms of the irreducible representations of its maximal subgroups. Explicit constructions of the irreducible representations were later obtained independently by Rhodes and Zalcstein and by Lallement and Petrich. All of these approaches make use of Rees's theorem characterizing 0-simple semigroups up to isomorphism. Here we provide a short modern proof of the Clifford-Munn-Ponizovski{\u\i} result based on a lemma of J. A. Green, which allows us to circumvent the theory of 0-simple semigroups. A novelty of this approach is that it works over any base ring.
This mission is the statement-level formalization of On the irreducible representations of a finite semigroup (arXiv:0712.2076v2). 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 Every simple semigroup module has an apex (Theorem 5, 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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
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:
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:
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:
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:
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:
Karmarkar's 1984 algorithm solved linear programs in polynomial time by reducing a logarithmic potential function by a constant at every step (doi:10.1007/BF02579150). Its successors replaced Karmarkar's projective transformations with a primal-dual potential that measures the duality gap and the distance from the central path together. Tanabe, and Todd and Ye (1990, doi:10.1287/moor.15.3.508), introduced this potential. Ye (1991) and Kojima, Mizuno and Yoshise (1991) showed that one fixed reduction per step, for the parameter , gives the best known iteration bound . The potential-reduction method needs no step that stays close to the central path. It became one of the standard interior-point methods, and its analysis was later carried over to semidefinite and conic programming.
Chapter 4 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley, 1997, doi:10.1002/9781118032701) proves this one-step estimate for two algorithms. The first is the primal-dual potential-reduction algorithm (§4.3), which alternates a primal projected-gradient step with an update of the dual lower bound. The second is the symmetric primal-dual algorithm (§4.4), which moves along the Newton direction toward a point of the central path. This mission formalizes both estimates and the lemmas they rest on.
Let be a real matrix of rank , with , , . The standard-form pair is
and both are assumed to have interior feasible points. Vector inequalities are componentwise, is the all-ones vector, , , is the Euclidean norm and . The interior consists of the triples with , , , . For , the primal-dual potential and the primal potential with lower bound are
The potential-reduction step (§4.3, ). At with , let
The dual update is with , and .
The symmetric step (§4.4). With and , the direction solves , , . The step size is for a constant .
There is a constant such that for every such LP and every , with , and ,
Theorem 4.9 says that the potential can be lowered by a fixed amount no matter where the iterate is. Either the primal step makes progress, or the dual update produces a feasible, nearly central dual point with a smaller gap. Since , a constant decrease per step yields the bound of Corollary 4.10 without any neighborhood of the central path. Lemmas 4.11 and 4.12 give the same conclusion for the symmetric algorithm, with decrease . These are the per-step facts behind practical potential-reduction codes and their conic extensions.
The platform has no statement of these results. LinearOptimization.interior_point_potential_reduction (proved) turns a constant decrease of a different potential into an iteration count. The Mizuno–Todd–Ye bounds on the second-order term of the Newton step, which are Ye's Lemmas 4.14, 4.15 and 4.19, are already formalized as AdaptiveStepIPM.PredCorr.lemma_1a, AdaptiveStepIPM.WideNbhd.lemma_1b, lemma_1c and lemma_2c. They belong to the path-following part of the chapter and are not repeated here. Formalizing Theorem 4.9 checks the case split and its numerical constants, and produces a reusable layer: the weighted projection , the dual estimates , , and the potential identities.
The case split is driven by , which is defined through a projection, but Lemma 4.8 reasons about it through the identity (4.11). The book states that identity without proof. It needs the normal equations for , , and so the invertibility of . The primal case needs and before any logarithm is evaluated. It also needs the first-order term to equal exactly, which uses that is an orthogonal projection. The dual case combines Lemma 3.1, applied to , with the arithmetic–geometric mean inequality and the bound . The constant must be checked for every : with and the two decreases are about and , so the margin over is small. Lemma 4.11's proof is omitted in the book. Unlike its Chapter 3 analogue it needs no normalization , but the exact cancellation of its first-order term has to be verified. Lemma 4.12 is left as an exercise.
Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; indices are -based. The Euclidean norm is written out as norm2. The rank of , the existence of interior points (p. 63) and (Chapter 4 preamble, p. 109) are bundled as StandingAssumptions A b c and are a hypothesis of every theorem, together with . The vector is defined by its projection formula, not by (4.11), so (4.11) is something to prove. Matrix inverses are Mathlib's ⁻¹, which is on singular matrices and never reached under the rank assumption.
Explicit constants: Theorem 4.9 does not fix the step length , and the proof chooses (with in the case split). The goal is stated for the step (4.10) with . Its is quantified before , , , , and the iterate, so one number serves every instance. A formalization in which depends on the instance, or in which the step is any point that happens to lower the potential, would be trivial; both are ruled out by stating the theorem for the book's step (4.10) and dual update (4.12)–(4.13) with a uniform . No result in this mission uses .
Beyond the paper. One variant is posed: a strengthened Theorem 4.9 for every with the same (finding F1). The proof uses only through and , and both hold for .
Not in scope: the iteration-count statements (Theorems 4.4, 4.7, 4.13, 4.20, Corollary 4.10), which the book gives with ; Karmarkar's algorithm and the path-following analysis of §§4.1–4.2 (Proposition 4.2, Lemmas 4.5–4.6), which need the max-potential of the dual level set; and the predictor-corrector Lemmas 4.16–4.17 and Theorem 4.18, which are statements about an algorithm's sequence.
Interior-point methods for linear programming do not move along the boundary of the feasible region; they follow a curve of points that stay "central". The basic notion of centrality is the analytic center of a polytope, the interior point that maximizes the product of the slacks of its defining inequalities (Sonnevend, 1986, doi:10.1007/BFb0043914). Every path-following and potential-reduction algorithm repeatedly computes an approximate analytic center, so it matters how "approximately centered" is measured and what one Newton step does to that measure.
Chapter 3 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley, 1997, doi:10.1002/9781118032701) answers both questions for a polytope given by linear inequalities. It introduces three measures of proximity to the analytic center (dual, primal and primal-dual), proves that they are equivalent, and shows that the corresponding Newton steps square them. The same estimates reappear, with minor changes, in the complexity analysis of Karmarkar's algorithm and of the primal-dual potential-reduction methods of the later chapters. This mission formalizes those statements.
Let be a real matrix and . Vector inequalities are componentwise, is the all-ones vector, , , and is the Euclidean norm. The chapter works under standing assumptions: has rank , , and the polytope
is bounded with nonempty interior. An interior point of has . The homogeneous primal set is ; its interior points have , .
Three potential functions are used:
The analytic center is the interior point of maximizing , and the primal potential minimizer is the interior point of with minimizing .
The three proximity measures are
The dual Newton step is ; the primal Newton step is ; the primal-dual Newton directions solve , , , and are taken with step size for a constant .
For an interior point of , an interior point of , the analytic center and the primal minimizer :
Theorem 3.2 is what makes an "approximate analytic center" a well-defined notion: whichever of the three measures an algorithm controls, the other two and the potential gaps follow. Parts 3 and 4 convert a small residual into a bound on the logarithmic-volume gap and on the relative distance to the true center. These are the quantities used to start the Newton procedures of Theorem 3.3 and Corollary 3.8, and to bound the number of central-section and potential-reduction steps elsewhere in the book. Lemma 3.12 and Theorem 3.13 are the per-step estimate of the primal-dual potential-reduction method, the template for the linear-programming algorithms of Chapter 4.
None of these statements is formalized on Prove2Me. The platform has self-concordant Newton analysis (ConvexOptimization.newton_quadratic_phase_contraction) and proximity measures for self-scaled cones (SelfScaledIPM.FuncProx.*, open), but neither works with Ye's measures or steps. The results are classical and proved in the book. Formalizing them yields a reusable linear-algebraic layer (projections , scaled least squares, the primal-dual Newton system) for any later interior-point mission. It also checks hypotheses the book leaves implicit: Lemma 3.12 is false without the normalization that §3.4.2 states only once.
Most of the chapter's arguments are short on paper but depend on facts that are only described in words. In (i), and are the optimal values of weighted least-squares problems, and the domination needs that variational characterization, which goes through the invertibility of and (rank ). Part 4 is not a one-step estimate: it is obtained by running the Newton procedures of Theorem 3.3 and Corollary 3.8 indefinitely, summing a geometric series of quadratically shrinking corrections, and identifying the limit with the analytic center. That identification requires uniqueness of the center (strict concavity on a bounded polytope) and the correspondence between and through . Part 3 needs that correspondence as well. The positivity of the damped iterates in Lemma 3.12, which the book asserts "can be verified", has to be established before any logarithm is evaluated. Theorem 3.13 requires constants independent of , which rules out every argument that loses a dimension factor.
Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; indices are -based. The Euclidean norm is written out as norm2, since Mathlib's norm on Fin n → ℝ is the sup norm. Matrix inverses are Mathlib's ⁻¹, which is on singular matrices. The rank hypothesis makes every inverted matrix positive definite at the points where the theorems use it, so the junk value is never reached. The standing assumptions (rank , , bounded with nonempty interior) are bundled as StandingAssumptions A c and are a hypothesis of every theorem. The normalization of §3.4.2 is a hypothesis of Lemma 3.12 and Theorem 3.13. The analytic center and the primal minimizer are defined by their extremal properties, not by the optimality system , so the goal cannot be obtained by unfolding a definition. The theorems are stated for the steps exactly as the book defines them, never for an arbitrary "good" step.
Explicit constants: no result in this mission uses . Theorem 3.13's constants are existential in the book ("we can choose … for a positive constant "). They are stated as quantified before , , and , which is what the proof establishes. A formalization in which or depends on the instance would be trivial and is ruled out by this quantifier order.
Beyond the paper. One variant is posed: a sharpness probe of Lemma 3.12 with the normalization removed (findings F1, F3). With , , , , the step only rescales , so the potential is unchanged while the claimed bound is about . A disproof is the expected outcome.
Not in scope: Theorem 3.11 (the primal-dual Newton step), whose positivity claim fails as printed (finding F2); the iteration-count theorems 3.4, 3.7, 3.9, stated with ; the central-section Lemmas 3.5–3.6; and Theorem 3.10 (affine scaling). Contributions welcome: the least-squares characterization of , as reusable lemmas, and the uniqueness of the analytic center.
Primal-dual interior-point methods for linear programming generate strictly positive iterates that approach the solution set but never reach it: the duality measure tends to zero, yet no iterate is ever an exact solution. Many applications need more than an approximate point — an exact optimal basis, a vertex, or the optimal partition of the variables into those that are positive and those that vanish at optimality. Chapter 7 of Stephen J. Wright's Primal-Dual Interior-Point Methods (SIAM 1997) studies the end game of these methods: how fast decreases once the iterates are close to the solution set, and how to jump from an interior iterate to an exact solution.
The finite termination procedure formalized here is due to Ye (Math. Programming 1992): guess the optimal partition from the current iterate and project onto the face of the feasible set it determines. The superlinear analysis of the affine-scaling step goes back to Ye, Güler, Tapia and Zhang (Math. Programming 1993); its key uniform bound on weighted least-squares solutions was proved independently by Stewart (Linear Algebra Appl. 1989) and Todd (Oper. Res. 1990). The bound on solutions of linear systems used throughout is Hoffman's (J. Res. Nat. Bur. Standards 1952).
Fix , , , with no assumption on the rank of . The primal problem is subject to , ; the dual is subject to , . Let and be their sets of optimal solutions and . The optimal partition is
A strictly complementary solution is with for and for . The quantity
measures how far the solution set reaches into each coordinate, and .
The strictly feasible set consists of triples with , , , . The duality measure is . The wide neighborhood is for , and the 2-norm neighborhood is , where is the vector of products and is Euclidean.
The affine-scaling direction at is any solution of
The partition estimate at is , , and the projection problem of Ye's procedure is
For there is a threshold such that every with
satisfies (i) and , and (ii) the projection problem has a solution, and every solution is a strictly complementary solution. The threshold is existential, as printed; the goal does not fix its value.
Theorem 7.12 turns any path-following method into a finite algorithm: once falls below , one linear least-squares problem, costing about one interior-point iteration, returns an exact strictly complementary solution, and with it the optimal partition. For integer data the threshold is bounded below by , which is how interior-point methods are made to terminate exactly within their polynomial iteration bounds (Chapter 3 of the book). Theorem 7.4 and Lemma 7.6 give the competing route — the affine-scaling step is , so predictor steps approach full length and the predictor-corrector method converges two-step quadratically.
None of these results is formalized on the platform. Hoffman's error bound exists there for a single consistent system with a constant chosen after the right-hand side; Lemma A.3 and its variant need one constant for all right-hand sides. The optimal partition, , the uniform weighted least-squares bound and the projection step are reusable for any formal treatment of interior-point methods, degenerate linear programs or error bounds.
Near a degenerate solution set the linear systems defining the affine-scaling step become arbitrarily ill-conditioned: the diagonal scaling has entries tending to and to , and the coefficient matrix has no nonsingular limit unless the solution is unique. Any bound that passes through the conditioning of that matrix degrades as ; the constants of Theorem 7.4 and Lemma 7.2 must be independent of the scaling. For Theorem 7.12 the difficulty is uniformity in the other direction: the threshold must be one number for the whole neighborhood, which needs a bound on the distance from an iterate to a face of the feasible set that does not depend on the iterate.
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, points are triples (x, lam, s); the Euclidean norm is defined explicitly (Mathlib's default on Fin n → ℝ is the sup norm). Directions and the projection problem are defined by their equations and optimality, never by closed-form formulas. uses real suprema, which agree with the book's whenever ; every theorem is vacuous otherwise. No rank assumption on is made except in Lemma A.4, where the page states it. is not a hypothesis: membership in a neighborhood implies it.
Explicit constants: the book writes "there is a constant" in Lemmas 5.13 and 7.1; their proofs give (5.32) and (7.6), which are used. The constants , , , , have no closed form in the book (they come from Lemma 2.5, Hoffman's lemma and Lemma 7.2) and stay existential, but each is quantified before the point, the right-hand side or the scaling it must work for; a constant chosen after the point would make Theorem 7.4 trivial. A trivializing form of the goal — a threshold allowed to be , or a conclusion about some minimizer chosen by the solver — is ruled out by requiring , existence of a minimizer, and strict complementarity of every minimizer ( is not unique). In Lemma 7.6 the largest step is a hypothesis (IsGreatest), and the statement also asserts that the whole interval is admissible.
Beyond the paper: one variant is posed. lemma_A_3_strong (strengthened, finding F1) is Lemma A.3 for every consistent system , instead of ; this is Hoffman's 1952 theorem. Finding F2 records that the printed proof of Theorem 7.4 covers only full-row-rank ; the statement is kept as printed.
Needed infrastructure: LP optimal solution sets and the optimal partition, matrix inverses and ranks, finite sums. A uniform Hoffman bound and the Stewart–Todd bound are reusable well beyond this mission; contributions of either are welcome.
Interior-point methods for linear programming are usually analysed under the assumption that the primal-dual pair has a strictly feasible point, or at least a solution. A solver used in practice cannot assume this: it must either return a solution or report that the primal or the dual problem is infeasible. The homogeneous self-dual approach embeds the linear program into one larger problem that always has a solution and reads the answer off that solution. Ye, Todd and Mizuno introduced the HSD form (Ye, Todd, Mizuno 1994); Xu, Hung and Ye simplified it (Xu, Hung, Ye 1996). The approach is used in production interior-point codes. This mission formalizes Chapter 9 of Wright's textbook (Wright 1997), together with the parts of Appendix A on which its proofs rest.
Let , , . No assumption is made on the rank of . Vector inequalities are componentwise. The primal-dual pair is
The primal solution set consists of the feasible that attain the minimum of . The dual solution set consists of the feasible that attain the maximum of . The primal-dual solution set is .
The simplified HSD form introduces scalars and asks for with
Here is free. This is a mixed monotone linear complementarity problem (mLCP) with a skew-symmetric matrix. It always has the zero solution. A solution is strictly complementary if and .
More generally, a self-dual linear program (9.1) has the form subject to , , , where and are skew-symmetric. Its mLCP (9.2) asks for with , , and . A solution is strictly complementary if .
The HSD form of Ye, Todd and Mizuno starts from an initial point with , . It sets , and , and adds a free variable . The result is the mLCP (9.8):
The right-hand side quantifies over all strictly complementary solutions. It is not vacuous, because such solutions always exist.
In attack order:
Theorems 9.2 and 9.3 make the simplified HSD form a complete decision procedure for linear programming. Any strictly complementary solution of (9.5) has one of two forms. Either , and then solves the original pair. Or , and then the solution certifies that the primal or the dual problem is infeasible. Path-following methods converge to strictly complementary points. An algorithm applied to a problem that always has a solution therefore settles the original problem, without any feasibility assumption. Theorems 9.4–9.6 transfer this to the HSD form, which also admits the strictly feasible starting point (p. 184) and so can be solved by a feasible interior-point method.
On the formalization side, nothing about the simplified HSD form is on the platform yet. The Ye–Todd–Mizuno form appears in other missions as open statements about a single strictly self-complementary solution, under a hypothesis of the form . Theorems 9.5 and 9.6 here instead quantify over all strictly complementary solutions and use the hypothesis , so they are separate statements. Appendix A's Theorem A.1 is the classical KKT theorem for linear constraints, and Theorem 9.1 is a structural fact about skew-symmetric complementarity problems. Both can be reused beyond this chapter.
The "if" direction of Theorem 9.2 is short once strictly complementary solutions of (9.5) are known to exist. That existence is Theorem 9.1, which is the substance of the chapter. Monotone LCPs in general need not have strictly complementary solutions. A solver has to show that the self-dual structure rules out the failure seen for general monotone LCPs, for a problem in a nonstandard form with free variables and equality rows.
The "only if" direction needs more than one well-chosen solution. It needs the fact that all strictly complementary solutions of (9.5) have the same support. The book asserts this without proof (finding F3 in FINDINGS.yaml), so a solver must supply it. Theorem 9.5 also requires a strictly complementary solution of (9.8) with whenever . Here the normalisation row of (9.8) has to be satisfied, which the simplified form does not ask for.
Vectors are Fin n → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ; and may be zero. The definitions file WrightPDIPM.SelfDual.Setup writes out the systems (9.2), (9.5) and (9.8) row by row, exactly as printed, together with their solution and strict-complementarity predicates. and are defined by optimality against every feasible point, with no infimum, so they are empty when the optimum is not attained. The gradient in Appendix A is the vector of Fréchet partial derivatives, and every statement that uses it assumes differentiability. The Euclidean norm is defined explicitly.
Several standing hypotheses of the book are made explicit:
The page writes for in Theorem 9.6. This is a misprint, and the formal statement uses . No statement in this selection carries an constant.
Theorem 9.2 must not be formalized with "strictly complementary" weakened to "solution", since the zero solution would then falsify the right-hand side. Its right-hand side must not be read as an existence claim either. The statement keeps the book's universal quantifier over strictly complementary solutions.
Beyond the paper. Two variants are posed beside the faithful statements. theorem_9_3_strong (strengthened, finding F1) is Theorem 9.3 for every solution of (9.5) with , since the book's proof never uses strict complementarity. theorem_9_6_strong (strengthened, finding F2) is the same strengthening of Theorem 9.6, via Theorem 9.4.
A complete development needs:
The KKT and Goldman–Tucker statements, and the mLCP definitions, are reusable for the LCP material of Chapter 8. Contributions of any milestone are welcome. Theorems 9.7–9.8, about Algorithm IPF diverging on infeasible problems, are not included.
Primal-dual interior-point methods solve a linear program by following the central path from a point with strictly positive primal variables and dual slacks . The classical analysis assumes that the starting point is feasible: it already satisfies the equality constraints and . In practice such a point is rarely available, and the production codes of the early 1990s (OB1, and later the solvers built on Mehrotra's method) instead start from an arbitrary positive point and let the Newton steps reduce the constraint violation together with the duality gap. These infeasible-interior-point methods worked well long before they were understood. Global convergence was first proved by Kojima, Megiddo and Mizuno (Math. Programming 61, 1993), and polynomial complexity of a long-step variant by Zhang (SIAM J. Optim. 4, 1994).
Chapter 6 of Stephen J. Wright's Primal-Dual Interior-Point Methods (SIAM 1997) gives a self-contained account of this theory for one representative long-step method, Algorithm IPF. This mission formalizes the statements of that chapter.
Let (no rank assumption), , , and consider the primal s.t. , and the dual s.t. , . The solution set consists of the triples with , , and for all . For a triple the residuals are and , and the duality measure is . Norms are Euclidean unless marked.
Fix a starting point with , with residuals and duality measure . For and , the neighborhood is
Algorithm IPF has parameters and . At iterate it picks and solves the linear system
where , and . It takes the largest such that the point lies in and there is at most . That point is the next iterate. The analysis uses and the scaling .
A positive sequence converges Q-linearly if for some and all large . It converges R-linearly if it is dominated by a Q-linearly convergent sequence.
If and the start is infeasible, , then along Algorithm IPF
The statement fixes no rate. It asserts only the shape of the convergence, so it survives any improvement of the constants.
Theorem 6.1 is the reason infeasible starts are safe. A practitioner may start from any positive point. If the problem has a solution, the method then removes the infeasibility and the duality gap at a linear rate, without a Phase I. Lemma 6.7 is the core estimate: one uniform lower bound on the step length gives both rates, and its -explicit form (6.38) gives the complexity of Theorem 6.2. Theorems 6.8 and 6.9 show that the iterates identify the optimal partition . This is the basis of the finite-termination procedures of the next chapter.
These results are proved in the literature and in the book. They have not been machine-checked: the Prove2Me corpus contains a formalized convergence theorem for Vanderbei's path-following method under a boundedness hypothesis, but no infeasible-interior-point theory with the neighborhood . The mission would produce the first checked proof of global linear convergence for an infeasible primal-dual method. The definitions it introduces (the algorithm as a predicate on sequences, Q-/R-linear convergence) can be reused for the self-dual and termination chapters.
The obvious argument for a feasible method bounds the second-order term by a multiple of through the orthogonality . With infeasible iterates this orthogonality fails, and the cross terms involve the iterates themselves, which are not bounded a priori. The step from "the residuals shrink" to "the step length stays bounded below" therefore needs a bound on in terms of . That bound has to come from a solution of the linear program. The hypothesis is essential. The page prints Theorem 6.1 without it, but on the infeasible program , , the neighborhood condition keeps bounded away from zero. A solver should also note that the explicit displayed in the proof of Lemma 6.7 drops a factor against the bound (6.47) derived just before it, and can equal . Only the existential statement survives as printed. The bound (6.38) is left to the reader in the book (Exercise 4).
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ. Euclidean norms and the 1-norm are defined explicitly, because Mathlib's default norm on Fin n → ℝ is the sup norm. "Generated by Algorithm IPF" is a predicate on the sequences , , and the directions. The direction is given by its linear equations, not by a closed form, and "the largest " is an IsGreatest hypothesis on the admissible set rather than a constructed maximum. The neighborhood is anchored at the run's own start. Every statement carries the hypotheses the chapter states once and then omits: ; (p. 111); where the proof starts from a solution (pp. 127, 185); and, for Lemma 6.7, a start inside (pp. 109, 120). Constants , , , are positive and quantified before the iteration index. in (6.38) is quantified after the algorithm's parameters and before the dimension and the instance. That is how "independent of " is rendered.
Explicit constants. Lemma 6.6's "a constant independent of " is stated with the value its proof sets, . The book gives no explicit for (6.38), and none is invented. Theorem 6.2 () is not posed, because an explicit iteration count would rest on that unproved exercise.
A trivializing formalization is ruled out. The Q-linear predicate requires and , not only a ratio bound, and R-linear convergence is domination by such a sequence. is explicit, since division by zero would make (6.49) vacuous. No hypothesis beyond the book's is added to make a run easier to exhibit, and the greatest step length is required to exist exactly as the algorithm prescribes.
Beyond the paper. One sharpness probe accompanies the goal: Theorem 6.1 with removed, expected to be false by the counterexample above; a disproof is the sought outcome.
Infrastructure that would help: the identity , orthogonality of and when and , the Goldman–Tucker theorem (strictly complementary solutions exist; Wright, Theorem 2.4), and Hoffman's bound for Theorem 6.9. Contributions of reusable lemmas on Q-/R-linear sequences are welcome.
Primal-dual interior-point methods are the standard polynomial-time algorithms for linear programming and the basis of most commercial LP solvers. Among them, path-following methods are the ones with the cleanest complexity theory: they keep every iterate inside a neighborhood of the central path and shrink the duality measure by a fixed factor per step. Chapter 5 of Stephen J. Wright's Primal-Dual Interior-Point Methods (SIAM 1997) presents three such methods — a short-step method, the Mizuno–Todd–Ye predictor-corrector method, and a long-step method — and analyzes each from a small set of one-step estimates.
The short-step method and its iteration bound go back to Kojima, Mizuno and Yoshise (1989) and Monteiro and Adler (1989); the predictor-corrector method with two nested 2-norm neighborhoods is due to Mizuno, Todd and Ye (Math. Oper. Res. 1993); the long-step method in the wide neighborhood with its bound is in the same line of work. Wright's chapter gives a single, uniform treatment of the three, with explicit constants.
Fix , , , with no assumption on the rank of . The primal problem is subject to , , and the dual is subject to , . A primal-dual point is a triple . The strictly feasible set consists of the triples with , , and (componentwise).
For vectors write , and , so is the vector of pairwise products . The duality measure is . The 2-norm neighborhood of the central path is
and the one-sided -norm neighborhood is , .
Given a centering parameter , a search direction is any solution of the step equations
Along it, and . The vector of products is the second-order term that the linearization ignores.
Let satisfy
If and solves the step equations with this , then
This is a one-step statement with no algorithm loop. It is the invariant of the short-step method (, ).
Theorem 5.6 is the step that turns the linear decrease of (Lemma 5.1) into a convergence proof: once the full step is known to stay in , the duality measure falls by the factor at every iteration, and the generic complexity theorem of Chapter 3 gives the iteration bound, the standard bound for primal-dual interior-point methods. Lemmas 5.7 and 5.8 give the same bound for the adaptive predictor-corrector method, and Lemma 5.10 with Theorem 5.11 the bound for the long-step method, which is the variant closest to practical codes.
On the platform, the Mizuno–Todd–Ye predictor-corrector analysis has been formalized in a different parametrization (pairs with an existential dual multiplier, and a different step bound); the results of this chapter in Wright's triple form, the general Lemma 5.3, the short-step invariant and the long-step reduction are not yet formalized. A machine-checked version yields reusable infrastructure: the step equations, the two neighborhoods and the pairwise-product bounds are used by every later chapter of the book (infeasible methods, superlinear convergence, finite termination).
The step equations are linear, but neighborhood membership is not: the products are quadratic in , and the quadratic coefficient is not controlled by the equations individually — only the sum vanishes. A bound on in terms of alone, uniformly over the neighborhood, is the crux; a naive bound through the norms of and separately involves the conditioning of and is not uniform. The second subtlety is strict positivity: the proximity inequality at every does not by itself rule out a coordinate of or changing sign, and the conclusion of Theorem 5.6 requires , for the whole segment.
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, points are triples (x, lam, s). The norm is the explicit Euclidean norm (Mathlib's default norm on Fin n → ℝ is the sup norm). and are subsets of , so membership includes both equality constraints and strict positivity. The direction is defined by its linear equations, never by a closed-form solution, so no rank assumption and no nonsingularity are presupposed. Where the page leaves the ranges implicit, the standing ones are hypotheses: for , for , for the step equations. In Lemmas 5.1 and 5.5, ranges over all reals, as the page places no restriction on it.
Explicit constants: the book's "there is a constant independent of " in Theorem 5.11 is replaced by the its proof derives (p. 100); every other constant is printed in the statements. In (5.19), the case is read as ; real division by zero, which would make and Lemma 5.7 trivial on the interval , is excluded by an explicit case split. "The largest " in Algorithms PC and LPF is a hypothesis (IsGreatest) on the chosen step, never a construction. A trivializing formalization — one that states only the proximity inequality without strict feasibility — is ruled out by the definition of .
Beyond the paper: one variant is posed beside the faithful goal. theorem_5_6_strong (strengthened, finding F1) is Theorem 5.6 for every real : condition (5.15) already forces when , and the bound is not used by the argument.
Needed infrastructure: finite sums and the Euclidean norm on Fin n → ℝ, Matrix.mulVec and dot products, real powers. Proofs of Lemma 5.3 and of the positivity argument along the segment are reusable well beyond this mission; contributions of either are welcome.