Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The value of a maximal flow is the basic output of network-flow models of transport, communication and supply systems. A planner who can enlarge the capacity of a link wants to know what the enlargement buys. For a single link the answer is simple. For two links it is a question about interaction: does enlarging one make enlarging the other more valuable (the links reinforce each other) or less valuable (they interfere)? L. S. Shapley answered it, and Ford and Fulkerson give his theorems and proofs in Section 13 of Chapter I of Flows in Networks. Any two arcs either always reinforce or always interfere, and in several positions the network's geometry alone decides which. These are early instances of supermodularity and submodularity of an optimal value in its parameters, a theme that later became central in parametric optimization and discrete convex analysis.
A network is a finite set of nodes together with a set of ordered pairs of distinct nodes, the arcs. The arc has initial node and terminal node . There is at most one arc from to , but and may both be arcs. The nodes are split into a set of sources, a disjoint set of sinks, and the remaining intermediate nodes . Each arc carries a capacity .
A flow from to is a function on the arcs with on every arc, and with conservation at every intermediate node . Here is the total flow on arcs leaving and the total on arcs entering it. Its value is the net amount leaving the sources, . The maximal flow value is the largest value of a flow. A node set containing every source and no sink determines the cut , the set of arcs from to its complement, with capacity , the sum of their capacities.
Fix two distinct arcs and and keep every other capacity fixed and finite. Write for the maximal flow value when is replaced by , and for the value when and are replaced by and . These two capacities may also be , and then may be . For a rectangle with corners , , , in the nonnegative quadrant, with , the difference quotient is
The interaction constant is
which may be , or indeterminate ().
The goal leaves the sign open. Which sign occurs depends on the whole network: in the book's Fig. 13.3, removing a third arc turns into .
Corollary 13.2 refines the goal by naming the sign. Theorem 13.3 and Corollary 13.4 fix the sign from positions alone.
Theorem 13.1 says that the cross effect of two capacities on the maximal flow value never changes sign. The marginal value of capacity on one arc is monotone in the capacity of the other, in a direction fixed once and for all by the network. Corollary 13.2 reduces that direction to a single number computed from four maximal-flow values at the corners and . Theorem 13.3 and Corollary 13.4 show that some directions are forced by position: arcs in series reinforce, and arcs that compete at a common node interfere. These facts underlie sensitivity analysis of maximal flows. They are also the two-parameter case of the lattice and submodularity structure of minimal cuts.
The theorems were proved by Shapley and printed with proofs by Ford and Fulkerson (RAND, 1962). Their proofs argue from a picture of how the regions of linearity of can sit in the quadrant (Fig. 13.2). No machine-checked proof of any statement of Section 13 exists on Prove2Me. Proved max-flow min-cut statements exist there for a single source and sink and in other conventions, and are related to milestone 1 rather than identical to it. Formalizing the section gives a checked account of the parametric behaviour of the maximal flow value. That includes the infinite capacities the section allows, and the indeterminate case of , which a picture handles only informally.
The first idea is to read the sign off formula (13.4): is the minimum of four affine functions, so its mixed second difference is determined by which pieces are active at the four corners of a rectangle. A minimum of four arbitrary affine functions, however, can have mixed differences of both signs. The claim depends on constraints that the four corner values satisfy because they come from one network, and on how the regions of linearity can meet. The book's proof uses a case analysis of these configurations: at most one diagonal boundary segment, and its slope fixed by . Making that analysis rigorous, including the degenerate configurations where regions are empty or corner values are infinite, is the core of the goal and of Corollary 13.2.
Milestone 1 also has to be established in the several-source form, with arcs allowed to enter sources and to leave sinks, where the reduction to a single source and sink must respect flows whose sources have net inflow.
Nodes form a finite type with decidable equality; arcs are a finite set of ordered pairs without loops; sources and sinks are disjoint finite sets, either of which may be empty (then and every statement holds trivially, as in the book). Capacities of the fixed arcs are finite nonnegative reals. The two varied capacities and every maximal flow value lie in (ℝ≥0∞). A flow is a real function vanishing off the arcs, and the maximal flow value is the supremum of flow values in . That supremum is taken over a nonempty set (the zero flow), so it is never a default value, and it is exactly when flow values are unbounded. The maximal flow value is not defined as a minimum cut capacity; equality with the minimum cut is milestone 1.
The difference quotient is taken at finite real arguments over every rectangle with and ; and may be negative. The book prints the third term of (13.12) as . The rectangle the theorem names needs , which is the formalized quotient; with the printed term the claim already fails for two arcs in series. The constant is a four-way value (indeterminate, , , real), so is never silently assigned a number.
"Of one sign" is formalized as one sign for all rectangles at once. The rectangle-by-rectangle reading, under which every real number is trivially or , is ruled out.
A complete development needs flows with several sources and sinks, cuts, and the max-flow min-cut theorem in that form; the definitions here are self-contained and reusable for any parametric max-flow statement. Contributions of the general piecewise-linear structure of in one or two capacities are welcome.
The maximal flow problem asks how much of a commodity can be sent from one node of a network to another when every arc has a capacity. It was posed in the 1950s in the study of rail networks, and its answer, the max flow min cut theorem of L. R. Ford, Jr. and D. R. Fulkerson, became the organizing result of combinatorial optimization: the bottleneck of a network, a cheapest set of arcs separating the two terminals, has exactly the capacity of the best flow. Chapter I of Ford and Fulkerson's Flows in Networks is the canonical exposition. This mission formalizes Chapter I, §§1–9, in the RAND typescript of the book (Report R-375-PR, 1962), whose numbering is used throughout.
Timeline. Ford and Fulkerson proved the theorem in 1956 for undirected networks in an arc–chain formulation ("Maximal flow through a network", Canadian J. Math.); Elias, Feinstein and Shannon gave an independent proof the same year (IRE Trans. Inf. Theory). The book restates the theory for directed networks with node–arc flows, which is the form used in all later applications and the form formalized here.
A network is a finite set of nodes together with a set of ordered pairs of distinct nodes, the arcs. At most one arc leads from to , but both and may be arcs. Each arc has a capacity , a real number. For node sets , is the set of arcs from to , and is the sum of a function over those arcs; .
Fix two distinct nodes, the source and the sink . A flow of value from to is a function on the arcs with such that the net flow out of every node, , is at , at , and elsewhere. A flow is maximal if no flow has larger value. A node set with , determines the cut separating and , of capacity ; a minimal cut has least capacity.
A flow augmenting path with respect to is a sequence of distinct nodes from to in which each consecutive pair is joined either by a forward arc with or by a reverse arc with . The source set of a flow is the smallest node set containing and closed under such steps; the sink set is the smallest node set containing and closed under such steps taken backwards. With lower bounds , , the bounds are replaced by .
with both extrema attained. The goal fixes nothing beyond the book's hypotheses: any finite network, any nonnegative real capacities.
The result itself. The theorem converts an optimization over a continuum of flows into a finite minimum over node sets, and the integrity theorem makes the conversion combinatorial. The later chapters of the book derive from these two results the supply–demand and circulation theorems, the König–Egerváry theorem, Menger's theorem, Dilworth's theorem and Hall's theorem on distinct representatives. Corollary 5.2 is the correctness criterion of every augmenting-path algorithm, and Corollaries 5.3–5.4 and Theorems 5.5–5.6 describe the lattice of minimal cuts that later work on parametric flows and cut enumeration uses.
Formalizing it. The theorem is proved, and several machine-checked versions exist on this platform in other conventions: FordFulkerson56.MinCut.minimal_cut_theorem (the 1956 undirected arc–chain form), AppliedComb.Flows.max_flow_min_cut and AppliedComb.Flows.integral_max_flow (networks without 2-cycles and without arcs into the source or out of the sink), LinearOptimization.max_flow_min_cut (positive extended-real capacities, parallel arcs), VanderbeiLP.Networks.max_flow_min_cut (value measured on a return arc), and the augmenting-path criteria GoldbergTarjan.Generic.max_flow_iff_no_augmenting_path and EdmondsKarp.ShortestPath.isMaxFlow_iff_no_augPath. None states the book's node–arc theorem for directed networks in which antiparallel arcs, arcs into the source and zero capacities are all allowed. This mission states it in exactly the book's conventions, together with the minimal-cut structure theory of §5 and the lower-bound form of §9, which have no platform counterpart.
The inequality "max flow min cut" holds for every pair of a flow and a cut and is routine. The difficulty is the reverse inequality together with attainment: the theorem asserts that a maximal flow exists, and this is not free over the reals. The labeling method of §8 need not terminate when capacities are irrational: the book gives a network in §8 where it converges to a flow of value one quarter of the maximum. So an argument that only runs the algorithm covers rational or integral data and leaves the general statement open. Theorems 5.5 and 5.6 add reasoning about inductively defined node sets and about arc sets rather than node sets: two different node sets can determine the same cut, which is why Theorem 5.6 compares arc sets and needs .
Nodes are a Fintype with decidable equality; arcs a Finset (N × N) with no loops; capacities and flows functions , flows required to vanish off and to be nonnegative on it. Capacities are finite reals throughout. The source and sink are distinct (), the book's "two distinguished nodes". A cut is given by its node set ; where the book compares cuts (Theorem 5.6) the Lean compares the arc sets . Every maximum and minimum is stated as attained (IsGreatest, IsLeast) or through explicit "maximal flow" and "minimal cut" predicates; no sSup or sInf appears. The source and sink sets are defined as intersections of all node sets closed under the book's rules (a), (b) and (a′), (b′), not through a reachability algorithm.
The statement admits a trivializing formalization that is ruled out here: defining the maximal flow value as the minimal cut capacity, or minimal cuts through flow values, or replacing by ; flows, cuts, maximality and minimality are each defined from the network alone.
Beyond the paper. Two variant items accompany the faithful statements. A strengthening of Corollary 5.3: one flow, not assumed maximal, that saturates and is zero on already makes the cut minimal and the flow maximal, since by Lemma 4.1 its value equals the cut capacity. A sharpness probe for Theorem 5.6: the statement with weakened to , which the book's Fig. 5.2 shows to be false (two arcs, capacities 1 and 0, give two minimal cuts while the source-set and sink-set cuts coincide); a disproof is the sought outcome.
A complete development needs finite sums over arc sets and their splitting along (the identities (3.3)–(3.4)), compactness of the flow polytope or an augmenting-path argument, and an inductive closure argument for the source set. The network, flow and cut definitions are reusable by the rest of this series (circulations, dynamic flows, flow functions) and by any formalization of matching or connectivity theorems through flows. Proofs by either route, compactness or the labeling method with integrality, are welcome.
Many questions in operations research and combinatorics ask whether a system of linear inequalities on a network has a solution: can the demands at a set of warehouses be met from the supplies at a set of factories through roads of limited capacity; is there a nonnegative matrix with bounded entries whose row and column sums lie between given limits; can a periodic schedule be met when every activity has a minimum and a maximum rate. Chapter II of L. R. Ford, Jr. and D. R. Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962, doi:10.1515/9781400875184) answers these questions by feasibility theorems: a system of flow constraints has a solution exactly when a family of inequalities, one for each set of nodes, holds.
The history in the chapter's first three sections is short. D. Gale proved the supply-demand theorem in 1957 (A theorem on flows in networks, Pacific J. Math. 7 (1957) 1073–1082). A. J. Hoffman proved the circulation theorem, with lower and upper bounds on every arc, in 1960 (Some recent applications of the theory of linear inequalities to extremal combinatorial analysis, Proc. Sympos. Appl. Math. 10, AMS, 1960), originally through the separation theorem for convex sets. Ford and Fulkerson derive all of these, and the two-sided variants, from the max flow min cut theorem of their Chapter I.
A network is a finite set of nodes together with a set of ordered pairs of distinct nodes, the arcs; there is at most one arc from to , but both and may be arcs. Each arc carries a real capacity . For a real function on the arcs and node sets ,
so is the total of on arcs leaving and the total on arcs entering . For a node set , ; for a node function , .
In §§1–2 the nodes are partitioned into sources , intermediate nodes and sinks (any of them may be empty). Sources carry a supply , sinks a demand . A function on the arcs is a feasible flow for the supply-demand problem when the net outflow is at most at every source, zero at every intermediate node, the net inflow is at least at every sink, and on every arc.
In §3 there are no distinguished nodes. A lower bound function with is given on the arcs, and a feasible circulation is a function on the arcs with
For a network with capacities and lower bounds , a feasible circulation exists if and only if
With this is the goal.
The circulation theorem is the most general of the chapter's feasibility criteria for directed networks: the supply-demand theorem, the existence of – flows between lower and upper arc bounds (Chapter I, §9), and the transportation-matrix criterion of Corollary 2.3 all follow from it or from its extension, Theorem 3.2, by adjoining arcs, and the rest of Chapter II applies them to systems of distinct representatives and (0, 1)-matrices.
All results of the mission have been proved for more than sixty years. None of them, in this form, is formalized on Prove2Me: the platform has decomposition results for circulations and max flow min cut statements in other conventions, but no Gale or Hoffman feasibility criterion. The mission produces machine-checked versions of the six numbered results and the goal over one shared notion of network, in the book's notation.
Necessity is the routine half of every theorem. Sufficiency asks for a flow built from a family of inequalities, one per node set, and constructing a flow arc by arc or node by node with local repairs gives no argument that the repairs stop or that all constraints hold at once. The statements also differ in ways that are easy to get wrong: §§1–2 bound the net outflow at sources but the net inflow at sinks, §3 bounds the net inflow everywhere, the node bounds of Theorem 3.2 carry no sign condition and may be negative, and Theorem 2.1 needs two inequalities per node set rather than one. Real-valued data rule out any argument by induction on integer flow values without a separate limiting step.
Nodes form a Fintype with decidable equality; arcs are a Finset (N × N) with no loops; capacities and flows are real functions . A flow is required to vanish off , and every sum runs over arcs only, so the values of and off never matter. Supplies, demands and node bounds are real functions on all of whose values enter only through sums over the sets the book names (, , …). The partition is three pairwise disjoint Finsets covering . ranges over all subsets of , including and . Each section's sign convention is copied: §§1–2 bound the net outflow at sources and the net inflow at sinks, §3 bounds the net inflow. Corollary 2.3 is stated for real matrices indexed by Fin m × Fin n. All data are finite reals; no integrality is assumed.
Feasibility is always stated as the existence of a function on the arcs satisfying the book's displayed constraints. Defining feasibility through the cut condition itself, or through a linear-programming solver predicate, would make every theorem definitional and is ruled out.
Beyond the paper. One variant is posed beside the faithful goal: [Strengthened] Theorem 3.1, the circulation theorem for any real lower bound without (capacities stay nonnegative). The substitution reduces it to a supply-demand problem with nonnegative capacities , whose Gale condition is regardless of the sign of ; it implies the faithful statement.
A complete development needs Chapter I's max flow min cut theorem in some form (or the linear-programming duality theorem, or Farkas' lemma), the manipulation of arc sums over node sets, and the auxiliary-network constructions. The definitions of networks, arc sums and partitions are reusable by the later Chapter II missions. Proofs of any milestone, of the variant, and alternative proofs through LP duality are welcome.
A convex program whose objective and feasible set are known only through oracles, routines that answer queries about one point at a time, can still be solved to any prescribed accuracy with a number of queries bounded in advance. The ellipsoid method is the classical algorithm that achieves this. It was introduced for convex minimization by Yudin and Nemirovski (Ekonomika i Matematicheskie Metody, 1976) and by Shor (Cybernetics, 1977), and it became widely known when Khachiyan used it to prove that linear programming is solvable in polynomial time (Soviet Math. Dokl., 1979). Grötschel, Lovász and Schrijver turned the method into a general tool of combinatorial optimization, the equivalence of separation and optimization (Springer, 1988).
Ben-Tal and Nemirovski's Lectures on Modern Convex Optimization (SIAM 2001) present the method in §5.2 as the engine of their theorem that convex programs are polynomially solvable, and prove an explicit, fully quantified complexity bound for it, Theorem 5.2.1. This mission is the tenth of a series formalizing the book's main results and covers §5.2 (pp. 342–352).
Vectors are elements of , , with the Euclidean norm . The problem is
where is convex and is a closed, bounded, convex set with nonempty interior. Two radii are known in advance (assumption A): lies in the ball and contains some ball , whose centre is not known.
The data are accessed through two oracles. A separation oracle for answers a query by "" when that holds, and otherwise returns a vector with for all . A first order oracle for returns and a subgradient of at : for all .
An ellipsoid is with . For , put and
The ellipsoid method with accuracy starts from , , . At step it queries the separation oracle at . If a separator is returned, the step is nonproductive, and . Otherwise the step is productive: the first order oracle is queried at ; a zero subgradient stops the method with result ; a nonzero one becomes , and . Then , (computed from ), , and the method stops if
returning the productive search point , , with the smallest value of . Finally .
For every accuracy , every separation oracle for and every first order oracle for , the ellipsoid method terminates after no more than
steps, and its result satisfies
Theorem 5.2.1 bounds the number of oracle calls by a quantity that depends only on the dimension, on and on : the cost of each additional digit of accuracy is steps, whatever the instance. Each step costs one call of each oracle and arithmetic operations. This is the ingredient the book's Theorem 5.3.1 combines with polynomial computability to conclude that convex programs are polynomially solvable, and it is the reason semidefinite and conic quadratic programs, the subject of the earlier lectures, are tractable in theory. The bound is also explicit enough to be checked numerically, with no hidden constants.
On the formal side, the platform has machine-checked versions of related results in other forms: Bertsimas and Tsitsiklis's half-ellipsoid lemma with the weaker ratio and polyhedral feasibility version, Bubeck's version for objectives bounded on with a convergence-rate conclusion, and Shor's localization theorem. None of these is the book's method: its guesses , its stopping rule (5.2.17), the explicit step count (5.2.18), or the exact volume identity (5.2.14). A formal proof of Theorem 5.2.1 gives a machine-checked oracle complexity bound with a stopping rule computable from the run alone.
The book's description of the method runs to two pages; the central difficulty is the termination analysis, not the geometry. The volume of the ellipsoids decreases geometrically, but their diameters need not, so the search points need not converge, and the method cannot know how close it is to the optimum. A naive argument that the search points approach the optimum therefore fails, and the stopping test (5.2.17), which only sees , and the guesses , has to be related to the unknown optimality gap. The analysis must also cover runs in which no step was productive for a long time, and the possibility that the result is undefined. On the geometric side, (∗) requires the exact determinant of a rank-one update and the elementary but not immediate inequality . Reasoning about a recursively defined algorithm also means carrying invariants (the ellipsoid contains every point of not yet cut off, ) through the induction.
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and the Euclidean norm eucNorm x = √(x ⬝ᵥ x) is defined explicitly (Mathlib's norm on Fin n → ℝ is the sup norm). Volumes are MeasureTheory.volume on Fin n → ℝ, valued in ℝ≥0∞. The setting (5.2.9) with assumption A is the predicate IsBlackBoxProgram f X r R. The oracles are arbitrary functions of the query point satisfying (5.2.10) and (5.2.11); every theorem is quantified over all of them, and none sees the centre . The method is a function run from the number of steps performed to an outcome, running with the current and best productive point, or stopped with an optional result; TerminatesAt t res says the run stops exactly at step . and are reals given by IsGreatest/IsLeast, and is expressed by comparison with every point of , so no supremum or infimum with a default value occurs. Ceil is Int.ceil and the step bound is compared in . A statement about an arbitrary sequence of ellipsoids or an arbitrary "state" carrying no link to the run would trivialize the goal; here the ellipsoids, guesses and result are those the method constructs from the oracles' answers.
Beyond the paper. The book's statement (∗) also has a case , whose printed centre moves by regardless of the segment's length; the containment fails for , , . The case is posed as printed (expected to be disproved) and as a corrected variant with centre . Theorem 5.2.1 assumes and is unaffected.
A complete development needs the determinant of a rank-one update (Matrix.det_add_replicateCol_mul_replicateRow), Lebesgue measure of linear images (MeasureTheory.Measure.addHaar_image_linearMap), the continuity of convex functions on , and an induction over run. The ellipsoid update lemma and the oracle and method definitions are reusable for other cutting-plane methods. Proofs of individual milestones, in particular (∗), are welcome as separate contributions.
Semidefinite programming (SDP), the optimization of a linear function over the intersection of an affine subspace with the cone of positive semidefinite matrices, is the workhorse behind relaxations in combinatorial optimization, robust optimization and control. Its practical and theoretical tractability rests on interior point methods: algorithms that follow the central path, a curve of strictly feasible primal-dual pairs parametrized by a penalty parameter , along which the duality gap equals . The polynomial-time analysis of these methods, due to Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994) and, for the primal-dual SDP family considered here, to Monteiro and Zhang and others in the 1990s, reduces to one local statement: a single Newton-type update, started close to the path, lands close to the path again while the penalty parameter grows by a factor .
This mission formalizes that local statement in the form given by Ben-Tal and Nemirovski, Lectures on Modern Convex Optimization (SIAM 2001), Lecture 6, Theorem 6.5.2, for the whole family of primal-dual updates obtained from commutative scalings.
Let and let be the space of real symmetric matrices with the Frobenius inner product and norm . For , is its positive semidefinite square root. Fix a linear subspace , its orthogonal complement in , and . The primal-dual pair is
is strictly primal feasible if and ; is strictly dual feasible if and . For such a pair the duality gap is .
The distance of a pair to the point of the central path with parameter is
and the neighbourhood consists of the triples with , strictly feasible and distance at most .
The updating (U), with parameters , takes a strictly feasible pair and
The choices , and the Nesterov–Todd scaling are all admissible in step 2.
If and the strictly feasible pair satisfies , then for every admissible the system of step 3 has exactly one solution, and
The proof reduces to the case with , and , and the milestones are the numbered facts of that reduced situation, with and :
Theorem 6.5.2 is the step that turns the central path into an algorithm: once a pair in is known, iterating (U) keeps every iterate in and increases the penalty parameter by a constant factor every steps, so the duality gap (Proposition 6.4.2) falls below after steps. The statement covers a whole family of search directions at once, including the Nesterov–Todd direction used by SDP solvers, and by Remark 6.5.2 it specializes to LP when all matrices are diagonal.
The result is classical and proved in the book; it has not been machine-checked. The platform has formalizations of central-path facts for LP and for inequality-form barrier problems, and open items on self-scaled short-step methods, but no statement about primal-dual Newton steps for SDP. A formal proof would supply reusable matrix-analysis infrastructure: Frobenius estimates through eigenvalues, the Löwner order under congruence, and unique solvability of Sylvester-type systems with subspace constraints.
The obvious approach, perturbation analysis of the Newton system in the original variables, does not close: the bound has to hold uniformly in the condition of and , and only the scaled quantities , are controlled by and . The reduction to with diagonal commuting has to be justified, including invariance of the distance under scaling and the change of the subspaces , to , . Uniqueness uses the orthogonality in an essential way. The final estimate passes from the scaled distance to the distance measured at the new point , which needs the Löwner bound and monotonicity of the trace under congruence. The concluding numerical inequality holds for every , not only asymptotically.
All matrices are Matrix (Fin k) (Fin k) ℝ with . is a Submodule ℝ of matrices with every element symmetric, and is the set of symmetric with for all , so the unknowns of the linear systems are symmetric. is Mathlib's CFC.sqrt (with open scoped MatrixOrder), positive (semi)definiteness is Matrix.PosDef/Matrix.PosSemidef, and the Frobenius norm is defined explicitly. The book's (P) comes from a conic problem under Assumption A ( injective) with ; every subspace is such an image, so the formal statements quantify over subspaces. The distance to the central path is defined by its SDP closed form (6.4.11), so no existence result for the central path is needed. The goal is stated for every admissible scaling , and "the system has a unique solution" is a separate conjunct from the properties of that solution, so the goal cannot hold vacuously through an unsolvable system. The milestones of the proof are stated in the book's reduced situation (diagonal , , ) with all of its hypotheses.
Results of §§6.3–6.4 for general canonical cones (products of semidefinite and Lorentz cones with their barriers and ), namely Propositions 6.3.1–6.3.2 and Theorems 6.4.1–6.4.2, and Theorem 6.5.1 (primal path-following), are not part of this mission: they need a calculus of canonical barriers on block-structured spaces. Proofs of any milestone, reusable lemmas on the Löwner order and the matrix square root, and a sorry-free proof of the numerical inequality are welcome.
Many questions in robust control and robust optimization reduce to one test: does a whole family of symmetric matrices, generated by perturbing a nominal matrix along several directions at once, stay positive semidefinite? A linear system whose coefficients are only known to lie in intervals is a typical case. Showing that one quadratic Lyapunov function certifies stability of every member of such an interval matrix comes down to exactly this test. Ben-Tal and Nemirovski isolate it as the Matrix Cube problem. The problem is NP-hard (Ben-Tal & Nemirovski, On tractable approximations of uncertain linear matrix inequalities affected by interval uncertainty, SIAM J. Optim. 12 (2002)). They prove that a simple semidefinite sufficient condition is never far from exact. The gap is controlled by a universal factor that depends only on the ranks of the perturbation directions.
This mission formalizes that result as it appears in §4.4.3 of Lectures on Modern Convex Optimization (Ben-Tal & Nemirovski, SIAM 2001), pp. 189–197, together with the lemmas its proof uses and its application to interval Lyapunov stability.
Matrices are real. is the space of symmetric matrices, its positive semidefinite cone, and means . For , is its vector of eigenvalues, so is the sum of their absolute values.
Fix with . For a level the matrix cube is
the image of the cube under an affine map. The Matrix Cube problem asks for the largest with .
The system of LMIs in symmetric variables is
Its feasibility can be checked by semidefinite programming. The largest for which it is solvable is , the optimal value of the semidefinite problem (4.4.45).
The approximation factor is the function
where is the standard Gaussian density on . The relevant rank is ; is not included.
For the application, is a stable matrix (all eigenvalues in the open left half-plane). has nonnegative entries, and is the interval matrix. asks for with for all , and is the supremum of the for which it is solvable. is the analogue of for this cube. It uses matrix variables and for , and is its supremum.
For all , all , all and all :
and
The result. Proposition 4.4.5 and Theorem 4.4.1 together bound the cube radius. It lies between the efficiently computable and . The factor is in general, independent of and , and exactly when every perturbation has rank at most two. Rank two is the situation of interval matrices, of Lyapunov certificates for interval systems (Proposition 4.4.6), and of a re-derivation of Nesterov's theorem for quadratic maximization over the unit cube (pp. 200–201). The same estimate underlies tractable approximations of robust LMIs with box uncertainty in robust semidefinite optimization.
Formalizing it. The results are proved in the book. None of them, and nothing on the matrix cube, the function or interval Lyapunov stability, is machine-checked on the platform. The formalization adds three things: a checked definition of as a Gaussian integral; a checked proof of the constants and ; and a checked bridge from semidefinite duality to a probabilistic rounding argument. The proof of Proposition 4.4.5 already has a sorry-free local check, which also exposed a sign slip in the printed proof.
The sufficient direction is elementary. The converse is not. Unsolvability of is a statement about a semidefinite program, and turning it into an explicit point with and needs three ingredients:
Bounding coordinate by coordinate, or using a worst-case vertex of the cube, gives a factor that grows with . The rank-dependent constant is what makes the theorem useful.
The constants need real analysis on Gaussian integrals. requires an exact minimization of over . The bound requires a symmetrization and an independence argument. Lemma 4.4.4 needs rotational invariance of the Gaussian measure and diagonalization inside an integral.
Matrix (Fin n) (Fin n) ℝ, and is (X - Y).PosSemidef (which includes symmetry). The index is Fin m, and is for every .CFC.sqrt W under MatrixOrder. Eigenvalues are Mathlib's IsHermitian.eigenvalues, used only through order-independent quantities.EReal, so is represented. Ratios are stated in product form, for example . The "max" in (4.4.45) is stated as attained.A formalization that replaced by an arbitrary function satisfying (4.4.37), or set , or allowed , would state a different (false or ill-posed) theorem; the statements here rule these out.
Infrastructure needed and reusable beyond this mission:
Contributions of separate lemmas are welcome, for example monotonicity of or .
A homogeneous quadratic inequality may hold at every point where other quadratic inequalities hold. Deciding when this happens is the quadratic analogue of the question the Farkas lemma answers for linear inequalities. It is the core of robust optimization with ellipsoidal uncertainty, of absolute stability in control (where it is known as the S-procedure), and of trust-region and quadratically constrained programming. The answer one wants is a linear certificate: nonnegative multipliers with , a condition that can be checked by semidefinite programming.
Lecture 4 of Ben-Tal and Nemirovski, Lectures on Modern Convex Optimization (SIAM, 2001, doi:10.1137/1.9780898718829), states the classical case and, in its exercises (§4.10.5), traces how far it extends:
Vectors are and matrices are real . For a symmetric matrix , the quadratic form is . means that is positive semidefinite, and means is positive definite. A quadratic inequality is a consequence of a system , if it holds at every satisfying the system. The system is strictly feasible if some satisfies both inequalities strictly.
The inhomogeneous case uses and . For the topological steps, is the unit sphere of . The projective space is with each identified with , and is the canonical projection.
Let and let be symmetric matrices such that (i) some linear combination is positive definite and (ii) , for some . Then
The S-lemma converts a semi-infinite family of quadratic implications into one linear matrix inequality. This is what makes robust counterparts of conic quadratic constraints with ellipsoidal uncertainty semidefinite-representable (Proposition 4.5.1 of the book), and it gives trust-region subproblems and quadratic programs with one constraint their exact semidefinite duals. The two-constraint version extends this exactness to problems with two quadratic constraints in dimension at least three. Polyak's convexity theorem is the structural fact behind it, and it is of independent use in the study of joint numerical ranges.
All statements are proved in the literature. On Prove2Me, the inhomogeneous S-procedure in another sign convention is proved (ConvexOptimization.s_procedure), as is the finite Helly theorem (FamousTheorems.helly_theorem). The homogeneous S-lemma is a special case of the former but is not stated on the platform. The infinite Helly theorem with the boundedness condition, Polyak's theorem, the projective-space connectedness facts and the two-constraint S-lemma have no machine-checked statement or proof there. Two statements beyond the book are posed alongside it (see Formalization scope).
The "if" directions are one line each. Every "only if" direction must produce multipliers from a pointwise implication, and there is no Farkas lemma for quadratic inequalities to do it. With two constraints a direct separation argument needs the joint range of three quadratic forms to be convex. That range is not convex in general, and it can fail to be convex for , so any argument has to use the dimension. The book's milestones for this step are topological: paths on spheres, quotients by the antipodal map, and connectedness in projective space. None of this is packaged for this use in Mathlib. Two printed details mislead a solver who follows the page. The matrix in Proposition 4.10.1 omits in its northwestern entry. The hint for (SL.C) (Exercise 4.48) asks for a positive definite combination , where only semidefiniteness can be obtained. The proof of Theorem 4.3.3 also swaps the roles of and at one step.
Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The form is x ⬝ᵥ (A *ᵥ x) and symmetry is Matrix.IsHermitian. and are Mathlib's Matrix.PosSemidef and Matrix.PosDef, both of which include symmetry. The bordered matrix of Proposition 4.10.1 is indexed by Unit ⊕ Fin n with the scalar entry first, as printed. For Propositions 4.10.2 and 4.10.4, the sphere is Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1. is its quotient by with the quotient topology (one definition item), which has the same topology as the book's metric . The book's linear connectedness, which allows the empty set, is stated pairwise. Every hypothesis of the page is an explicit binder. In particular, strict feasibility appears in every S-lemma variant, appears in (SL.C), (SL.D) and Proposition 4.10.4, and the positive definite combination in (SL.C) involves all three of with coefficients of any sign. The implication is quantified over all of and the multipliers carry their sign constraints. Dropping (ii), or leaving unconstrained, turns the goal into a statement that is false or trivial, and neither is the book's.
Beyond the paper. Two variants are posed beside the faithful items. One is a corrected Proposition 4.10.1 with northwestern entry : as printed, the matrix criterion fails for , , . The other is a sharpness probe of (SL.C) without , for which , , is a counterexample; its disproof is the sought outcome.
Contributions welcome: the joint range of quadratic forms (Dines's theorem, Polyak's theorem), the projective space as a topological space, and infinite Helly-type intersection theorems. All are reusable beyond this chapter.
Truss topology design asks for the stiffest elastic bar construction that can be built from a given set of potential bars with a given amount of material. It is one of the oldest test cases of structural optimization (Bendsøe and Sigmund, Topology Optimization, Springer 2003) and one of the main applications in Ben-Tal and Nemirovski's Lectures on Modern Convex Optimization (SIAM 2001). The quantity being minimized, the compliance of the truss under a load, is defined through the solution of a linear system and takes the value when the structure cannot carry the load, so it is not obviously a convex function, let alone one a solver can handle. Lecture 1 of the book shows that the single-load problem happens to become a linear program. Section 3.4.3 explains why: the compliance, as a function of the bar volumes and of the load jointly, is conic quadratic representable, and its epigraph has an explicit description by second-order cone constraints. That description is what turns multiload designs, bounds on bar volumes and other variants into conic quadratic programs.
This mission is the fourth of a series formalizing the book's main results, and covers Lecture 3, §3.4.3 (pp. 120–128), together with Proposition 2.4.2 of Lecture 2, on which it relies.
A ground structure consists of real matrices , (for a classical truss and is the direction vector of bar ). A truss is a vector with (the bar volumes) and a load is . The bar-stiffness matrix is
and the compliance is
with when the equilibrium equation has no solution; the value does not depend on which solution is used. For that are not nonnegative the compliance is extended by . The potential energy of the loaded truss is .
The ice cream cone is . A set is conic quadratic representable (CQr) if there are finitely many inequalities , affine in and in additional variables , such that exactly when some satisfies all of them; a function with values in is CQr when its epigraph is. A linear vector inequality is almost solvable if for every some with makes solvable.
For all , and , (extended compliance) if and only if there are vectors with
where and for . In particular, is CQr.
The proposition gives an explicit second-order cone description of the epigraph of the compliance, jointly in the design and the load . Consequences: single-load, multiload and volume-constrained truss design problems become conic quadratic programs solvable by interior-point methods; the compliance is a convex function of ; and the proposition contains a second variational principle (the reaction forces minimize the stored energy subject to equilibrium, p. 128). It also explains the linear-programming formulation of Lecture 1.
The results are classical and proved in the book; none of them is machine-checked. A formalization adds checked statements of the variational principle for positive semidefinite quadratic forms, the conic theorem of the alternative for almost solvability, and a first instance of conic quadratic representability on the platform, with the convention made explicit.
The compliance is defined through solvability of a singular linear system, so neither convexity nor any representation is visible from the definition. The equivalence in the goal must handle trusses with missing bars (), where is singular and the convention matters, and loads outside the range of , where the compliance is infinite. The book's route goes through a conic theorem of the alternative, which in the conic case characterizes only almost solvability, not solvability; passing from the strict epigraph to the non-strict one in the goal requires a separate attainment argument. A step-by-step translation must keep track of the perturbations of the right-hand side.
Vectors are functions on finite index types (Fin m → ℝ, Fin n → ℝ, Fin (k i) → ℝ); the stacked inequality of (3.4.49) is indexed by the pairs , , followed by two extra coordinates, the last of which is the distinguished coordinate of . The compliance takes values in EReal: ⊤ exactly when is unsolvable, and otherwise the real number ; it only ever appears in comparisons with a real . The convention , is encoded by requiring whenever together with Lean's real division; Lean's alone would let a missing bar carry any force, and this trivializing reading is ruled out. The CQr conclusion is not "some representation exists" in an unconstrained sense: it is a finite system of Lorentz-cone constraints , , affine in the variables, exactly as on p. 86. Proposition 2.4.2 carries the book's standing assumptions: a pointed closed convex cone with nonempty interior, and Assumption A (full column rank of , p. 53, in force by Remark 2.4.1).
Beyond the paper. One variant is posed: a strengthened Proposition 2.4.2 without Assumption A and on arbitrary finite index sets. Evidence: the systems involved depend on only through its column space, so a basis of that space reduces the general case to the stated one. This is the form actually used on p. 126, where the matrix of (3.4.49) can fail Assumption A (for example , ), a gap in the printed argument recorded as a finding.
Needed infrastructure: positive semidefinite quadratic forms and their minimization (Mathlib's Matrix.PosSemidef), dual cones and separation in finite dimension, the ice cream cone and its self-duality, and continuity of minimum values of quadratic forms under perturbation. The definitions of the Lorentz cone, CQr sets and functions, and almost solvability are reusable across the series. Proofs of individual milestones are welcome independently; Lemma 3.4.1 and statement (O) are self-contained.
Linear, second-order cone and semidefinite programming are three instances of one format: minimize a linear objective subject to the requirement that an affine image of the decision vector lie in a fixed convex cone. Ben-Tal and Nemirovski's Lectures on Modern Convex Optimization (SIAM 2001) builds its whole treatment of modelling and algorithms on this conic programming format, and the first result it needs is a duality theorem for it. That theorem is what certifies optimality of a solution returned by an interior-point solver, what turns a robust or semidefinite reformulation into a tractable problem, and what every later lecture of the book uses when it passes to a dual problem. Conic duality in this form goes back to Nesterov and Nemirovski's monograph on interior-point methods (SIAM 1994); the Lagrangian form of the same phenomenon (Slater's condition) is the textbook version in Boyd and Vandenberghe (Cambridge 2004).
This mission is the second of a series formalizing the book's capstone results, and covers Lecture 2, §2.3–2.4.
Let be a good cone: a nonempty set closed under addition and under multiplication by nonnegative reals (a convex cone), pointed (if and then ), closed, and with nonempty interior. Write for and for . The dual cone is
Given an matrix , and , the conic problem and its conic dual are
A point is feasible for (CP) if ; (CP) is strictly feasible if for some ; it is bounded below if is bounded below on the feasible set (an infeasible problem counts as bounded below); it is solvable if some feasible attains the infimum . The same notions for (D) use , , , and upper bounds. Throughout the book (from p. 53 on) Assumption A is in force: the columns of are linearly independent.
Under the standing assumptions:
Item 1 of the printed theorem (the dual of the dual is equivalent to the primal) is an informal equivalence of problems and is not part of the target.
One strengthened variant is posed beside the goal: items 2 and 3.a of Theorem 2.4.1 for every matrix , without Assumption A (finding F3: the printed proof of 3.a never uses the rank of ). The faithful theorem remains the goal.
The theorem gives, for any of the cones used in practice (nonnegative orthant, Lorentz cones, positive semidefinite matrices and their products), the existence of a dual certificate of optimality and the absence of a duality gap under strict feasibility. The rest of the book uses it constantly: the conic-quadratic and semidefinite representations of Lectures 3–4, the S-lemma, the analysis of semidefinite relaxations and the primal-dual path-following method of Lecture 6 all pass to a dual problem through it. Propositions 2.4.2 and 2.4.3 are the conic analogues of the theorem on alternatives and the inhomogeneous Farkas lemma.
The result is classical and fully proved in the book. Related statements are machine-checked on the platform in other forms: a Lagrangian strong duality under a generalized Slater condition (ConvexOptimization.conic_slater_strong_duality), duality for equality-form conic quadratic programs (ConicQuadIPM.Homogeneous.*), and the bipolar theorem for proper cones. None of them is the pair (CP)/(D) of this book with attainment in both directions and the optimality conditions of item 4. The mission produces the book's statement and its supporting results as a coherent, reusable layer for the rest of the series.
Weak duality and the gap identity are one-line computations. The content lies in items 3.a and 3.b. The obvious attempt—copying the LP proof via Farkas' lemma—fails because the image of a nonpolyhedral cone under a linear map need not be closed, so a limit of dual certificates need not be a certificate. The book's Example 2.4.1 is strictly feasible and bounded below with optimal value but no optimal solution, and Example 2.4.2 is solvable with an infeasible dual: any argument that does not use strict feasibility essentially is wrong. Separation is needed in finite dimension for convex sets that are neither open nor closed, which is not the form in which Mathlib states it, and item 3.b, which the book obtains from 3.a by symmetry, depends on the dual-cone facts of Theorem 2.3.1, including and .
Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, inner products ⬝ᵥ; the topology is the product (Euclidean) topology. The cone properties, the dual cone, feasibility, strict feasibility, boundedness, optimal solutions and optimal values are explicit predicates in one definition file, ModernConvex.ConicDuality.ConicProblem. Optimal values are never a real-valued sInf/sSup: " is the optimal value" is IsGLB/IsLUB of the set of feasible objective values, which no real satisfies for an infeasible or unbounded problem, and "" is stated through an optimal solution whose value is the other problem's infimum or supremum. A formalization that dropped strict feasibility, or that expressed the optimal values as sInf/sSup with their junk value , would make the conic duality theorem either false or trivially true; the targets rule this out by stating attainment and value equality as explicit predicates. Assumption A is Function.Injective A.mulVec, an explicit hypothesis wherever the book has it in force, including Propositions 2.4.2–2.4.3 per the book's Remark 2.4.1.
Needed infrastructure: finite-dimensional separation of convex sets (Mathlib has geometric_hahn_banach_open and relatives for open sets; the nonopen finite-dimensional case goes through relative interiors), dual-cone facts (Mathlib's innerDualCone lives on inner-product spaces, while this mission works on Fin m → ℝ with the dot product), and closedness arguments for cones. The definitions and Theorem 2.3.1 are reusable by the later missions of this series. Proofs of individual milestones, and proofs or refutations of the variant, are welcome.
Conic quadratic programs (second-order cone programs) minimize a linear objective subject to finitely many constraints of the form . They are solved by interior-point methods in polynomial time, and a large share of convex models in engineering, statistics and robust optimization can be rewritten in this form. Whether a given convex problem can be so rewritten is a question about its feasible set and objective: can they be described by conic quadratic inequalities, possibly after adding auxiliary variables? Ben-Tal and Nemirovski answer this question in Lecture 3 of Lectures on Modern Convex Optimization (SIAM, 2001, doi:10.1137/1.9780898718829) with a calculus of conic quadratic representability: a list of elementary representable sets and functions together with operations that preserve representability, each operation producing an explicit representation from given ones. The same calculus underlies modelling tools such as CVX and YALMIP.
The more advanced operations in §3.3 — conic hulls, projective transformations, polars, Legendre transformations, convex hulls of unions and recessive cones — are only nearly representability-preserving: each holds exactly under a closedness or strict feasibility condition, and otherwise produces a set sandwiched between the target and its closure. The rule for convex hulls of unions is credited in the book to Nesterov.
For the ice cream cone (Lorentz cone) is . Let be a direct product of ice cream cones, and write for and for .
A set is CQr (conic quadratic representable) if there are such a , a number of additional variables and data with
the system is a conic quadratic representation (CQR) of . No rank condition is imposed on it. A function is CQr when its epigraph is.
For the mission uses the convex hull and its closure; the conic hull and its closure ; the polar ; and the recessive cone . For as above it uses the Legendre transformation and the projective transformation , whose epigraph is the closure of .
Let be nonempty convex CQr sets, , and let
Then
and if (i) all are closed and bounded, or (ii) with closed and bounded and convex and closed, all three sets are equal and CQr.
The goal shows that a disjunction of conic quadratic constraints — " lies in one of " — can be convexified exactly, under a compactness-type condition, by a conic quadratic system whose size is the sum of the sizes of the given representations. This is the conic quadratic analogue of Balas's disjunctive programming formulation for polyhedra and is the basis of perspective reformulations in mixed-integer conic optimization. The milestones are the other closure rules of the calculus: they let a modeller pass to conic hulls, perspectives, polars, conjugates and recession cones without leaving the conic quadratic class, always with an explicit representation.
These results are classical and proved in the book; none of them is formalized on the platform, and there is no formal library of conic quadratic representability. The mission produces that library's core definitions and its main closure theorems as machine-checked statements. Propositions 3.3.3 and 3.3.4 depend on conic duality, which a companion mission of this series (II: The Conic Duality Theorem) states.
The inclusions are not symmetric in difficulty. is a direct substitution, but contains points with some , where the block inequality no longer certifies membership in any ; such points are only limits of convex combinations, and showing they lie in the closure requires the nonemptiness of every . The equality under (i) or (ii) is a closedness statement for a convex hull, which fails in general (two closed convex sets can have a non-closed convex hull of their union), so the compactness of the must be used. Closedness of projections (Lemma 3.3.1) is the analogous obstacle in the milestones: the projection of a closed convex set is not closed in general.
Vectors are Fin n → ℝ; the Euclidean norm is written out (eucNorm) because Mathlib's norm on this type is the sup norm. A product of ice cream cones is a structure IceCreamProduct with factors of dimensions , its vectors indexed by (block, coordinate) pairs, the last coordinate of each block being the dominant one. cqrSet K A B b is the represented set and IsCQr X says equals some cqrSet; the existential is over the fixed shape (finitely many Lorentz factors and an affine map), so an arbitrary set is not CQr by fiat. Pairs of the conic hull are vectors of Fin (n+1) → ℝ with last coordinate . Functions into are EReal-valued and assumed never ; the Legendre transformation is an EReal supremum, in which points with contribute . Conv is convexHull ℝ, and closures are topological closures. Every "is CQr" conclusion is stated together with the book's explicit representation as an equality or sandwich of sets; stating "is CQr" alone would be a weaker theorem.
Beyond the paper. Proposition 3.3.2 as printed omits and is false for (the right-hand side contains while the left-hand side is empty; a Lean refutation of the formal statement was built during drafting). The faithful statement is kept as a milestone, and a corrected variant adds the missing hypothesis.
Reusable beyond this mission: the definitions of ice cream products, CQr sets, conic hull, polar, recessive cone and projective/Legendre transformations, and Lemma 3.3.1 as a closedness criterion. Contributions toward a general "closed projection" lemma and conic duality for products of Lorentz cones are welcome.
Every linear program comes with a second linear program, its dual, whose feasible points certify lower bounds on the first program's optimal value. The duality theorem says that these certificates are complete: the best bound equals the optimal value whenever either is finite. It is the reason an LP solver can return a proof of optimality alongside a solution, the basis of sensitivity analysis and of primal–dual algorithms, and the template for every duality theory in convex optimization.
This mission opens a series formalizing A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization (SIAM 2001, doi:10.1137/1.9780898718829). Lecture 1 develops LP duality from a theorem on the alternative for mixed strict and non-strict linear inequalities, and proves that theorem from the homogeneous Farkas lemma by way of the theorems of Helly and Radon. Lecture 2 reruns the same argument for conic programs, so the statements here are the ones later missions of the series generalize.
Let have rows , and let , . Vector inequalities are componentwise. The LP program and its dual are
A point with is feasible, and (LP) is feasible if such a point exists. (LP) is bounded below if is bounded below on the feasible set. It is solvable if some feasible point minimizes . A real is a lower bound on the optimal value if for every feasible . The optimal value is , which is for an infeasible and for an unbounded program. The same notions apply to the dual with "bounded above" and "maximizes". No rank condition is imposed on .
The system on the alternative is
and its two certificate systems in are
In Lean, vectors are functions Fin n → ℝ, is c ⬝ᵥ x, and the definitions live in ModernConvex.LPDuality.LinearProgram and ModernConvex.LPDuality.AlternativeSystems.
LP duality underlies most of the book's later material. The conic duality theorem of Lecture 2 has the same statement with the nonnegative orthant replaced by a cone. Robust counterparts, the S-lemma and the semidefinite relaxations of Lecture 4 are all proved by dualizing an inner problem. A machine-checked version in exactly this form, with explicit predicates for "bounded" and "solvable", is the base that later missions of the series can cite.
The results here are classical and proved. The platform already has proved LP duality theorems, in other standard forms: LinearOptimization.lp_strong_duality (general form with equalities), MatousekLP.Duality.duality_theorem (max/ form, four-case statement) and VanderbeiLP.StrictComp.strong_duality. It has Farkas lemmas in several forms (LinearOptimization.farkas_cone_corollary, which is one direction of Lemma 1.4.1, and MatousekLP.Duality.farkas_geometric). It also has Helly and Radon in Mathlib's form (FamousTheorems.helly_theorem, which assumes at least sets and subfamilies of size exactly ; FamousTheorems.radon_theorem, which assumes affine dependence). The open MangasarianFJ.GenFJ.motzkin_transposition is a related alternative theorem. None of them states the book's inequality-form pair (LP)/(LP), the five-way equivalence, or the mixed strict/non-strict theorem on the alternative. These are the remaining work. Several of them should follow quickly from the existing items, and solvers are encouraged to reuse them.
The obstacle is the existence of certificates of infeasibility. Proposition 1.3.1 is a one-line computation, but its converse, Theorem 1.3.1, is not: the existence of a certificate is a global statement about the system that no local computation produces. The mixed system needs care: when only can certify, and the homogenization that reduces Theorem 1.3.1 to the Farkas lemma has to keep strict and non-strict rows apart. In the duality theorem, the step from "feasible and bounded below" to "solvable" is where attainment must be shown. It is true for LPs and false for general convex programs (), so a proof cannot avoid the linear structure.
The book's own proof of item 1 has a sign slip. The displayed dual of the rewritten (LP) has the constraint with , which describes rather than a program equivalent to (LP). The formal statement uses the correct computation, with .
Vectors are Fin n → ℝ. Indices are 0-based, so the strict rows of are i < ms, and ms ≤ m is a hypothesis. Optimal values are never written as sInf/sSup, whose junk value on empty or unbounded sets would make the equal-values clause trivially true. A lower bound is the predicate . " is the optimal value" is IsGLB/IsLUB of the set of objective values, which no real satisfies for an infeasible or unbounded program. Item 1 of the goal is not formalized as True. It states the explicit feasible-set correspondence that "equivalent" means in the book's proof. The five properties are a List.TFAE.
In Bernstein's theorem the sup-norm inequality is stated as "every bound on over gives the bound on ". Coefficients are complex, which covers the real case.
The book prints the trigonometric polynomial as , with the same two coefficients in every term. This is a subscript typo: the theorem is stated for every trigonometric polynomial of degree , and its own tightness example is not of the printed form for . The formal statement uses general coefficients .
A complete development needs only Mathlib's finite-dimensional linear algebra and convexity (convexHull, Convex). The definitions of the LP pair and of the alternative systems are reusable by any later mission that dualizes a linear inner problem.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
We investigate whether the use of a noiseless, classical feedback channel will increase the capacity of a quantum discrete memoryless channel to transmit classical information. This problem has been previously analyzed by Bowen and Nagarajan for the case of protocols restricted to product input states. They showed that feedback did not increase the information capacity. In this paper we introduce a quantum analogue of classical causality and prove a capacity theorem (in regularized form) for the transmission of classical information.
This mission is the statement-level formalization of Classical feedback for quantum channels (arXiv:quant-ph/0409207v3). 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 Whole-codeword Markov property of the executed feedback protocol (§2, paragraph continuing PDF p.5, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
This paper is devoted to the study of various maximal ergodic theorems in noncommutative -spaces. In particular, we prove the noncommutative analogue of the classical Dunford-Schwartz maximal ergodic inequality for positive contractions on and the analogue of Stein's maximal inequality for symmetric positive contractions. We also obtain the corresponding individual ergodic theorems. We apply these results to a family of natural examples which frequently appear in theory of von Neumann algebras and in quantum probability.
This mission is the statement-level formalization of Noncommutative maximal ergodic theorems (arXiv:math/0505308v2). 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 Operator block matrix norm comparison (Lemma 3.2, 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.
62 results of the paper are not stated yet, because the library lacks an interface they need:
We study the Weyl representation of metaplectic operators associated to a symplectic matrix having no non-trivial fixed point, and justify a formula suggested in earlier work of Mehlig and Wilkinson. We give precise calculations of the associated Maslov-type indices; these indices intervene in a crucial way in Gutzwiller's formula of semiclassical mechanics, and are simply related to an index defined by Conley and Zehnder.
This mission is the statement-level formalization of On the Weyl Representation of Metaplectic Operators (arXiv:math/0503708v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symplectic Cayley transform and its inverse (§3.1, unnumbered, 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.
9 results of the paper are not stated yet, because the library lacks an interface they need:
We give an algorithm for constructing the algebraic hull of a given matrix Lie algebra in characteristic zero. It is based on an algorithm for finding integral linear dependencies of the roots of a polynomial, that is probably of independent interest.
This mission is the statement-level formalization of Constructing algebraic Lie algebras (arXiv:math/0611414v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Trivial permutation component and power traces (Lemma 5: trivial permutation component and trace, 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.
18 results of the paper are not stated yet, because the library lacks an interface they need:
In this note we show that the representation of the additive group of the Hilbert space on given by the multiplication operators is continuous but its space of smooth vectors is trivial. This example shows that a continuous unitary representation of an infinite dimensional Lie group need not be smooth.
This mission is the statement-level formalization of A non-smooth continuous unitary representation of a Banach-Lie group (arXiv:0811.4234v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The phase representation is continuous and has only the zero smooth vector (Theorem 2.3, 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.
Based on the ideas in [CKP], we introduce the weighted analogue of the branching rule for the classical hook length formula, and give two proofs of this result. The first proof is completely bijective, and in a special case gives a new short combinatorial proof of the hook length formula. Our second proof is probabilistic, generalizing the (usual) hook walk proof of Green-Nijenhuis-Wilf, as well as the q-walk of Kerov. Further applications are also presented.
This mission is the statement-level formalization of The weighted hook length formula (arXiv:1006.0043v1). 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 Four weighted branching identities (Theorem 2(a)–(d), 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.
3 results of the paper are not stated yet, because the library lacks an interface they need:
A single-party strategy in a multi-round quantum protocol can be implemented by sequential networks of quantum operations connected by internal memories. Here provide the most efficient realization in terms of computational-space resources.
This mission is the statement-level formalization of Minimal computational-space implementation of multi-round quantum protocols (arXiv:1006.1780v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1 and Eq.(8): Haar averaging preserves the optimum and yields covariance (Lemma 1 and Eq.(8): Haar averaging preserves the optimum and yields covariance, 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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper, a new axiomatization for unbounded functional calculi is proposed and the associated theory is elaborated comprising, among others, uniqueness and compatibility results and extension theorems of algebraic and topological nature. In contrast to earlier approaches, no commutativity assumptions need to be made about the underlying algebras. In a second part, the abstract theory is illustrated in familiar situations (sectorial operators, semigroup generators, normal operators). New topological extension theorems are proved for the sectorial calculus and the Hille--Phillips calculus. Moreover, it is shown that the Stieltjes and the Hirsch calculus for sectorial operators are subcalculi of a (small) topological extension of the sectorial calculus.
This mission is the statement-level formalization of On the Fundamental Principles of Unbounded Functional Calculi (arXiv:2009.04733v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
31 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 6.1 (Extension Theorem) (Theorem 6.1 (Extension Theorem), 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:
Any multiplicity-free family of finite dimensional algebras has a canonical complete set of of pairwise orthogonal primitive idempotents in each level. We give various methods to compute these idempotents. In the case of symmetric group algebras over a field of characteristic zero, the set of canonical idempotents is precisely the set of seminormal idempotents constructed by Young. As an example, we calculate the canonical idempotents for semisimple Brauer algebras.
This mission is the statement-level formalization of Canonical idempotents of multiplicity-free families of algebras (arXiv:1606.08900v5). 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 Introduction (1), made precise by Proposition 1.6: canonical partition and GT basis (Introduction (1), made precise by Proposition 1.6: canonical partition and GT basis, 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.
21 results of the paper are not stated yet, because the library lacks an interface they need:
We describe an efficient quantum algorithm for the quantum Schur transform. The Schur transform is an operation on a quantum computer that maps the standard computational basis to a basis composed of irreducible representations of the unitary and symmetric groups. We simplify and extend the algorithm of Bacon, Chuang, and Harrow, and provide a new practical construction as well as sharp theoretical and practical analyses. Our algorithm decomposes the Schur transform on qubits into operators in the Clifford+T fault-tolerant gate set and uses exactly ancillary qubits. We extend our qubit algorithm to decompose the Schur transform on qudits of dimension into primitive operators from any universal gate set, for .
This mission is the statement-level formalization of A Practical Quantum Algorithm for the Schur Transform (arXiv:1709.07119v6). 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 Exact three-register Schur encoding space (§3.3 Eqs.(24)–(27), 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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
Relations between states and maps, which are known for quantum systems in finite-dimensional Hilbert spaces, are formulated rigorously in geometrical terms with no use of coordinate (matrix) interpretation. In a tensor product realization they are represented simply by a permutation of factors. This leads to natural generalizations for infinite-dimensional Hilbert spaces and a simple proof of a generalized Choi Theorem. The natural framework is based on spaces of Hilbert-Schmidt operators and the corresponding tensor products of Hilbert spaces. It is proved that the corresponding isomorphisms cannot be naturally extended to compact (or bounded) operators, nor reduced to the trace-class operators. On the other hand, it is proven that there is a natural continuous map from trace-class operators on (with the nuclear norm) into compact operators mapping the space of all bounded operators on into trace class operators on (with the operator-norm). Also in the infinite-dimensional context, the Schmidt measure of entanglement and multipartite generalizations of state-maps relations are considered in the paper.
This mission is the statement-level formalization of On the relation between states and maps in infinite dimensions (arXiv:0706.2617v1). 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 Finite-dimensional Jamiolkowski permutations are unitary and equivariant (Theorem 1; equations (12)–(17), 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.
15 results of the paper are not stated yet, because the library lacks an interface they need:
Inspired by a recent experiment by Steinhauer and co-workers, we present a simple model which describes the formation of an acoustic black hole in a Bose-Einstein condensate, allowing an analytical computation of the evolution in time of the corresponding density-density correlator. We show the emergence of analog Hawking radiation out of a "quantum atmosphere" region significantly displaced from the horizon. This is quantitatively studied both at and even in the presence of an initial temperature T, as is always the case experimentally.
This mission is the statement-level formalization of Ramp-up of Hawking radiation in Bose-Einstein condensate analogue black holes (arXiv:2005.04443v3). 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 Sonic horizon and the two flow regions (Following (4), 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.
8 results of the paper are not stated yet, because the library lacks an interface they need:
We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski's original QE algorithm and the Ben-Or, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL.
This mission is the statement-level formalization of A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL (arXiv:2209.10978v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The coefficient-sum conversion equals the canonical univariate conversion (§3.3: lemma multivar_as_univar, 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.
10 results of the paper are not stated yet, because the library lacks an interface they need: