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.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In the last of the twenty-four questions that closed his 1982 survey Three-dimensional manifolds, Kleinian groups and hyperbolic geometry (Bull. Amer. Math. Soc. 6 (1982), 357–381), Thurston asked to "show that volumes of hyperbolic -manifolds are not all rationally related" (p. 380). Twenty-two of the twenty-four have since been answered — geometrization by Perelman, tameness by Agol and by Calegari–Gabai, the ending lamination conjecture by Brock–Canary–Minsky, virtual fibering by Agol — and this one is among the two that remain open.
Some rational relations are forced, and for a trivial reason: a degree cover of a hyperbolic -manifold has times its volume, so any two commensurable manifolds have rationally related volumes. The question, which remains open, is whether every rational relation arises that way — equivalently, whether some two hyperbolic -manifolds have irrational volume ratio. Remarkably, not a single such pair is known.
The bundle fixes the meaning of every term. Hyperbolic -space is the upper half-space . Its volume is Lebesgue measure with density — the Riemannian volume of the metric written out, so that no Riemannian machinery is required. The hyperbolic distance is given by its closed formula
A Kleinian action is a free, properly discontinuous action by hyperbolic
isometries; the quotient is a complete hyperbolic -manifold, discreteness and
torsion freeness being consequences rather than hypotheses. The volume of the
quotient is the measure of a fundamental domain, in the sense of Mathlib's
MeasureTheory.IsFundamentalDomain, and the set of volumes collects those that
are finite and positive.
Two conventions are stated rather than derived, and are worth flagging. Isometries are not required to preserve orientation, so the set of volumes also contains those of non-orientable quotients; this enlarges the set but not its -span, so neither goal is affected. And preservation of the hyperbolic volume is a field of the structure rather than a consequence of preserving the distance: it holds for every hyperbolic isometry, but deriving it amounts to classifying , which is not the subject of this mission.
The goal is that the volumes are not all rationally related: there are two of them, and , with for every rational .
Two milestones support it. The first is that passing to a subgroup of index multiplies the volume by , a fundamental domain for the subgroup being the union of translates of one for the whole group; this is the source of every known rational relation, and it is why the question is phrased as it is. The second is that the set of volumes is nonempty — that some finite-volume hyperbolic -manifold exists at all — without which the goal would be vacuously false rather than open.
A stronger form of the question, that the -span of the set of volumes is infinite dimensional, is also stated.
The question is a geometric statement whose difficulty is arithmetic. For the Bianchi groups of an imaginary quadratic field , Humbert's formula gives the covolume as , so the ratio of two such volumes is, up to explicit algebraic factors, a ratio of Dedekind zeta values at ; and Neumann and Yang showed that the Bloch invariant of a hyperbolic -manifold lies in a subgroup of finite -rank determined by its invariant trace field, so that manifolds sharing an invariant trace field with a single complex place, such as an imaginary quadratic one, have rationally related volumes. Producing one irrational ratio therefore means separating two such transcendentals — a statement of the same order of difficulty as the irrationality of . The value of formalizing the question is not that it will be closed, but that its statement, and the elementary relations that make its naive form false, are pinned down exactly.
Invertible modules over a commutative semiring are Zariski-locally free, so local semirings have trivial Picard group. The source asks whether the ring-theoretic semilocal conclusion survives without subtraction: must every invertible module over a semiring with finitely many maximal ideals be free? If not, is the conclusion at least true for finite semirings?
This mission turns CUHK-Shenzhen AI Math Problem 19, Picard groups of semi-local or finite semirings, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
The main theorem asserts freeness for every invertible module over a commutative semiring with finite maximal spectrum. A separate milestone states the finite-semiring fallback. Both are positive formulations; a concrete counterexample to either resolves that target negatively and should motivate a corrected classification.
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in semirings, Picard groups, invertible modules, finite semirings. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
Ring proofs use subtraction-sensitive k-ideal properties and decompositions into local factors that can fail for semirings. Finite indecomposable semirings need not be local and may have positive Krull dimension. Invertible modules are projective with strong duality, but familiar rank and determinant arguments may not survive additive noncancellation.
Formalize the known local-freeness proof from the evaluation isomorphism and study patching over finitely many principal opens. Identify exactly where partitions of unity require k-ideals. For finite semirings, enumerate idempotent matrices representing projective modules, impose the invertibility constraints, and seek either a reduction to principal rank-one modules or a minimal counterexample. Product decompositions and faithful-action lemmas should be reusable.
The Lean targets use Mathlib's commutative semiring, maximal spectrum, module, invertible-module, and free-module notions. 'Semilocal' is encoded only as finiteness of MaximalSpectrum; no unproved decomposition theorem is assumed. The finite fallback assumes the underlying semiring type is finite but does not assume the module itself finite separately. Cardinality-only variants from the source are not the capstone.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
Resolve the finite-semiring statement, computationally or structurally, while developing the local-to-semilocal patching lemmas needed by the main theorem.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
The CUHK-Shenzhen AI Math Problems page added this problem on June 24, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
Compressing an operator to a closed subspace keeps the information visible within that subspace but can discard interactions with its orthogonal complement. The compression-rigidity question asks whether a particular equality detects that no such interactions were present. Its inputs are two commuting positive contractions and an ordinary strictly convex function of two real variables. The issue is the equality case, not the existence of a general operator inequality for every convex function.
The question was contributed by Boris Bilich to the CUHK-Shenzhen AI Math Problems collection and added on June 1, 2026. The original problem asks about operators on a Hilbert space without imposing finite dimension. The first formal target in this mission treated matrices with supplied joint spectral data. That finite-dimensional declaration has a verified proof on Prove2Me, but it does not settle the unrestricted Hilbert-space question. The September 2026 correction restores arbitrary complex Hilbert spaces as the main target and preserves the earlier result as a supporting artifact.
Let be a complete complex Hilbert space, and let be its algebra of bounded complex-linear operators. The multiplication means composition, with acting first, and denotes the adjoint. A positive contraction is self-adjoint, satisfies for every , and has operator norm at most one. Both zero and the identity are permitted.
Write . Let be positive contractions satisfying . Their joint continuous functional calculus assigns an operator to each continuous real function on . It is characterized as a continuous unital real star-algebra homomorphism from to that maps the two coordinate functions to and . The domain has the uniform norm and the codomain the operator norm. The existence and uniqueness of this calculus follow from the standard joint spectral theorem; the relevant source is Dereziński, Lemma 6.6, printed page 43.
An orthogonal projection is an operator satisfying and . The compressed operators and are still viewed as operators on the original space , not as operators on a separately chosen finite-dimensional range. The question includes the additional hypothesis that these compressed operators commute. The original commutation of and does not remove the need to state this hypothesis.
The main target is the entire compression implication from the source. Let be continuous and strictly convex: for distinct and , its value at is strictly less than . For as above, the question is whether
Both outer projections on the right are part of the original assertion. There is no hypothesis that . Commutation of with each coordinate operator is exactly the reducing-subspace conclusion asked for in the source.
The accompanying standard infrastructure target asserts that, for every commuting pair of positive contractions on ,
where is continuous, unital, real-linear, multiplicative and star-preserving. This is the unit-square, real-valued-function specialization of Lemma 6.6, not a claim that this known theorem is a new research conjecture. Its Lean proof is a separate supporting obligation. The earlier two-dimensional milestone and the proved finite-dimensional capstone remain available; neither replaces the new main target.
A positive resolution would show that exact preservation of one strictly convex functional-calculus value, under the specified commuting-compression hypothesis, forces both operators to preserve the projection's range and its orthogonal complement. A negative resolution would require an actual Hilbert space, operators and strictly convex function satisfying every hypothesis while at least one of the two reducing identities fails.
The formal development separates this research question from the standard spectral infrastructure needed to express it. The new main declaration is an open proof obligation. The joint-calculus existence-and-uniqueness declaration is also unproved in this contribution, although mathematically standard. Local compilation and server publication check the declarations' well-formedness; they are not proofs of either statement. Only the earlier finite-dimensional result is being reported here as already proved.
Arbitrary bounded commuting self-adjoint operators need not have a joint eigenbasis. Consequently a matrix formulation that records finitely many joint spectral atoms cannot serve as the general operator model. The compressed pair may also have different spectral data from the original pair. The equality involves these two different functional calculi, with a projection on either side of each value.
Strict convexity in this question is ordinary scalar strict convexity on the square. Operator convexity, finite rank of the projection, compactness of the coordinate operators, and a multivariable operator Jensen inequality are not additional assumptions. Introducing any of them would change the requested question. The general formulation must also retain boundary cases rather than exclude them to simplify an argument.
The Lean model uses actual bounded complex-linear maps on an arbitrary complete inner-product space. It imposes no finite-dimensionality, separability, common-eigenbasis or nonzero-space assumption. It includes , and the zero Hilbert space. The scalar field convention is complex; a real-Hilbert-space transfer is not separately formalized here.
The function is stored on the ambient real plane, but continuity, strict convexity and evaluation use only its restriction to . Values outside are irrelevant, and continuity outside the square is not required. Thus storing an ambient function does not exclude any continuous function originally defined only on the square.
Joint evaluation is a total definition. If a representing continuous unital real star-algebra homomorphism exists, it chooses one for the operator pair and then evaluates the supplied function. Otherwise it returns zero. The separate existence-and-uniqueness target establishes that this fallback is inapplicable to commuting positive contractions and that the choice is immaterial. No field in the model assumes the compression-rigidity conclusion. The supporting standard theorem must also apply to the compressed pair using the original projection and positivity hypotheses, without adding representation existence as a new restriction on the main question.
The replacement definition and both statements were built at Lean 4.30.0 with supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, and their final versions received independent blind readbacks. Published older declarations and their proof identities are preserved. They should be cited with their finite-dimensional scope, not described as a solution of the arbitrary-Hilbert-space target.
Submission hold — source-fidelity repair (2026-09-04). The public goal restricts answers to elementary expression trees and is only a stronger subquestion. It does not formalize the source's broader special-function closed-form question. The existing published target is preserved, with this scope warning. Do not confirm or submit this version as a faithful formalization of the full source. The legacy mathematical target below is retained for traceability while the replacement is prepared.
A standard Brownian motion starts below the exponentially decaying boundary b(t)=b0 exp(-ct). The first time it crosses the boundary has a continuous density characterized by a generalized Abel--Volterra integral equation. The source asks for an explicit distribution, motivated in part by neuronal threshold models with a decaying refractory boundary.
This mission turns CUHK-Shenzhen AI Math Problem 13, First-passage time of Brownian motion to an exponentially decaying boundary, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
Construct one expression in a fixed elementary language whose evaluation is a continuous nonnegative density on positive times, solves the Abel equation, and integrates to one. The language contains real constants, rational constants, arithmetic, exp, log, square root, trigonometric functions, and the normal density. The first milestone drops elementary representability and normalization and asks for a continuous nonnegative Abel solution.
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in Brownian motion, first-passage times, stochastic processes, Volterra integral equations. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
Moving-boundary first-passage laws rarely have elementary closed forms. The Abel kernel is singular at the upper endpoint, and showing that a candidate equation solution is the actual passage density requires uniqueness and probability normalization. The capstone may be false under the selected expression language; a non-elementarity theorem would be a legitimate disproof of this precise formal target.
Formalize existence and uniqueness for the Volterra equation using weakly singular kernels, then connect it to Brownian first passage. Explore transformations suggested by the exponential boundary, Laplace transforms, and iterative resolvent kernels. Symbolic or numerical calculations may reveal special-function rather than elementary structure. If so, characterize the required extension of the expression language and prove why the current language is insufficient.
The already-published goal uses finite elementary-expression trees with arithmetic, exp/log/sqrt, sin/cos and normal density. The source explicitly permits standard special functions beyond this language. Accordingly the published declaration is a stronger elementary-only subquestion, not a faithful replacement for the full closed-form question. It is preserved as an existing result; its proof or disproof must not be reported as settling every special-function formula. The Abel-solution milestone asserts only existence of a continuous nonnegative solution; uniqueness, normalization, and identification with the first-passage density remain separate obligations. A complete source-faithful replacement needs an agreed formula class or a concrete proposed formula, not an unrestricted function renamed a closed form.
For each positive boundary height and decay parameter, there exists a continuous nonnegative solution of the stated Abel equation on positive times. This node asserts existence only, not uniqueness, unit mass, or an elementary closed form.
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
Linear approximation is only one instance of distance minimization. Feasible sets in optimization are typically convex rather than subspaces, so a useful certificate must compare a target point with an entire convex set and must allow an affine offset. Chapter 5 of Luenberger's Optimization by Vector Space Methods builds this certificate through geometric forms of the Hahn--Banach theorem, supporting hyperplanes, and separation of convex sets. The resulting minimum-distance theorem expresses the distance from a point to a convex set as an optimal gap measured by a norm-bounded continuous linear functional (Luenberger, §§5.12--5.13, pp. 130--137).
This mission advances the series from subspace annihilators to affine separation. It formalizes the Minkowski gauge used by the chapter, three progressively stronger separation statements, and a capstone distance-duality certificate. These results are standard infrastructure for constrained optimization: they turn a geometric exclusion or distance into a scalar inequality that can later become a multiplier or a dual bound.
Let be a real normed space and a nonempty convex set. Convexity is represented by Convex ℝ K, and topological interior, closure, and infimum distance use Mathlib's interior, closure, and Metric.infDist. A continuous affine separator is described by a continuous linear functional and a scalar level . The inequality for all places in one closed half-space.
When a convex set contains zero in its interior, its Minkowski gauge is the functional gauge K. The source characterizes it by nonnegativity, positive homogeneity, subadditivity, continuity, and the level sets
These properties are bundled into the first milestone, following Lemma 1 of §5.12 (pp. 131--132).
For two convex sets , Eidelheit separation means finding nonzero and with for and . The source assumes that has nonempty interior and that its interior does not meet . The Lean statement records the nonemptiness of explicitly, since otherwise nonzero separation is not forced.
Formalize the six gauge properties above. Then, for a convex with nonempty interior and an affine subspace disjoint from that interior, produce and such that
This is Mazur's geometric Hahn--Banach theorem as stated in §5.12, Theorem 1 (p. 133).
For , formalize a nonzero functional satisfying for all . Next formalize Eidelheit separation:
These are Theorems 2 and 3 of §5.12 (pp. 133--134).
Let have positive distance from . Produce and a real upper-bound level with , on , and
Every other feasible pair must satisfy . If realizes the distance, require to align with . This is the finite real certificate form of §5.13, Theorem 1 (pp. 136--137).
The capstone is an exact strong-duality statement for distance to a convex set. A feasible pair yields a certified lower bound on the distance, and the distinguished pair reaches the primal value. Unlike a nearest-point characterization, it remains meaningful when is not closed and no minimizing point exists. The conditional alignment clause identifies the equality case when attainment is available.
Formalizing the chapter's progression creates more than one isolated equality. The gauge package links convex geometry to sublinear analysis; Mazur separation handles affine constraints; the supporting-hyperplane and Eidelheit statements provide reusable interfaces for later multiplier rules. The results are known and proved in the 1969 text; the mission's contribution is a coherent machine-checked Lean layer that preserves the source hypotheses and can support later chapters on duality and optimization.
A direct reuse of subspace distance duality is insufficient because a general convex set is neither closed under subtraction nor described by an annihilator. An affine level is unavoidable. The common shorthand introduces a second problem: need not be bounded, so a real-valued supremum is not available for an arbitrary functional. The capstone therefore quantifies over a real upper bound and asserts its optimality through a universal inequality; this records the same finite support value without imposing boundedness absent from the source.
Topological hypotheses also differ across the milestones. Separation uses nonempty interior, whereas the final distance theorem only assumes convexity, nonemptiness, and positive distance. Replacing positive distance by mere exclusion would be invalid for a nonclosed set. Similarly, requiring closure or compactness would make formalization easier but would lose the theorem's intended infinite-dimensional scope.
The mission is restricted to real normed spaces. Sets use Set X; affine varieties use AffineSubspace ℝ X; separators use ContinuousLinearMap. The gauge is Mathlib's existing gauge, so no competing definition is introduced. The bundled gauge milestone deliberately includes both level-set identities as well as continuity, positive homogeneity for positive real scalars, subadditivity, and nonnegativity.
The Eidelheit theorem includes K₂.Nonempty, an assumption used implicitly by the source's separating conclusion. The capstone includes K.Nonempty and 0 < Metric.infDist x₁ K; it does not assume closedness, boundedness, compactness, or attainment. Its pair represents a finite support level, and the universal comparison over all feasible rules out a weakened statement in which an arbitrarily loose upper bound could trivialize existence. The optional nearest-point clause uses the exact equality and fixes the sign of alignment. Contributions may add reusable lemmas on gauges, interiors, affine subspaces, or support bounds, but the public results should remain independent of finite-dimensionality and completeness.
Many convex programs impose inequalities valued in a vector space: componentwise inequalities, positive-semidefinite constraints, and families of ordered resource constraints are all instances of one cone order. Chapter 8 of David G. Luenberger's Optimization by Vector Space Methods develops a global theory for this setting. A perturbation of the constraint produces a convex value function, continuous linear functionals positive on the ordering cone become Lagrange multipliers, and a strict-feasibility condition yields an attained dual optimum. This mission formalizes the progression in §§8.2–8.6, culminating in the book's Lagrange Duality Theorem.
Let and be real normed spaces, let be a nonempty convex set, and let be a convex cone. The cone induces the relation
A continuous linear functional is dual-positive when for every . A map is cone-convex on when its value at a convex combination is below the corresponding convex combination of its values in this cone order. The primal program is
where is real-valued and convex on .
For a multiplier , the Lagrangian and its possibly infinite dual value are
The perturbed primal value replaces the zero right-hand side by . Lean represents and in EReal, so infeasible perturbations have value and objectives unbounded below can have value without arbitrary defaults.
Assume has nonempty interior, the primal value is finite, and there is a strictly feasible point with
Prove that a dual-positive exists and attains
If attains the primal infimum, also prove complementarity and that minimizes over .
Five source milestones delimit the reusable theory. A closed convex cone is recovered from all dual-positive inequalities (§8.2, Proposition 1). The finite-height epigraph of the extended perturbation value is convex, and that value is antitone in the cone order (§8.3, Propositions 1–2). A Lagrangian saddle point is sufficient for primal feasibility and optimality when the cone is closed (§8.4, Theorem 2). Finally, multipliers for two perturbed right-hand sides bound the change in optimal objective value from both sides (§8.5, Theorem 1). The root then states §8.6, Theorem 1 rather than duplicating the equivalent multiplier theorem from §8.3.
The capstone provides both equality of optimal values and an attained multiplier. It applies to a single vector inequality, so finite systems of scalar inequalities and matrix-cone constraints fit the same statement once their ordering cones are supplied. Complementarity and Lagrangian minimization turn a primal optimizer and multiplier into a certificate. The sensitivity milestone additionally gives quantitative information about how the optimum changes when the constraint right-hand side moves.
Formalization produces a reusable cone-order layer independent of coordinate choices. coneLE, dualPositive, and ConeConvexOn can support later Kuhn–Tucker, vector optimization, and conic programming developments. The EReal value functions preserve infeasibility and unboundedness, two cases that a real-valued sInf encoding would collapse. This is a formalization mission for a classical theorem, not a claim that the underlying duality result is open.
The theorem's strict-feasibility condition is load-bearing. Feasibility cannot replace interior feasibility, and nonempty interior of alone does not supply a Slater point. Equality constraints also cannot be converted into pairs of inequalities while retaining strict feasibility; Luenberger explicitly warns about this after the theorem.
The cone assumptions differ across milestones. The main strong-duality theorem does not require to be closed or pointed, whereas the bipolar and saddle-sufficiency statements require closedness. Using Mathlib's stronger ProperCone everywhere would silently add both topological and order hypotheses and shrink the theorem. Another tempting simplification is to make both value functions real. That loses the empty feasible set and unbounded dual subproblem, precisely the boundary cases used when comparing perturbations. The saddle inequalities must also have the correct orientation: the multiplier coordinate is maximized and the primal coordinate is minimized.
The mission uses ConvexCone ℝ Z with a custom induced relation; it deliberately does not assume a lattice order on . Multipliers are continuous linear maps . The root assumes a real finite optimum through IsGLB and a real witness , while lagrangeDualValue and perturbationValue retain EReal codomains. The strict condition is written as membership of in interior P, exactly matching .
No finite-dimensionality, reflexivity, completeness, closedness, or pointedness is added to the root. Closedness appears only where the source uses cone separation to recover primal feasibility. The sensitivity item assumes the two candidate points are feasible, their multipliers are dual-positive and complementary, and each point minimizes its shifted Lagrangian; these hypotheses spell out “solutions and corresponding multipliers” without relying on informal terminology.
Contributions may formalize cone separation, perturbation-value geometry, saddle certificates, or strong duality. Finite-dimensional orthant and positive-semidefinite specializations are useful corollaries but do not replace the general goal. Local multiplier rules, equality constraints, differentiable Kuhn–Tucker conditions, and Chapter 9's local theory remain outside this mission.
AI generated, I think it's correct
The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. A bound means that, over the field under consideration, matrices can be multiplied in field operations for every . Matrix multiplication is a central benchmark in algebraic complexity and a basic subroutine in linear algebra, graph algorithms, and symbolic computation.
The Coppersmith--Winograd tensor and the laser method produced the strongest bounds on for several decades. The 1990 tensor-square analysis gave . Later analyses of larger powers improved the numerical bound, but they organized their recursion through values assigned independently to constituent tensors. Duan, Wu, and Zhou identified a loss in that organization: several fine constituents that can coexist inside one coarse block may be counted as though they had to be selected independently. Their asymmetric-hashing framework partially compensates for this combination loss. The paper's full second-power specialization improves the best bound obtainable from the square of the Coppersmith--Winograd tensor to ; see Section 6.3 and its parameter Table 2 in Duan--Wu--Zhou.
This mission isolates that second-power result. It is smaller than the paper's record-setting eighth-power calculation, but it contains the genuinely new asymmetric-hashing and hole-repair mechanisms in their first complete form. It therefore provides a focused bridge from the existing formalization of the classical square analysis to later combination-loss methods.
For a field , the matrix-multiplication tensor
encodes multiplication of an matrix by a matrix. A restriction applies one linear map to each tensor leg, while a degeneration permits polynomial families of such maps and takes their first nonzero coefficient. A degeneration from the diagonal tensor gives a border-rank upper bound of .
The Coppersmith--Winograd tensor with parameter is
It has border rank at most . Its coordinate partition has six supported types, and the square has fifteen coarse constituent types with . A large tensor power contains many blocks with prescribed joint and marginal type distributions. The laser method retains blocks whose variables are disjoint and interprets their direct sum through Schönhage's asymptotic sum inequality.
Duan--Wu--Zhou refine this organization by also retaining a split distribution for the fine indices inside each coarse constituent. Coarse - and -blocks are made unique, while compatible coarse triples may initially share a -block. The resulting partially damaged constituent tensors are described as broken copies of a standard-form tensor. The formal target uses , the full Section 6 construction, and the paper's released second-power parameters.
For every field ,
The source reports the stronger numerical endpoint , so the displayed rational inequality has strict slack. The Lean declaration has exactly the same field quantification and uses exactly the same matMulExp definition as the existing Coppersmith--Winograd mission; only the theorem name and rational endpoint change.
The mission first isolates the available-block shuffling interface extracted from Definitions 5.3--5.5 and Claims 5.8--5.10, then formalizes the finite covering core of the Hole Lemma 5.6. The subsequent tensor realization by zeroing and identification, the multiple-copy Corollary 5.11, the compatibility-rate identity of Lemma 6.7, the probabilistic part of Claim 6.8, and the global restricted-splitting value inequality in Equation (25) remain visible structural leaves rather than being hidden inside scalar assumptions. The numerical milestone instantiates Equation (25) with the exact data of Section 6.3 and Table 2 and checks a strict value surplus at . The structural proof must also make explicit the conversion from the paper's six-symmetrized value to a direct HasTauValueAtLeast witness for the mode-symmetric CW square. The final bridge applies the existing tau-value/rank machinery and transfers the Strassen-preorder exponent bound to matMulExp.
The mathematical result gives the first improvement over the classical Coppersmith--Winograd number while continuing to use only the tensor square. It separates improvement of the tensor analysis from improvement obtained merely by moving to a much higher tensor power. The same standard-form and restricted-splitting language is then reused by the paper's higher-power algorithm, which reports .
For formalization, the mission adds reusable infrastructure for nested tensor partitions. Existing CW-square work records coarse support types and actual matrix-multiplication restrictions. This mission extends that layer with fine split distributions, compatibility between levels, broken-block bookkeeping, and repair of holes without replacing tensor statements by unverified scalar values. Those definitions are prerequisites for later asymmetric-hashing, complete-split, and more-asymmetry analyses.
The bound is known mathematically and was published at FOCS 2023. The open work is a machine-checked reconstruction. The underlying CW tensor, border-rank certificate, canonical tensor-square grading, Salem--Spencer sets, direct-sum tau-value notion, asymptotic sum inequality, and exponent equivalence already exist on Prove2Me. The new frontier is the cross-level combination-loss analysis and its exact numerical specialization.
The central difficulty is that coarse and fine decompositions cannot be optimized independently. Two coarse triples may share a -block, and a fine -block can be useful for one triple, compatible with several, or removed by a collision. Counting all locally valuable fine constituents therefore does not certify a direct sum. Conversely, requiring every coarse -block to be unique discards precisely the combinations that produce the improvement.
The Hole Lemma must also preserve the actual tensor. A broken copy lacks some fine variable blocks; combining several such copies is useful only when a degeneration covers every required block with controlled loss and does not duplicate monomials. On the numerical side, the same-marginal maximum-entropy term and restricted-splitting values must be bounded with certified real inequalities. Floating-point output from MATLAB is evidence for a witness, not a Lean proof.
The mission uses the existing TensorObj, MMObj, restriction, degeneration, asymptotic-rank, HasTauValueAtLeast, matMulExp_strassen, and matMulExp declarations in environment 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Top-level results quantify over an arbitrary field. Finite supports and block indices are represented by finite types; probability and split distributions are nonnegative real functions of total mass one; entropy and numerical optimization live in the reals.
The formalization is restricted to for the capstone, although generic definitions and source lemmas may quantify over levels and finite index types. A valid proof must connect scalar rate inequalities to witnessed restrictions or degenerations yielding direct sums of concrete matrix-multiplication tensors. A constant-valued surrogate for the restricted-splitting value, a hypothesis that already assumes the desired exponent bound, or a certificate definition containing its own conclusion is outside scope.
Contributions are welcome for standard-form tensor encodings, finite permutation arguments, hole repair, type and split counting, entropy maximization certificates, certified logarithm and power inequalities, and the final tau-value/rank assembly. Statements should identify the corresponding definition, lemma, claim, equation, or table in the source.
Convex duality converts an optimization problem over points into one over linear functionals. It supplies lower bounds, certificates of optimality, and alternative formulations whose geometry can be simpler than the primal problem. In §§7.8–7.12 of David G. Luenberger's Optimization by Vector Space Methods, this theory is developed for finite-valued convex and concave functions on convex subsets of a real normed space. The capstone is Fenchel duality with restricted domains and an attained continuous-linear-functional dual optimum. This mission preserves that functional-analytic setting rather than reducing the theorem to Euclidean space or silently extending the functions to the whole space.
Let be a real normed space, let be nonempty convex sets, let be convex on , and let be concave on . For a continuous linear functional , the restricted convex conjugate and restricted concave conjugate are
The convex conjugate is admitted into only when its defining set is bounded above; the concave conjugate is admitted into only when its defining set is bounded below. Because and are nonempty and the functions are real-valued, these predicates exactly exclude the unwanted infinite endpoint. The Lean definitions use real sSup and sInf, with boundedness carried explicitly by theorem hypotheses.
The restricted epigraph of is the set of satisfying and ; the restricted hypograph of reverses the scalar inequality. Luenberger's qualification requires a common point of the relative interiors of and , represented by Mathlib's intrinsicInterior, and also requires ordinary nonempty interior of at least one of these two graph sets.
Assume the finite primal value is the greatest lower bound of
Prove that some attains
If attains the primal infimum, also prove that attains both conjugate extrema at : and .
The mission records four source milestones. A local minimum of a convex function on its convex domain is global (§7.8, Proposition 1). Convexity of a restricted function is equivalent to convexity of its restricted epigraph (§7.8, Proposition 2). The finite-conjugate domain and the convex conjugate are convex (§7.10, Proposition 1). Finally, a closed restricted epigraph agrees pointwise on with the continuous-linear biconjugate (§7.10, Proposition 2). Together these statements expose the geometric and conjugacy interfaces on which the capstone depends without turning every paragraph of the chapter into a separate item.
The theorem gives an attained dual certificate in an arbitrary real normed space. Equality of primal and dual values eliminates a duality gap, while attainment produces a specific functional that can certify an optimal primal point through simultaneous conjugate equality. The biconjugate milestone is independently useful: it expresses a closed convex function as a supremum of continuous affine minorants on its domain.
Formalizing this material adds a restricted-domain conjugacy API that is not supplied by the existing project artifact named fenchelConjugate. That artifact accepts finite-valued functions on a Euclidean space and has no independent convex domain or concave conjugate. Reusing it here would erase hypotheses that are central to Luenberger's theorem. The new definitions remain small, but their exact boundedness contracts make them reusable for later separation, minimax, and Lagrange-duality missions. The theorem is classical; the mission asks for a checked development faithful to the 1969 source and the current Mathlib representation of continuous dual spaces.
The qualification is not the usual finite-dimensional slogan that relative interiors merely intersect. The source additionally demands that either the restricted epigraph or restricted hypograph have nonempty ordinary interior. Dropping that condition changes the theorem in infinite-dimensional spaces. Replacing intrinsicInterior by topological interior would also make valid lower-dimensional domains appear empty.
Extended values create another boundary. Real sSup and sInf are meaningful here only together with nonempty domains and the respective boundedness hypotheses. Treating their default values outside those hypotheses as genuine conjugates would admit false dual candidates. A finite-dimensional conjugate definition avoids neither issue and would prove only a special case. The biconjugate target must quantify over continuous linear functionals, not all algebraic linear maps, because closed epigraph separation is topological. Finally, the dual statement must include actual attainment; proving only equality with a supremum would omit a principal assertion of §7.12.
All primal functions are finite-valued real functions. Infinite conjugate values are represented by domain predicates—BddAbove for and BddBelow for —rather than by changing the public conjugate codomain. The primal finiteness assumption is encoded by a real number together with IsGLB, which simultaneously rules out an empty feasible intersection and an infimum of . Epigraph pairs are ordered as to match Mathlib conventions, although Luenberger prints the scalar coordinate first.
The ambient space is normed but is not assumed finite-dimensional, reflexive, or complete. Both and are explicitly nonempty. The main theorem keeps the common intrinsic-interior condition and the disjunctive ordinary-interior condition verbatim. Contributions may develop separation lemmas, boundedness facts for restricted conjugates, or direct proofs of the milestone statements. A whole-space Euclidean specialization is welcome only as a corollary, not as a replacement for the root. The minimax theorem of §7.13 and extended-real lower-semicontinuous variants are outside this mission.
Every full-dimensional convex body is sandwiched between an ellipsoid and its -fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid about its centre by the factor lands inside the body,
and the factor is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes , exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum (, , ), the convex-combination step that produces the ball, and affine invariance.
A nonlocal game is played between a classical referee and two or more cooperating players who are not allowed to communicate during the game. In the two-player, one-round setting, the referee samples a pair of questions from a distribution , sends to Alice and to Bob, and receives answers and . The players win when a predicate accepts. Before the game begins they may agree on a strategy and share a resource, but after receiving their questions they are isolated from one another.
Nonlocal games occupy a useful interface between complexity theory and quantum information. From the perspective of complexity theory, they are the basic objects underlying multiprover interactive proofs: a verifier delegates a computation to separated provers and uses the consistency of their answers to distinguish valid from invalid claims. Classical two-prover games play a central role in the PCP theorem, hardness of approximation, and soundness amplification. Allowing the provers to share entanglement leads to the class and to a substantially richer theory. The theorem shows how dramatically entanglement changes this landscape: even estimating the entangled value of a nonlocal game can encode undecidable computation Ji--Natarajan--Vidick--Wright--Yuen 2020.
From the perspective of quantum information, nonlocal games are operational formulations of Bell experiments. A separation between classical and entangled values witnesses correlations that cannot be explained by a local hidden-variable model. The same framework supports self-testing, in which near-optimal behavior certifies the underlying state and measurements up to local equivalence, and device-independent cryptography, in which security or randomness is certified from observed input-output statistics rather than a trusted description of the devices. Representative references include Cleve--Høyer--Toner--Watrous 2004, Reichardt--Unger--Vazirani 2013, and Pironio et al. 2010. The survey of Palazuelos--Vidick 2016 describes further connections among nonlocal games, Bell inequalities, operator spaces, and quantum information.
Thus the value of a nonlocal game is simultaneously a complexity-theoretic soundness parameter and a quantitative measure of the power of nonclassical correlations. Understanding how this value changes under natural operations on games is important in both subjects.
We take the finite answer alphabets to be nonempty. In a classical strategy, Alice's answer depends only on , Bob's answer depends only on , and the players may coordinate using shared randomness. In a finite-dimensional entangled strategy, the players share a bipartite state and use POVM measurement operators
for their respective questions. The probability of producing answers on questions is
The supremum of the winning probability over all such finite-dimensional strategies is the entangled value . This optimization ranges over arbitrary local dimensions, shared states, and local measurements, which is one reason even apparently elementary questions about nonlocal games can be difficult.
For a positive integer , the repeated game consists of independently sampled copies of played simultaneously. Alice receives , Bob receives , and they answer with tuples and . They win only if
for every coordinate .
Parallel repetition is a basic method of soundness amplification. Starting from a game that dishonest players cannot win with certainty, the verifier repeats the test in the hope of driving the optimal success probability rapidly toward zero. The difficulty is that independence in the verifier's sampling does not force independence in the players' strategy. Alice may choose her entire answer tuple as a function of all her questions, Bob may do the same, and an entangled strategy may use a single state and joint measurements spanning all coordinates. In particular, one cannot obtain an upper bound on merely by analyzing the strategy that plays each coordinate independently.
For classical games, Raz's parallel repetition theorem gives exponential decay whenever the one-shot value is below one Raz 1998. Establishing the corresponding behavior for entangled games has been a long-running problem. A general polynomial bound was proved in Yuen 2016, implying for the first time that tends to zero for every finite two-player entangled game with .
The full exponential-decay theorem was recently settled by OpenAI. In Chapter 6 of Ten Advances in Mathematics and Theoretical Computer Science, OpenAI proves that for every finite two-player entangled game with , there is a constant such that
for every positive . OpenAI also released a Lean certificate for the result. This resolves the general quantum parallel-repetition conjecture, but it does not end the study of the problem. The proof introduces quantitative losses and a substantial technical apparatus, and there remains considerable value in finding alternative arguments, isolating the essential mechanism, improving the dependence on the one-shot gap and answer size, and producing shorter or more conceptual formal proofs.
This mission develops a reusable Lean framework for parallel repetition rather than formalizing only one paper. Its targets are organized by the strength of the asserted decay.
The main mission theorem is the fundamental asymptotic statement:
Equivalently, for every , all sufficiently large satisfy . This statement deliberately specifies no rate. It is a stable top-level theorem that can be recovered from any sufficiently strong quantitative bound.
A stronger target asks for game-dependent constants and such that
The abstract formulation avoids fixing a particular exponent or logarithmic correction. More refined formalizations can record explicit dependence on the gap , the answer alphabet, or other game parameters. Yuen's 2016 theorem is one important result at this level.
The exponential target asks for game-dependent constants such that
Following OpenAI's recent resolution, this target is now a theorem rather than an open conjecture. Within this mission it remains a central milestone: contributors may formalize the released argument in the mission's common interface, construct an independent proof, seek a more elegant or modular proof, or establish sharper quantitative variants.
These levels do not exhaust the project. The same framework can accommodate explicit finite- inequalities, stretched-exponential estimates, bounds for structured classes of games, improved parameter dependence, and reductions showing that one decay statement implies another.
The foundational Lean development represents a game by finite question sets , finite answer sets , a nonnegative normalized question distribution , and a Boolean verification predicate . The parallel-repetition theorems explicitly assume that and are nonempty. The development defines finite-dimensional entangled strategies using density matrices and POVM measurement operators, defines the repeated game on tuples, and takes the entangled value as a supremum over all finite-dimensional strategies. Repeated strategies are indexed by complete question tuples and are not required to factor coordinatewise.
A complete development will draw on formal libraries for finite probability, tensor products, positive semidefinite matrices, density matrices, POVMs, trace norms, fidelity, entropy, mutual information, and correlated sampling. These components should be formulated for reuse and should expose the dependence of each bound on the relevant game parameters.
The goal is both to verify parallel-repetition theorems and to build a dependable language for nonlocal games in Lean. Formalization forces distinctions that are easy to suppress on paper: whether constants depend on the game, whether a bound holds for all or only asymptotically, which strategy model is optimized over, and which hypotheses are needed for a particular rate. The mission welcomes reconstructions of known proofs as well as new, shorter, or conceptually different proofs.
Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For the logarithmic barrier
replaces the constraint ; the minimizers of over trace the central path, characterized by the KKT conditions (9.17): , , , , (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink , maintaining the proximity invariant
. The goal theorem is Theorem 9.7: with and a -close start, after iterations the algorithm reaches primal and dual feasible solutions with duality gap — the explicit form of the celebrated iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting by per step reaches gap within an explicit .
Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is
with symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid is contained in the explicitly constructed ellipsoid ,
and the volume contracts:
. Two integer-data estimates make the contraction decisive: every extreme point of with entries bounded by has coordinates in (Lemma 8.2), and a full-dimensional bounded such polyhedron has (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball of volume at most containing , with a lower bound on when is nonempty, the ellipsoid method correctly decides whether is empty within iterations — the explicit iteration count behind the polynomial-time headline.
Why do network linear programs return integer answers for free? This mission formalizes the structural theory of the minimum cost network flow problem of Chapter 7 of Bertsimas & Tsitsiklis: a directed graph with external supplies , arc costs , and the node-arc incidence matrix — an matrix in which every column has exactly one (start node) and one (end node) — so that flow conservation reads , forcing the standing assumption . Because the rows of sum to zero, the book works with the truncated matrix of the first rows. The combinatorial heart is the correspondence between algebra and graph structure: a set of arcs forming a tree determines a unique tree solution of , off (Theorem 7.3); connectedness makes full-rank (Corollary 7.1); and a flow vector is a basic solution if and only if it is a tree solution (Theorem 7.4). The goal theorem is the integrality theorem (Theorem 7.5): for the uncapacitated problem on a connected graph, every basis matrix has an integer inverse (its determinant is by the tree/lower-triangular argument), integer supplies make every basic solution integer, and integer costs make every dual basic solution integer — whence integer optimal primal and dual solutions exist whenever the optimal cost is finite (Corollary 7.2). This is the fountainhead of combinatorial integrality in linear optimization, feeding the max-flow min-cut mission that follows.
How does the optimal cost of a linear program respond when the problem data change? Chapter 5 of Bertsimas-Tsitsiklis studies the standard form problem (rows of linearly independent) as the requirement vector and the cost vector vary. On the convex set of feasible right-hand sides, and under the standing assumption that the dual feasible set is nonempty, the optimal cost is finite and convex (Theorem 5.1) — indeed over the extreme points of the dual feasible set, a piecewise linear convex function whose breakpoints are exactly where the dual optimum is non-unique. The capstone (Theorem 5.2) identifies the generalized gradients of : if the primal at is feasible with finite optimal cost, then is an optimal solution of the dual if and only if is a subgradient of at (Definition 5.1: for all ) — the precise sense in which dual variables are marginal costs. Dually (Theorem 5.3), the set of cost vectors with finite optimal cost is convex, the optimal cost is concave on , and near any with a unique primal optimum , is linear with gradient . Local ranging (Section 5.1) and parametric programming (Section 5.5) are the procedural companions, folded into the design notes.
Every linear programming problem has a shadow. To the primal we associate the dual , whose variables price the primal constraints: one dual variable per primal constraint and one dual constraint per primal variable, with signs governed by the correspondence of Table 4.1. This mission formalizes §4.1–4.5 of Bertsimas–Tsitsiklis: the dual of a general-form linear program, the involution "the dual of the dual is the primal" (Theorem 4.1), and weak duality for any primal-feasible and dual-feasible (Theorem 4.3) with its two corollaries — an unbounded primal forces an infeasible dual (Corollary 4.1), and feasible with are automatically both optimal (Corollary 4.2). The goal theorem is strong duality (Theorem 4.4): if a linear programming problem has an optimal solution, so does its dual, and the respective optimal costs are equal — proved in the book by running the simplex method with the lexicographic pivoting rule of Mission IV on a standard-form transform. The statement is deliberately the book's attainment form: by Table 4.2 the primal and the dual can be simultaneously infeasible (Example 4.5), so an unguarded equality of optimal values is false. The mission closes with complementary slackness (Theorem 4.5): feasible and are simultaneously optimal if and only if for all and for all — the certificate structure behind the dual simplex method and every LP optimality check.
How does one actually solve a linear program? Chapter 2 showed that if a standard-form problem subject to , has an optimal solution, it has an optimal basic feasible solution; the simplex method searches among basic feasible solutions, moving along edges of the feasible set in cost-reducing directions. This mission formalizes the mathematics of Chapter 3 of Bertsimas–Tsitsiklis: feasible directions, the reduced costs
measuring the cost rate along the basic directions, the optimality conditions of Theorem 3.1 ( implies optimality, and conversely at nondegenerate optima), the basis change of Theorem 3.2, and the pivot iteration itself — encoded as a predicate relating a basis/BFS pair to its successor, so that every theorem covers every pivoting rule. The goal theorem is Theorem 3.3: if the feasible set is nonempty and every basic feasible solution is nondegenerate, the simplex method terminates after a finite number of iterations, ending either with an optimal basis and an associated optimal basic feasible solution, or with a direction satisfying , , certifying optimal cost . The secondary capstone, Theorem 3.4, removes the nondegeneracy assumption: under the lexicographic pivoting rule every tableau row other than the zeroth stays lexicographically positive, the zeroth row strictly increases lexicographically, and the simplex method terminates on every problem — the anticycling guarantee that also supplies the optimal-basis existence used by the strong duality theorem of Mission V.
Every linear programming problem asks to minimize a linear cost over a polyhedron — a set of the form , or in standard form . Chapter 2 of Bertsimas–Tsitsiklis develops the geometry of these feasible sets, and its central achievement is making the intuitive notion of a "corner point" rigorous. There are three natural candidates: the extreme point — a point of that cannot be written as a convex combination of two other points of (purely geometric, representation-independent); the vertex — the unique minimizer of some linear cost over (geometric, via supporting hyperplanes); and the basic feasible solution — a feasible point at which linearly independent constraints are active (algebraic, the object the simplex method actually computes with). This mission formalizes polyhedra, active constraints, vertices and basic (feasible) solutions, and proves the fundamental Theorem 2.3: for a nonempty polyhedron all three notions coincide. Around the capstone sit the supporting pillars: polyhedra are convex (Theorem 2.1), the characterization of points pinned down by linearly independent active constraints (Theorem 2.2), finiteness of the set of basic solutions (Corollary 2.1), and the basis-column characterization of basic solutions in standard form (Theorem 2.4) — the combinatorial engine behind the simplex method of Chapter 3 and the root of the entire series.
A continuous piecewise linear (CPWL) function is one assembled from finitely many flat pieces glued along flat seams. Every ReLU network computes such a function, and every such function is computed by some ReLU network. Questions about how deep a network must be are therefore questions about the internal structure of CPWL functions.
In 1993 Breiman built such functions from hinges: maxima of two affine maps. Sums of hinges approximate anything, but from two dimensions up they fail to represent most CPWL functions exactly. Wang and Sun (2005) widened the maxima, proving that every CPWL function on ℝⁿ is a signed sum of maxima of at most n+1 affine maps. Twenty years on it remains the workhorse structural fact, reducing any question about a network to a question about a single max gate and underpinning every known upper bound on the depth of exact representation.
That includes the newest one: at STOC 2026, Bakaev et al disproved the short standing conjecture that ⌈log₂(n+1)⌉ hidden layers are necessary, showing ⌈log₃(n−1)⌉+1 suffice. In this mission we deliver a machine-checked proof of the Wang and Sun theorem so future formalizations of network expressivity can invoke it rather than reprove it. Note that we take as given the lattice representation of Tarela and Martínez, independently proved by Ovchinnikov, which writes any CPWL function as a max of mins of its affine pieces. That is the one external ingredient the argument consumes, and our definition of CPWL builds it in.
How quickly does the empirical mean of independent random variables concentrate around the true mean? This question is the analytic engine of the entire theory of stochastic bandits: every optimistic algorithm (Explore-Then-Commit, UCB and its relatives) is calibrated by a tail bound on the sample mean. This mission formalizes the subgaussian framework of Chapter 5 of Lattimore–Szepesvári's Bandit Algorithms: a random variable is -subgaussian when for all , and the Cramér–Chernoff method converts this moment-generating-function control into the exponential tail . The goal theorem is the Hoeffding-type bound: the sample mean of independent -subgaussian deviations exceeds the true mean by with probability at most , together with its confidence form — the exact bound every UCB index is built from. These few lines of analysis are cited by every regret bound in the series.
Multi-agent reinforcement learning approximates a global value function by summing per-agent local value functions learned independently — a trick that works surprisingly well in practice (ride-hailing dispatch, restless bandits) but had no general theoretical justification. Chen and Peng (arXiv:2506.02385) explain why: they define a Markov entanglement measure for the joint transition dynamics of a multi-agent MDP, directly analogous to quantum entanglement of a two-party state, and show it controls exactly how much error this value-decomposition trick incurs. This mission formalizes their sharpest quantitative bound (Theorem 4): the error of decomposing the global Q-function into per-agent local Q-functions is controlled, entrywise, by the agent-wise total-variation measure of Markov entanglement.
A platform sourcing items from monopolistic sellers with private quality cannot tractably maximize its true profit: the bundle revenue is neither monotone, submodular, supermodular, subadditive, nor superadditive. Theorem 4.6 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers shows that the simple surrogate threshold mechanism — maximize the linearized objective — is profit-optimal up to a factor in large markets. Prove it: Bernoulli concentration for the bundle quality plus sub-exponential control of the dispersion gap (Lemma 4.5).
A Hadamard matrix is a square array of +1s and −1s whose rows are mutually orthogonal — equivalently, one whose determinant attains the absolute maximum that Jacques Hadamard proved in 1893 any ±1 matrix can reach. The story opens earlier, with James Joseph Sylvester's 1867 doubling construction producing such matrices in every power-of-two order; Hadamard himself added orders 12 and 20. The conjecture bearing his name asserts that a Hadamard matrix exists for every order divisible by four. Raymond Paley's 1933 construction from finite fields settled vast new families, and computer searches filled stubborn gaps — beginning with order 92 at JPL in 1962 and reaching order 428 only in 2005, after which 668 became the smallest order whose existence is still unknown. Far from a curiosity, these matrices are workhorses of applied mathematics, underpinning error-correcting codes (the Reed–Muller code that sharpened Mariner spacecraft imagery), spread-spectrum and CDMA signal design, optimal statistical designs of experiments, and coded-aperture spectroscopy. Settling the conjecture would close a 130-year-old gap where combinatorics, number theory, and design theory meet.
Show that every nonconstant complex polynomial has a complex root.
A complete formal proof of Fermats Last Theorem for exponent 5: for all positive natural numbers a,b,c, a^5 + b^5 != c^5. The proof follows the classical Legendre-Dirichlet approach (1825-1830): Case 1 (5 does not divide a,b,c) is dispatched by congruences, and Case 2 (5 divides one of them) uses infinite descent through the ring Z[zeta_5]. The open hard leaf is the Z[zeta_5] PID step (flt5_zeta5_ring_witnesses).
Nearly every measure of Boolean function complexity was known to be equivalent — except sensitivity. Proving the conjecture unified the whole picture.