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?
The minimum-cost circulation problem is a central problem of network optimization: transportation, assignment, shortest-path and maximum-flow problems are all special cases, and it is one of the few classes of linear programs with fast combinatorial algorithms. The oldest algorithm for it, the cycle-canceling algorithm of Klein (1967), repeatedly finds a residual cycle of negative cost and pushes as much flow as possible around it. With an arbitrary choice of cycle it can take exponentially many iterations even on integer data, and it need not terminate at all when capacities are irrational.
Goldberg and Tarjan (J. ACM 36(4), 1989) showed that one simple selection rule repairs this: always cancel a residual cycle whose mean cost (cost divided by number of arcs) is as small as possible. The resulting algorithm is strongly polynomial: its number of iterations is bounded by a polynomial in the number of vertices and arcs alone, independent of the magnitudes of capacities and costs. This mission formalizes that bound.
Timeline:
A circulation network is a finite directed graph with vertices and arcs, which is symmetric ( iff , so counts both directions), together with real capacities and real costs , the cost being antisymmetric: .
A circulation is a real function on arcs satisfying , on every arc, and conservation at every vertex . Its cost is , and is minimum-cost (optimal) if no circulation has smaller cost.
The residual capacity of an arc is ; arcs with are residual arcs. A residual cycle is a simple cycle of residual arcs; its capacity is the minimum residual capacity along it, its cost is the sum of its arc costs, and its mean cost is . Canceling a residual cycle raises the flow on each of its arcs by its capacity (and lowers the flow on each reverse arc by the same amount).
The minimum-mean cycle-canceling algorithm starts from any circulation and, while some residual cycle has negative cost, cancels a residual cycle whose mean cost is minimum among all residual cycles. Ties are broken arbitrarily, so the algorithm is a nondeterministic process; a run of length is any sequence of circulations produced by such iterations.
The analysis uses a price function , the reduced cost , and ε-optimality: for , is ε-optimal if some gives on every residual arc. The quantity is the least such , and an arc is ε-fixed if all ε-optimal circulations carry the same flow on it.
For every circulation network with vertices, arcs, arbitrary real capacities and arbitrary real antisymmetric costs, every run of the minimum-mean cycle-canceling algorithm has length
The statement quantifies over all starting circulations, all tie-breaking choices and all real data; it is the paper's with the constant its proof establishes.
In the order the proof uses them: Theorem 2.1 (optimal iff no negative residual cycle), Theorem 3.1 (optimal iff some price function has on residual arcs), Theorem 3.3 ( for nonoptimal , where is the minimum cycle mean of the residual graph), Lemma 3.5 (a minimum-mean cancellation does not increase ), Lemma 3.6 ( cancellations shrink by a factor ), and Theorem 3.8 (an arc with is ε-fixed).
Theorem 3.9 shows that a classical, natural algorithm is strongly polynomial: its iteration count depends only on the combinatorial size of the network. Combined with Karp's minimum-mean cycle algorithm it yields an strongly polynomial algorithm (Theorem 3.10), and its method, measuring progress by the minimum cycle mean and fixing arcs once is small, underlies the faster cancel-and-tighten algorithm of Section 4 and later strongly polynomial analyses of network-flow and related algorithms.
The theorem has been proved since 1989; this mission's contribution is a machine-checked proof. To the best of the platform's catalogue, no cycle-canceling bound, minimum cycle mean or ε-optimality statement has been formalized. The platform does hold the negative-cycle optimality criterion in a different model (LinearOptimization.network_no_negative_cycle_optimal, Bertsimas–Tsitsiklis Theorem 7.6, with nonnegative flows and supplies) and a flow decomposition theorem (LinearOptimization.network_flow_decomposition); both are related to milestones here but are stated for a different network model.
The obvious potential function, the cost of the circulation, decreases at every iteration but by amounts that depend on the data, so it yields no bound independent of the capacities and costs. The analysis instead has to track , an infimum over price functions, and relate it to the minimum cycle mean of a residual graph that changes after each cancellation, including arcs that appear only because of earlier cancellations. The strongly polynomial part needs a second ingredient: showing that the flow on some arc never changes again, which requires comparing the current circulation with all other ε-optimal circulations of the network, not only those the algorithm visits.
Vertices form a finite type V; the arc set is E : Finset (V × V); capacities, costs and flows are real functions V → V → ℝ read only on E. is Fintype.card V and is E.card, counting and separately, as in the paper. Cycles are nonempty duplicate-free vertex lists, whose arcs are the cyclically consecutive pairs; one- and two-vertex cycles are allowed and have cost . Minimum mean is taken over all residual simple cycles of the current circulation. is an infimum (sInf) over a set that is nonempty and bounded below for every circulation; its attainment is to be proved, never assumed.
Explicit constants replacing the paper's :
"Terminates after at most iterations" means that every run has length at most . Asserting only that some run is short, or that the process eventually stops, does not formalize the theorem; nor does a step relation that drops negativity, simplicity of the cycle, minimality of the mean over all residual cycles, or the update by exactly the cycle's capacity.
A complete development needs cycle decomposition of the difference of two circulations, LP duality for circulations (Theorem 3.1), and bookkeeping for the residual graph under cancellation. These are reusable for any cycle-canceling or cost-scaling analysis, and contributions of that infrastructure as separate lemmas are welcome. Theorem 3.7 (the integer-cost bound) and Section 4 are outside this mission.
Average-cost criteria are standard in inventory, queueing and maintenance models that run indefinitely. For a Markov decision process (MDP), the central object is the average-cost optimality equation (ACOE). It couples a constant (the optimal long-run cost per period) with a relative value function . A stationary policy that attains the minimum in the ACOE is average-cost optimal. When the state space is uncountable, the one-step cost is unbounded and the transition probability is only weakly continuous, the ACOE is not automatically available.
Feinberg, Kasyanov and Zadoianchuk (2012) proved that under their Assumptions W* and B the weaker average-cost optimality inequality (ACOI) holds. For setwise continuous transition probabilities, Hernández-Lerma and Lasserre (1996, Theorem 5.5.4) gave conditions for the ACOE via equicontinuity. Feinberg and Lewis (2015) established the ACOI and optimality of policies for periodic-review inventory control with setup costs and general demand. Feinberg and Liang (2022, online 2017) extended the equicontinuity condition to weakly continuous transitions and used it to show that the inventory problem satisfies the full equation, not just the inequality.
An MDP has a state space and an action space (Borel subsets of Polish spaces). It has a one-step cost , bounded below, and a transition probability . A policy chooses actions from the observed history, possibly at random. A stationary policy is a measurable map . For a discount factor :
The average cost of a policy is , and . Set . For a sequence , define
Assumption EC for has two parts:
The inventory problem has inventory level (negative means backlog) and order quantity . Inventory evolves by , with i.i.d. nonnegative demands . The cost is
with setup cost , unit cost , and convex with as . Let and . A function is -convex if for and . An policy orders up to whenever the inventory is below .
For every sequence of nonnegative discount factors with , the inventory MDP satisfies Assumption EC. Along a subsequence, , and some stationary satisfies
Moreover:
The ACOE is stronger than the ACOI. It identifies the optimal actions of an average-cost problem as the minimizers of a one-step lookahead with , and it makes a genuine relative value function: is the pointwise limit of the discounted relative values along a subsequence. For inventory control, Theorem 4.5 gives three further conclusions:
The results are proved in the paper, and in the cited works of Feinberg and coauthors for the cited milestones. None is formalized. There is no formal library of MDPs on Borel spaces with history-dependent randomized policies. This mission builds that layer (strategic measures via Ionescu Tulcea, discounted and average costs, Assumptions W*, B and EC) and states the general ACOE theorem on it. A proof of the goal would also require formal proofs of the cited inventory results of Feinberg–Lewis (2015) and Feinberg–Liang (2017a), which are milestones here.
One obvious route is to pass to the limit in the discounted optimality equation . After subtracting , this needs two things: convergence of , and exchanging limit and integral. Pointwise lower limits give only the inequality (ACOI). The reverse inequality needs actual convergence of a subsequence and a dominating function. For weakly continuous , convergence of additionally requires uniform convergence on compacts, which is where equicontinuity enters.
For the inventory problem the hard step is equicontinuity itself. The functions are not uniformly Lipschitz. It must be shown that costs from two nearby starting inventories stay close uniformly in . This comparison runs through the time until inventory falls below the reorder point, and it is controlled by renewal-theoretic bounds on the number of demand arrivals.
The Lean development lives in the namespace FeinbergLiang.ACOE. It commits to the following conventions.
Kernel.trajMeasure. They are never defined as solutions of an optimality equation.α 0.Equicontinuous, applied to the real values of together with their finiteness.atTop ×ˢ 𝓝 x.TendstoUniformlyOn on every compact set.Contributions welcome: proofs of the milestones, especially the general Theorem 3.2 and the renewal estimates behind Lemmas 4.6–4.7. The Borel-space MDP definitions are reusable by later average-cost and discounted MDP missions.
In stochastic linear optimization under bandit feedback a learner repeatedly chooses a point from a compact decision set and observes only the random cost of that point, whose mean is for an unknown vector . The problem models online routing, ad placement and other sequential decisions with linearly structured costs. The quality of a learner is measured by its regret against the best fixed decision.
For the -armed bandit the achievable regret for a fixed instance is logarithmic in the horizon (Lai and Robbins 1985; Auer, Cesa-Bianchi and Fischer 2002). Dani, Hayes and Kakade (COLT 2008) showed that for linear costs the picture depends on the geometry of . Their Theorem 1 gives polylogarithmic regret when the decision set has a positive gap between the best and second-best extreme point (a polytope, for instance), and their Theorem 2 gives regret for every decision set. Their Theorem 3 shows that the second rate cannot be improved in general: on a decision set with zero gap, every algorithm pays in expectation.
Timeline:
The decision set is the unit circle . An unknown mean vector is drawn once, uniformly from the circle of radius ; concretely with uniform on .
On each round the algorithm plays and observes a cost with , so that . Given the decision, the cost is independent of the past.
An algorithm may be randomised. It draws a seed once from a probability measure on a measurable space , and chooses as a function of and the costs observed so far, measurably in .
The regret over rounds is
so each round costs when . The expected regret averages over the seed, the prior and the costs.
In the Lean development these objects are unitCircle, meanVec, optCost, RandomizedPolicy and expectedRegret in the namespace StochLinOpt.LowerBound.
There is a universal constant such that for every randomised algorithm and every ,
The constant is left existential, which is the form that survives any later improvement of the constant; it is chosen before the algorithm and before .
The lower bound shows that the dependence of the problem-independent upper bound (Theorem 2 of the same paper) is necessary. It also shows that the gap-dependent polylogarithmic rate of Theorem 1 cannot extend to decision sets without a gap, such as the sphere. Together with the upper bound it characterises the minimax regret of stochastic linear bandits in up to logarithmic factors, and in the paper's general- form it also underlies the claim that the price of bandit information is .
The result is proved in the paper for and has not been machine-checked. The mission produces a checked Bayesian lower bound over all randomised algorithms, with an explicit probability model for the protocol. Two related platform results are different theorems: BanditAlgorithm.linear_bandit_unit_ball_minimax_lower_bound (Lattimore–Szepesvári Theorem 24.2: unit ball, Gaussian noise, a worst-case ) and BanditAlgorithm.linear_bandit_hypercube_minimax_lower_bound (Theorem 24.1: hypercube). The costs, the circle and the uniform prior used here are not covered by either.
The obvious attempt is a two-point change-of-measure argument with a fixed pair of means at distance . It fails as stated because the decision set has no gap: an algorithm that plays close to the optimum of both candidates learns slowly but also pays little. The per-round trade-off between regret and information (Lemma 15) is exact only while the posterior is undecided, . Turning it into a bound on the whole horizon requires controlling how long the posterior stays undecided, which is a statement about a martingale whose step sizes are chosen by the algorithm; a concentration bound that ignores the accumulated conditional variance (Azuma–Hoeffding with worst-case steps) is too weak for this. The averaging step from a two-point prior to the uniform prior on the circle is also part of the formal work.
Vectors are Fin 2 → ℝ with the dot product ⬝ᵥ; Euclidean norms are written through dot products, never with Lean's sup norm. Rounds are 0-indexed internally: the Lean index is the paper's round . The expected regret is the exact finite expectation
so no infinite product of measures is needed. A randomised algorithm is a seeded policy, which covers every randomised algorithm. The optimal cost is the infimum of over the compact circle and is attained. Every junk value in the model (a non-integrable integrand) could only make the lower bound harder to prove, never easier.
A statement over deterministic algorithms only, over a worst-case instead of the uniform prior, or with the constant allowed to depend on the algorithm or on would be a weaker theorem. The goal quantifies before the algorithm and , and fixes the prior.
Corrections relative to the printed paper:
Welcome contributions: a Lean proof of Freedman's inequality (reusable across the bandit and concentration missions on the platform); the averaging argument from two-point priors to the uniform prior; and the stopped-martingale bookkeeping for the bias sequence.
Many combinatorial optimization problems are linear programs over a polytope whose vertices are the zero–one incidence vectors of the feasible objects: matchings, stable sets, spanning trees. The edges of such a polytope (pairs of vertices joined by a one-dimensional face) govern the behaviour of the simplex method and of local-search procedures, which move from vertex to vertex along edges: a pivot of the simplex method on a nondegenerate basis replaces a vertex by one of its neighbours.
In December 1971 M. L. Balinski asked when two matchings of a graph are neighbours on the matching polyhedron determined by Edmonds (Edmonds 1965). V. Chvátal answered a more general question in §6 of On certain polytopes associated with graphs (Chvátal 1975): he characterized the neighbours on the stable set polytope of an arbitrary graph. Since matchings of are the stable sets of the line graph , Balinski's question is the special case of line graphs (Corollary 6.3 of the paper).
Let be a finite undirected loopless graph. A stable set is a set of vertices no two of which are adjacent. denotes the set of all zero–one vectors such that is stable, and the stable set polytope is
For the corresponding stable set is .
For an integer-valued vector write . Two vectors are neighbours in if there is an integer-valued such that and are the only two vectors which maximize over ; in particular . This is the definition the paper states at the start of the proof of Theorem 6.2.
A bicoloration of a graph is a partition , , such that every edge joins to . Every tree has one.
In the Lean development these objects are stableVectors G (), stablePolytope G (), onesSet y (), AreNeighbors G y z and IsBicoloration T B R, all in the namespace ChvatalPolytopes.Neighbors.
For with corresponding stable sets ,
For a tree with a bicoloration there are nonnegative integers () and with
with equality exactly when is the incidence vector of or of .
If is connected with spanning tree , and (), are as in Lemma 6.1 for , extend by on and outside . Then
with equality if and only if or .
Theorem 6.2 describes the 1-skeleton of the stable set polytope of every graph by a condition that can be checked in linear time, although optimizing over is NP-hard in general and no complete linear description of is known for general graphs. Through line graphs it gives the adjacency criterion for the matching polytope (two matchings are neighbours if and only if their symmetric difference is a single path or cycle), which settled Balinski's question. Characterizations of this type underlie the analysis of simplex-type and pivoting algorithms on combinatorial polytopes and the study of their diameters.
The result has been proved since 1975. The mission asks for a machine-checked proof of the theorem as stated in the paper; no formal proof of Theorem 6.2 or of the matching-polytope corollary is known to exist on Prove2Me or in Mathlib. The two milestones isolate the constructive half (Lemma 6.1 and the weighting built from it), which is reusable for any statement that needs an explicit objective singling out two stable sets.
The "only if" direction and the equality analysis are elementary; the substance lies in the "if" direction. An objective that makes both and optimal is easy to write down, for example ; the difficulty is to make them the only optimal vectors. Any stable set that agrees with on some connected pieces of and with on others ties with and under naive weightings, so the weights on must be chosen so that every mixed choice loses strictly. The integrality requirement on and the need to control all of , not only the stable sets contained in , rule out a direct perturbation argument.
SimpleGraph V; loops and multiple edges are excluded, as in the paper.V → ℝ of stable finsets; is convexHull ℝ (S G).G.induce of the set , and "connected" is Mathlib's SimpleGraph.Connected, which requires at least one vertex. For both sides of the goal are therefore false.SimpleGraph.IsTree, which includes connectedness; a spanning tree of is a graph on the vertex set of with and T.IsTree. In Lemma 6.1 the integers and are natural numbers.A trivializing formalization — defining neighbours through the symmetric-difference condition or through Lemma 6.1's certificate, or omitting from the definition — is excluded: neighbours are defined only through unique maximizers of integer objectives over .
A complete development needs only finite graphs, induced subgraphs, spanning trees of connected graphs (available in Mathlib) and finite sums. Contributions welcome beyond the milestones: the equivalence of this notion of neighbours with the one-dimensional faces of , and Corollary 6.3 for the matching polytope via line graphs.
The stability number of a graph, the largest number of pairwise non-adjacent vertices, is the optimum of an integer program over the stable set polytope . Linear programming duality turns any explicit linear description of into a certificate of optimality for , which is why the question "which inequalities are needed to describe ?" has been central to polyhedral combinatorics since Edmonds' description of the matching polytope (Edmonds 1965). Chvátal's 1975 paper (doi:10.1016/0095-8956(75)90041-6) initiated the systematic study of for arbitrary graphs: which graph operations preserve a known description, and which inequalities are facets, i.e. indispensable in every description.
Section 4 of the paper treats one such operation, gluing two graphs along a complete subgraph, and one family of facets, the "rank" inequality for graphs whose critical edges connect all vertices. Combining the two yields a purely graph-theoretic fact about -critical graphs (graphs in which deleting any edge increases the stability number): no complete subgraph separates such a graph. The fact is due to Berge (Graphes et hypergraphes, 1970, Ch. 13, §3, Corollary 2); Chvátal's derivation obtains it from polyhedral arguments. -critical graphs were studied by Erdős and Gallai, Hajnal, Andrásfai and Lovász, and their structure is closely tied to the facets of .
Graphs are finite, undirected and loopless: . A stable set is a set of pairwise non-adjacent vertices; is the largest size of a stable set. The incidence vector of is with for and otherwise. is the set of incidence vectors of stable sets and
A finite system is a defining linear system of if its solution set is exactly . An inequality is a facet of if every defining linear system of contains, for some , the inequality .
An edge of is critical if ; denotes the set of critical edges, , and is -critical if every edge is critical. For graphs , put and . A vertex set is a cutset of if two vertices outside are joined by no path of , the subgraph induced on .
In Lean, all objects live in the namespace ChvatalPolytopes.Separation: stablePolytope G, IsFacet P a b, IsCriticalEdge, criticalGraph G (for ), IsAlphaCritical G and IsCutset G K.
For a finite connected -critical graph and any inducing a complete subgraph,
The goal is pure graph theory; its proof in the paper consists of the two polyhedral theorems below.
is a facet of .
Theorem 4.1 says that clique-sums are harmless for linear descriptions of : a description of a graph glued along a clique is the union of descriptions of the pieces. It underlies the later decomposition theory of stable set polytopes (clique cutsets appear throughout the study of perfect and -perfect graphs). Theorem 4.2 supplies a large class of facets with a combinatorial certificate, and was the starting point of the study of rank facets. Corollary 4.3 illustrates how polyhedral statements yield structural graph theory: the facet in Theorem 4.2 cannot coexist with a clique cutset.
All three results are proved in the paper, and Berge's corollary was known before it. None of them has, to the knowledge of this mission, a machine-checked proof; Mathlib has stable sets (IsIndepSet, indepNum), cliques and convex hulls, but no stable set polytope, no notion of facet via defining systems, and no -critical graphs. The mission produces these definitions and the formal proofs of Proposition 2.1, Theorems 4.1, 4.2 and Corollary 4.3.
Proposition 2.1 requires LP duality in the form "min = max with both optima attained" together with a separation argument that reduces arbitrary objectives to integral ones; the "if" direction fails without the nonnegativity rows, so the statement is sensitive to the exact form of the system. In Theorem 4.1 the inclusion (solutions of the union) is routine; the difficulty is the converse: a point whose restrictions lie in and in is a convex combination of stable sets on each side, and the two combinations have to be matched on the clique to produce stable sets of . Theorem 4.2 concerns every defining linear system, so it cannot be proved by exhibiting one description; the natural route via "affinely independent tight points" is a different definition of facet and needs full-dimensionality of to be equivalent. Finally, the goal requires translating a cutset into a decomposition with complete intersection, and then showing that a union of two systems on smaller vertex sets cannot contain a positive multiple of .
SimpleGraph V on a Fintype V with DecidableEq V. is a set of functions V → ℝ (incidence vectors of stable finsets), and is convexHull ℝ (stableVectors G).IsFacet quantifies over all finite index types J : Type and all real systems whose solution set equals the polytope; it is the paper's definition, not the affinely-independent-points characterization.Connected, which requires — for the statement would be false. is indepNum, cast to .G.IsClique K, not only maximal cliques (the paper reserves "clique" for maximal complete subgraphs, but the corollary speaks of complete subgraphs), including . "Cutset" means two vertices outside joined by no path of . The formalization " is not connected" is ruled out: under Mathlib's convention it would make a cutset and the statement false for and .Many combinatorial optimization problems ask for the best subset of a finite set subject to combinatorial side conditions. The polyhedral method replaces the finite family of feasible subsets by the convex hull of their incidence vectors and asks for an explicit system of linear inequalities describing that convex hull; once such a system is known, linear programming duality gives min–max theorems and certificates of optimality. The maximum weight stable set problem is the central test case: it is NP-hard in general, so no tractable complete description of its polytope is expected for all graphs, and the question becomes for which graphs a simple description suffices.
V. Chvátal's 1975 paper On certain polytopes associated with graphs answers this question for the two simplest families of valid inequalities, and its Section 3 connects the answer to Berge's perfect graphs. The result is a standard entry point to polyhedral combinatorics and is one of the ingredients behind the later polynomial-time algorithms for stable sets in perfect graphs by Grötschel, Lovász and Schrijver.
Timeline. Berge (1961) introduced perfect graphs and conjectured that a graph is perfect if and only if its complement is. Lovász (Normal hypergraphs and the perfect graph conjecture, Discrete Math. 1972; A characterization of perfect graphs, J. Combin. Theory Ser. B 1972) proved this, together with the characterization of perfection by and the invariance of perfection under vertex duplication. Fulkerson's theory of antiblocking polyhedra (1971–72) gave a polyhedral route to the same equivalence. Chvátal (received 1972, published 1975) gave the self-contained polyhedral statement formalized here, with a proof based on Lovász's two theorems.
A graph is finite, undirected and loopless. A stable set is a set of vertices no two of which are adjacent. A clique is a maximal complete subgraph, and is the set of vertex sets of the cliques of .
is the set of zero–one vectors such that is stable, and the stable set polytope is . A finite system of linear inequalities is a defining linear system of if its solution set is exactly . For write .
is perfect (the paper's -perfect) if for every zero–one vector ,
For , is the induced subgraph, its stability number and its clique number. To duplicate a vertex is to add a new vertex adjacent to all neighbours of but not to .
In the Lean development these are stableVectors G, stablePolytope G, maximalCliques G, IsPerfect G and duplicate G u in the namespace ChvatalPolytopes.Perfect.
For every graph , the system
is a defining linear system of if and only if is perfect. Both directions are required.
The result. The nonnegativity and clique inequalities are valid for for every graph. Theorem 3.1 says they are complete exactly for perfect graphs, so on perfect graphs the maximum weight stable set problem is a linear program over an explicitly described polytope, and weighted min–max theorems (stable sets versus clique covers) follow from LP duality. Combined with the perfect graph theorem, it gives a polyhedral characterization of perfect graphs, and it is the model for later results that identify graph classes by the facets of their stable set polytopes (odd-cycle inequalities, -perfection, Section 7 of the same paper).
Formalizing it. The result is classical and proved. No machine-checked version of it is known, and Mathlib has neither perfect graphs nor stable set polytopes. The mission produces a formal statement of the polyhedral characterization with the paper's own notion of perfection, a formal version of the convex-hull/LP min–max principle (Proposition 2.1), which is reusable for any 0–1 polytope, and formal statements of the two theorems of Lovász that the proof relies on.
Proposition 2.1 reduces Theorem 3.1 to the equivalence of perfection with a fractional min–max for all integer weights. The obvious approach to that equivalence fails in both directions. From perfection one only gets the min–max for zero–one weights and zero–one multipliers; general integer weights do not reduce to zero–one weights by linearity, because the minimum over clique covers is not additive in . Conversely, a fractional clique cover of value does not directly produce an integral one. The paper crosses this gap with two theorems of Lovász: a numerical certificate of nonperfection, and the invariance of perfection under vertex duplication. Both are substantial graph-theoretic results in their own right, and neither follows from the definitions by routine manipulation.
Proposition 2.1 itself needs separation of a point from a polytope by an integral objective and LP strong duality with the nonnegativity rows handled separately.
Vertices form a finite type V with decidable equality; a graph is a SimpleGraph V. is a set of functions V → ℝ, and is Mathlib's convexHull ℝ of it. is the finset of finsets that are maximal among cliques (Maximal), as on the page; with the only maximal clique is . "Defining linear system" is an equality of sets. Every "max = min" is written out in full: there is a value that is the maximum over (attained and an upper bound), some feasible multiplier vector attains , and every feasible multiplier vector has objective at least . Clique multipliers are functions Finset V → ℝ read only on .
Explicit conventions and added hypotheses:
indepNum and cliqueNum (natural numbers) of G.induce A.Option V, with none the new vertex.Perfection is the paper's zero–one min–max, not "the clique system defines " (which would make the goal a tautology) and not Berge's (a different definition, equivalent only through the perfect graph theorem). is the convex hull of , never the solution set of an inequality system.
Needed infrastructure, all reusable: integral separation from a rational polytope and LP strong duality in the form ; basic facts about stable sets and maximal cliques of induced subgraphs and of duplicated graphs; invariance of IsPerfect under graph isomorphism and under taking induced subgraphs. Proofs of the Lovász milestones, which have independent value for a Mathlib theory of perfect graphs, are welcome.
Matrix completion asks to recover a low-rank matrix from a small random subset of its entries. It models collaborative filtering (a ratings matrix with most entries missing), sensor-network localization from partial distance matrices, and system identification. The natural estimator, the matrix of least rank that agrees with the observations, is NP-hard to compute in general. Candès and Recht (Found. Comput. Math. 2009) proposed to replace the rank by the nuclear norm (the sum of the singular values), its convex envelope, and proved that this convex program recovers the matrix exactly from random entries under incoherence assumptions.
Candès and Tao (IEEE Trans. Inf. Theory 2010) sharpened the sample size to within logarithmic factors of the information-theoretic minimum . This mission formalizes their first result, Theorem 1.1, whose proof is a direct moment computation, together with the lemmas on which that proof rests.
Timeline:
Let have rank and singular value decomposition with and orthonormal , . Write , and . The matrix obeys the strong incoherence property with parameter if, for all indices ,
For a set of observed positions, the nuclear-norm program is
In the uniform model is a uniformly random -subset of ; in the Bernoulli model each entry is included independently with probability .
The proof works with the tangent space at and its projection , the sampling projection , and the centered operators and , where and . The candidate certificate of (III.10) is the matrix of least Frobenius norm with and .
There is an absolute constant such that, for every strongly incoherent of rank and every ,
The Bernoulli-to-uniform transfer (at most doubling the failure probability) is already on the platform and is included as a supporting item.
Theorem 1.1 shows that a tractable convex program recovers every strongly incoherent matrix of bounded rank from random entries, while Theorem 1.7 of the same paper shows that no method can succeed with fewer than order . The gap is a single logarithmic factor. The result also requires nothing of the singular values, only of the singular vectors.
The theorem is proved in the literature, and later work improved the rank dependence (Theorem 1.2 of the same paper, and the golfing-scheme results of Gross and Recht). As far as is known, none of these results has a machine-checked proof. The mission produces a formal version of the full moment-method argument. Its combinatorial core, the admissible-pair calculus of Sections IV–V, is a self-contained counting problem for closed paths in a grid and is reusable for other trace-moment bounds of random operators. The Candès–Recht mission on the platform already supplies the deterministic duality step (Lemma 3.1) and the model transfer.
The obvious route bounds the Neumann series term by term with noncommutative Khintchine inequalities and decoupling. That is how the earlier bound was obtained, and it degrades as grows because the indicator variables in the higher terms are strongly coupled. The moment method replaces these tools by an exact expansion of as a sum over "spider" configurations of paths in . The difficulty moves into combinatorics. Configurations have to be grouped by admissible pairs, the exponent of has to be matched against the powers of (Lemma 5.1), and the configurations have to be counted with enough precision that the sum over converges (Lemma 5.2). A naive count of pairs gives , which is too large by a square.
Matrix (Fin n) (Fin n) ℝ.successProb (a ratio of finite counts). The Bernoulli model uses bernoulliEventProb and bernoulliExpectation with . The logarithm is natural, and the failure probability is written 1 / n^3.IsUniqueMinimizer: every other matrix that agrees with on has strictly larger nuclear norm. Stating recovery conditionally on the existence of a certificate would reduce the goal to Lemma 3.1; the goal instead bounds the probability of recovery itself.finRotate, and the lexicographic order is compared through positions. Pair values are counted in Fin (2j(k+1)+1), which contains every admissible value, so the count is exact and finite.centeredTangentProjection (), momentMatrix (), and the admissible-pair calculus. Strong incoherence (A1–A2) is the shared definition CandesTao.Shared.StrongIncoherence, used by this mission and by the companion mission II. The definition is drafted independently in mission II.Contributions are welcome on any milestone. Lemmas 5.1 and 5.2 are finite combinatorics and need no analysis. Theorem 3.4 additionally needs the expansion (IV.4) of the trace moment and the moment bounds for centered Bernoulli variables of Section IV-C. Corollary 3.5 also uses Theorem 3.2 (Rudelson selection estimate) and Lemma 3.3 (replacing by ), which are milestones of the companion mission The Power of Convex Relaxation: Near-Optimal Matrix Completion II.
A system that processes a stream of tasks can often be configured in several ways, and the configuration affects both the cost of the current task and the cost of switching before the next one: paging schemes, replicated files, server placements. When the future is unknown, the natural worst-case yardstick is competitive analysis, introduced by Sleator and Tarjan for list update and paging (Sleator–Tarjan 1985): an on-line strategy is compared with the optimal strategy that knows the whole input in advance.
Borodin, Linial and Saks (J. ACM 1992; conference version STOC 1987) proposed metrical task systems as a single model containing all such problems, and determined the exact deterministic competitive ratio of every such system. Their theorem is the starting point of the on-line-algorithms literature on metrical task systems, the -server problem (Manasse–McGeoch–Sleator 1990) and their randomized variants.
Timeline. 1985: Sleator and Tarjan introduce competitive analysis for paging and list update. 1987: Borodin, Linial and Saks prove for every -state metrical task system (journal version 1992). 1990: Manasse, McGeoch and Sleator extend the task-system model to restricted task sets and pose the -server conjecture. The randomized ratio of the uniform task system, bounded in the same paper between and , is the subject of the companion mission.
A task system has a finite set of states and a transition-cost matrix with , for , and the triangle inequality . It is metrical if also .
A task is a vector of nonnegative processing costs , . Given a task sequence and an initial state , a schedule is a map with ; task is processed in state , and the cost is
The off-line optimum is the minimum over all schedules. An on-line algorithm chooses knowing only and ; its cost is . For , is -competitive if there is a constant with for every finite task sequence. The competitive ratio of is , and the competitive ratio of the task system is .
For the upper bound the paper also uses continuous-time schedules, in which task occupies the interval and the scheduler may change state at any real time, paying for processing. For a general (possibly asymmetric) matrix , the cycle offset ratio is the maximum over closed walks of ; it equals when is symmetric.
For every metrical task system with states,
The value depends on only, not on the distances.
The theorem settles the deterministic competitive ratio of the whole class of metrical task systems: the lower bound says that no deterministic on-line strategy can beat on any metric, and the upper bound supplies one algorithm that achieves it on every metric. For asymmetric costs the same algorithm gives . The lower bound is also the benchmark against which restricted models, such as paging and the -server problem, measure their improvements, and the randomized question it leaves open drove much of the later work on metrical task systems.
The result was proved in 1987 and is standard; to the best of our knowledge no machine-checked proof exists. A formal development would provide a reusable model of deterministic on-line algorithms and competitiveness (on-line maps from task prefixes, additive competitiveness, infima over algorithms), an adversary construction by mutual recursion with an arbitrary algorithm, and an exact treatment of continuous-time schedules with piecewise-constant task costs. These pieces are reusable for other competitive-analysis results.
The lower bound is not a single bad input: the adversary is built from the algorithm it plays against, so the hard task sequence exists only as a recursion interleaved with the algorithm's choices, and the bound must hold for every deterministic on-line map, including ones that behave erratically. Obtaining the exact constant , rather than some bound, requires a sharp estimate of the off-line cost of that sequence.
The upper bound needs an algorithm defined in continuous time, whose transition times are determined by accumulated processing costs; the budgets can be zero, so transitions can be instantaneous, and a formal cost must remain well defined before one knows that only finitely many transitions occur. Relating the off-line cost function at those times to the recursively defined (Lemma 6.2) requires reasoning about all continuous-time off-line schedules. Finally, the goal combines both directions through infima over all on-line algorithms, and the discretization of Lemma 3.1 must be composed with the continuous-time algorithm.
States form a finite type S (Fintype, DecidableEq, Nonempty); the goal is stated for all , where gives . Task costs are finite nonnegative reals; the paper also allows entries, which are excluded (this affects neither bound). A task sequence is T : Fin m → S → ℝ, with T i the paper's , and a schedule is σ : Fin (m+1) → S. An on-line algorithm is a map sending to , so on-line behaviour is built into the type. Competitiveness is written additively, , with independent of the task sequence and of .
The competitive ratio competitiveRatio d is the real infimum of the set of all for which some on-line algorithm is -competitive. It is not defined as an infimum of per-algorithm real infima: a non-competitive algorithm has , whose real infimum is , and that would drag to for every system. Since the goal's value is at least while the empty set's real infimum is , the goal cannot hold vacuously.
Continuous-time algorithms are given as lists of pieces per unit interval; processing integrals are exact finite sums. The algorithm minimizes over states different from the current one, as its proof requires (the printed rule ranges over all states, and would stall); ties are left arbitrary. Its budgets may be , its entry times are Option ℝ, and its cost is a sum in , so that Theorem 6.1 itself asserts that only finitely many transitions occur. The ratio excludes closed walks that never move, and Theorems 2.2 and 6.1 require , where and are defined. Lemma 3.1 is stated comparing with (the printed statement says "as well as ").
A complete development needs: the discrete model and off-line optimum (finite minimum over schedules), limsup arguments in EReal, continuous-time schedules with piecewise-constant costs, and the recursion defining . Proofs of any milestone, including the purely combinatorial Lemmas 6.3 and 6.4, are welcome, as is a formal composition of Lemma 3.1 with Theorem 6.1.
The combinatorial diameter of a polyhedron is the largest distance, in its vertex-edge graph, between two vertices. It is a lower bound on the number of pivots any edge-following method such as the simplex method needs in the worst case, which is why the polynomial Hirsch conjecture — the diameter of is bounded by a polynomial in and — is a central open question of linear optimization and discrete geometry. The best general upper bound is quasi-polynomial, (Kalai–Kleitman 1992); the original Hirsch bound is false for polytopes (Santos 2012).
A different line of work bounds the diameter by the arithmetic of the constraint matrix instead of its size. For an integer matrix let be the largest absolute value of a sub-determinant of . Dyer and Frieze (1994) showed that for totally unimodular () the diameter is polynomial, . Bonifas, Di Summa, Eisenbrand, Hähnle and Niemeier (SoCG 2012; Discrete Comput Geom 52, 2014) improved and generalized this to for all polyhedra and for polytopes, bounds that do not depend on the number of inequalities. This mission formalizes the polytope case.
Let with rows , let , and let . A vertex of is an extreme point; for a polyhedron this is a point of at which linearly independent inequalities are tight. Two vertices are adjacent if the segment is an edge (a one-dimensional face) of . This gives the polyhedral graph , and the diameter of is at most if every two vertices are joined by a walk of at most edges.
has sub-determinants bounded by if every submatrix, for every , has determinant in . In particular every entry is at most in absolute value.
For a vertex the normal cone is the set of objectives for which maximizes over . With the closed unit ball, the volume of a set of vertices is
and the neighbourhood of is the set of vertices outside adjacent to a vertex of . A spherical cone is with closed under non-negative scaling; its dockable surface is the -dimensional measure of the part of its boundary inside the open ball. A cone of revolution of angle is . is non-degenerate if every vertex has exactly tight inequalities.
If has all sub-determinants bounded by and is bounded, then
No non-degeneracy, full-dimensionality or rank condition is assumed, and the bound is uniform in and .
The result. Theorem 2 bounds the diameter of every integral polytope by a polynomial in the dimension and the largest sub-determinant, independently of the number of facets. For totally unimodular matrices, which cover network-flow, bipartite matching and transportation polytopes, it gives , improving the Dyer–Frieze bound by a large polynomial factor. It shows that the obstruction to a polynomial Hirsch bound, if any, must come from matrices with large sub-determinants. The volume-expansion method — measuring breadth-first search by the volume of the normal fan it has covered — was later refined, for instance in the shadow-vertex analysis of Dadush–Hähnle, which improves the dependence on .
Formalizing it. The theorem is proved (2012/2014); no machine-checked proof is known. A formal development needs, on top of Mathlib, the normal fan of a polytope and its relation to the vertex-edge graph, a Hausdorff-measure calculus for cones (surface of a cone in terms of its base), Lévy's isoperimetric inequality on the sphere in a measure-theoretic form, and explicit Gamma-function estimates. Each of these is reusable well beyond this paper.
The combinatorial side is short; the geometry is not. Lemma 4 is the spherical isoperimetric inequality of Lévy, which Mathlib does not have in any form, and which the paper cites rather than proves; the relations between the volume of a spherical cone, the area of its base, its lateral surface and the length of the base's boundary (Eq. (3), "basic integration") are also absent. Lemma 3 depends on the structure of the normal cone of a vertex of a non-degenerate polytope (full-dimensional, simplicial, generated by rows of ), none of which is available for Mathlib's extreme points. Lemma 1 depends on the normal fan of a polytope: the normal cones have pairwise disjoint interiors, cover , and share a facet exactly when their vertices are adjacent. The step from non-degenerate to arbitrary polytopes perturbs and needs the diameter not to decrease, a statement about the vertex-edge graph under perturbation. A shortcut through a finite graph abstraction is not available: the constant depends on the geometry of the normal cones, not only on the graph.
The polyhedron is Hirsch.Hpoly (rowVec A) b, with rowVec A i the -th row of Matrix (Fin m) (Fin n) ℤ as a vector of EuclideanSpace ℝ (Fin n). Vertices are Set.extremePoints ℝ P, adjacency is Hirsch.Adj, "diameter at most " is Hirsch.DiamLE P B, all from the published Hirsch_model. The normal cone is the published FirstOrderOpt.ConvexTheory.normalCone. Volumes are Lebesgue measure with values in ; the dockable surface uses μHE[n-1], the Hausdorff measure normalized to agree with Lebesgue measure on hyperplanes, applied to frontier S ∩ Metric.ball 0 1. is a natural number and the sub-determinant bound ranges over all sizes .
Explicit constants. The paper writes in Theorem 2; the proof on pp. 105–106 yields with , from Eq. (1), the bound and the fact that the diameter is at most twice the number of breadth-first-search iterations needed to cover more than half of . This explicit bound is the goal. The ratios of Lemmas 3, 5, 6 are stated in multiplicative form.
Non-degeneracy is a hypothesis of Lemma 3, Lemma 1 and Eq. (1) only, as in the paper's §1.1, and never of Theorem 2. The neighbourhood excludes ; including it would make Lemma 1 trivial, since its constant is below . Lemma 4 is stated against every competitor: for every measurable spherical cone and every cone of revolution of the same volume, ; it does not assert existence of a cone of a prescribed volume. The goal is Theorem 2 about the polytope and its graph, not an abstract statement about set families with a volume-expansion property; integrality of and the bound on minors of every size are both essential (scaling a real matrix down makes arbitrarily small), and the raw Hausdorff measure μH[n-1] would put Lemmas 3 and 6 on incompatible scales.
Contributions are welcome at every level: the normal fan and its adjacency structure, cone surface formulas, the Gamma estimate , and a formal Lévy inequality.
Minimizing a smooth function over a closed convex set on which projection is cheap (a box, a ball, a simplex) is a routine subproblem in large-scale optimization: box-constrained minimization is the inner solver of augmented Lagrangian methods, and bound-constrained least squares, image restoration and density estimation all have this form. The classical projected gradient method of Goldstein and of Levitin and Polyak is simple and needs only gradients and projections, but with constant or Armijo-type step lengths it is slow.
Spectral projected gradient (SPG) methods, introduced by Birgin, Martínez and Raydan (paper), combine three ingredients: the projected gradient direction; the Barzilai–Borwein (spectral) step length , an inverse Rayleigh quotient of the average Hessian along the last step; and the nonmonotone line search of Grippo, Lampariello and Lucidi, which compares a trial value with the worst of the last objective values instead of the current one. The method is widely used in practice, and its analysis is the template for many later nonmonotone projected methods.
Timeline:
Let be nonempty, closed and convex, with the Euclidean inner product and norm . Let have continuous partial derivatives on an open set and write . The orthogonal projection is the unique point of nearest to . The scaled projected gradient is for , . A point is a constrained stationary point if for all .
The parameters are an integer , reals , a sufficient-decrease constant and safeguards . Algorithm SPG2 starts from and and at iteration :
fails, replace by any . When (3) holds, and . 3. Spectral step. With , , : if , else .
In Lean the projection is a function P with the predicate IsProjOnto Ω P, is scaledProjGrad P f t, stationarity is IsConstrainedStationary Ω f, the maximum in (3) is nonmonotoneRef f x M k, and an infinite run is IsSPG2Run Ω f P M αmin αmax γ σ₁ σ₂ x α.
For every infinite run of SPG2 and every accumulation point of ,
The statement fixes no parameter values and assumes neither convexity of nor a bounded level set.
Theorem 2.1 is the global convergence guarantee for SPG2. It holds without monotone decrease of and without any restriction on the spectral step beyond the safeguards. These are the two features that make the method fast in practice, and together they mean that no classical monotone projected-gradient argument applies directly. The same statement underlies the convergence claims of the SPG software (ACM TOMS Algorithm 813) and of the many methods that reuse the nonmonotone spectral framework: inexact SPG, augmented Lagrangian inner solvers, and projected BB methods for machine learning.
Status: the theorem is proved in the literature. This paper's proof reads "See [7]", a pointer to Birgin, Martínez and Raydan (2003). No Lean formalization of this theorem, of the nonmonotone Armijo analysis, or of the projected-gradient stationarity lemma is known. The mission produces a formal proof and a reusable Lean interface for projection-based first-order methods on convex sets.
The obvious argument for monotone descent methods is to show that decreases, so that the total decrease is finite and the per-iteration decrease tends to zero. Here need not decrease. Only the reference value is nonincreasing, and a small decrease of this maximum along the whole sequence does not by itself give a small decrease at the iterates that approach a given accumulation point . A second difficulty is that the accepted step lengths may tend to zero along the subsequence, while is only on a neighbourhood of and no Lipschitz constant for is available, so no uniform sufficient-decrease estimate holds. The spectral steps vary within , so the directions are not a fixed function of .
EuclideanSpace ℝ (Fin n) with inner ℝ and the 2-norm. is a total function EuclideanSpace ℝ (Fin n) → ℝ with ContDiffOn ℝ 1 f U on an open U ⊇ Ω, and is Mathlib's gradient f. The algorithm evaluates and only at points of .MapClusterPt x̄ atTop x.iInf form: norm_eq_iInf_iff_real_inner_le_zero), continuity properties of the projection, a mean-value estimate for functions on segments in , and the nonmonotone reference-value bookkeeping. The projection lemmas and the nonmonotone bookkeeping are reusable beyond this mission, in particular for the companion mission on SPG1, and contributions of them as separate lemmas are welcome.Robust optimization protects a decision against every scenario in an uncertainty set. When the uncertain data are probabilities, a natural uncertainty set is a ball around a nominal distribution measured by a φ-divergence (Kullback–Leibler, Burg entropy, χ², Hellinger and others). Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) show that the robust counterpart of a linear constraint over such a set is a finite convex system, and then ask whether that system is computationally tractable: can an interior-point method solve it in polynomial time?
For the Burg and Kullback–Leibler divergences the reformulated constraints (Eqs. (29) and (32) of the paper) have the shape , a perspective constraint. Polynomial-time solvability by interior-point methods follows once the constraint set carries a self-concordant barrier in the sense of Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994). Theorem 2 of the paper supplies such a barrier for every perspective constraint whose generating function satisfies a one-dimensional differential inequality. The same question arises for perspective and relative-entropy cones in conic optimization generally, so the criterion is of interest beyond φ-divergences.
A function on an open convex set is -self-concordant () if it is three times continuously differentiable on and for every and every direction
where is the -th differential of at in direction (Definition 1, p. 350). In Lean this is PhiDivRobust.Barrier.IsSelfConcordant κ F φ.
Let be a real function on . Its perspective is for (perspective f). The constraint set (34) is
and its logarithmic barrier (35) is
(logBarrier f), finite on the open set (barrierDomain f). Directions are for , with along and along , and for .
If is convex on and, for some ,
then is -self-concordant on .
Milestones 3 and 4 give the goal, since . A further item records the paper's application: (the Burg case) satisfies (33) with .
The result. Theorem 2 turns a two-line calculus check on a scalar function into a certificate of polynomial-time solvability for a three-dimensional convex constraint. The paper uses it to conclude that the robust counterparts for the Burg entropy and Kullback–Leibler uncertainty sets are tractable, and the criterion applies to any other convex satisfying (33); for example satisfies it with , which covers the relative-entropy cone. The constant enters the complexity bound of any path-following method through the barrier parameter.
Formalizing it. The theorem is proved in the paper, but the decisive step is delegated to Lemma A.2 of den Hertog's monograph, which in turn belongs to the compatibility theory of Nesterov and Nemirovski. As far as is known none of these statements has a machine-checked proof. The mission produces a checked version of the compatibility lemma for perspective constraints, which is reusable for any barrier of the form , together with explicit second- and third-differential formulas for perspectives in Mathlib's iteratedFDeriv language. The printed third-differential display contains a typo (see below); the formal statements fix it.
The differential identities (milestones 1 and 2) are routine but heavy: they require computing iterated Fréchet derivatives of a composition with a quotient in two variables and matching them with one-variable iterated derivatives of . The inequality (milestone 3) is elementary real-variable algebra once the differentials are available.
The central difficulty is den Hertog's lemma. The obvious approach, bounding the three terms of separately against , fails: the cross term with couples the first and second differentials, and bounding it separately loses the constant . A further practical difficulty is that is open and convex only because the perspective of a convex function is jointly convex and continuous, which must itself be established.
Points are and directions for are in . Differentials are iteratedFDeriv ℝ k applied to the constant tuple ; and are iteratedDeriv 2 f and iteratedDeriv 3 f. The power is Real.rpow, which is for ; this makes the Lean definition of self-concordance no weaker than the paper's. Real.log and division have junk values outside , but is open, so no differential at a point of sees them.
Committed conventions and disclosed deviations:
A trivializing formalization is excluded. The self-concordance predicate requires regularity and quantifies over all directions , the domain is exactly (not a subset such as ), and is as printed. The constant of the conclusion is tied to the same as in (33).
Useful infrastructure, reusable beyond this mission: iterated derivatives of perspectives, joint convexity of perspectives, and the calculus of self-concordance (sums, of a concave function composed with an affine map). Proofs of the milestones independently of the goal are welcome, as are proofs of the Burg item's consequence and of the analogous statement for .
Many decision problems contain a constraint whose coefficients are an expectation under a probability vector that is not known exactly: an expected cost under uncertain scenario probabilities, an expected payoff of an asset under an estimated distribution, the expected demand in a newsvendor model. The probabilities are usually estimated from data, and a solution that is feasible for the estimate can be infeasible for the true distribution. Robust optimization protects against this by requiring the constraint to hold for every probability vector in an uncertainty region around the estimate.
A natural region is a ball in a φ-divergence, a family of statistical distances between probability vectors that contains the Kullback–Leibler divergence, the Burg entropy, the χ² distances, the Hellinger distance and the variation distance. Such balls arise as asymptotic confidence sets for the true distribution given observed frequencies (Pardo 2006), so the radius has a statistical meaning. Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) showed that the robust version of a linear constraint over such a ball is equivalent to a finite convex system involving the convex conjugate of φ. This reformulation is a standard tool in the later literature on distributionally robust optimization.
A φ-divergence function is a function that is convex on , finite on , and satisfies ; the value may be . Examples are (Kullback–Leibler), (Burg), (modified χ²) and (variation). For with the φ-divergence is
and the conjugate of is , a function with values in .
Fix , with columns , , with columns , , a nominal vector and a radius . The uncertainty region is
where the linear constraints can encode and any further information on . A decision satisfies the robust linear constraint if
Inequalities between vectors are componentwise throughout.
Assume and . Then satisfies (11) if and only if there are and with
where for and for . The statement fixes no constants and no particular φ; it holds for the whole class.
The proof in the paper has three displayed steps, which are the milestones. With the Lagrange function and the dual objective :
An additional item states Corollary 1, the specialization to , where the multiplier of the normalization is free in sign.
Theorem 1 turns a semi-infinite constraint, one inequality for each in a convex set, into a single convex inequality in . The left side of (13) is jointly convex because is the perspective of a convex function. For the divergences of Table 4 of the paper the conjugate has a closed form, and the robust constraint becomes a linear, conic quadratic or self-concordant-barrier-representable constraint. The paper's applications (robust asset pricing, a robust newsvendor, and the tractability results of its §5) all start from this theorem, as do its Corollaries 2–5.
The theorem is proved in the paper; no machine-checked proof of it is known. Formalizing it adds a checked robust-counterpart theorem for φ-divergence regions, a reusable encoding of φ-divergences with extended values, and a strong-duality statement with attainment for convex programs whose constraint function takes the value on the boundary of the orthant. It also records a correction: the paper states the theorem for , and that version is false (see Formalization scope).
The separation step (15) and the conjugate identity are elementary manipulations of suprema, but in extended arithmetic: may be at , the conjugate may be , and the case follows its own convention. The central difficulty is the duality step. The worst-case problem is a convex program whose constraint is not a finite convex function on a closed set: for the Burg or χ² divergence it is on the boundary of the orthant, and itself need not be closed. Textbook statements of Slater-type strong duality usually assume finite-valued convex functions on a closed domain, so they do not apply as stated. The statement also requires attainment of the dual minimum, not only the absence of a duality gap, and this is the part a naive limiting argument does not give.
Conventions:
Fin n → ℝ with the componentwise order; and are Matrix (Fin n) (Fin m) ℝ and Matrix (Fin k) (Fin m) ℝ; and are the columns fun j => B j i and fun j => C j i.ℝ → EReal, never , finite on , with and convexity on written out in EReal. is allowed, so the Burg, χ² and J divergences are covered.EReal-valued. is the EReal product, in which . The term is defined by an explicit case split at , and in (13) is read as with the convention applied term by term.Corrected slip. The paper's standing assumption is . The third equality of (15) substitutes , which needs , and Theorem 1 is false for : with , , , , both columns of equal to , , , , , , , the vector lies in and violates (11), while , satisfy (13). Every statement of the mission therefore assumes for all . The hypothesis (the paper's "such that ") and are kept.
Ruled-out trivializations: a conjugate taken as a supremum over all of a real-valued φ with junk values at is a different function; computing the term as with Lean's makes it identically ; a real-valued, everywhere finite φ silently excludes the Burg, χ² and J divergences; dropping or removes the Slater point and changes the theorem. The mission's definitions avoid all four.
Needed infrastructure: suprema of EReal-valued families over half-lines and orthants, the interchange of a supremum over a product with a finite sum, and a Lagrangian strong-duality theorem with attainment for a convex program with finitely many affine inequality constraints and one convex, possibly infinite-valued, inequality constraint with a Slater point in the interior of its domain. That duality theorem, and the φ-divergence definitions, are reusable beyond this mission, in particular for the paper's Corollaries 2–5 and for other distributionally robust formulations. Contributions of any of these pieces as separate theorems are welcome.
Networks of queues model computer systems, communication networks and manufacturing lines: customers (jobs, packets, parts) move between service centers, wait, receive service and move on. Their equilibrium behaviour determines throughputs, utilizations and response times, and for most networks it can only be computed by solving the full balance equations of a continuous-time Markov chain whose state space grows combinatorially with the number of centers and customers. A product-form network is one whose equilibrium distribution factorizes over the centers; for such networks performance measures can be computed exactly by efficient algorithms (convolution, mean value analysis), and this is the basis of much of classical computer-performance modelling.
Timeline of the main product-form results:
A network has service centers and customer classes. A class- customer finishing service at center next requires center in class with probability and leaves the network with probability . The pairs are partitioned into subchains that routing never leaves. Each center has one of four types:
At types 2–4 the class- service time is Coxian: exponential stages of rates , and after stage the customer continues with probability or finishes with probability . The state records the FCFS order of classes at type 1, the number of class- customers in stage at types 2 and 3, and the LCFS order of (class, stage) pairs at type 4. External arrivals are Poisson, either with rate depending on the total population (process A) or with one stream per subchain of rate (process B); an arrival joins center in class with probability . A subchain with is closed and keeps a fixed population .
With relative arrival rates solving the traffic equations and (the probability of reaching stage , stages numbered from 0), the paper defines per center type and a factor from the arrival rates.
satisfies the global balance equations of the network, and, under the paper's assumption that the equilibrium distribution is unique, every equilibrium distribution equals whenever is finite and positive. The goal covers all four center types, open, closed and mixed networks, and both arrival processes.
A further supporting item, also from §4.1 (p. 254), states that summing over local states with fixed class counts gives . So depends on the service times only through their means .
The theorem places the four disciplines, class switching and mixed open/closed populations under one formula. Its corollary in §4.1, that aggregate probabilities depend on service time distributions only through their means (insensitivity), is what makes the model usable with measured mean service times, and it underlies the convolution and mean value analysis algorithms for normalizing constants.
The result is classical and proved on paper. As far as the platform's catalogue shows, it is not formalized: the platform has Kelly's single-class migration process with exponential service, a special case. A machine-checked BCMP theorem would provide a verified multiclass queueing-network model (states, event-driven transition rates, balance equations) on which later results can build: mean value analysis, the state-dependent rates of §5, and the open-network marginals of §4.2.
The printed statement contains an error. The paper defines (p. 253). With the branching of its Figs. 1 and 3, this product includes the branch out of stage . For exponential service () it gives , so every of a type 2–4 center with a customer present vanishes, and a closed network of such centers would have no normalizable solution. The mission states the corrected theorem with , which the mean-service-time identity of §4.1 also requires. The type-2 factor is read as .
The algebra of the paper's proof is local: each independent balance equation reduces to the traffic equations. The difficulty is in making that statement precise for a real state space. The independent balance equations need a consistent labelling of each moving customer by the "stage" it leaves and enters. That labelling has to cover FCFS centers, where per-class labels are inconsistent (p. 253), the outside world of each open subchain, and LCFS preemption. Every in-flow into a state is a sum over predecessor states, and those states differ by list operations (appending at an FCFS tail, pushing on an LCFS head) or by stage-count updates. The factorials in the processor-sharing and infinite-server factors, and the telescoping identity for departures, must line up exactly with the rates. The obvious shortcut is to check global balance directly for a single class with exponential service. That covers neither class switching, nor Coxian stages, nor mixed networks.
Centers are Fin N, classes Fin R and subchains Fin m. The class- stages at center are Fin (u i r) with u i r : ℕ+, numbered from 0. A local state is an inductive type with three shapes (FCFS list, stage-count array, LCFS list of (class, stage) pairs). The state space is the subtype of configurations whose shapes match the center types and whose closed subchains hold their fixed populations. Transition rates are the sums of the rates of explicit events (arrivals, FCFS completions, stage moves and completions, LCFS moves and completions). Global balance uses tsum; every state has finitely many successors and predecessors with nonzero rate, so these sums are finite. The standing assumptions (substochastic routing closed on subchains, closed subchains with no arrivals and no departures, positive rates, continuation probabilities in vanishing at the last stage) are collected in Network.IsValid. Irreducibility of subchains is not assumed, and any nonnegative solution of the traffic equations is allowed. Under process B the product in runs over open subchains only. Uniqueness of the equilibrium is a hypothesis, as in the paper. The type-1 rate is constant, and the state-dependent rates of Condition 1 and §5 are not covered.
The following formalizations would trivialize the mission and are ruled out: stating only global balance of (satisfied by ), quantifying over arbitrary rate functions instead of the rates built from the network data, and restricting the goal to exponential service or to a single class.
Needed infrastructure: finite-support tsum manipulations, multinomial identities for the §4.1 sums over orderings and stage assignments, and bookkeeping for list and array updates. The model and the balance-equation layer can be reused for later queueing missions. Contributions are welcome on each milestone, on the per-center-type pieces of the independent balance check, and on helper lemmas about the event system.
This mission formalizes §6 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: the definition of Thompson's group and Thompson's proof that is simple.
Thompson's groups and , introduced in unpublished notes of Richard Thompson in 1965, were the first known examples of infinite, finitely presented, simple groups. The notes of Cannon, Floyd and Parry were written in part "to make available Thompson's unpublished proofs … of the simplicity of and " (p. 216); §6 is the proof for .
contains , which contains . Earlier missions on this platform formalize and its commutator subgroup (§1 and §4), its tree-diagram normal form (§2), its presentations (§3), and the simplicity of (§5). Unlike , the elements of need not be continuous: they cut the circle into pieces and rearrange them in any order, so contains every finite symmetric group.
The circle is with its endpoints identified, in Lean UnitAddCircle (); denotes the image of . Maps compose right to left, , and .
The group (p. 240) consists of the right-continuous bijections of that map images of dyadic rationals to images of dyadic rationals, are differentiable except at finitely many images of dyadic rationals, and are linear with slope a power of on each maximal interval of differentiability. In Lean a permutation of the circle satisfies IsThompsonV f when it maps dyadic points to dyadic points and, for a finite set of dyadic breakpoints, is on each half-open piece between consecutive breakpoints modulo . V is the subgroup generated by these maps; that they already form a group is the first milestone.
The elements. , , are 's generators, and (mapPi0) exchanges and by and . The words , , , and (p. 241) are defined once, as words in four symbols, and read both as maps of the circle and in .
The presented group (p. 242) is the free group on , , , modulo fourteen relators: the six relators of (§5), and eight more involving the , such as , and . In , is the subgroup generated by , , and an element is positive when it is a product of nonnegative powers of the .
The goal is the sentence in which the notes state what §6 does, "In §6 we define and give Thompson's proof that is simple" (p. 216):
The route is the section's own. Lemma 6.1 shows that , , , generate and satisfy the fourteen relations, so maps onto . Lemmas 6.2–6.8 establish how the move past the and , leading to Theorem 6.9, is simple, and hence . The goal follows.
The result. is the third of Thompson's groups and the one whose elements rearrange pieces of the circle: it is infinite, finitely presented and simple, and it contains every finite group (through the finite symmetric groups). Together with it gave the first examples of infinite finitely presented simple groups.
Formalizing it. No machine-checked proof that is simple exists on this platform, and Mathlib has nothing on Thompson's groups. This mission reuses the formalization of and : 's first six relators are 's, and the proof of Theorem 6.9 applies Theorem 5.7 and Theorem 5.8 inside .
The central difficulty is the generation half of Lemma 6.1. The notes' proof uses tree diagrams with labelled leaves: every element of permutes the intervals of one standard dyadic partition onto those of another, moves any partition to a standard comb, and the subgroup generated by and acts as the full symmetric group on the comb's intervals. Each step is stated in one sentence; the milestones make each a separate statement.
The algebra of (Lemmas 6.2–6.6) is a chain of inductions. The proofs lean on two facts the notes use without isolating them: that maps to (so §5's lemmas hold in ), and the normal form in , stated inside the proof of Theorem 6.9. Both are milestones here. The notes also cite two facts about the finitary symmetric group without proof, its presentation and the behaviour of its proper quotients, and deduce ; the proof of Theorem 6.9 uses all three, and each is a milestone.
Subgroup (Equiv.Perm UnitAddCircle) generated by IsThompsonV. Half-open pieces make every element right-continuous; "linear" is read modulo , so a piece may wrap past , as a rotation does. Unlike , no lift to the line is available, since elements of need not be monotone.PresentedGroup on the four-element type FormalV. Relators are written out as .SigmaPerm, the subgroup of Equiv.Perm ℕ of permutations moving finitely many points, and is the transposition of and ; its presentation is a PresentedGroup on ℕ. is taken as the subgroup of generated by all the , which is the union of the .IsStandardDyadicPartition.Gibbons and Hawking conjectured that the cosmological horizon of a de Sitter static patch carries an entropy, computed semiclassically by the Euclidean gravitational path integral on the sphere. For three-dimensional de Sitter gravity the relevant quantity is , whose leading term is the Gibbons–Hawking entropy . A microscopic account of this entropy — a count of states in some ordinary quantum or statistical system — is one of the long-standing goals of de Sitter holography.
Collier, Eberhardt and Mühlmann (arXiv:2501.01486) propose that pure dS quantum gravity is dual to the double-scaled two-matrix integral of the complex Liouville string (arXiv:2409.17246). In §4.4 they test this by counting the "effective number of eigenvalues" of the matrix model and comparing with . The comparison reduces to explicit identities between elementary functions of the Liouville parameter ; this mission formalizes exactly those identities.
Fix a complex number with , i.e. with (the paper's footnote 2; then the central charge lies in ). Write and let be the genus-counting parameter of the matrix model.
For any function whose modulus equals for a fixed constant (the content of (4.5)), there is a real constant , independent of and , such that
This is the paper's statement that the matrix-model count reproduces the de Sitter entropy "regardless of the specific value of ", up to the order-one constants that (4.37) later fixes.
The identity (4.36) is the step the authors single out as "a genuinely nontrivial check": it holds for the complex Liouville string but, as they note, not for the Virasoro minimal string. The goal packages the argument of §4.4 into one exact statement, valid for every admissible (i.e. exactly in ), under the single physical input (4.5). The physical assumptions — the choice of cutoff at the first zero, the interpretation of as an entropy, and (4.5) itself — are not formalized; they enter as definitions and as the hypothesis on . The mathematical content is a definite-integral evaluation plus trigonometric/hyperbolic identities for complex arguments.
The integral in (4.32) has a complex-looking integrand, a branch of , and an upper limit given by a complex cosine; one must first show that everything is real in the admissible regime and then evaluate the integral exactly, including the endpoint behaviour at where is not differentiable. The entropy statements additionally involve the complex principal logarithm, so one must control the argument (positivity) of and of the tension ratio; identities such as fail for general complex .
Real.arcosh (defined as ); its values for never enter.Complex.log), and is complex-valued; the goal forces it to equal a real number.Heisenberg's uncertainty principle is the first quantitative statement a student meets about the incompatibility of position and momentum measurements in quantum mechanics. In A. O. Lopes' textbook Uma Breve Introdução à Matemática da Mecânica Quântica (31º Colóquio Brasileiro de Matemática, IMPA, 2017), written for mathematics students with no physics background, it is the capstone of Chapter 8 (Princípio da Incerteza e o Pacote de Onda Gaussiano), Teorema 8.2, p. 131. It collects the operator formalism built in Chapters 1, 3 and 4 — position and momentum operators, commutators, expected values — into one inequality. This mission is the first of a series formalizing the capstone results of the book.
A wave function is a map . The book uses the inner product (linear in the first slot) and the norm . A state is a wave function with . Fix , an index and the (reduced) Planck constant .
For every state ,
The inequality is the prototype of all Robertson-type uncertainty relations and is the point where the commutator formalism of the book produces a numerical, physically testable consequence. Milestone 5 shows the constant cannot be improved. The mathematics is classical and fully proved in the source; what this mission adds is a machine-checked version of the textbook's operator calculus on — integration by parts for compactly supported functions, symmetry of and , commutation relations, and explicit Gaussian integrals — reusable by later missions of the series (Ehrenfest's theorem, density operators, quantum statistical mechanics).
The algebraic core is a short Cauchy–Schwarz argument, but it silently uses facts about unbounded operators: that may be rewritten as requires integration by parts with vanishing boundary terms, and the reduction to mean-zero observables requires the expected values to be real. Each of these needs integrability bookkeeping that the book leaves implicit. The Gaussian milestone requires evaluating first and second moments of Gaussian integrals in dimensions.
EuclideanSpace ℝ (Fin n) with Lebesgue measure; wave functions are plain functions ℝⁿ → ℂ (not classes), operators are maps on such functions, and domains are imposed as explicit hypotheses (InPositionDomain, InMomentumDomain).Contributions welcome: integration-by-parts lemmas on for compactly supported functions, Gaussian moment computations, and an abstract Robertson inequality.
Ramsey's theorem says that every red/blue colouring of the pairs of an infinite set has an infinite monochromatic subset. For well-ordered sets one can ask for more: the monochromatic set should have the same order type as the whole set. Erdős and Rado introduced the partition relation to measure exactly this, and asked which countable ordinals satisfy — every colouring either has a red copy of the whole order or a blue triangle. Such ordinals are called partition ordinals. Every partition ordinal is a power of , so the question becomes: for which countable is a partition ordinal? This is Erdős Problem 592.
The question is a basic test case for ordinal Ramsey theory: it is the smallest nontrivial "unbalanced" relation (a whole order type against a finite clique), and progress on it has repeatedly required new combinatorial methods.
Timeline (as recorded on erdosproblems.com/592):
The case where is a sum of exactly three indecomposable ordinals appears to be the remaining open case.
An ordinal is identified with a well-ordered set of order type . A red/blue colouring of the complete graph on assigns to every pair of distinct vertices exactly one of two colours; equivalently, it is a pair of complementary simple graphs (red, blue) on .
For ordinals and a cardinal , the partition relation holds when every red/blue colouring of has
The Lean predicate is Erdos592.OrdinalCardinalRamsey α β c, following the encoding used by the Formal Conjectures project. A partition ordinal is an with .
An ordinal is additively indecomposable if it is nonzero and for all ; the additively indecomposable ordinals are exactly the powers . An ordinal is the sum of indecomposable ordinals when
i.e. its Cantor normal form has terms counted with multiplicity. The Lean predicate is Erdos592.IsSumOfIndecomposables k γ.
This is the positive answer in the open case, as predicted by the Galvin–Larson conjecture. Because the truth is unknown, a formal disproof (exhibiting a countable with three Cantor-normal-form terms for which the relation fails) is an equally valid resolution of the goal. Together with the milestones below, a proof of the goal gives a complete answer to Problem 592: for countable , is a partition ordinal iff or with a sum of at most three indecomposables.
The result itself. A resolution of the three-term case would, together with the results above, finish the classification of countable partition ordinals of the form asked for in Problem 592. Either answer is informative: a positive answer shows the threshold between the positive and negative cases lies between three and four terms, and a negative answer shows it lies between two and three.
Formalizing it. The drafter is not aware of any of the milestone results in Mathlib. The Formal Conjectures entry for Problem 590 links an external Lean formalization of Chang's theorem; the other results (Specker's positive and negative theorems, Galvin–Larson, Schipperus) have, to the best of the drafter's knowledge, no public machine-checked proofs. Formalizing them is a substantial project on its own, independent of the open case, and the goal itself is an open research problem.
The property is not monotone in : it holds for , fails for every finite , holds again for , and, by Schipperus, both holds and fails for various larger depending on the number of terms in the Cantor normal form of . So no induction on can settle the question, and a naive transfer of the argument for a smaller exponent to a larger one can fail. The known positive and negative results use different arguments, and the three-term case lies exactly on the boundary between the ranges they cover.
Ordinal.{u} and Cardinal.{u} in an arbitrary universe u; "countable" is γ.card ≤ ℵ₀.α.ToType, the canonical well-ordered type of order type α; a colouring is a pair of complementary SimpleGraphs (IsCompl red blue). A red is a red clique s with typeLT s = β; a blue is a blue clique of cardinality exactly 3.IsSumOfIndecomposables k γ requires a non-increasing list of exponents of length exactly k; without the ordering requirement, "sum of " would not be well defined, since for instance .ω ^ ω ^ γ means .The goal is not trivially satisfiable: the hypotheses hold, for example, for and , and the conclusion is a genuine partition relation on an infinite ordinal.
Useful reusable infrastructure includes Cantor-normal-form combinatorics for countable ordinals, order-type calculations for subsets of , and a library of the classical colourings (Specker-type constructions). Contributions formalizing any milestone are welcome.
This mission formalizes §5 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: the definition of Thompson's group and Thompson's proof that is simple.
Thompson's groups and , introduced in unpublished notes of Richard Thompson in 1965, were the first known examples of infinite, finitely presented, simple groups. Every finitely presented simple group known before them was finite. The notes of Cannon, Floyd and Parry were written in part "to make available Thompson's unpublished proofs … of the simplicity of and " (p. 216), and §5 is that proof for .
is the circle's counterpart of Thompson's group . Earlier missions on this platform formalize and its commutator subgroup (§1 and §4 of the same notes), its tree-diagram normal form (§2), and its two presentations (§3). is not simple: its abelianization is . is simple, it has elements of finite order (the generator below has order ), and it contains as the stabilizer of a point.
The circle is with its endpoints identified, in Lean UnitAddCircle (); denotes the image of . Maps compose right to left, , and , the convention of the notes.
The group (pp. 233–234) consists of the piecewise linear homeomorphisms of that map images of dyadic rationals to images of dyadic rationals, are differentiable except at finitely many images of dyadic rationals, and have slopes that are powers of . In Lean a permutation of the circle satisfies IsThompsonCircle f when it has a lift to the line: an order isomorphism of with and , mapping dyadic rationals to dyadic rationals, and affine with slope a power of between consecutive integer translates of finitely many dyadic breakpoints. T is the subgroup generated by these maps. That they already form a group is the first milestone.
The elements , , (Example 5.1). and are the generators of from the §1 mission (mapA, mapB), carried to the circle by toCircle, which sends an order isomorphism of to . (mapC) is given on by , and on , and . symT sends the formal symbols , , to these three maps.
The presented group (p. 236) is the free group on formal symbols , , modulo six relators:
In , and (XT1); and (CT1) for . An element is positive (IsPositiveT1) when it is a product of nonnegative powers of the .
The goal is the sentence in which the notes state what §5 does, "In §5 we define and give Thompson's proof that is simple" (p. 216):
The route is the section's own. Lemma 5.2 shows that , , generate and satisfy the six relations, so maps onto (Lemma 5.3). Lemmas 5.4–5.6 and a normal form (Theorem 5.7, every is with , positive and ) lead to Theorem 5.8, is simple, and hence to Corollary 5.9, . The goal follows.
The result. The simplicity of is one of the two facts that made Thompson's groups famous: is an infinite, finitely presented, simple group. Corollary 5.9 gives more, an explicit presentation of on three generators and six relators.
Formalizing it. No machine-checked proof that is simple exists on this platform, and Mathlib has nothing on Thompson's groups. The proof in the notes is short and complete. This mission connects the analytic definition of with the combinatorial group , reusing the platform's formalization of : the presentation of (Theorem 3.4), its normal form (Corollary 2.7), and the fact that its proper quotients are Abelian (Theorem 4.3).
The algebra of (Lemmas 5.5 and 5.6) is a chain of explicit inductions. The substance lies at two points.
The first is Theorem 5.7. The notes' proof that the set of elements is closed under multiplication moves past and using the normal form of , transported into through Lemma 5.4, and then re-indexes, all inside the abstract group with no geometry to lean on.
The second is the analytic side of Lemma 5.2. Generation reduces an arbitrary to an element of by composing with and with an element of that moves to . That needs the fact that an element of fixing comes from , which the notes state in one line. The relations are identities between explicit piecewise linear maps of the circle.
Subgroup (Equiv.Perm UnitAddCircle) generated by IsThompsonCircle. The lift makes every element an orientation-preserving homeomorphism, so continuity is not stated separately. Unlike for , the condition that dyadics map to dyadics cannot be dropped: an irrational rotation satisfies every other clause.PresentedGroup on the three-element type FormalABC. Relators are written out as , not with commutator notation.A -dimensional complex abelian variety is of Weil type for an imaginary quadratic field if acts on by rational endomorphisms in such a way that each of the two eigenspaces of on meets in an -dimensional subspace. A. Weil observed that such carry a two-dimensional space of rational -classes, the Hodge–Weil classes, that are in general not generated by divisor classes. Whether they are algebraic is one of the main test cases of the Hodge conjecture; by work of Schoen, Moonen–Zarhin and others, algebraicity for abelian fourfolds of Weil type implies the Hodge conjecture for all abelian fourfolds.
E. Markman (arXiv:2502.03415) proves this algebraicity by a new construction. Its starting point, developed in §§1.2 and 2 of the paper, is linear algebra: the even cohomology of an abelian -fold is a half-spin representation of , where , and a rational plane meeting the variety of pure spinors in two conjugate -points (a -secant) equips with the structure of an abelian variety of Weil type. This mission formalizes that construction and its explicit example in §2.4.
Timeline (as summarized in §1.1 of the source).
Let be a complex torus of dimension . Fix a basis of , so that , and write in dual coordinates. The complex structure of is a real matrix with acting on ; its -eigenspace is . A number acts on by and on multiplicatively; a class of type is multiplied by . The Hodge ring is .
For a complex torus of dimension with ample , and a positive integer : are even pure spinors with , and there is a rational acting by on with
That is, is a polarized abelian variety of Weil type.
Equation (2.4.6) (the annihilator of ), Equation (2.4.5) (the plane lies in the Hodge ring), Lemma 2.2.6 (Weil's condition), the rational similarity of (2.2.4)/(2.4.1), the commutation (§2.4, p. 20), and Lemma 2.4.2 (the formula for ).
The result. The construction supplies, for every imaginary quadratic field and every polarized abelian -fold, a polarized abelian variety of Weil type , together with a description of its Weil structure in spin-representation terms. The rest of the paper deforms this structure ( plays the role of the special Mumford–Tate group) and uses Orlov's derived equivalence to obtain the Hodge–Weil classes from sheaves; the final application is the Hodge conjecture for abelian fourfolds.
Formalizing it. The results of this mission are proved in the paper; none of them has a machine-checked proof. The mission produces a reusable Lean model of the spin representation of , of pure spinors and their annihilators, and of Hodge types on , all built on Mathlib's exterior and Clifford algebras.
The algebra in the explicit example is short, but the general milestones rest on facts about pure spinors (their annihilators are maximal isotropic; a conjugate pair with splits ; rationality of by Galois descent) and on Lemma 2.2.6, whose proof in the source uses Chevalley's isomorphism as a morphism of Hodge structures. A coordinate computation settles the example but not the general statements. Sign conventions (the choice of , the complex structure on , and the sign of ampleness) all enter the final negativity claim.
ExteriorAlgebra ℂ (Fin (2n) → ℂ); contraction is Mathlib's CliffordAlgebra.contractLeft; is the truncated exponential .General relativity is summed up, in S. M. Carroll's A No-Nonsense Introduction to General Relativity (2001), by two statements: spacetime is a curved pseudo-Riemannian manifold with a metric of signature , and the metric obeys Einstein's equation . The first exact solution of that equation, and still the most important one, is the Schwarzschild metric: it describes the gravitational field of the Sun outside its surface, the classical tests of GR (perihelion precession, light bending), and non-rotating black holes. Carroll's notes state its key property in one sentence: for a spherically symmetric metric, the vacuum equation has a unique solution, (72) — Birkhoff's theorem. This mission is the first of a series formalizing the capstone results of those notes.
We work in a single coordinate chart of four-dimensional spacetime. A point is ; a metric is a field of real symmetric matrices of signature , i.e. congruent to . From and its inverse one builds, exactly as in Carroll's equations:
In spherical coordinates the general spherically symmetric metric is (71)
and the Schwarzschild metric (72) is the case , .
The goal is the uniqueness statement of §6 of the notes, in the form: for smooth and positive on a rectangle with ,
The milestones follow the notes in order:
The result. Birkhoff's theorem says the exterior field of any spherically symmetric body — static, pulsating or collapsing — is the Schwarzschild field, determined by a single constant . It is why the Schwarzschild solution governs the solar system and spherical collapse, and why spherically symmetric gravitational radiation does not exist. The identities (37), (47)–(51) and (67)–(69) are the working toolkit of every GR computation; (51) is what makes Einstein's equation consistent with local energy–momentum conservation.
Formalizing it. All results here are classical and proved in the textbooks. The value of the mission is a machine-checked, coordinate-level development of the curvature identities in Carroll's exact conventions, and a checked proof of Birkhoff's theorem, which requires solving the vacuum equations as a system of PDEs rather than verifying a given solution. The platform already contains a separate Einstein-field-equations development (built from a Wikipedia-based definition file with a slightly different index placement) in which Ricci-flatness of the Schwarzschild metric is proved; this mission uses its own Carroll-faithful definitions, and that earlier work may help with milestone 12.
Verifying that a given metric is Ricci-flat (milestone 12) is a long but mechanical computation of derivatives of explicit functions. The goal is different in kind: in the "only if" direction one must extract from that (from ), integrate an ODE in to get with independent of , and then show depends on only — all with the coordinate derivatives of the formal definitions, inside a region where are only known to be smooth and positive. The general identities (47)–(51) need symmetry of second and third derivatives and the derivative of the matrix inverse.
Coord = Fin 4 → ℝ, a metric is a function Coord → Matrix (Fin 4) (Fin 4) ℝ, partial derivatives are Fréchet derivatives in coordinate directions. All functions are total: non-differentiable points give derivative , singular matrices have inverse , and . For that reason every statement names the open region (smoothness, signature , , , ) on which it is claimed.CarrollGR_Defs (Christoffel symbols, covariant derivatives, curvature, Einstein tensor in coordinates) is shared by the whole series. Contributions welcome: general lemmas about partialD of products, quotients and matrix inverses, and a tensoriality lemma for the Ricci tensor under changes of coordinates.General relativity describes gravitation through the curvature of the Levi-Civita (Christoffel) connection of a spacetime metric. An alternative description, going back to Einstein's 1928-1930 papers on distant parallelism and developed in modern form as the teleparallel equivalent of general relativity, uses instead a tetrad field and the Weitzenböck connection it defines, a connection with vanishing curvature but non-zero torsion. The paper of Aldrovandi, Pereira and Vu (Braz. J. Phys. 34 (2004) 1374) reviews this formulation as a gauge theory of the translation group, and uses it to discuss the weak equivalence principle and a global (phase-factor) formulation of gravitation.
The claim that both descriptions are physically equivalent rests on a small number of exact tensor identities: the Weitzenböck connection splits as the Christoffel connection plus the contortion tensor, its curvature vanishes identically, and the teleparallel Lagrangian differs from the Einstein-Hilbert Lagrangian only by a total divergence. This mission asks for machine-checked proofs of these identities, in coordinates, exactly as used in Sections 2-3 of the paper.
Timeline (for orientation): Einstein introduced distant parallelism in 1928 (translations in the Delphenich collection Selected Papers on Teleparallelism); Weitzenböck studied the differential invariants of the theory the same year; the modern teleparallel equivalent of general relativity was developed from the 1960s-1970s onward, and the gauge-theoretic reading used here is the one reviewed by Aldrovandi-Pereira-Vu (2004).
Work in a single global chart and write for coordinate partial derivatives. Tangent-space (Latin) indices are raised and lowered with the Minkowski metric .
Curvature of a connection is , Ricci , scalar (Landau-Lifshitz conventions, consistent with the paper's Eq. (15)). The Einstein-Hilbert density is .
For a smooth, positively oriented tetrad (, so ):
The paper states only "up to a divergence"; the divergence term is written explicitly because an unspecified divergence would make the statement empty (every function on is a divergence).
The goal identity is the precise sense in which teleparallel gravity is "equivalent" to general relativity: the two actions differ by a boundary term, so they give the same field equations (the paper's Eqs. (12) and (15)). Milestone 4 is what turns the teleparallel force equation into the geodesic equation (Eq. (20)), and milestone 2 is the dictionary between the gauge field strength and torsion used throughout Sections 3-4. The results are classical and proved on paper; to our knowledge they are not formalized in Mathlib, which has no coordinate tensor calculus of this kind. A formal development would provide reusable coordinate lemmas (derivative of an inverse matrix field, symmetry of second derivatives in index form, Christoffel symbols of ).
Each identity is elementary on paper, but the index computations are long, and in Lean every derivative carries differentiability side conditions: derivatives of inverse matrices and of determinants, and symmetry of mixed partial derivatives, must be justified from smoothness and invertibility of the tetrad. The goal identity involves second derivatives of the inverse metric and a careful bookkeeping of about a hundred index contractions.
Spacetime is as Fin 4 → ℝ with one global chart; partial derivatives are Fréchet derivatives applied to coordinate basis vectors. A tetrad is a family of real functions h a μ, assumed with invertible matrix at every point (IsTetrad). Inverses are matrix inverses (which would be for singular matrices; the invertibility hypothesis excludes this). The physical constants are arbitrary reals. All definitions live in the single definition file of the mission, namespace TeleparallelGravity.
The bosonic string can be quantized consistently only in spacetime dimensions. In lightcone quantization this appears in two ways in David Tong's Cambridge Part III lecture notes. First (Sections 2.2.2–2.3), the normal-ordering constant in the mass formula is identified with a regularized Casimir energy , using "" ; Lorentz invariance then forces the first excited states to be massless, which happens only for . Second (Section 2.4), the commutator of lightcone Lorentz generators, which must vanish for the quantum theory to be Lorentz invariant, is proportional to a coefficient that vanishes for all oscillator levels exactly when and (Goddard–Goldstone–Rebbi–Thorn 1973).
Let be the number of spacetime dimensions, so there are transverse oscillator directions, and let be the Regge slope. In lightcone gauge the mass of a closed-string state at level is (2.25)
with an undetermined normal-ordering constant . The heuristic evaluation of replaces the divergent zero-point sum by its cut-off regularization , or by the Riemann zeta function value , giving (2.26). The first excited states (2.28) are in number and have . In one sector the level-2 states are (unordered pairs , since the oscillators commute) and . Finally, Section 2.4 states that
For and ,
The result. The critical dimension is the single most-quoted prediction of the bosonic string, and the pair fixes the entire lightcone spectrum: the tachyon , the massless graviton, -field and dilaton, and the massive tower .
Formalizing it. This mission formalizes the mathematical steps of Tong's lightcone derivation: the two regularizations of , the mass-shell and state-counting arithmetic, and the final algebraic step of the Lorentz-algebra argument. It does not formalize the operator computation of in the lightcone Fock space, which Tong quotes ("After a tedious computation, one finds ...") without derivation; that computation is a natural follow-up mission. The value is already available in Mathlib through the Bernoulli-number formula for at negative integers.
The individual statements are elementary once formalized; the difficulty is faithfulness rather than proof. The regularized sum is an asymptotic statement whose leading term diverges, so it has to be stated as an remainder along rather than as an equation; and the goal is a statement for all levels , where a single level () only forces and two levels are needed to force .
The dimension is a natural number and the normal-ordering constant a real number. The regularized sum is Mathlib's tsum of over (the term vanishes), and the asymptotic claim uses Mathlib's big-O along the right neighbourhood filter of . Level-2 states of one sector are counted as unordered pairs with repetition of transverse indices (Mathlib's Sym2 (Fin (D-2))) plus the states ; natural-number subtraction and division are safe because is assumed and is even. The zeta function is Mathlib's riemannZeta, i.e. the analytic continuation.
In 1973 Bardeen, Carter and Hawking showed that stationary black holes in general relativity obey four laws with the same structure as the laws of thermodynamics, with the surface gravity of the horizon playing the role of temperature and the horizon area the role of entropy (Bardeen–Carter–Hawking 1973). Two years later Hawking showed that quantum fields near a black hole produce thermal radiation at temperature (Hawking 1975), which turned the analogy into an identification, with entropy .
The M.Sc. dissertation Termodinâmica de Buracos Negros (F. H. de C. Menezes, UFMG, 2021) presents this construction for the Kerr black hole, the rotating stationary solution of Einstein's vacuum equations. The first law, eq. (3.79), is its central quantitative statement:
relating first-order changes of mass , horizon area and angular momentum between neighbouring Kerr black holes, where is the angular velocity of the horizon.
Timeline: Kerr found the rotating solution (1963); Smarr derived the mass formula (1973); Bardeen, Carter and Hawking stated the four laws (1973); Hawking derived the thermal emission (1974–75).
Units are geometrized, (and for quantum quantities). A Kerr black hole has mass and rotation parameter with ; its angular momentum is . In Boyer–Lindquist coordinates the metric involves
with angular components and . The zeros of are ; the event horizon is .
A Kerr black hole is non-extremal when , equivalently .
Regard as functions of with . For and , the area is differentiable at and, as linear forms in ,
In the dissertation the first law is the sum of the variation (3.45) of the Smarr formula and the relation (3.78).
The first law is the identity behind the identification , : with these values it becomes , the ordinary first law of thermodynamics for a rotating body. The Smarr formula is its integrated (Euler-relation) form, and the vanishing of at extremality underlies the dissertation's formulation of the third law.
All results are classical and proved in the literature. The contribution of the mission is a machine-checked version of the explicit Kerr relations, with the horizon area computed from the metric rather than taken as given, and a check of the dissertation's formulas. One such check is already recorded: the coefficient printed in eq. (3.78) conflicts with the dissertation's own eqs. (3.70) and (3.77), which give , the value required for (3.79); the milestone uses .
The dissertation derives the first law geometrically, from Komar integrals and a perturbation of the horizon Killing field. That route needs Lorentzian geometry, Killing horizons and Stokes' theorem on manifolds, which the Lean library does not provide. The explicit route through the Kerr formulas avoids this, but has its own obstacles: the horizon area is a double integral of a square root of a rational trigonometric expression that simplifies only on the horizon, where ; and the differentials involve , which is not differentiable at extremality, so the non-extremal hypothesis must be used when differentiating.
All quantities are real-valued functions of real arguments, defined in one definition file in the namespace KerrBlackHoleThermo. Every theorem restricts to the physical range explicitly ( and , or and for statements involving derivatives), so Lean's conventions for of negative numbers and division by zero do not enter the physical content. First-order variations "between two neighbouring Kerr configurations" are formalized as Fréchet derivatives (HasFDerivAt) of the explicit family in the coordinates ; the first law is an identity of linear forms on . The horizon area is defined as a metric integral, not as the closed form (3.44), so the goal cannot be reduced to a pure algebraic identity by definition.
Out of scope: the general-spacetime versions of the zeroth, second (area theorem) and third laws, which need a theory of Lorentzian manifolds, event horizons and energy conditions, and the quantum field theory derivation of Hawking radiation in Chapter 4. Contributions building that infrastructure are welcome as separate missions.
Modern machine-learning systems are routinely assembled by grafting: pretrained components (an encoder, a decoder) are re-used inside a new architecture, parts of them are frozen, and only selected coordinates are trained. When the full computation does not fit in memory, practitioners cut the loss into tiles (microbatches, row blocks, vocabulary shards), accumulate gradient contributions, and apply the optimizer once. Every memory-constrained trainer assumes this tiled schedule computes the same update as the monolithic one — but the folklore proof hides real failure modes: updating parameters after each tile, averaging tile means, clipping per tile, detaching a frozen component's input, or saving a weights-only checkpoint all silently change the learner.
This mission turns that folklore into a theorem with explicit hypotheses. The design source is the Vathek Graft white paper (Davis, 2026), which proposes an open-predicate extractor trained as a graft and makes the schedule-preservation claim its first proof obligation (Theorem T0). The architectural precedents are established: parallel set-based extraction (DetIE), set-prediction objectives, pointer-generator copying, and low-rank adaptation of frozen bases. What none of them supplies is the exact-arithmetic statement that the memory-saving row schedule preserves the mathematical update — that is the target here.
Fix finite-dimensional spaces: logical parameters , of which only coordinates are trainable ( zeroes frozen coordinates), and a shared-state space . One training frame carries a differentiable shared computation (the donor encoder plus shared projections), finitely many occurrence losses with fixed coefficients over a finite occurrence set , and all discrete choices, fixed during one logical update. The monolithic objective is
A tile partition splits into pairwise-disjoint tiles. The tiled evaluator streams the tiles through an accumulator of three slots — running loss, direct parameter-gradient contribution , shared cotangent — everything read at the same pre-update point , and finishes with one reverse pass:
Then the gradient is projected to trainable coordinates, globally clipped at radius , and a deterministic optimizer is applied exactly once: , where is the complete transition-relevant state (parameters, optimizer moments, step counter). One concrete masked-optimizer instance (masked AdamW) is included so "no decay on frozen coordinates" is a theorem, not a hope.
The goal theorem packages exact one-step, trajectory, and restart preservation:
and, by induction over a deterministic frame sequence, equality of the tiled and monolithic state trajectories, plus restart equality: saving at any completed update boundary and reloading the round-tripped structural snapshot preserves the remaining trajectory,
Twelve milestones build the result: partition flattening; weighted partition sums; the shared-path chain rule ; linearity of the reverse pass over summed cotangents; the streaming-accumulator invariant and order independence; frozen-input differentiation with a concrete nonzero witness ( through a frozen donor gives gradient at ); projection–clipping–optimizer congruence; one-step equivalence; trajectory equivalence; checkpoint round trip; restart equivalence; and the full two-tile non-vacuity witness, whose tiled gradient is the nonzero while its detached (input-frozen) variant falsely gives .
The result itself. Each clause rules out a real implementation bug: per-tile means change the objective on uneven tiles; updating after each tile reads moved parameters; clipping per tile differs from global clipping (gradients and sum to , but clipped-then-summed give ); a weights-only checkpoint loses optimizer state and changes the resumed trajectory. A verified tiled trainer — or a verified compiler schedule for one — can cite this mission's lemmas as its exactness certificate.
What formalizing it adds. The paper states Theorem T0 informally with a proof sketch; no machine-checked version exists. The load-bearing content is precisely the discipline of hypotheses: the certificates that per-occurrence gradients are genuine derivatives (partial derivatives alone do not give the chain rule), the single pre-update point for all tiles, and the complete transition state. Follow-on missions in the same vocabulary (source-byte integrity, masked normalization, matching invariance, numerical refinement, resource bounds) can import these definitions.
The analysis is elementary; the danger is vacuity and silent strengthening. A statement that hypothesizes "the tiled gradient is correct" proves nothing; one that hypothesizes differentiability of every branch at every point in a way no real frame satisfies proves nothing either. The encoding must let tiles be empty and uneven, let the occurrence set be empty (zero objective, not division by zero), quantify certificates only at the points used, and keep the optimizer deterministic-but-arbitrary. The counterexamples above are disproof fixtures: a correct statement survives all of them without ad-hoc exclusions.
Parameters are EuclideanSpace ℝ (Fin d); gradients use HasGradientAt with genuine Fréchet derivatives paired by inner-product duality, and the reverse pass is ContinuousLinearMap.adjoint — no uninterpreted gradient oracle appears anywhere. Partitions are lists of Finsets; the accumulator is an executable fold. The checkpoint is a real-valued structural snapshot (coordinate lists); finite-byte codecs and floating-point associativity are explicitly out of scope — the theorem is exact-arithmetic. A trivializing formalization (defining the tiled gradient as the monolithic one, or hypothesizing the conclusion) is ruled out: milestone M12 exhibits a concrete instance with nonzero gradient that satisfies every hypothesis, and the detachment mutant shows the hypotheses have teeth.
Definitions are shared across the whole mission series under the VathekProof namespace: the frame, derivative-certificate, state, and optimizer files are reusable beyond this mission. Contributions welcome on any milestone; the witness computations (M06, M12) are self-contained entry points.
For a field , two invariants built from very different data turn out to carry the same mod-2 information. One is Milnor K-theory , defined by generators and relations from the multiplicative group alone. The other is Galois cohomology , the continuous cohomology of the absolute Galois group of . In 1970 Milnor considered a natural map in all degrees, verified that it is an isomorphism for several classes of fields, and remarked that he knew of no field where it fails (Milnor 1970). The statement that it is always an isomorphism when became known as the Milnor conjecture. Its companion conjecture on quadratic forms was later deduced from it (Orlov–Vishik–Voevodsky 2007). Together they identify the graded Witt ring of quadratic forms, Galois cohomology mod 2, and .
Timeline. The attributions below follow the introduction of Voevodsky 2003.
Let be a field with in .
Milnor K-theory. For , is the quotient of the -fold tensor power , taken over with written additively, by the subgroup generated by the pure tensors in which some adjacent pair satisfies . This is the degree- part of , where is the two-sided ideal generated by . The class of is the symbol . In particular and . In Lean these are MilnorK F n and symbol a for a : Fin n → Fˣ.
Galois cohomology. Let be a separable closure and the absolute Galois group, a profinite group under the Krull topology. is the continuous cohomology with trivial action, computed from -invariant continuous homogeneous cochains. In Lean this is H F n, Mathlib's continuousCohomology n of the trivial representation.
The Galois symbol. For fix . The Kummer character is if and otherwise. It is a continuous homomorphism representing the Kummer class . The Galois symbol of is the class of the homogeneous cocycle
the homogeneous form of , i.e. the cup product . In Lean this is galoisSymbol a.
For every field with and every there is a homomorphism
which is surjective and whose kernel is exactly .
Since symbols generate , such a is unique; it is the norm residue homomorphism. The statement is therefore equivalent to via the norm residue map. Its existence, i.e. the fact that the Steinberg relations map to zero, is part of the claim.
The result itself. The theorem gives a presentation of mod-2 Galois cohomology by generators and relations: every class is a sum of cup products of degree-one classes, and every relation among such products comes from Steinberg relations and multiples of 2. With Orlov–Vishik–Voevodsky 2007 it yields Milnor's conjecture on quadratic forms, which classifies quadratic forms up to Witt equivalence by their Galois-cohomological invariants.
Formalizing it. The theorem is proved but not formalized. At the time of writing, Mathlib has neither Milnor K-theory nor cup products in group or continuous cohomology, and has Hilbert 90 only for finite Galois extensions. This mission's definitions provide a sorry-free Galois symbol in Mathlib's continuous cohomology, which already makes the degree 0 and degree 1 cases (Kummer theory) meaningful targets. A complete development would formalize the IHES proof, including motivic cohomology with coefficients and the motivic Steenrod algebra. No part of that is currently available in Lean. Related existing work: on this platform, a graded cup product (groupCohomology.exists_isGradedCupProduct) and a Kummer theory and Hilbert 90 for level-constant cocycles have been formalized on top of Mathlib's discrete groupCohomology. The cup product is for discrete groups, and the Kummer and Hilbert 90 results use finite-level hypotheses in place of continuity, so none of them transfers directly to continuousCohomology.
Degrees 0 and 1 follow from Kummer theory and Hilbert 90. Degree 2 is Merkurjev's theorem, whose proof goes through the K-theory of Severi–Brauer varieties. No argument internal to Galois cohomology or K-theory of fields is known in higher degrees. The known proof reformulates the statement as a vanishing theorem for motivic cohomology of fields, the "Hilbert 90" property for weight . It then argues by induction on through geometry over : splitting varieties of symbols (Pfister quadrics), their motives, and cohomology operations on motivic cohomology. Each of these is a substantial theory, none of it exists in Mathlib, and the induction passes through statements about arbitrary smooth varieties, not only fields.
Scope. The target is the Milnor conjecture, i.e. the prime with coefficients . The Bloch–Kato conjecture for odd primes is out of scope.
Conventions.
F : Type, universe 0. Mathlib's continuousCohomology requires the coefficient module to live in the universe of the group. For in a higher universe this forces ULift (ZMod 2), for which the needed Module and ContinuousSMul instances are not available as global instances. Universe polymorphism is not part of this mission. It does not follow by plain transport, since a field in a higher universe need not be isomorphic to any field in Type; one route is a limit argument, using that both sides commute with directed unions of fields and that every field is the directed union of its countable subfields, each isomorphic to a field in Type.[NeZero (2 : F)].continuousCohomology, built from homogeneous cochains, with as a trivial representation of with the Krull topology.Ruling out trivializations. The Galois symbol is not a free parameter. It is a fixed, sorry-free definition, and the existence of with the prescribed values on symbols is part of the goal. Neither can be chosen to make the statement vacuous.
Route. Reductions should follow Voevodsky 2003 together with Voevodsky 2003b. That route avoids resolution of singularities and works in every characteristic . The following rely on resolution of singularities (or on characteristic-0 reductions) and should not be used as inputs:
Infrastructure needed and reusable. A complete development needs:
Most of this is reusable well beyond the mission. The homogeneous-cochain construction in the definition files, which turns an invariant continuous cocycle into a class in Mathlib's continuousCohomology, applies to any locally compact group with trivial coefficients. Contributions of any of these components, and of the degree 0 and 1 cases, are welcome.