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 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?
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).
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.
All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph. It is a fundamental problem in graph algorithms and a fundamental problem in fine-grained complexity.
This mission formalizes a deterministic algorithm for APSP on directed -vertex graphs with polynomially bounded integer edge weights and no negative cycles, on a word RAM with -bit words. This is a truly subcubic bound and refutes the integer-weight APSP hypothesis in this model.
Theorem_22_APSP.This completed entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from 90 to 87. The goal is already proved in Lean on Prove2Me: for every real p ≥ 87, the foundation's cyclic constant K_p is the least constant that works for every triple of complex coordinate vectors in every finite dimension.
The statement includes arbitrary unequal-norm and zero triples, as well as dimension zero. It uses the foundation's unchanged definitions and combines admissibility with uniform optimality. This concerns complex diagonal matrices; it does not claim the corresponding result for general matrices or settle the conjecture for all p ≥ 2.
The campaign template is instantiated with value 87. Both items reference the existing accepted theorems.
The proof extends the accepted cutoff-90 Lean development by BrunoDCDO, adapting Ezzeri Esa's construction and analytic argument. The contributions at cutoffs 89, 88 and 87 were submitted by moona3k.
For p ≥ 88, the proof uses the accepted cutoff-88 result. On 87 ≤ p ≤ 88, it retains the localization, box-convexity and cyclic-averaging argument, with confinement parameter q₀ = 5351/15000, an improved cyclic witness (3/(4p))^(1/p), sharper Taylor estimates and exact rational polynomial certificates.
The foundation established cutoff 256; the supplied argument was formalized at cutoff 90. The subsequent accepted results extend the same formula to cutoffs 89, 88 and 87. This entry records the proved cutoff 87 on the campaign timeline; the campaign's cutoff-85 mission remains open.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the accepted cutoff-87 theorem already covers every , the new work is the range from 85 to 87.
The cutoff came down from 90 to 87 in a day, through moona3k's proofs at 89, 88 and 87. The 89 proof reran the cutoff-90 argument with sharper, second-order estimates. A numerical model of that argument with retuned constants puts its limit between about 86.6 and 87.5: two of its steps pull the same parameter in opposite directions, and below that point no setting satisfies both. So reaching 85 is expected to need a new idea, not just tighter numbers. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 85 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryTwo observers, Alice and Bob, share a quantum system. Alice performs some intervention (a measurement, possibly followed by discarding part of her apparatus) and Bob, somewhere else, performs his own. If the statistics of Bob's outcomes could depend on what Alice chose to do, Alice could send Bob a message through the shared system alone, and if the two interventions are spacelike separated this would be a signal faster than light. Quantum mechanics and special relativity coexist peacefully only because this does not happen: the no-communication theorem guarantees that Bob's marginal statistics are independent of Alice's intervention whenever the two interventions are "local" to different parts of the system.
The review article of Peres and Terno, Quantum information and relativity theory (Rev. Mod. Phys. 76, 2004), develops the operational toolkit of quantum information (Kraus matrices, positive-operator-valued measures, completely positive maps) in Sec. II.D and then derives, in Sec. II.E, a sufficient algebraic condition for the absence of instantaneous information transfer: all of Alice's Kraus matrices commute with all of Bob's (their Eq. (9)). This mission formalizes that derivation together with the facts about Kraus matrices and complete positivity that the same pages state.
A quantum state on a finite-dimensional Hilbert space is a density matrix : a positive semidefinite complex matrix with .
An intervention with outcomes is described by Kraus matrices , where the label ranges over a finite set indexing the subsystems discarded at the end of the interaction. When outcome occurs, the state is updated (Eq. (6)) to the unnormalized matrix
and the probability of outcome is . The matrices
(Eq. (8)) are the POVM elements; the intervention is complete when .
A map on matrices is positive if it sends positive semidefinite matrices to positive semidefinite matrices, and completely positive if , acting blockwise on matrices over , is positive for every ancilla dimension .
For the no-communication theorem, Alice's Kraus matrices and Bob's Kraus matrices act on the same finite-dimensional space. The probability that Bob obtains , irrespective of Alice's outcome, is (Eq. (10))
If for all , Alice's POVM is complete, and is a density matrix, then for every outcome of Bob
so all of Alice's operators disappear from Bob's statistics.
The no-communication theorem is the consistency check between quantum measurement theory and relativistic causality, and it is the starting point of the relativistic measurement theory developed in Sec. III of the review. The commutation condition (9) is exactly what local quantum field theory provides for spacelike separated regions, so this algebraic form is the one later used for microcausality arguments. The Kraus representation (milestones 4-5) is a basic structural theorem of quantum information theory, and the failure of complete positivity for transposition (milestones 6-7) underlies the partial-transpose entanglement criterion.
The results are classical and their proofs are known; the mission produces machine-checked versions on top of Mathlib's matrix library. The finite Kraus representation theorem (milestone 5) requires Choi-matrix machinery that is not, to the knowledge of this proposal, available in Mathlib in this form; it is reusable well beyond this mission.
The goal and milestones 1-3 and 8 are finite-dimensional trace manipulations; the care needed is in keeping the order of products right, using the adjoint of the commutation relation, and summing over indices in the correct order. Milestone 7 needs an explicit entangled witness on . Milestone 5 is the substantial one: the obvious approach of writing in a basis does not produce Kraus operators directly; a positivity argument (via the Choi matrix of and its spectral decomposition) is needed.
All Hilbert spaces are finite dimensional: matrices are indexed by arbitrary finite types with complex entries. Outcome sets and discarded-subsystem label sets are finite types; Alice's and Bob's label sets may depend on the outcome. Kraus matrices for the single-intervention milestones may be rectangular (), reflecting that the system after the intervention may differ from the original one; in the no-communication theorem both observers' matrices are square on a common space. The order on used for "nonnegative probability" is the standard partial order ( iff is real and nonnegative). Complete positivity quantifies over ancillas for every , with acting blockwise. Time reversal is encoded by the linear map ; on Hermitian matrices this coincides with complex conjugation, and only the linear extension gives a meaningful complete-positivity statement.
The goal keeps the hypotheses of the source setting (both POVMs complete, a density matrix); none of them can be dropped silently by a degenerate encoding, and the conclusion is an identity of complex numbers, so no hypothesis is vacuous: for instance, single-outcome trivial interventions with satisfy all of them.
Note: the sentence on p. 100 of the source claiming that commuting POVM elements are necessarily orthogonal projections is not included; as stated it fails (e.g. ).
Finding the quickest route between two points of a road network is among the oldest problems of operations research. It is the subproblem inside vehicle routing, network flow and many dynamic programs. Richard Bellman's four-page note On a routing problem (Quarterly of Applied Mathematics, 1958) treats it as a dynamic program. The minimal travel times satisfy a nonlinear system of equations, and that system can be solved by successive approximations that terminate after a number of steps bounded in advance. The iteration is now known as the Bellman–Ford method. A footnote added in proof records that Max Woodbury and George Dantzig had obtained the same scheme independently, and Ford's RAND report of 1956 describes a closely related labelling procedure.
Timeline.
There are cities, numbered . Every two of them are linked by a direct road, and city is the destination. The travel time from to is a real number ; the matrix need not be symmetric. Throughout, for .
A route from to is a sequence of cities in which consecutive cities differ. Its stops are , and its time is . The minimal time (3.1) is the least time of a route from to , and .
The routing equation (3.2) is the system
Approximation in policy space (§5) starts from the direct-route policy (5.2), , and iterates (5.1):
The second scheme (§7, (7.1)) starts instead from and uses the same step.
For every the following hold. Each is the minimal time from to , attained by a route. The vector solves (3.2). Every real solution of (3.2) equals :
This is the claim of the Summary ("converges after at most iterations") and of the last sentence of §5. The paper's bound is kept, although also suffices.
The result. The note turns an enumeration over exponentially many paths into rounds of minimisations each, with a bound fixed before the computation starts. The uniqueness theorem makes the routing equation a characterisation of the minimal times, not merely a property of them. This is the template for later correctness proofs of shortest-path and value-iteration algorithms. The monotone decrease (5.5) is the first instance of policy improvement: every iterate is the value of an actual routing policy.
Formalizing it. The results are classical and proved. What this mission adds is a machine-checked development against the paper's own objects. Routes, their times and minimal times are defined from scratch. The iteration is stated exactly as printed, apart from the corrected initial value at the destination. The (N − 1)-step termination is asserted as an equality, not a limit. Related platform items treat other methods and do not cover these statements. One is the label-correcting method (BertsekasDP.label_correcting_correctness_of_nonneg_arcs, BertsekasDP.label_correcting_terminates). Another is the stochastic shortest path problem under a termination assumption that fails for deterministic routing (BertsekasDP.ssp_main_theorem). There are also the generic candidate-list algorithm (BertsekasNetwork.generic_shortest_path_algorithm), Floyd's Algorithm 97 and Dijkstra's method.
The minimum in (3.2) may be attained at a whose own optimal route passes back through . The routing equation is a fixed-point equation for an operator that is monotone but not a contraction in any fixed norm. The standard contraction argument for discounted dynamic programs therefore does not apply. Uniqueness has to use to exclude zero-time cycles: with , the system (3.2) has infinitely many solutions. The bound depends on the at-most--stops reading of and on the fact that an optimal route never needs to revisit a city. Neither is visible from the recursion alone. For the scheme of §7, the page gives no bound on the number of iterations, and none holds uniformly in .
Cities are Fin (n + 1), so , with standing hypothesis . City is Fin.last n, and travel times are t : Fin (n + 1) → Fin (n + 1) → ℝ with for . Diagonal entries are unconstrained and never used. No symmetry, triangle inequality or integrality is assumed. A route is a list of cities with distinct consecutive entries ending at . Repeated cities are allowed; with positive times this changes no minimum. Minimal times are attained minima over routes (IsMinTime, IsMinTimeWithin), not real infima. The minimum in (3.2) is a Finset.inf' over all , the destination included.
The paper's loose phrases are made explicit as follows.
Two printed slips are corrected. (5.2) is printed for , which would set , and with statements (5.4), (5.5) and the goal would be false. The formalization uses , the value the paper's own justification needs. (7.1) prints "" for . Section 6 (computational aspects) and the closing expectation of §7 that the first method converges faster are not formalized.
The goal cannot be satisfied trivially. The minimal times are defined from routes, not as a solution of (3.2) or as a limit of the iteration, so the goal connects the recursion to the routing problem itself.
The development needs only finite minima, lists and induction; nothing beyond core Mathlib. The route and minimal-time layer is reusable for other deterministic shortest-path results. Proofs of any milestone are welcome, as are proofs of the sharper bound .
Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract notion of dependence that captures what linearly dependent columns of a matrix and cycles of a graph have in common. A distinctive feature of the paper is that it gives several independent axiom systems for the same structure: one in terms of rank, one in terms of independent sets, one in terms of bases, and one in terms of circuits (minimal dependent sets). It then proves they are interchangeable. These equivalences, now called cryptomorphisms, are what allow matroid theory to move freely between the algebraic picture (rank of a set of vectors) and the combinatorial one (cycles of a graph, minimal dependent column sets). Every textbook on the subject relies on them, for example J. Oxley, Matroid Theory, Chapter 1.
This mission treats one of them: the equivalence of Whitney's rank postulates (§2) and circuit postulates (§8). The circuit side is the one used in combinatorial optimization, where circuits appear as cycles in network flows, as minimal infeasible subsystems, and in the exchange arguments behind the greedy algorithm.
Let be a finite set of elements. For subsets we write for and for .
Rank system. A function assigning an integer to each satisfies the rank postulates if
With the number of elements of , the nullity is . An element is dependent on if . A circuit of is a minimal dependent set: a subset with such that for every proper subset of . In Lean these are IsRankSystem r, nullity r N, IsDependentOn r e N and circuitsOfRank r P.
Circuit system. A family of subsets, called circuits, satisfies the circuit postulates (§8, p. 516) if
(C₁) No proper subset of a circuit is a circuit.
(C₂) If P₁ and P₂ are circuits, e₁ is in both P₁ and P₂, and e₂ is in P₁ but not in P₂, then there is a circuit P₃ in P₁ + P₂ containing e₂ but not e₁.
In Lean this is IsCircuitSystem C for a predicate C : Finset α → Prop.
Rank from circuits. Whitney defines (p. 516):
Let e₁, ⋯, e_p be any ordered set of elements of M. Set Γᵢ = 0 if there is a circuit in e₁ + ⋯ + eᵢ containing eᵢ, and set Γᵢ = 1 otherwise (compare Theorem 5). Let the "rank" of (e₁, ⋯, e_p) be r(e₁, ⋯, e_p) = Σ_{i=1}^{p} Γᵢ.
In Lean, rankSeq C l is this sum for a list l, and rankOfCircuits C N is its value on the enumeration N.toList of a subset .
For every finite set :
where is the family of circuits of and is the rank defined from . This is Whitney's closing sentence of §8 (p. 517): "The definitions of rank and of circuits under the two systems (R), (C) agree, and hence the systems are equivalent."
The equivalence makes the circuit postulates a complete description of a matroid: everything stated about rank, nullity, independence and bases can be phrased through circuits and back. Downstream in the same paper, the fundamental sets of circuits of §9 (Theorem 9) and the binary-matroid characterization of the Appendix are stated in terms of circuits, and they depend on circuits and rank being interchangeable. Theorem 5, read on its own, expresses the nullity of a set as a count of circuit-closing steps. This is the abstract form of the fact that the cycle space of a graph has dimension equal to the number of non-tree edges.
On the formal side, Mathlib's Matroid is built on the base axioms and proves circuit elimination (Matroid.IsCircuit.strong_elimination) as a theorem about that structure. Whitney's own route is different: rank defined from circuits by an ordered sum of , with order-independence (Lemmas 7 and 8) as the central step. That route has no machine-checked version that we know of, on Prove2Me or elsewhere. This mission formalizes the 1935 argument as stated: the rank and circuit systems as Whitney wrote them, and the two translations between them.
The obvious definition of the rank of a set from its circuits enumerates the set and counts the elements that do not close a circuit with their predecessors. This definition depends on the enumeration, and nothing in , obviously prevents two orderings from giving different counts. Lemma 7, the swap of two adjacent elements, is where does real work, through a case analysis on which of the two swapped elements closes a circuit. In the other direction, for circuits of a rank function requires turning the local postulate into a statement about unions of two circuits. Defining the circuit rank as a maximum over orderings, or as the size of a largest circuit-free subset, sidesteps exactly the step the paper proves and is not this mission.
α with [Fintype α] [DecidableEq α]. The ground set is all of α, and subsets are Finset α. Whitney's matroid is a finite set .ℤ), so that is a true difference.N.toList. Its independence from the enumeration is Lemma 8, and the definition does not build it in.Matroid in the statements. Doing so would turn the equivalence into a library lemma. The statements are about Whitney's postulates on bare functions and predicates.The development needs only finite sets, lists and permutations from Mathlib. The definitions IsRankSystem and IsCircuitSystem can be reused for the other cryptomorphisms of the paper. Contributions are welcome on any milestone, and so are local helper lemmas, such as monotonicity of rank under – or invariance of rankSeq under prefix-preserving changes.
Mathlib/Combinatorics/Matroid/Circuit.lean (circuits of Mathlib's Matroid). https://github.com/leanprover-community/mathlib4Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets equipped with a rank function, or equivalently a family of independent sets, obeying a few postulates abstracted from the linear dependence of the columns of a matrix. The obvious first question about such an abstraction is whether it is genuinely more general than its model, that is, whether there are matroids that do not arise from any matrix. Section 16 of the paper answers it with a seven-element example, now called the Fano matroid , and proves that no real matrix corresponds to it.
The question has had a long life. Representability of matroids over a given field is a central theme of matroid theory: Tutte (1958) characterized the matroids representable over the field with two elements by a single excluded minor, the four-point line , and the regular matroids by three excluded minors, , and its dual; and Seymour's decomposition of regular matroids (1980) rests on the same objects. Whitney's §16 is the starting point of this line: the first proof that the abstract postulates admit matroids outside linear algebra over .
Timeline:
Let be an matrix with columns . For a set of columns, let be the rank of the submatrix formed by those columns. Regarding the columns as abstract elements gives a matroid on with rank function : the matroid of . A matroid corresponds to if it is the matroid of , with elements matched to columns.
A circuit of a matroid is a minimal dependent set. For a circuit of the matroid of , there are numbers with for every row , and exactly for ; the set of such vectors is written when only the support condition is meant. Stacking one such row per circuit gives the circuit matrix of , determined up to nonzero factors on its rows.
A fundamental set of circuits of a matroid with nullity ( the number of elements) is a family of circuits with such that the elements can be ordered with and for ; it is strict if for every .
The matroid of §16 has elements ; its bases (maximal independent sets) are all three-element sets except
The number of rows is arbitrary; the existence clause makes the non-existence statement non-vacuous.
The result. The theorem separates the abstract notion of matroid from linear dependence over : some matroids are not real-representable. It also exhibits that representability depends on the field, because the same matroid is the matroid of a matrix over the integers mod 2 (milestone 8). Everything later written about representability over particular fields, excluded-minor characterizations, and the gap between abstract and linear matroids starts from this distinction. Theorem 32 is of independent interest: it translates statements about circuits of a represented matroid into the vanishing of minors of a normalised circuit matrix.
Formalizing it. The result is classical and its proof is short on paper, but it is not formalized in Mathlib, which has matroids (Matroid, circuits, ranks) but no column matroid of a matrix with a rank-of-submatrix characterization, no circuit matrix, and no Fano matroid. The mission produces those objects and the bridge lemmas (Theorem 29, Lemmas 10–11, Theorem 32) that connect matroid circuits with linear algebra of the circuit matrix. No machine-checked proof of the non-representability of the Fano matroid over in Lean is known to the curators.
The obvious attempt is a direct search: suppose a real matrix has as its matroid and derive a contradiction from the seven dependent triples. This does not work as stated. Each rank condition is a determinantal (nonlinear) condition on the entries, the number of rows is unbounded, and a representation is determined only up to row operations and column scalings, so there is no finite case check and no single linear computation that settles the question. The contradiction has to come from an argument that is invariant under these symmetries, and the milestones (circuit vectors determined up to scaling, fundamental sets spanning, circuits detected by minors) are what such an argument needs to be stated in. The field also matters: the argument must use that in , since over a field of characteristic 2 the statement is false (milestone 8).
Matroids whose ground set is the whole (finite) type. The Fano matroid lives on Fin 7, Whitney's element being k - 1; the seven triples are written out literally. Matrices are Matrix (Fin m) ι K; "the matroid of " means: ground set everything, and the rank M.eRk N of every finite set of columns equals Matrix.rank of the column submatrix.Fin t with , and determinants are of square submatrices in the paper's row and column order.Reusable beyond this mission: the matroid of a matrix over a field, the circuit matrix, fundamental sets of circuits, and the Fano matroid. Contributions welcome: proofs of the milestones, and a proof of the goal by any route, including one that does not go through Theorem 32.