Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Duality is the organizing principle of convex optimization: a minimization problem's optimal value equals a maximization problem's optimal value, and this coincidence, rather than being a lucky accident, follows from a separating-hyperplane argument that applies whenever the two problems' feasible regions are shaped compatibly enough. Werner Fenchel formalized this in the 1950s for pairs of convex and concave functions related by the Legendre-Fenchel transform, and the resulting Fenchel duality theorem specializes, for linear objectives over polyhedral feasible regions, to linear programming duality — the fact, central to the entire theory of combinatorial optimization, that a linear program's optimal value can always be certified from above and below by a pair of primal and dual feasible solutions. Murota's Discrete Convex Analysis (SIAM, 2003) collects this classical machinery, together with the integrality theory that lets it produce combinatorial (integer-valued) certificates rather than merely real ones, as the technical foundation the rest of the book builds its discrete theory on top of.
For , the epigraph is , and is convex iff is a convex set; is proper if additionally its effective domain is nonempty, and closed if is topologically closed. A function is concave, proper, closed analogously via its hypograph. The convex conjugate is , and the concave conjugate . The relative interior of a set is the interior of relative to its affine hull. A function is polyhedral if its epigraph (or hypograph) is a finite intersection of half-spaces. Given an matrix , , , the primal and dual linear programs are and , with feasible regions , . A matrix is totally unimodular if every square submatrix has determinant , , or . A discrete set is hole free if , where is the convex hull of 's real embedding; the discrete Minkowski sum is .
Goal (Theorem 3.6, Fenchel duality). For proper convex and proper concave satisfying at least one of four alternative conditions — a relative-interior condition on , a polyhedrality condition on the same, or the analogous pair of conditions on together with closedness of , —
with the extremum on the appropriate side attained whenever the common value is finite. This is the mission's capstone: the four alternative hypotheses make it the most broadly applicable statement of the four convex-duality results in this mission, each of the other three being either a special case in substance (Theorem 3.5, separation, which 3.6 is proved from) or a literal specialization to linear data (Theorem 3.10, LP duality).
Supporting milestones. Theorem 3.2 (biconjugation: is always closed proper convex, and for closed proper convex ); Theorem 3.5 (the separation theorem for convex/concave functions, under two of Theorem 3.6's four hypotheses); Theorem 3.9 (the Farkas lemma, equality form); Theorem 3.10 (LP duality: weak duality, strong duality with attainment, and complementary slackness); Theorem 3.13 (total unimodularity of the constraint matrix guarantees an integral optimal solution whenever an optimal solution exists); Proposition 3.14 (an explicit potential function certifying a minimum-weight bipartite perfect matching, via the totally unimodular incidence-matrix LP); and Proposition 3.16 (for a translation-invariant family of hole-free discrete sets, the property that discrete disjointness implies closure disjointness is equivalent to the discrete Minkowski sum matching the integer points of the closures' Minkowski sum).
Fenchel duality is the single result from which the separation theorem, LP duality, and (via the
totally-unimodular incidence matrix of a bipartite graph) the combinatorial duality underlying
weighted bipartite matching all descend, in one unbroken chain of specialization; formalizing
this chain in one mission exhibits that structure directly, rather than treating each result as
an independent fact. Proposition 3.16 plays a different role: it is the chapter's warning that
naive discrete analogues of convexity (hole-freeness) do not automatically inherit convexity's
good closure properties under Minkowski sums, which is exactly the gap the book's later
M-convexity and L-convexity machinery is built to close — this mission's Proposition 3.16 is
therefore the motivating negative result for the rest of the book's positive theory, not a loose
end. So far as a platform search shows, no existing formalization matches this chunk's specific
combination of extended-valued (possibly ) functions, the four-alternative Fenchel
duality hypothesis, or the bipartite-matching-via-total-unimodularity argument; the one related
platform result (VectorSpaceOpt.fenchel_duality, from Luenberger) is for real-valued functions
on general normed spaces under a single relative-interior-and-solidness hypothesis, a different
generality from the extended-valued, four-hypothesis statement here.
The naive approach to Theorem 3.6 tries to prove the duality gap is zero directly from the definitions of the two conjugates, which only gives the easy inequality (a one-line computation, shown in the book's own proof in three lines); the substantive content is the reverse inequality, and it genuinely fails without a constraint-qualification hypothesis like (a1)-(b2) — Example 3.8 in the book exhibits a convex/concave pair with when none of the four conditions hold. The book's actual route reduces Theorem 3.6 to the separation theorem (Theorem 3.5) applied to shifted down by the (assumed finite) infimum, which produces the separating affine function directly; this is why Theorem 3.5, although logically a special case in spirit, earns its own milestone rather than being subsumed silently.
All convex and concave functions are represented uniformly as (V → ℝ) → EReal-valued
(Fintype V), rather than mixing WithTop ℝ for convex and WithBot ℝ for concave functions,
so that Theorem 3.2's biconjugate — whose properness is a conclusion, not an assumption — has a
well-defined codomain without extra casts. Convexity is defined via the epigraph being a convex
subset of the ordinary real vector space (Mathlib's Convex ℝ),
following the book's own equivalent characterization, rather than unfolding the direct
inequality definition, which would require a extended-arithmetic scalar-multiplication
convention (0\cdot(+\infty)=0) that Mathlib does not provide for EReal. The relative interior
is defined directly from the book's own metric-ball-intersected-with-affine-hull description,
since Mathlib has no relative-interior primitive at the pinned revision. Polyhedra are finite
intersections of explicit half-spaces. A bipartite perfect matching is represented as a bijection
between the two vertex sides restricted to the edge set — a faithful, not narrower,
representation since every perfect matching between equal-size parts arises this way. The
formalization does not trivialize: Theorem 3.6's four hypotheses are carried in full (not reduced
to the easiest single case), and no result is stated only for finite-valued (never )
functions, which would discard the entire point of the extended-value convex-analysis framework
this chapter sets up for the rest of the book. Infrastructure needed beyond Mathlib's Convex,
Matrix, and EReal API: all epigraph/hypograph, conjugate, relative-interior, and polyhedral
apparatus is defined fresh in DiscreteConvex.IntegralConvexityB; a contribution proving any of
the seven milestones independently, or supplying Mathlib-quality relative-interior lemmas, would
be a natural entry point.
Real investors do not merely accumulate wealth for a single terminal payoff; they consume along
the way, and the market they invest in is rarely a single fixed statistical regime for years at
a time — bull and bear markets, business cycles, and volatility regimes shift the distribution
of returns. Bäuerle and Rieder's §4.3 extends the terminal-wealth theory of chunk 04a by
adding a consumption choice at every stage (the Ramsey/Merton consumption-investment problem),
and §4.4 extends it again by letting the return distribution itself depend on a hidden,
Markov-modulated environment state. Both extensions are shown to be genuine instances of the
same abstract finite-horizon Markov Decision Process machinery from Chapter 2 — the joint
consumption-investment choice and the extra regime coordinate change the state and action
spaces, but not the proof strategy, which is exactly the point.
The consumption-investment problem: state (wealth), action (consumption , amounts invested), transition , reward , terminal reward . Value functions . The one-period sub-problem: , , .
The regime-switching extension (§4.4): an environment process , a finite-state Markov chain with transition probabilities , modulates the risky-asset return law: given , the next relative risk has law , and has joint law given , . The augmented state is ; value functions are defined analogously, with the recursion incorporating a finite sum over the next regime.
with strictly increasing, strictly concave, continuous, and an optimal strategy realized
by per-stage maximizers. This is chunk 04a's Theorem 4.2.2 with consumption added, and every
closed-form corollary below specializes it.
Eight milestones: the one-period existence/regularity theorem (Theorem 4.3.1); the zero-mean special case (Theorem 4.3.5); power- and logarithmic-utility closed forms (Theorems 4.3.6, 4.3.7); the regime-switching generalization of the goal itself (Theorem 4.4.1), its power-utility closed form (Theorem 4.4.2), and two comparative-statics results on how the optimal policy moves across regimes under a stochastic order (Theorems 4.4.4, 4.4.5).
Theorem 4.3.3's consumption-investment structure theorem is the basis for every result about optimal spending and saving under uncertainty; its power/log closed forms (Theorems 4.3.6/4.3.7) recover the classical facts that a power-utility investor consumes and invests constant fractions of current wealth (myopic, wealth-independent policy fractions) while a log-utility investor's optimal consumption fraction, , is the textbook "consume your remaining horizon's worth" rule. The regime-switching extension (§4.4) is the discrete-time analogue of Hamilton's regime-switching models, now standard in empirical finance; Theorems 4.4.4-4.4.5 give a rigorous comparative-statics answer to "does a riskier regime call for more or less stock exposure," using the increasing-concave stochastic order rather than a first- moment heuristic — the mathematically correct notion of "regime 's returns dominate regime 's for every risk-averse (concave, monotone) preference," not merely "regime has a higher mean."
No result of this chunk was found on the platform (searched "consumption investment", "regime
switching", "stochastic order"). The proofs largely mirror chunk 04a's (the book itself says
so explicitly for Theorems 4.3.1, 4.3.7, 4.4.2), so this mission's contribution is the precise
joint-choice statement of each result and, for the comparative-statics theorems, the correct
increasing-concave order (≤_icv, Definition B.3.9c) rather than the plain concave order
(≤_cv) chunk 02c already needed for a different theorem — the two are genuinely different
relations and must not be conflated.
The naive approach to the goal decouples the consumption and investment choices into two independent optimizations; the book's own proof shows they do separate at the level of the per-stage optimization (Theorem 4.3.6's proof: the transformed problem factors into a consumption fraction and an investment fraction optimized independently once the wealth scale is normalized out), but the admissible sets remain jointly constrained ( interacts with the investable amount ), so treating them as literally independent unconstrained problems would silently solve an easier, different problem. For the regime-switching comparative statics (Theorem 4.4.5), the natural first attempt tries to prove monotonicity of in directly from alone; the book's own induction needs both hypotheses simultaneously (the environment chain's own stochastic monotonicity, governing how the regime itself evolves, and the return-distribution order, governing the one-period objective) — Theorem 4.4.4's monotonicity of handles the second factor of the induction's product (Eq. (4.22)) while the chain's stochastic monotonicity handles the first; dropping either hypothesis breaks the induction step.
The consumption-investment vocabulary (ConsumptionInvestmentMarket, its value function, the
one-period sub-problem) mirrors chunk 04a's pure-investment TerminalWealthMarket pattern
exactly, extended to a joint action. The regime-switching model
(RegimeSwitchingMarket) represents the finite regime set abstractly (a Fintype with a
row-stochastic transition matrix p : EY → EY → ℝ, not a PMF/product-measure construction on
the joint disturbance): the book's own formula for is already a finite sum over the
next regime of an integral against , so this is the direct, faithful representation and
needs no additional measure-theoretic machinery — Jpi/J are built via an accumulator
recursing through this finite-sum-of-integrals at each step (the natural generalization of
chunk 04a's EFromToAcc pattern to a kernel that depends on an evolving state coordinate,
rather than an exogenous process). Theorem 4.4.4/4.4.5 introduce LEIncreasingConcaveOrder
(Definition B.3.9c) fresh, since chunk 02c's stochastic-order triple (≤_st/≤_cv/≤_cx)
does not include the increasing-concave order this chunk's theorems actually use — reusing one
of those three would silently substitute a different hypothesis, exactly the trap the chunk
brief warns against. IsStochasticallyMonotoneChain (Definition B.3.13) is likewise restated
fresh for a finite chain given by its transition matrix.
No trivializing formalization: D_n(x) is a genuine joint constraint on (c,a) (not two
independent unconstrained choices); the six closed-form theorems (4.3.6, 4.3.7, 4.4.2, plus the
comparative-statics pair) each state their own explicit recursion for — matching the
brief's own note that the index-base convention is not uniform across them (Theorem 4.3.6
gives and recurses backward; Theorem 4.4.2 gives and recurses forward) — encoded
exactly as each theorem states it, not standardized to one direction.
Stochastic approximation is the family of recursive algorithms that locate a zero of a function observed only through noisy evaluations. It goes back to Robbins and Monro (1951) and today underlies stochastic gradient descent, temporal-difference learning, Q-learning and actor–critic methods in reinforcement learning, and models of learning by boundedly rational agents.
The standard analysis is the O.D.E. method (Ljung 1977; see Kushner and Yin 1997): the interpolated iterates are compared with the solutions of an ordinary differential equation, and convergence of the algorithm follows from the stability of that ODE. The method has one well-known gap. It assumes, rather than proves, that the iterates remain bounded with probability one. In applications this stability hypothesis is often the hardest part: for asynchronous Q-learning and adaptive critic algorithms, almost sure boundedness had been proved only for discounted cost or after adding a projection step (Borkar and Meyn, p. 460).
Borkar and Meyn (SIAM J. Control Optim. 38 (2000)) close this gap with a scaling argument borrowed from the fluid-model approach to the stability of queueing networks (Dai 1995; Dai and Meyn 1995). They show that boundedness itself follows from the asymptotic stability of the origin for a second, "fluid-limit" ODE obtained by rescaling the drift. This mission formalizes that stability theorem for tapering step sizes, and the convergence theorem that follows from it.
Fix and work in with the Euclidean norm. Let and let be a deterministic sequence of positive step sizes. On a probability space , random vectors and satisfy the stochastic approximation recursion
Its mean ODE is (1.2). For the scaled field is , with the scaled ODE (1.4).
A point is globally asymptotically stable for if it is a Lyapunov-stable equilibrium and every solution converges to it.
Under (A1), (A2) and (TS), if has a unique globally asymptotically stable equilibrium , then for every initial condition ,
The goal contains no constants and no rates, only the qualitative conclusion.
Under (A1), (A2) and (TS), for every initial condition,
The result. Theorem 2.1 (i) turns the stability hypothesis of the O.D.E. method into a checkable condition on a deterministic ODE. Theorem 2.2 then gives convergence to with no a priori boundedness assumption. The paper applies this to reinforcement learning, obtaining the first convergence proof for asynchronous Q-learning and adaptive critic algorithms for average-cost Markov decision processes (the asynchronous extension, Theorem 2.5, is sketched in the paper and is not part of this mission). The same fluid-limit criterion is now a textbook tool; see Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint (2008), Chapter 3.
Formalizing it. The theorems are proved in the paper, and the proofs are short but rely on several standard facts stated informally: uniform convergence of to on compact sets, continuous dependence of ODE solutions on initial data and on the vector field, and the martingale convergence theorem. No machine-checked version of the O.D.E. method or of this stability criterion is known to exist. A formal development would give a verified link between discrete-time stochastic recursions, martingale convergence in Mathlib, and the stability theory of Lipschitz ODEs.
The obvious approach is to compare the iterates with solutions of over windows of fixed ODE time and to control the accumulated noise by martingale convergence. This fails without boundedness: the noise bound in (A2) grows with , so the deviation from the ODE can only be controlled relative to the current size of the iterate, and nothing prevents the iterates from escaping to infinity.
A second difficulty is that the hypothesis (A1) concerns only the fluid limit , which describes the drift at infinite scale. It says nothing directly about at any finite state, and nothing about the noise. Any argument therefore has to transfer information from the limit to the recursion at random, path-dependent scales, uniformly over those scales, while the noise is controlled only relative to the current size of the iterate. In Lean this involves ODE comparison and Gronwall estimates on a random partition of the time axis, conditional second-moment estimates for a rescaled recursion, and a vector-valued martingale convergence argument, none of which is available off the shelf for this setting.
The state space is EuclideanSpace ℝ (Fin d). An ODE solution is a forward solution on : the derivative is taken within at each , which makes solutions continuous there. Stability notions are the standard ones (Lyapunov stability; asymptotic, global asymptotic and global exponential stability, the last in the form ). All vector fields in the mission are Lipschitz, so forward solutions exist and are unique, and quantifying over "every solution" is meaningful.
The filtration in (A2) is the natural filtration of the iterates. Because , it carries the same information as the paper's . (A2) includes integrability of and , so that the conditional expectations are meaningful. The theorems quantify over every probability space and every noise process satisfying (A2); the goal and Theorem 2.1 (i) take a deterministic initial condition, as the paper does. Stating the goal for a particular noise model (no noise, or i.i.d. noise) would be a different and much weaker theorem, and is ruled out. "" is boundedness above of the set of norms, not a real supremum, which Lean sets to on unbounded sets. Second-moment suprema in Lemma 4.5 are taken in .
The proof objects of Section 4.1 (time grid , blocks and , scales , the interpolation , the rescaled iterates and noise sum) are separate definitions built from the step sizes and the sample path, as on the page. The piecewise ODE solutions and are characterized by a predicate, and the lemmas hold for every function satisfying it.
Useful infrastructure, reusable beyond this mission: Lipschitz ODE comparison and continuous-dependence estimates in Mathlib's ODE library, uniform convergence of on compact sets, the discrete Gronwall lemmas, and -bounded vector-valued martingale convergence. Contributions are welcome on any milestone. The two Gronwall lemmas and Lemma 4.1 are self-contained entry points.
Scheduling jobs on unrelated machines so as to minimize the makespan (the time at which the last machine finishes) is one of the central problems of approximation algorithms. For the general problem, Lenstra, Shmoys and Tardos (1990) gave a 2-approximation and showed that no polynomial-time algorithm achieves a factor below unless P = NP; closing the gap between and has been open since.
The restricted assignment problem is the special case in which every job has a single size and may only run on a given set of machines. The hardness already holds here, and the best known algorithms were still -approximations. Every linear program previously used for the problem has integrality gap , so a better LP lower bound was the natural target.
Svensson (2011) showed that the configuration LP of Bansal and Sviridenko (2006), whose variables assign whole sets of jobs to machines, has integrality gap at most . Its optimum therefore gives a polynomial-time estimate of the optimal makespan within a factor strictly better than .
An instance consists of finite sets (jobs) and (machines), sizes , and for each job a set . A schedule is a map with . The load of machine is , and the makespan is the largest load. is the least makespan of a schedule.
For a target makespan , a configuration for machine is a set of jobs that may all run on ( for ) with . Write for the set of configurations. The configuration LP asks for with
Its dual has variables and constraints for all and . is the least at which [C-LP] is feasible, and .
In the Lean development these are configs Γ p T i, CLPFeasible Γ p T, CLPDualFeasible Γ p T y z and schedLoad p σ i, in the namespace RestrictedAssignment.Svensson.
For every instance with and every ,
Equivalently . The statement is scale-free and does not define .
The milestones follow the paper's proof, which normalizes and sets :
Three facts from Section 2 complete the list: normalization by scaling, , and monotonicity of feasibility in .
The theorem shows that the configuration LP is a strictly stronger relaxation than those behind the factor- algorithms. With the known polynomial-time approximate solvability of the LP, it gives a polynomial-time algorithm that estimates the optimal makespan of restricted assignment within . The local search in the proof finds a schedule of the same quality, but it is not known to run in polynomial time. Later work lowered the constant to (Jansen and Rohwedder, 2017) along the same lines.
The result is proved on paper. As far as known, no part of it has a machine-checked proof. Formalizing it gives:
The milestones are stated with the corresponding hypotheses.
The obvious approach, rounding a fractional configuration solution, loses a factor . If each machine takes one configuration and the collisions of jobs chosen twice or not at all are repaired, the repair can double a load. This is where every earlier LP-based bound stalls.
The milestones along the paper's route are hard for two reasons. First, the dual pair rounds job sizes down by class (big to , medium to ). Proving requires a case analysis over how each blocked machine came to be blocked. The two claims are therefore false for arbitrary states of the search and hold only for states the algorithm actually reaches, so the invariants of reachable states have to be formalized too. Second, the search both adds and removes blockers, so no simple quantity decreases at every step. Termination needs a potential defined on the whole history of the search.
Jobs and machines are finite types with decidable equality, sizes are real numbers with , and admissible machines are a Finset per job. Schedules are total maps with stated explicitly. Partial schedules are maps Option M. Constants are exact rationals in . Values of moves live in Lex (ℝ × ℝ).
Algorithm 2 is a step relation Step, not a function. The move of minimum lexicographic value is a hypothesis on the chosen pair, so every tie-breaking rule is covered. The blocker tree is stored as its list of blockers in insertion order. Claims 4.7, 4.8 and Lemma 4.6 quantify over states reachable from the initial state, as their proofs require. Lemma 4.9 asserts that no infinite run exists.
Three statements would trivialize the goal, and the formalization rules them out:
Theorem 1.1 (polynomial time), the separation oracle, and Section 3's two-size case are not part of the mission.
Useful contributions include:
The configuration LP definitions are reusable for the Santa Claus problem and for bin packing.
Mission III's Theorem 6.2 — "fluid limit stability implies SPN stability" — converts a probabilistic stability question into a real-analysis question, but it only supplies the generic fluid equations (6.1)-(6.6), which hold under any control policy and therefore say nothing policy-specific: (6.1)-(6.6) alone never force a fluid path to reach zero. To actually prove a concrete queueing network stable, one must first identify the extra fluid equation a specific policy forces on every fluid limit path, and prove that this extra equation genuinely holds — a task the book calls "justifying" the equation "through the same fluid limit procedure used in the proof of Theorem 6.5." J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) carries out this derivation for four control-policy families in Chapter 7, laying the groundwork every later stability chapter of the book (feedforward networks, the Rybko–Stolyar boundary, back-pressure, proportional fairness, task allocation) builds on.
The first-come-first-served (FCFS) analysis traces to Rybko and Stolyar's 1992 fluid-scaling argument and was first stated in closed form as Eq. (2.6) of M. Bramson's 1996 paper on FCFS queueing networks; Bramson also showed by example (1994) that FCFS networks can be unstable even under the standard load condition, motivating the need for a precise fluid-equation characterization rather than an informal one.
A queueing network (Section 2.6) is an SPN with one activity per buffer: buffer/class is served by a unique pool , and on completion a class- job becomes class with probability (the routing matrix). denotes the set of classes served by pool . The fluid equations (6.1)-(6.6) specialize accordingly: consumption is the identity () and the output matrix is .
Three control-policy families are studied. A policy is non-idling if no server sits idle while a job waits in one of its buffers. A static buffer priority (SBP) policy is non-idling and additionally orders same-pool classes by a fixed priority permutation , always serving the highest-priority non-empty class first; it is non-preemptive if a job's service, once begun, is never interrupted by a later higher-priority arrival. Under FCFS, jobs at a pool are served strictly in arrival order — the workload-based analysis of Section 7.3. Section 7.4 studies a fourth, more general family: a unitary network (one service type per class) under a relaxed control policy , where is the updated job-count vector and is any capacity-respecting, degree-zero-homogeneous function (Assumption 7.6) — a family general enough to include non-idling and SBP policies as special cases, and to anticipate the proportionally fair allocation studied in Chapters 9-10.
For a queueing network under FCFS control, every fluid limit path satisfies (6.1)-(6.6) and
where is the fluid arrival rate into class and is pool 's fluid-scaled immediate workload. This is the weakest natural target: an identity that pins down exactly the time-shift FCFS imposes, without asserting anything about how quickly or whether the fluid model reaches zero (that is left to the Lyapunov arguments of later chapters, once this equation is in hand).
Theorem 7.2 (non-idling): forces pool 's aggregate service rate to run at full capacity . Theorem 7.3 (non-preemptive SBP): the same conclusion with sharpened to the priority set (Eq. 7.5), for every buffer . Theorem 7.8 (general relaxed control): under Assumption 7.6, forces 's derivative to equal exactly — the common generalization from which the non-idling and SBP fluid equations both follow as special cases of a suitable .
The result itself. Theorem 7.5 is the precise bridge that lets FCFS-specific stability questions be attacked by the Lyapunov-function method Theorem 6.2 licenses: without a closed-form fluid equation, "does an FCFS network satisfy the standard load condition stably?" has no tractable deterministic reformulation. Bramson's 1994 example (an FCFS network unstable despite satisfying the standard load condition) shows the equation's content is not vacuous — FCFS fluid limits genuinely can misbehave, and this equation is precisely what any subsequent stability or instability argument for FCFS networks must reason about.
Formalizing it. No result about FCFS, non-idling, static-buffer-priority, or general relaxed
control policies exists on Prove2Me (q=first-come-first-served, q=FCFS, q=priority policy
all return zero hits, consistent with triage.json's record that none of this book's Chapters
6-14 machinery is on the platform). This mission is a from-scratch formalization of queueing
networks, their three named control-policy families, and the four policy-specific fluid
equations Chapter 7 derives for them.
The obvious shortcut for Theorem 7.3 — reuse Theorem 7.2's hypothesis and conclusion verbatim with replaced by — conflates the preemptive and non-preemptive SBP policies: Remark 7.4 explicitly notes the underlying pathwise identity (7.4) (used directly by Theorem 7.2) holds unconditionally under preemption but only asymptotically, via a vanishing-remainder argument bounding the leftover processing time of interrupted-but-continuing jobs, under non-preemption — the theorem actually being formalized is about the harder, non-preemptive case. For Theorem 7.5, the central difficulty is that FCFS's defining property is a genuinely time-shifted identity (departures at match arrivals at ), not a same-instant conditional statement like the non-idling and SBP equations — an approach that tried to state FCFS as a same-instant condition on or alone, without introducing the auxiliary workload process , could not express the theorem's actual content. A further subtlety Theorem 7.8's proof flags directly (Remark 7.9) is that the tempting converse — " implies zero service rate" — is false in general (a corrected version appears only later, as Lemma 8.9); this mission's goal and milestone statements are careful to assert only the one-directional implication the book actually proves.
Mission III's fluid-limit-path apparatus (Definition 6.6, u.o.c. convergence) is restated locally
in this chapter's own namespace rather than imported, since drafts in this series do not import
one another; the restatement is trimmed to the four raw processes this
chapter's proofs need, omitting mission III's "delayed random walk" machinery. The non-idling and
non-preemptive-SBP hypotheses are both formalized via one shared predicate, FullyUtilized,
applied to different index sets ( vs. ) — the pathwise full-utilization identity
(7.4) that each policy's proof establishes for its own priority classes, taken as a hypothesis
rather than re-derived from a lower-level model of server scheduling (Chapter 2's construction of
the service-starting mechanism is out of scope for this chapter, exactly as it was for mission
III's SPNProcessFamily). Likewise, the FCFS goal theorem hypothesizes the raw identity (7.12)
(rewritten via the material-balance equation to avoid needing the raw arrival process) and the
fluid-scaled limit of the raw workload process (7.17), rather than re-deriving either from the
"delayed random walk" of Eq. (6.47). A formalization that dropped the workload shift
from Theorem 7.5's conclusion, or that stated Theorem 7.8's converse implication
(which Remark 7.9 explicitly disclaims), would each be an unfaithful trivialization or
overstatement ruled out here. QueueingNetworkData, ProcessFamily, FullyUtilized, and
SatisfiesAssumption76 are the primary reusable contributions of this mission; contributions
completing the four by sorry proofs — each of which needs the u.o.c.-convergence and
dominated-convergence arguments mission III's own proofs still lack — are welcome.
A stochastic processing network (SPN) is the general model behind manufacturing lines, call centers, computer systems, communication networks and hospital wards: a collection of buffers holding waiting work, a collection of activities (servers) that consume items from buffers and produce items into others, and stochastic primitives — arrival processes and service requirements — that drive the whole system forward in continuous time. Before any control policy can be designed, evaluated, or proved to work, the modeler needs a single, unambiguous, checkable notion of what it means for such a system to be stable: to settle into statistical equilibrium rather than pile up work without bound.
The difficulty is that "stability" has several natural, superficially different candidate definitions — positive recurrence of the underlying Markov chain, existence of a unique stationary distribution, convergence in distribution of queue lengths — each convenient for a different purpose (positive recurrence for verifying via drift criteria, a stationary distribution for computing long-run averages, distributional convergence for interpreting simulation output). J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' own pre-publication draft, 2020-4-2, http://spnbook.org) opens its technical development by proving these candidates coincide, so that the rest of the book — and, in practice, most stability results for queueing networks published since Rybko and Stolyar's and Dai's foundational work in the 1990s — can speak of "SPN stability" as one well-posed property.
An SPN has buffers, indexed , and activities (service types), indexed . External work arrives into buffer according to a counting process ; activity , whenever engaged, requires a service time and produces an output vector into the buffers on completion. The baseline stochastic assumptions (Assumption 2.1) specify these primitives precisely: the external arrival processes are independent Poisson processes with rates (no arrivals into a buffer with rate ); for each activity , the matched pairs of processing variables — service time and output vector, — form an i.i.d. sequence with finite means and ; each such pair has a joint phase-type distribution (realized as the absorption time and terminal mark of a finite-state continuous-time Markov chain, per Appendix D.9); and the initial processing variables, the arrival process, and the processing-variable sequences are, collectively, mutually independent.
Under a fixed control policy, the SPN generates two continuous-time processes: the service-count process and the buffer-contents process . Assumption 3.1 (Markov representation) requires these to be embeddable in a richer, irreducible Markov chain on a countable state space : a function with on every sample path, whose level sets are finite for every buffer-content vector , and which has at least one empty state with .
and, when these hold, for every bounded and every initial distribution of ,
Definition 3.6 then names an SPN stable exactly when these equivalent conditions hold — the weakest possible target, since it commits to no particular one of the three characterizations, only to their joint truth or falsity.
Two strong laws of large numbers for the primitive stochastic elements (Propositions 2.2 and 2.3) — the arrival counts and the processing-variable sample means , — and two structural results about the ambient chain: Lemma 3.7, a drift-type sufficient condition for positive recurrence that foreshadows the fluid-model methodology of later chapters, and Proposition 3.9, a sufficient condition (reachability of the empty state) for the irreducibility that Assumption 3.1 itself demands.
The result itself. Proposition 3.5 is what turns "is this queueing network stable?" into a single question rather than three potentially different ones, and it licenses every later chapter of the book (and a large fraction of the queueing-theory literature going back to the 1990s fluid-limit program of Rybko–Stolyar, Dai, and others) to prove stability via whichever characterization is most convenient — typically positive recurrence via a Lyapunov drift argument — while concluding all three, including the practically important long-run-average SLLN. Every one of the thirteen other missions in this series builds directly on Definition 3.6: their goal theorems all conclude "the SPN is stable," meaning exactly the three-way equivalence established here.
Formalizing it. No result in this mission or its milestones has a prior formal counterpart on
Prove2Me: a search for "positive recurrent," "stationary distribution Markov chain," and
"irreducible Markov chain" surfaced only MarkovMixing's PositiveRecurrent predicate, defined
for a countable-state discrete-time chain — a different object from Assumption 3.1's
continuous-time ambient chain, reused here only conceptually (as the pattern for a mean-return-time
definition), not as a Lean dependency. This mission is a from-scratch formalization of the
model (baseline stochastic assumptions, Markov representation) and of positive recurrence,
stationary-distribution uniqueness, and distributional convergence for it.
The obvious first attempt — define as an arbitrary countable-state Markov chain and directly
import a Mathlib theorem relating its recurrence, its stationary distribution, and long-run
convergence — fails because Mathlib currently has no general countable-state continuous-time
Markov chain theory of the kind Appendix D of the book develops (its own finite-state CTMC
stationary-distribution result is unproven substrate, not applicable to a countably infinite
state space). The formalization instead works at the level of the chain's embedded discrete-time
jump chain, which is where Lean's PMF-based machinery is available, and states the three
equivalent conditions and the SLLN conclusion directly as hypotheses to be discharged, rather than
inheriting them from a pre-existing continuous-time framework. A second difficulty is Assumption
2.1(d)'s independence clause, which is a genuine three-way mutual independence of -algebras
(initial processing variables, arrival process, and the collection of all processing-variable
sequences), not the pairwise independence a careless reading might substitute — a weaker
hypothesis here would silently make later derivations in the series unsound.
The ambient chain's state space Xstate is an arbitrary countable type ([Countable Xstate],
not Fintype) — no result may assume finiteness anywhere. The chain itself is represented by its
one-step jump kernel jump : Xstate → PMF Xstate (stepIter gives -step iteration,
Irreducible requires every state to reach every other in finitely many jump-chain steps);
positive recurrence is mean return time under jump, defined via the standard first-return-time
renewal decomposition. IsStable is defined as positive recurrence of the jump chain — one of
the three equivalent conditions — with the goal theorem itself certifying the equivalence, so the
choice carries no loss of faithfulness. Buffer contents and service counts are Fin I → ℕ and
Fin J → ℕ-valued, matching the book's , . A formalization that
took IsStable to mean, say, only distributional convergence of (dropping the chain-level
characterizations) would be a strictly weaker, trivializing shortcut — ruled out here by proving
all three equivalent and stating the SLLN as part of the same goal theorem. The definitions in
this mission (BaselineAssumptions, MarkovRepresentation, IsStable) are the shared substrate
every other mission of the series is built on, and are the primary reusable contribution;
contributions completing the by sorry proofs, particularly of the goal theorem (which the book
proves via appeal to general CTMC theory in its Appendix D, not reproduced here), are welcome.
Many 0–1 optimization problems can be written as linear programs over the convex hull of the 0–1 points of a polytope, but that hull usually has no manageable description by inequalities. Lift-and-project methods approximate it by a sequence of convex sets. Each set comes from a linear or semidefinite system in more variables, followed by a projection. Lovász and Schrijver introduced the operator in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim. 1(2), 1991). For any polytope in the unit cube, rounds of reach the 0–1 hull (their Theorem 1.4), and each round keeps linear optimization tractable.
The stable set problem is the paper's main test case, and the question is quantitative: how many rounds does a given valid inequality need? Section 2.c answers it with a single number read off a linear program. Later work on the rank of lift-and-project hierarchies uses this measure: Balas, Ceria and Cornuéjols's lift-and-project cuts (1993), the Sherali–Adams and Lasserre comparisons of Laurent (2003), and the rank lower bounds for stable set relaxations in the decades since.
Let be a finite graph with no isolated nodes, which is the paper's standing assumption for Section 2. For let be its incidence vector.
Homogenize with a new coordinate . Let be the cone spanned by the 0–1 vectors with , and let be the cone given by and . For a convex cone with polar cone , the matrix cone is the set of symmetric matrices that satisfy two conditions:
The operator is . Its iterates are and . On the graph side, , so and for every .
Let be valid for , with and . Two numbers are attached to it:
For a node with neighbourhood , the deletion of zeroes . The contraction of zeroes on and lowers the right-hand side to .
For every such inequality with defect and N-index ,
formalized as and . The goal holds for every graph without isolated nodes and every valid inequality with nonnegative integer coefficients and nonnegative defect.
Corollary 2.8. Let have nodes, stability number and graph N-index . Then
Theorem 2.13 turns the N-index, which is defined through an infinite family of matrix-cone projections, into a quantity computable by one linear program over . Some consequences:
The result is proved in the paper; the mission's work is to formalize it. Nothing on Prove2Me or in Mathlib covers stable set polytopes, the Lovász–Schrijver operator or its index, and no machine-checked version of Theorem 2.13 is known. A formal proof would give the first verified rank bound for a lift-and-project hierarchy. It would also build a reusable library for , , half-integrality of vertices, and the operator.
The upper bound is an induction on the defect, and it needs several facts about :
The last is the heart of Lemmas 2.11 and 2.12. The induction also climbs through for every , so Lemma 2.2 must hold for an arbitrary closed convex cone inside , not only for polytopes given by inequalities.
The lower bound is where the obvious argument fails. The printed proof tests at and obtains . That equals only when , which Lemma 2.10 gives for facets alone. For a general valid inequality can exceed , so the uniform vector does not suffice. The theorem is stated, as printed, for every valid inequality, and a complete proof must supply the missing step.
Option V, with none as . Graphs are finite SimpleGraphs with the hypothesis that every node has a neighbour.IsGreatest and IsLeast hypotheses, so no default value such as can make a statement vacuous.The work needs half-integrality of , Lemma 1.3 of the paper () and monotonicity of . Each of these is reusable and welcome as a separate contribution.
A jobshop is a factory in which each job visits a sequence of machine groups, the sequence differing from job to job. J. R. Jackson's 1963 paper Jobshop-Like Queueing Systems (Management Science 10(1), 131–142) models such a shop as a network of queues and computes its long-run distribution of queue lengths in closed form. It generalizes his 1957 paper Networks of Waiting Lines (Operations Research 5(4)), which treated Poisson arrivals and multi-server centers, to arrival rates that depend on the total number of customers present and service rates that depend arbitrarily on the local queue length. The resulting product-form equilibrium is the starting point of queueing-network theory, which is used in performance analysis of manufacturing systems, computer systems and communication networks.
Timeline:
There are service centers, Center . A state vector has non-negative integer components, being the number of customers at Center , and . The system is given by:
The paper's standing Assumptions (2.1)–(2.4): (2.1) either all , or exactly for ; (2.2) and for ; (2.3) each row is a probability distribution; (2.4) the traffic equations
have a unique solution, and it is non-negative.
The process is defined by its transition probabilities over a short interval (p. 134), from which the paper derives the balance equations (3.1) for . An equilibrium state probability distribution is a probability distribution on state vectors such that solves (3.1). With
the constant is when the series converges and otherwise.
If , then
is an equilibrium state probability distribution; and if the arrival rates are bounded, it is the only one. The goal fixes no constants; the condition is the paper's.
Theorem (6.3) in its case , : with constant arrival rate and for every , the equilibrium is , being the normalized .
Theorem (4.5) states that the queue lengths of a whole network have an explicit stationary law, determined by the routing only through the visit ratios , and that conditionally on the total it does not depend on the arrival process. With constant arrival rate it factorizes into independent one-center laws (Theorem (6.3)), each that of a single queue fed at rate ; this is the form in which Jackson networks enter textbooks. State-dependent arrivals cover systems with balking or finite capacity: taking for caps the population.
The result is classical and proved; it has no machine-checked proof on this platform. The platform has Kelly–Yudovina's open migration process (KellyStochasticNetworks.open_migration_equilibrium): constant external arrivals, no self-loops, a full-balance conclusion without uniqueness. It is the companion (6.3) in substance but not the general theorem: arrival rates depending on the total population are not in it. This mission contributes the state-dependent model, a stationary form of Jackson's own equations (3.1), and a uniqueness statement.
The balance equations are an infinite system in . Substituting (4.6) gives terms with shifted states, guarded by non-negativity of components, a double sum over ordered pairs of distinct centers, self-loops appearing only in the outflow factor , and centers with , where vanishes. Checking each state term by term against the traffic equations requires the diagonal of (2.5), excluded in (3.1), to be handled exactly. Summing (4.6) to one requires regrouping a series over by the finite fibres of .
Uniqueness is the hard part. The paper gives no proof: footnote 5 refers to a limit theorem for Markov processes and to the communication structure of non-transient states. A solution of the algebraic balance equations need not be the stationary law of the process when the process can explode, and the model allows explosion with (e.g. , , ). Uniqueness therefore depends on non-explosion as well as on the communication structure of the states, and neither is addressed on the page.
Centers are Fin N with ; states are Fin N → ℕ; rates are real. The routing is one function r : Option (Fin N) → Option (Fin N) → ℝ, where none is the index in the first argument and in the second. A structure JobshopSystem N bundles with Assumptions (2.1)–(2.4) as fields; is a parameter satisfying (2.5), uniqueness and non-negativity, not a formula. Balance sys q k is the stationary equation (3.1) at k for an arbitrary q, and IsEquilibrium sys q is , HasSum q 1, and Balance at every state. is defined with an explicit if Summable … then … else 0.
Explicit choices, each stated in the item where it applies:
Correction of (3.1). The paper prints the arrival outflow as :
Its transition probabilities (p. 134) give , since an arrival with an empty routing leaves the state unchanged. The two agree only when , and with the printed coefficient Theorem (4.5) is false (, , , constant rates, at ). The formalization uses the coefficient the transition probabilities give. It does not assume : the paper allows empty routings.
Uniqueness under bounded arrival rates. Uniqueness (milestone 4 and the goal's second conjunct) assumes . The paper asserts uniqueness without proof, citing a limit theorem for regular processes; bounded arrival rates make the process regular and hold for every example in the paper. Existence and the formula carry no added hypothesis.
Companion (6.3). System of §5 is not formalized in the paper and not here; only its case , is stated.
A trivializing formalization is ruled out: Balance and IsEquilibrium are stated for an arbitrary function on states and never mention , or , and equilibrium is neither defined as (4.6) nor as detailed or partial balance.
Useful infrastructure: summation over Fin N → ℕ grouped by total (Finset.Nat.antidiagonalTuple), and a non-explosion and uniqueness theory for countable-state continuous-time chains, which is reusable beyond this mission. Not included: the limit , which needs a construction of the process; the equivalence of (2.4) with finiteness of routings; Theorem (5.5) and (5.7)–(5.9).
The maximum weight matching (MWM) problem asks, for a graph with edge weights, for a set of vertex-disjoint edges of largest total weight. It is a central problem of combinatorial optimization, with applications to transportation, assignment and scheduling, and as a subroutine for shortest paths, planar max cut, Chinese postman tours and metric TSP. Edmonds' blossom algorithm (1965) solves it on general graphs; the fastest implementation, due to Gabow, runs in time, and the scaling algorithm of Gabow and Tarjan (1991) runs in time on graphs with vertices, edges and integer weights of magnitude at most . Applications such as switch scheduling, graph clustering and sparse linear solvers accept a slightly suboptimal matching in exchange for speed. This motivates -approximate maximum weight matchings: matchings whose weight is at least a fraction of the optimum.
Timeline of linear and near-linear time approximation for general graphs (Section 1.3 and Table IV of the paper; the entries below are as the paper attributes them):
Let be a finite simple graph with integer weights , . A matching is a set of vertex-disjoint edges, with weight ; a vertex is free if no edge of touches it. is a -MWM if for every matching .
A blossom is built recursively: a single vertex is a trivial blossom with ; an odd number of disjoint blossoms joined in a cycle by edges form the blossom with edge set . It is full if . The algorithm keeps a laminar set of full blossoms; a root blossom is a maximal one, and contracts each root blossom to a single vertex.
Dual values and on odd vertex sets give each edge the value
The scaling algorithm (Figure 2 of the paper) has parameters and . It runs scales with granularity and truncated weights . Each scale repeats four steps: augment along a maximal set of vertex-disjoint augmenting paths of the eligible graph , shrink a maximal set of new blossoms, adjust the duals by , and dissolve root blossoms whose -value has reached zero. It stops when the free vertices' -values reach a scale-dependent value, which is at scale . Eligibility is given by Definition 3.2; the linear-time variant keeps the algorithm unchanged and uses Definition 3.10, which additionally ignores an edge in scales unless it is a blossom edge.
For every with , the algorithm of Figure 2 with Definition 3.10 eligibility has a terminating run, and every terminating run returns a matching with
The result. Theorem 3.12 gives the first algorithm for -approximate maximum weight matching on general graphs that runs in linear time for every fixed ; earlier linear-time algorithms achieved only or . Its analysis is a relaxation of Edmonds' complementary slackness conditions that grows weaker over the scales, but not uniformly, and Lemma 2.3 certifies an approximate matching by approximately feasible duals.
Formalizing it. The result is proved in the paper. Mathlib (at the pinned revision) has matchings, alternating walks and Tutte's theorem, but no blossoms, contracted graphs or weighted matching algorithms. A complete development gives a Lean model of blossoms, contraction and augmenting paths through blossoms, a verified primal–dual invariant for a scaling algorithm, and a checked approximate-slackness certificate for matchings. Each of these can be reused to formalize Edmonds' exact algorithm or the Gabow–Tarjan scaling algorithm.
The two halves of the argument pull against each other. Lemma 2.3 needs near domination and near tightness as multiplicative bounds. The algorithm maintains only additive bounds whose slack for an edge of type is , and this slack does not shrink as the scales advance. Converting it into a factor requires a lower bound on the weight of every edge that ever became eligible, which in turn depends on the free vertices' duals following an exact schedule across scales.
For Definition 3.10 the obvious argument breaks down: an edge that is ignored after scale may violate near domination and near tightness by an amount that grows with every later dual adjustment. The claim is that the accumulated violation stays within an fraction of , and establishing this requires tracking every adjustment that can reach an ignored edge.
On the combinatorial side, the Augmentation and Blossom Shrinking steps work in the contracted graph . Their correctness uses the classical facts that augmenting paths lift through full blossoms and that blossoms stay full after augmentation (Lemma 2.1), which have to be formalized from scratch.
Graphs are SimpleGraph V on a Fintype V with decidable equality; edges are Sym2 V; matchings are Finset (Sym2 V) with pairwise vertex-disjoint edges of ; weights are with on edges. Duals, and are real numbers. is a function on all finite vertex sets and sums it over the odd sets that contain the edge, as on the page. and , , are given through their exponents. uses the convention . The paper's standing assumption is used only for running time and is omitted.
The algorithm is a nondeterministic relation. A state holds , with its blossom edge sets, , , a ghost record of the scale in which each edge last entered , and the common free-vertex dual that drives the loop test. The maximal sets of augmenting paths and of new blossoms and the lifts of paths through blossoms are choices. Invariants are stated for states reachable by a run, and the goal asserts both that a terminating run exists and that every terminating run returns a -MWM.
The running times of Theorem 3.8 and of Theorem 3.12 are not formalized: the paper fixes no cost model, and its bounds rely on a modified depth-first search and on word-RAM table lookups. The explicit constants (Theorem 3.8) and (Theorem 3.12) are the ones the proofs supply.
The following trivializing formalizations are ruled out: a "matching" that may contain non-edges or repeated edges; a goal about a state only assumed to satisfy Property 3.1 rather than reached by the algorithm; a run relation with no terminating run, which the existence conjunct excludes; eligibility or blossoms chosen freely instead of by the page's rules; and comparison only against matchings of the contracted graph instead of all matchings of .
Welcome contributions include a Lean treatment of blossoms and their contraction (Lemma 2.1, which is not a milestone here), the lift of augmenting paths, Lemmas 3.3 and 3.4 as auxiliary results, and proofs of the milestones in the order listed.
A convex risk measure assigns to a bounded financial position (a random net payoff) a number , interpreted as the capital that must be added to to make it acceptable. The axiomatic theory began with coherent risk measures (Artzner, Delbaen, Eber and Heath, 1999) and was extended to convex ones by Föllmer and Schied (2002) and Frittelli and Rosazza Gianin (2002). Its central structural result is a robust representation: a convex risk measure that is continuous from above equals a worst case of expected losses over a family of probabilistic models, each penalized by how implausible it is.
Regulators and risk managers do not assess positions once and for all; they reassess them as information arrives. Detlefsen and Scandolo (2005) extend the representation to conditional risk measures, whose value is itself a random variable measurable with respect to the information available to the agent. This is the building block of dynamic (time-consistent) risk measurement, studied in later work on dynamic risk measures and backward stochastic differential equations.
Timeline. Artzner et al. (1999): coherent risk measures on finite . Delbaen (2002): coherent risk measures on general probability spaces, Fatou property. Föllmer–Schied (2002) and Frittelli–Rosazza Gianin (2002): convex risk measures and their robust representation; Föllmer–Schied, Stochastic Finance, Theorem 4.26 (2002 edition) for with continuity from above. Detlefsen–Scandolo (2005): the conditional version, Theorem 3.2 of the paper formalized here.
Fix a probability space and a sub--algebra describing the available information. is the space of essentially bounded random variables and its -measurable part; every (in)equality between random variables holds -almost surely.
A map is a conditional convex risk measure if and, for :
The admissible models are
For a family of -valued random variables, the essential supremum is the -a.s. smallest random variable that dominates every member -a.s.; it replaces the pointwise supremum, which is not meaningful for uncountable families of equivalence classes.
A map is representable if there is a penalty with
The minimal penalty is . is continuous from above if -a.s. implies -a.s.
For a conditional convex risk measure , the following are equivalent:
The result. Theorem 3.2 shows that a conditional convex risk measure is determined by a random penalty on the models consistent with the available information, exactly when it satisfies a sequential continuity condition. The representation is the input for the paper's later sections: the conditional entropic risk measure, whose minimal penalty is the conditional relative entropy, and the consistency of dynamic risk measures via Lemma 3.4, which is expressed through the minimal penalty. The restriction to has an interpretation: the more information, the fewer models can enter the worst case.
Formalizing it. The theorem has been proved in the literature since 2005; to our knowledge neither it nor its unconditional counterpart has a machine-checked proof. The mission produces an essential supremum of arbitrary families of extended random variables with its existence theorem, the exchange of expectation and essential supremum for directed families, and the unconditional Föllmer–Schied representation on . The last of these is the standard representation theorem of the theory of convex risk measures and is useful well beyond this paper.
The obvious route, applying the unconditional representation pathwise or by , fails: is not a risk measure of anything, and conditional expectations are only defined up to null sets that depend on , of which there are uncountably many. The essential supremum is what turns an uncountable supremum of classes into a well-defined class, and passing expectations through it requires directedness. The unconditional step itself (continuity from above implies the dual representation) rests on a Krein–Šmulian / weak* closedness argument on , which is not available off the shelf.
MemLp X ⊤ P; is a map constrained only on . Because it acts on functions, is required to respect -a.s. equality, and is required to be -strongly measurable and essentially bounded; the paper's acts on classes, so this adds nothing in substance. is a MeasurableSpace m with m ≤ mΩ.Q[X | m]; it is -measurable, hence determined -a.s. for .EReal; penalties are ENNReal-valued and coerced, so only (real) occurs, never .IsEssSup P F Z (a.e. upper bound of every member, a.e. below every a.e.-measurable a.e. upper bound). The minimal penalty is a predicate IsMinimalPenalty on a candidate; statement (c) of the goal asserts that a -measurable -valued essential supremum of is a penalty for .⨆ over the family, or via Mathlib's essSup of a single function, and an index set equal to all or to the equivalent to ; each of these changes statement (b) or makes it vacuous.A spectrally negative Lévy process is a process with stationary independent increments whose jumps are all downward: Brownian motion with drift plus a compound Poisson or infinite-activity stream of negative jumps. It is the standard model for a risk reserve that earns premiums continuously and pays claims in lumps, for a storage level or a queue workload seen in reverse, and, in mathematical finance, for a log-price that can crash but not jump up. Exit problems (when and where such a process first leaves an interval) are the basic quantities in ruin theory, in dividend and barrier problems, and in the pricing of path-dependent options.
The reflected process , the distance of below its running maximum, is the drawdown of . Its first passage above a level is the time at which a drawdown of size first occurs. Avram, Kyprianou and Pistorius (AKP 2004) computed the joint Laplace transform of this passage time and of the overshoot in closed form, in terms of the scale functions of . This is the first of three missions on that paper. The two others use this identity for the perpetual Russian option and its Canadized version.
Timeline. Bertoin gave the upward two-sided exit identity for spectrally negative Lévy processes in terms of scale functions (Bertoin 1996, Theorem VII.8) and the downward one (Bertoin 1997, Corollary 1). Avram, Kyprianou and Pistorius (2004) obtained the joint transform of for every spectrally negative Lévy process of unbounded variation, or of bounded variation with absolutely continuous Lévy measure.
Let be a spectrally negative Lévy process on : it starts at , has independent and stationary increments, càdlàg paths, no positive jumps, and paths that are not monotone. Its Laplace exponent is , and "" means that is integrable. For such , the tilted exponent is .
The paper assumes throughout that has unbounded variation, or has bounded variation and a Lévy measure with .
For , is the largest root of . The -scale function is the unique function that vanishes on , is continuous on , and satisfies
For it is defined by the series , where and is convolution on . Further, . The functions and are the same objects built from instead of .
Under the process starts at with a prior maximum . Its running maximum is , and the reflected process is , which starts at . For ,
For and with , with and ,
Here may be negative, so may be negative, which is where the series extension of enters.
Items (13)–(22) are stated under the proof's restriction . The goal is not.
The identity gives, for every spectrally negative Lévy process, the law of the first drawdown of size and of its overshoot. With it is the Laplace transform of the drawdown time. With it is the transform of the overshoot. The paper uses it, through its Corollary 1, to solve the perpetual Russian option and the Canadized Russian option in closed form. Identities of this form, written in scale functions, are the standard tool for drawdown and reflected-process problems for spectrally negative Lévy processes.
The theorem is proved. As far as the platform and Mathlib show, none of it is formalized: Mathlib has independent increments and cumulant generating functions but no Lévy process, no scale function and no excursion theory. This mission produces a formal statement of the paper's model and of the exit identities. A complete development would also give Mathlib its first fluctuation-theory results for Lévy processes.
The natural first idea is to treat like and read off its exit from from the two-sided exit identities of Proposition 1. This works only until first returns to . Up to that time is a copy of . After it, is reflected at , it is not a Lévy process, and no two-sided exit problem of describes it. The whole content of the theorem is the constant of (13), the value of the functional for started at , where the reflection acts at every instant. A second difficulty is the range of . For the integrand is unbounded, because can jump far above . Its finiteness is part of the claim. So is the passage from the region , where every scale function in (12) comes from Definition 2, to all , where can be negative.
Time is (ℝ≥0). is a real process with . is encoded by the path , and by that path together with the prior maximum . Random times take values in WithTop ℝ≥0, with as "never". The functional and discount factors are set to where the time is infinite. Every stated expectation carries its integrability as part of the conclusion.
Readings of the paper's informal words:
The scale functions are defined from the exponent of the given . A formalization in which is an arbitrary function satisfying a Laplace-transform hypothesis is ruled out. So is one in which is defined as , which would make Remark 4 a tautology.
Infrastructure a complete development needs: Lévy processes and their Laplace exponent, the strong Markov property at stopping times, existence and regularity of scale functions (via Laplace inversion), and the Esscher change of measure. No statement of the mission mentions excursion theory. Contributions of reusable infrastructure for Lévy processes are welcome.
In a two-person zero-sum game with objective randomization, whatever one player gains the other loses: the value of the game is the most player 1 can guarantee and the least player 2 can hold him to, and no arrangement between the players can give player 1 more than and player 2 more than at the same time. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) replaces objective coin flips by ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. Sect. 6 of the paper shows that this breaks the zero-sum logic: once the players disagree about the probability of events they can observe, a zero-sum game becomes, in expectation as each player computes it, a game in which both can gain.
The phenomenon is the game-theoretic form of betting between people who disagree: two players with different beliefs can each expect to profit from the same wager. Aumann's proposition identifies exactly what information structure makes such an agreement possible inside a given zero-sum game, and shows by an example that informing only one player of a subjective event is not enough. The same paper introduced correlated equilibrium; the companion mission of this series formalizes its two-person result on subjective mixed equilibria (Proposition 5.1).
A game has a finite set of players, a finite set of pure strategies for each player, a finite set of outcomes and an outcome function from onto . Player has a utility ; write for .
A randomizing structure consists of a set of states of the world with a -field of events, a sub--field for each player (the events regarding which is informed), and a probability measure on for each player (the subjective probability of ). A strategy of is a map whose level sets lie in . For a profile of strategies, player 's payoff is computed under his own beliefs:
An event is objective if all coincide, and subjective otherwise. It is -secret if and every other player regards as independent of every event in the -field generated by the , . It is public if it lies in every . A measure is non-atomic on a -field if every event of of positive measure contains an event of of strictly smaller positive measure; a roulette is a sub--field of on which every is non-atomic, and a public roulette is a roulette of public events. Throughout, Assumption II holds: every player has a -field of -secret events on which every is non-atomic.
The game is two-person zero-sum if and for all . Its value is player 1's payoff at a Nash equilibrium of the classical mixed extension; by the minimax theorem all such equilibria give the payoff pair .
Let be a two-person zero-sum game with value , and assume
Then there is a pair of strategies with
The pair is not an equilibrium: it is an agreement that each player, by his own beliefs, strictly prefers to playing the game.
a special case of the goal in which the players share both the subjective event and the correlating device.
The proposition shows that the value of a zero-sum game is a property of objective randomization, not of the game alone. With subjective randomization available to both players, the conflict of a zero-sum game can be resolved by agreement, so the classical prediction (each player receives his security level) is not robust to disagreement about probabilities. The counterexample on p. 81 (the game with matrix rows and ) shows that hypothesis (6.3) is needed for both players, and the paper notes that in any specific game only one player need use a subjective strategy, though which one depends on the game.
Lemmas 4.2, 4.4 and 7.1 are the model's basic existence results for objective randomization: every probability can be realised by an event that is secret (or public) and independent of finitely many given events. They are used throughout the paper, including in the companion mission.
The paper's proofs are published and accepted; none of these statements has a machine-checked proof. This mission produces the formal statements and invites complete proofs; Lemma 7.1 requires Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures, which is not in Mathlib.
The central difficulty for the goal is that (6.3) gives each player only some subjective event, of unknown size and in his own information field, while (6.4) requires strict gains for both players under two different measures at once. The obvious approach, betting on one subjective event, gives one player a strict gain but, when that event is not known to the other player, the other player cannot condition his choice on it; the example on p. 81 shows that one-sided information genuinely fails. Both inequalities must be arranged simultaneously, and the strategies must remain measurable with respect to each player's own information.
For Lemma 7.1, a non-atomic scalar measure takes every value in , but the lemma asks for one event with prescribed values under measures and further measures simultaneously; this is the range of a vector measure, not of a scalar one.
0, 1 : Fin 2 (the paper's 1, 2). S 0, S 1, X are finite types and g is surjective.mΩ, an explicit parameter of RandomizingStructure; are σ-fields below it, and each is a probability measure on . Probabilities are ℝ≥0∞-valued; "probability " is ENNReal.ofReal α with .NoAtoms, which would trivialize the roulette hypotheses.IsValue u g v requires for a Nash equilibrium of the mixed extension (AGT.IsMixedNash from the published definition agt_games). A free would make the goal false. The minimax theorem is the published AGT.zero_sum_minimax.Needed infrastructure: Lyapunov's theorem (or a direct argument for the finite-dimensional case), manipulation of σ-fields generated by families of sub-σ-fields, and computation of for strategies with finitely many values. Lyapunov's theorem is reusable far beyond this mission. Contributions of any milestone are welcome.
Many sequential decisions are personalised: a physician chooses a drug dose for each arriving patient, a platform chooses which offer to show each arriving user. Each decision is made after observing a vector of covariates describing the individual, and its outcome is observed only for the option chosen. This is the contextual (covariate) bandit problem, studied in operations research and machine learning since Auer (JMLR 2002) and Goldenshluger and Zeevi (Stochastic Systems 2013).
In medical and e-commerce applications the covariate vector is often high-dimensional: the number of covariates is comparable to or larger than the number of decisions that will ever be made, while the outcome of each option depends on a few of them. Low-dimensional bandit algorithms then incur regret that grows polynomially with . Bastani and Bayati (Operations Research 2020) proposed the LASSO Bandit, which estimates each option's reward model with the LASSO, and proved a regret bound that grows only logarithmically in . The paper evaluates the method on warfarin dosing data.
Timeline:
There are arms with unknown parameters . At each time a covariate vector arrives; the are i.i.d. with law and take values in a fixed set . If arm is pulled, the reward is , where the noises are independent, -subgaussian ( for all ), and independent of the covariates. A policy chooses the arm from and the past covariates, arms and observed rewards. Its cumulative expected regret is
The sparsity is the smallest integer with for all .
The four assumptions are: (1) on and ; (2) a margin condition ; (3) arm optimality: every arm is either suboptimal by a margin at every covariate, or optimal by margin on a region of probability at least ; (4) a compatibility condition: the conditional second-moment matrix of each optimal arm lies in the set of matrices with whenever .
The LASSO estimator on samples is any minimizer of . The LASSO Bandit forces arm at the prescribed times . At every other time it keeps the arms whose forced-sample estimate is within of the best. Among them it plays the arm with the largest all-sample estimate , trained on every past pull of the arm, with .
For , , , , and ,
with the explicit constants , of the paper (p. 285).
The theorem shows that exploiting sparsity makes the regret depend on the ambient dimension only through , while its dependence on the horizon is within one factor of the lower bound known in low dimension. Proposition 1 is a LASSO oracle inequality for adapted designs, where each row may depend on earlier observations. It applies whenever a LASSO is fitted to data gathered by a feedback policy: adaptive experiments, dynamic pricing, sequential treatment assignment.
The results are proved in the paper and its online appendix; none of them has a machine-checked proof. This mission produces a formal model of the covariate bandit with a non-anticipating algorithm, a formal LASSO for adapted designs, and, when complete, a verified regret bound with every constant explicit. Proposition 1 and Lemma 1 are reusable beyond bandits.
The all-sample estimator is trained on the times at which the algorithm chose an arm, and those choices depend on earlier estimates. Its design rows are therefore neither independent nor identically distributed, and the standard LASSO analysis, which starts from i.i.d. rows and a restricted-eigenvalue bound on their population covariance, does not apply. The forced samples are i.i.d. but only in number, too few for the rate the regret bound needs. Controlling the compatibility constant of the adaptively selected sample covariance, and the martingale noise term, is where the naive argument breaks.
Arms are Fin K (paper arm is i.val + 1), coordinates Fin d, times are natural numbers from . The model is a structure IsCovariateNoiseModel on a probability space: i.i.d. measurable covariates in a measurable set , independent subgaussian noises (Mathlib's HasSubgaussianMGF with parameter ), noise independent of covariates. Assumptions 1–4 are separate predicates. is Mathlib's sup norm, logarithms are natural, and is the uncentred conditional second moment.
The LASSO minimizer and the arg max need not be unique, so the algorithm takes a selection rule and a tie-breaking rule as parameters, and the theorems hold for all of them. Each round reads only the current covariate, the past covariates, the past arms and their observed rewards. The regret theorem and Proposition 3, whose data set is chosen by the algorithm, require both rules to be measurable. Otherwise the trajectory would not be a random variable, and the expectations in could be integrals of non-measurable functions, which Lean evaluates to and which would make the goal trivially true. For the same reason every assumption constant is required to be positive, and is imposed on the horizon. Only the explicit inequality of Theorem 1 is stated, not the trailing or . Proposition 2 is stated for optimal arms (see its note).
A complete development needs matrix concentration for bounded i.i.d. rows, the Azuma–Hoeffding inequality, and the deterministic LASSO basic inequality under a compatibility condition. Contributions of any of these as standalone lemmas are welcome.
Retailers that sell the same product can raise their joint profit by pooling: stock left over at one location is shipped to meet unmet demand at another, and stock can be held in shared warehouses until demand is known (Eppen 1979; Eppen and Schrage 1981). When the retailers are independent firms, pooling creates two questions at once. After demand is realized, the extra profit from shipping must be split in a way no group of retailers would reject. Before demand is realized, each retailer chooses its own stock, and that choice depends on how the split will be made. A split that is fair ex post may lead to stocking decisions that are poor for the system as a whole.
Anupindi, Bassok and Zemel (MSOM 2001) model the ex-post split as a cooperative game, the ex-ante stocking as a non-cooperative game, and ask whether a single allocation rule can serve both. Their framework is a standard reference for "coopetition" models in supply chains, where firms compete on stocking decisions and cooperate on redistribution.
There are retailers and warehouses . Retailer has unit cost , revenue and salvage value ; warehouse has purchasing cost and salvage value . Shipping from location to retailer costs per unit, and a fraction of the customers at accept service from .
Before demand, retailer chooses a position : local stock and claims on warehouse stock, so warehouse holds . A profile is . Demand is random with law . After demand, retailer has local sales , residual inventory and residual demand .
The snapshot allocation game SAG gives each coalition the value : the optimal value of the linear program (6), which ships units from to at profit per unit, subject to , and . Its core is the set of allocations with for every and (7).
An allocation rule AR- assigns surplus ; retailer earns
and expects . A Nash equilibrium (10) is a profile at which no retailer gains by changing its own position. The first-best profile maximizes the expected centralized profit , where .
The fractional rule AR-f (11) pays with fixed shares , . The dual allocation (8) is for optimal dual prices of (6) for . The modified rule AR-c is with .
For a first-best profile and a measurable choice of dual prices at ,
with integrable side payments.
The goal answers the paper's central question positively: there is an allocation mechanism under which the centrally optimal stock levels are an equilibrium of the decentralized stocking game, while every ex-post split of the pooling surplus is stable against all coalitions. Theorem 4.1 is the ex-post half: shadow prices of the shipping LP give a stable split for every realization, independently of who owns which units. The paper also shows (Proposition 5.1, not included here) that the dual allocation alone does not induce first-best stocking, which is why the side payments of Theorem 5.1 are needed.
The results are proved in the paper; Theorem 4.1 is proved there only by reference to the LP-game literature (Owen 1975; Samet and Zemel 1984). None of them has a machine-checked proof. The mission would produce the first formal treatment on Prove2Me of a linear-production (LP) game and its core, and of a model combining a cooperative second stage with a non-cooperative first stage.
Theorem 4.1 is an instance of Owen's theorem on LP games, but the instance is not a standard linear production game: coalition LPs have variables only on arcs inside the coalition, warehouse capacity is limited to the coalition's own claims, and the acceptance constraint divides by , which may be zero, so the general theorem cannot be quoted as it stands. The paper leaves the dual of (6) unwritten, and Mathlib has no ready-made LP duality in this form.
The stochastic layer is the other obstacle. Expected payoffs are integrals, and the side payment is built from a choice of dual prices for each demand realization. Its integrability requires measurability of that choice and of the LP value as a function of demand; neither is given by the paper, which treats the side payments as "constants".
Retailers are Fin N, warehouses Fin W, locations Fin N ⊕ Fin W; quantities, prices and demands are real numbers; demand is a probability measure on Fin N → ℝ; expectations are Bochner integrals. is the real supremum of (6a) over the feasible set, and profiles are required to be nonnegative, which makes the feasible set nonempty and bounded. Arcs with carry no shipment. The core is the platform definition Supermodularity.Cooperative.Core. The dual of (6) is written out explicitly (the paper does not state it). The paper's continuous-CDF assumption is not used and is dropped.
Pinned readings:
Not acceptable: a core without the efficiency equation (7b); a feasible set that lets sell to customers who balk; an arbitrary side payment instead of the constructed one; or a Nash equilibrium evaluated through non-integrable payoffs, whose Bochner integral is and makes every profile an equilibrium.
Useful infrastructure: finite-dimensional LP duality in inequality form, measurable selection of LP optimal solutions, and continuity of LP values in the right-hand side. All of it can be reused in other LP-game and two-stage stochastic programming missions.
A Fisher market is the simplest model of a market in which prices are set by supply and demand: buyers bring money, sellers bring goods, and a price vector is an equilibrium when every buyer, spending her money optimally at those prices, leaves every good exactly sold out. Computing equilibria is one of the central questions of algorithmic game theory, because a polynomial-time algorithm is what would make the equilibrium concept usable as a prediction or as a pricing mechanism.
For linear utilities an equilibrium always exists, is rational, and can be computed in polynomial time (Eisenberg and Gale 1959; Devanur, Papadimitriou, Saberi and Vazirani, J. ACM 2008, https://doi.org/10.1145/1411509.1411512). The next natural class, additively separable, piecewise-linear, concave utilities, captures diminishing marginal utility and is the class studied by Vazirani and Yannakakis (J. ACM 58(3), Article 10, 2011, https://doi.org/10.1145/1970392.1970394). Their paper shows that equilibria in this class are hard to compute (PPAD-complete) and that deciding whether one exists is NP-complete. Both results rest on a structural fact proved first: whenever such a market has an equilibrium at all, it has one whose prices are rational numbers of polynomial bit length. That fact is the subject of this mission.
Timeline:
There are buyers and divisible goods , one unit of each good. Buyer has a rational budget . For each buyer and good a function gives the utility that derives from an amount of good . It is piecewise linear and concave: it is given by a finite list of bounded segments with rational amounts , followed by a last, unbounded segment, with rational slopes . The function has slope on and slope afterwards. Buyer 's utility for a bundle is additively separable:
Given prices , a bundle is optimal for buyer if and no bundle with has . The prices are equilibrium prices if there is an allocation that gives each buyer an optimal bundle and sells every good exactly: for every .
The bit size of a rational number in lowest terms is the binary length of plus that of . The encoding size of a market is plus the bit sizes of all budgets, slopes and amounts, plus the number of bounded segments.
For the intermediate results, fix positive prices . The bang per buck of a segment of good is and its value is (infinite for an unbounded segment). Sorting buyer 's segments by decreasing bang per buck into classes of equal bang per buck, the first class at which the cumulative value exceeds is her flexible class. Segments of strictly larger bang per buck are forced, the others undesirable. From these the paper defines (value of the forced segments), , (the part of good not taken by forced segments), and a network from a source through goods and buyers to a sink.
There is a polynomial such that for every Fisher market as above,
The polynomial is fixed before the market. Nothing beyond the existence of some real equilibrium is assumed.
The result is what makes the existence problem for these markets a problem in NP: a rational equilibrium of polynomial size is a certificate that can be checked, with Lemma 3.1, by one max-flow computation. The same rationality statement underlies the paper's PPAD-membership proof and its NP-completeness result for existence. It also marks the boundary with markets whose equilibria can be irrational, as happens for some non-separable utilities. In that sense it shows that separable piecewise-linear concave utilities keep the "linear" character of the problem even though computing an equilibrium becomes hard.
All three statements are proved in the source, and none of them has a machine-checked proof on the platform or, as far as is known, anywhere else. The mission produces the first formal account of piecewise-linear Fisher markets: the model, the forced/flexible/undesirable classification of segments, the max-flow test for equilibrium, and the linear program of §4. It also forces precision where the paper is informal. The §4 bang-per-buck inequalities are printed with their directions reversed, and the claim about optimal LP solutions needs positive prices. The formal statements record each of these choices.
The obvious argument is: "equilibria are solutions of a linear system, so a rational one exists". It fails as stated, because the set of equilibrium prices is not a polyhedron. Which segments a buyer buys depends on the prices themselves, through the ordering of the ratios , so the equilibrium conditions are a finite union of polyhedral pieces glued along the price-dependent ordering. The work is to freeze the combinatorial structure of one given equilibrium and to show that the resulting fixed linear program still certifies equilibrium at every one of its optimal points. That second step is what Lemma 3.1 is for. The polynomial bit bound then needs a quantitative bound on the vertices of a rational LP, uniform in the market's encoding.
Buyers and goods are Fin n and Fin g. Budgets, slopes and amounts are rationals (ℚ). Prices and allocations are reals (ℝ), so that "admits rational prices" is a real conclusion: the goal returns q : Fin g → ℚ whose cast is an equilibrium. The committed conventions are:
(slope, amount) pairs of bounded segments together with the slope of its last, unbounded segment ("the last (infinite) segment", §6), with nonnegative slopes, positive amounts and nonincreasing slopes, stored inside the market structure;Hypotheses added relative to the page, each disclosed in its statement:
The §2 condition on p. 10:7 is a sufficient condition for existence and is deliberately not a hypothesis of the goal, which assumes only that an equilibrium exists. Complexity-class statements ("in NP", "PPAD-complete") are out of scope. What is formalized is the explicit polynomial bit bound, with a polynomial chosen before the market. A goal with the polynomial chosen after the market, an encoding size that ignores the bits of the data, or an equilibrium notion without utility-maximizing bundles would be trivially satisfiable. The statements rule all three out.
Beyond this mission, a complete development needs LP theory with rational data: existence of optimal basic solutions and determinant bounds on their bit size. Existing platform results that may serve as substrate include SmaleNinth.exists_square_subsystem and SmaleNinth.abs_det_le_factorial_mul_pow. Contributions welcome: proofs of the milestones, a reusable bit-size theory for rational LP vertices, and the Arrow–Debreu analogue (Theorem 5.1).
Stochastic approximation finds a root of an unknown map from noisy evaluations , by the Robbins–Monro recursion . It underlies stochastic gradient descent, recursive estimation in statistics, adaptive control and simulation-based optimization. The classical theory (Sacks 1958) shows that the fastest attainable rate, with and the noise covariance, is achieved by the matrix step , which requires knowing .
Polyak and Juditsky (SIAM J. Control Optim. 30 (1992) 838–855) proved that the same optimal covariance is attained without any knowledge of : run the recursion with scalar steps that decrease more slowly than and output the running average of the iterates. Ruppert (Cornell ORIE technical report, 1988) obtained the one-dimensional case independently. The method, known as Polyak–Ruppert averaging, is the standard device for variance reduction in stochastic approximation.
Timeline:
Let be a filtered probability space and an adapted -valued noise process. Given a nonrandom and step sizes , algorithm (7) is
The error is and the estimation error is .
The hypotheses are:
The linear case, algorithm (2), is with every eigenvalue of having positive real part.
Under Assumptions 3.1–3.4,
Theorem 2 shows that averaging turns a robust, slowly-stepped recursion into an asymptotically efficient estimator. The covariance is the lower bound for this class of problems: for linear recursive estimates with independent noise it is the bound of [26] in the paper. Downstream, the result is what is invoked for the asymptotic efficiency of averaged stochastic gradient descent (Theorem 3 of the paper) and of recursive M-estimators in regression (Theorem 4).
The result is proved, with a published proof, but has no machine-checked version. As far as a search of the platform shows, no statement of Theorem 1 or Theorem 2 exists on Prove2Me. The platform does have a scalar martingale central limit theorem (Martingale.clt_of_mds, proved, with unconditional Lindeberg condition), which is usable through the Cramér–Wold device. Formalizing Theorem 2 also requires the Robbins–Siegmund almost-supermartingale theorem, a multivariate CLT for martingale differences under conditional Lindeberg and conditional covariance conditions, and the Kronecker lemma. Mathlib has none of these three in the required form, and each is reusable well beyond this mission. Non-asymptotic SGD rates already on the platform (the Bottou–Curtis–Nocedal and Lan missions) are different results.
The obvious approach analyses directly. It fails: with steps decreasing more slowly than , diverges, and only the average has the rate. The average must be compared with the averaged noise through the matrix sums of Lemma 1, whose bounds are uniform in both indices. Those bounds rely on the step condition in a quantitative way.
The nonlinear case adds a second difficulty. The iterates are first shown to converge almost surely, by a Lyapunov argument. The nonlinear error is then transferred to a linearised process at the scale, which needs a summability estimate on obtained through stopping times. A central limit theorem for the linear process alone does not give the result, because the linearisation error must vanish after multiplication by .
Points are in EuclideanSpace ℝ (Fin N) and matrices are Matrix (Fin N) (Fin N) ℝ, acting through Matrix.toEuclideanLin. Matrix norms are operator norms. Conditional expectations are MeasureTheory.condExp on a Filtration ℕ. "Given " is written with shifted indices ( given ). The algorithm is a recursive definition from , with unused and averaging . Convergence in distribution is TendstoInDistribution to multivariateGaussian 0 V. Convergence of conditional covariances in probability is entrywise TendstoInMeasure. A limsup or supremum "tending to 0 in probability" is unfolded into its – definition.
Corrections of the printed text, each used by the paper's own proof:
Several formalizations would make the goal trivial, and all are ruled out:
Welcome contributions: the Robbins–Siegmund theorem, a vector martingale CLT under conditional Lindeberg conditions, the Kronecker lemma, and the matrix estimates of Lemma 1.
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.
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.
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.
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.
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.
Formalization status, 10 October 2026: all eight milestones are complete. Both corrected addenda are Proved. The subgroup upper Hilbert estimate has an accepted proof with eight Proved inputs and no Open dependencies (submission 07198c4c-ea10-4c9a-89b8-b4a5319c40b5). Together with the accepted sharp contact-rank and ambient lower Hilbert bounds, this discharges every dependency of the corrected converse. The corrected 26-part full-paper goal remains Open, with exactly two frontier leaves: quadratic parameter-stalk germs and the local complex model for the closure action. The common-shift forward conclusion, quadratic first-input addition hypothesis in the converse, all constants and degree thresholds, and all 24 unaffected goal clauses are unchanged. The separately published Chardin theorem in arbitrary characteristic remains Open; it is no longer required by this mission proof.
An auxiliary polynomial in a transcendence proof is constructed to vanish to high order at many points. A multiplicity estimate limits how often that can happen without a geometric reason: a positive-dimensional algebraic subgroup can make the apparent vanishing conditions dependent. Such estimates are used to turn analytic approximations into algebraic-independence conclusions. The theory applies to products of commutative algebraic groups with both archimedean and nonarchimedean analytic directions.
The mission's objective is a faithful formalization of the complete 1986 paper, Patrice Philippon's Lemmes de zéros dans les groupes algébriques commutatifs, including every theorem, corollary, proposition, lemma, definition, and mathematical supporting claim. All results remain required whether or not a current application uses them. Necessary source corrections are explicit and their counterexamples remain part of the completion goal. The author's 1987 corrections are applied transparently, and the addendum's additional results are recorded separately (original, errata and addenda).
Let K be the complex field or the completed algebraic closure of the field of ℓ-adic numbers for a prime ℓ, as in the source. Let G be a product of finitely many commutative algebraic groups G₁,…,Gᵣ over K, with each factor embedded as a quasi-projective variety in a projective space. Write n for the sum of their dimensions. A point of the product embedding has one block of homogeneous coordinates for each factor.
A nonzero multihomogeneous polynomial P has a degree Dᵢ in its i-th block of coordinates. Its zeros define a hypersurface of the ambient product of projective spaces. An analytic subgroup A is locally parametrized by an analytic homomorphism from a finite-dimensional additive K-space. The order of P along A at a group point g is the vanishing order of P after composing local projective coordinates with the translated parametrization. This definition must be independent of the choice of nonzero local coordinate representatives.
Let Σ be a finite set of group points containing the identity. Its n-fold sumset Σ(n) consists of all sums of n, not necessarily distinct, elements of Σ; Σ(0) is the singleton identity. For a connected algebraic subgroup H, the integer s is the analytic codimension of A∩H in A. The expression |(Σ+H)/H| counts distinct H-cosets meeting Σ. Codimension concerns the analytic tangent dimension; it does not assert that the point-set intersection is finite.
The source's Hilbert degree form ℋ(V;D₁,…,Dᵣ) is (dim V)! times the highest homogeneous part of the multigraded Hilbert–Samuel polynomial of the projective closure of V, evaluated at the degrees. It must be constructed from the coordinate ring, rather than supplied as an arbitrary numerical function. For one projective factor it is deg(V)D^(dim V). These definitions are fixed in §§2–3 of the original paper.
The completion target is all results of the paper, with an aggregate goal that requires their individual formal statements. Theorem 2.1 is one milestone within that target. For each fixed family of embedded group factors, it chooses positive integers cᵢ, each depending only on its corresponding embedding. These constants precede the analytic subgroup, the finite sampling set, the polynomial degrees, the polynomial, and the contact parameter T. If P has order at least nT+1 along A at every point of Σ(n), there is a connected algebraic subgroup H with
The same H is contained in a translate of the zero locus of P on G and is incompletely defined by equations of multidegrees at most (c₁D₁,…,cᵣDᵣ): it is an irreducible component of the common zero locus in G of equations with those degree bounds. Both geometric conclusions are part of the target. A formalization retaining only the displayed numerical inequality would omit part of the original result.
The 1986 paper has 13 numbered results. Section 2 contains Theorem 2.1 and Corollaries 2.2–2.3, including the one-dimensional analytic result and the result for disjoint group factors. Section 3 contains Lemmas 3.1–3.2, Proposition 3.3 and Lemma 3.4. Section 4 contains Propositions 4.3–4.4, Lemmas 4.5–4.6 and Proposition 4.7. Section 5 contains Lemma 5.1. Every clause of these statements belongs to the mission.
Definitions 3.5, 4.1 and 4.2, the unnumbered setup, the internal Facts A–E, the counterexample after Proposition 3.3, and the mathematical claims in remarks also require coverage. Source numbers and page references identify the correspondence between the prose and Lean declarations. The two 1987 addendum targets are explicitly corrected variants. The forward statement assumes ambient connectedness and allows one common shift , so for every sampled , with the same connected subgroup satisfying incomplete definition and the full coset-count inequality. Its embedding-dependent constants are chosen before the sample and polynomial. This is not an exact transcription of the printed strengthening. The converse assumes ambient connectedness and explicit local addition formulas of degree at most two in the first input for every embedded factor. Its subgroup may remain disconnected; the degree threshold, constant , and polynomial nonzero somewhere on are unchanged. All original sampling and contact assumptions remain. No desired estimate is encoded as a geometric assumption.
The completion goal is PhilipponMultiplicity.paper_results_corrected_erratum, a conjunction of 26 concrete propositions. This is a collection goal requiring the source statements and the additional mathematical claims in the coverage record. It is separate from the paper's original Theorem 2.1, which remains individually named and reusable.
The mission has eight milestones; seven are currently Proved:
| Source | Milestone | Status |
|---|---|---|
| Theorem 2.1 | General multiplicity estimate, with every geometric and numerical conclusion. | Proved |
| Corollary 2.2 | One-dimensional analytic-subgroup consequence. | Proved |
| Corollary 2.3 | Consequence for disjoint group factors and sampling grids. | Proved |
| Proposition 3.3 | Multigraded intersection bounds, including the multiplicity-sensitive bound. | Proved |
| Proposition 4.7 | Binomial lower bound for contact multiplicity. | Proved |
| Lemma 5.1 | Stabilizer construction and the geometric counting estimate. | Proved |
| 1987 addendum, p. 398 | Corrected common-shift vanishing in a connected ambient group. | Proved |
| 1987 addendum, p. 398 | Connected converse with first-input addition degree at most two. | Open |
The full statement package has 27 compiled theorem statements: all thirteen numbered results, both addenda, eleven supporting or correction targets, and the aggregate goal. The fourteen original admission-free definition bundles and one erratum supplement supply their actual geometric and algebraic objects. All 41 original statement and definition items have independent blind readbacks. The eight milestones above retain their existing identities.
The supporting clauses include Hilbert-polynomial existence, primary components and Facts A–E; the geometric interpretation of mixed degree; the actual counterexample after Proposition 3.3; translation operators and their comparison with intrinsic ideals; contact invariance; translation-invariance and embedding remarks; the component/stabilizer construction; counting estimates; and the exact Masser–Wüstholz Theorem I consequence claimed on p.361. Proof-internal recursive ideals and tangent/exponential arguments belong to their corresponding theorem proofs.
Source corrections are visible for review. Lemma 3.1 and Corollary 2.2 require positive equation degrees; explicit zero-degree counterexamples are required goal clauses. Both addenda require positive ambient dimension; the goal also requires their dimension-zero counterexamples. The three-generator ideal printed on p.370 is nonradical, contrary to the printed word “prime”; its valid degree-four versus length-six counterexample is preserved, together with an explicit nilpotent witness. Connectedness is stated in the translation-invariance and Lange reembedding remarks. These are mathematical corrections documented during the source comparison, beyond the author's 1987 errata. They are not silent changes to the source.
Existing completed proofs and all 24 unaffected goal clauses are retained. The corrected forward addendum is Proved. The repaired converse and the replacement collection goal remain Open; two general geometry lemmas also remain on the frontier. The existing proved local-algebra references remain reusable ingredients.
The output is a reusable development of the paper's multigraded commutative algebra, translation and differential operators, geometric multiplicity theory, and zero estimates. All source results are required for completion. A downstream Weierstrass application can consume a specialization of Theorem 2.1; its needs do not determine the scope or completion of this mission (example application).
These are established mathematical results whose proofs are being formalized. The complete original Theorem 2.1 has an accepted proof. The selected Weierstrass application uses individually named Philippon results, with its application-specific model and subgroup bridges proved in the Senthil mission. The remaining general results stay required even though that application is complete.
Vanishing conditions need not be independent: many can occur on the same component or on translates with a nontrivial stabilizer. Counting coefficients of P therefore does not bound their total multiplicity. The development needs geometric degree for actual components, multiplicities measured by lengths of localized quotient rings, and uniform control of translations in fixed projective embeddings.
Proposition 3.3 supplies multigraded intersection bounds, Proposition 4.7 controls contact multiplicity, and Lemma 5.1 connects the stabilizer to the geometric counting estimate. These three results and Theorem 2.1 now have checked proofs. The remaining corollaries, general geometric and analytic claims, examples and addenda are independent deliverables. Application-specific contact results do not discharge the remaining general statements.
The declarations use the namespace PhilipponMultiplicity. Source statements retain their conclusions, constants, quantifier order, and complex or ℓ-adic scope, with the visible boundary and wording corrections listed above. Intermediate specializations are labelled as such and do not discharge a more general source result. Natural-number and zero-degree conventions have been compared with the original scans; the discovered failures and corrected hypotheses are recorded explicitly for human review. Corrections and inferred conventions must be documented rather than silently changing the source.
The required definitions include embedded commutative algebraic groups and their connected subgroups; products of projective spaces and multihomogeneous coordinate rings; analytic local homomorphisms and intrinsic contact order; multigraded Hilbert polynomials and their degree forms; local component lengths; and finite coset counts. No model may assume the desired multiplicity inequality, hide it as a structure field, or replace geometric degree by an unconstrained function.
The 26 individual target statements, replacement collection goal, original definition bundles, and erratum supplement compile in Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Source comparisons and independent readbacks document the fixed statements and their explicit corrections. The goal remains the concrete 26-part full-paper collection. The completed proofs supply reusable Hilbert theory, primary-component multiplicities, polynomial differential operators, bounded translation atlases and the Section 5 construction. Contributions to the remaining targets, including results unused by Senthil, complete the original scope.
The previous aggregate, original sampled-translates addendum, and original converse remain available with their prior submissions and disproofs. The replacement statements changed the mission goal explicitly before proofs were supplied. The corrected common-shift forward statement has since received an accepted proof.
A graph records pairs of objects that cannot be chosen together. An independent set is a choice with no conflicting pair. When each vertex has a nonnegative weight, maximum weighted independent set asks for a conflict-free set with the greatest total weight. This model occurs when choices have values and pairwise incompatibilities. On general graphs the optimization problem is difficult; the planar restriction gives a concrete geometric promise under which approximation is possible. Williamson and Shmoys state a polynomial-time approximation scheme for planar maximum independent set as Theorem 10.11 of The Design of Approximation Algorithms, in the author electronic manuscript at PDF/manuscript page 271.
The instance has vertices labeled by Fin n, an adjacency table edge : Fin n → Fin n → Bool, and a real weight weight i for each vertex. SimpleGraph.fromRel turns the table into an undirected simple graph G. The theorem requires every weight to be nonnegative. A finite set S is feasible when G.IsIndepSet (S : Set (Fin n)) holds. Its value is ∑ i ∈ S, weight i.
Planarity is expressed by HasPlanarDrawing G: vertices are placed at distinct points of the real plane, and every edge is represented by a continuous simple arc. An arc has no vertex in its interior, and distinct edges can meet only at endpoints. This is a concrete local drawing convention for the planar graph promise. The drawing witnesses the hypothesis; it is not passed as part of the algorithm's input.
The computational model is a fixed finite unit-cost RAM program. Its input includes the vertex count, an integer accuracy parameter, a complete adjacency table, and the real weights in named memory cells. Its instructions include natural-number and real addition and subtraction, exact comparisons, random-access loads and stores, branches, jumps, and halt. The machine starts with the instance preloaded and produces a bitmap after the adjacency table. This precise instruction set is a formalization convention: the book states an arithmetic-operation running time but does not specify a machine language.
For every real , let . The goal asserts that a single finite program and fixed positive natural constants work for every planar instance and every vector of nonnegative real weights. The program must halt after a number of operations satisfying
Its bitmap must represent an independent set , and for every independent set ,
Comparison with every feasible includes an optimal solution. The same program and constants precede all accuracy and instance quantifiers. The form includes the empty graph without imposing zero running time. The result corresponds to the bound in Theorem 10.11; the formal statement makes the constants and accuracy parameter explicit.
The result supplies an accuracy-time tradeoff for planar weighted independent set: any fixed positive accuracy has a quadratic dependence on graph size in this operation model, while the accuracy dependence is exponential. It separates the planar setting from the general graph problem. The finite instruction set and input layout make the computational claim inspectable, including what information the program receives and what counts as an operation.
The cited result is known in the textbook. This mission asks for a Lean proof of the packaged statement; the theorem currently has sorry, and no machine construction or correctness proof is claimed. The original local statement was compiled and source reviewed before packaging. That prior result establishes statement validity in its source workspace, while the upload payload is checked separately.
A high-quality independent set in each planar region does not immediately give a high-quality global set: edges across regions can create conflicts, and discarding boundary vertices can lose weight. A proof must coordinate the approximation inequality with a uniform operation bound for one program across all graph sizes, accuracies, and real weight vectors. It must also show the computed bitmap is always independent and that execution reaches an explicit halt instruction within the bound. These requirements rule out treating an optimizer, an embedding, or a best solution as preloaded input.
The goal uses finite labeled graphs, nonnegative arbitrary real weights, exact real arithmetic, and the concrete drawing predicate above. It does not claim a bit-complexity bound for encoded reals. The RAM starts from a complete adjacency table and weight vector, with no supplied drawing or optimum. Its step function is deterministic; an invalid program counter is stuck, so the theorem explicitly requires a halt instruction. Outputs are bits in designated natural memory cells and are checked for validity before their weighted value is compared.
The packaged definitions are the drawing predicate, instruction type, state, transition, iteration, input layout, and output decoder. They contain no proof axioms or optimization oracle. The rational-input polynomial bit-time fragment in the source workspace is a separate statement and is outside this goal. A complete contribution would construct the finite program and prove its running time and approximation guarantee in the specified model.
Almost every classical transcendence theorem is a statement about the interaction between the additive structure of and the exponential function. Hermite proved in 1873 that is transcendental, Lindemann in 1882 that is transcendental for every nonzero algebraic — hence that is transcendental and the circle cannot be squared — and Weierstrass in 1885 extended this to the linear independence of over for distinct algebraic . Gelfond and Schneider settled Hilbert's seventh problem in 1934, and Baker's 1966 theorem on linear forms in logarithms made the subject effective.
Schanuel's conjecture, formulated by Stephen Schanuel in the 1960s and first published by Lang (Introduction to Transcendental Numbers, Addison–Wesley, 1966, Chapter III), is a single statement that contains all of these as special cases, together with a large number of statements that remain open — for instance that and are algebraically independent, or that is irrational. No case of it is known beyond those already covered by the Lindemann–Weierstrass theorem or by Baker's theorem.
Timeline, with the hypotheses each result actually assumes:
Write for the complex exponential function. A tuple of complex numbers is linearly independent over when the only rationals with are ; here is viewed as a vector space over .
For a subset , let denote the subfield of generated by over . The transcendence degree is the cardinality of a transcendence basis of over : the largest number of elements of that are algebraically independent over . A number is transcendental over when no nonzero polynomial with rational coefficients vanishes at , and numbers are algebraically independent over when no nonzero polynomial in variables with rational coefficients vanishes at .
The goal fixes no numerical constant and no special shape for the : it asserts only the inequality, for every and every -linearly independent tuple. The case is vacuous and the conclusion is a bound on a cardinal, so nothing is hidden in a degenerate convention.
The milestone list consists of the landmark unconditional theorems that Schanuel's conjecture generalizes, the known function-field analogue, and one conditional corollary that records what the conjecture buys:
Schanuel's conjecture decides, in one stroke, a long list of questions that are individually open: the algebraic independence of and , the irrationality of and of , the transcendence of and , the four exponentials conjecture, and — combined with work of Macintyre and Wilkie — the decidability of the first-order theory of the real exponential field. Its restriction to algebraic is exactly the Lindemann–Weierstrass theorem, and its restriction to whose exponentials are algebraic is exactly Baker's theorem, so the conjecture is a common generalization of the two main unconditional pillars of the subject.
On the formalization side, the state of the art in Lean's mathematical library is modest relative to this history: the analytic core of the Lindemann–Weierstrass argument is present, but the Hermite–Lindemann theorem, the Lindemann–Weierstrass theorem, the transcendence of , the Gelfond–Schneider theorem, the six exponentials theorem and Baker's theorem are not available as usable statements in the pinned environment. Each milestone here is therefore a genuine formalization project with a known mathematical proof, and none of them is a restatement of an existing library result. The goal theorem itself is open mathematically; the realistic contributions to it are reductions — implications between the goal and other statements — and closing the milestones that the conjecture generalizes.
The obvious approach to any single case — build an auxiliary function with many zeros, bound its derivatives, and derive a contradiction from an integrality argument — is the method behind every result on the milestone list, and it is exactly what fails for the conjecture in general. Those proofs need the exponentials, or the arguments, to be algebraic somewhere, so that heights and denominators can be controlled; for a general -linearly independent tuple there is no arithmetic input at all, and no known construction produces the required auxiliary function. Ax's theorem shows that the differential-algebraic shadow of the statement is true, but its proof uses the derivation on the function field and has no arithmetic counterpart. A solver should not expect the conjecture itself to fall to a variation of the classical method.
All statements are over , with the complex exponential. Tuples are indexed by Fin n, ℚ-linear independence is Mathlib's LinearIndependent ℚ, transcendence degree is Mathlib's Algebra.trdeg, the generated field is IntermediateField.adjoin, and the inequality is between cardinals, so the goal reads (n : Cardinal) ≤ Algebra.trdeg ℚ (adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z))). Algebraicity is IsAlgebraic ℚ, transcendence is Transcendental ℚ, and algebraic independence is AlgebraicIndependent ℚ.
There is no trivializing formalization here: the hypothesis LinearIndependent ℚ z is satisfiable for every , so the goal is not vacuous, and the conclusion is an inequality of cardinals rather than a statement about a definition introduced for this mission.
The Ax milestone is stated for formal power series in one variable over : the exponential relation is expressed as the differential equation with PowerSeries.derivative, and the conclusion bounds Algebra.trdeg ℂ of the ℂ-subalgebra generated by the and the . The conditional corollary takes the full statement of Schanuel's conjecture as an explicit hypothesis, so it is provable unconditionally as stated.
Infrastructure that a complete development needs, and that is reusable well beyond this mission: Siegel's lemma and height machinery for algebraic numbers, the standard auxiliary-function construction with derivative bounds, and interface lemmas relating Algebra.trdeg, AlgebraicIndependent and Transcendental. Reductions between the milestones — for example deriving Hermite–Lindemann from Lindemann–Weierstrass, or the six exponentials theorem from a general Baker-type statement — are welcome as sketches.
The Hodge conjecture predicts that on a non-singular complex projective variety every rational cohomology class of type is a rational linear combination of the classes of algebraic subvarieties of . Abelian varieties are the oldest testing ground for the conjecture, and the hardest known classes on them were isolated by A. Weil. A -dimensional complex abelian variety is of Weil type for an imaginary quadratic field if embeds into in such a way that both eigenspaces of meet in an -dimensional subspace. Such an carries a distinguished two-dimensional space of rational -classes, the Weil classes, which for a generic of Weil type does not lie in the subring generated by divisor classes. Weil classes are therefore the standard obstruction to the Hodge conjecture in low dimension: for abelian fourfolds the conjecture reduces to their algebraicity.
Timeline of the unconditional results on algebraicity of Weil classes:
Fix and present a -dimensional complex torus by its first homology: a complex structure on with , the lattice being . A polarization is a rational alternating form on satisfying the Riemann relations and for . Cohomology is , realized as the alternating -multilinear forms on ; a class is rational if its values on rational vectors are rational, and it has type if it is multiplied by under the scaling action of . A Hodge class of degree is a rational class of type .
Let and with . A polarized abelian -fold of Weil type is such an together with a rational endomorphism of with
the last condition saying that multiplies the polarization class by the norm , and such that each of the two eigenspaces of meets the -eigenspace of in an -dimensional subspace. The Hodge–Weil classes are the rational classes in
equivalently the rational degree- classes that vanish on every tuple of vectors containing both a vector of and a vector of .
The form is -valued and hermitian on , viewed as a -vector space through . The determinant of its Gram matrix in a -basis lies in , and its class in is the discriminant of . Discriminant means that this determinant equals for some rationals not both zero.
Algebraicity is not modelled abstractly. An abelian variety is tied to a genuine non-singular projective variety by a projective realization: a smooth, -periodic immersion , surjective onto and injective modulo the lattice, whose differential intertwines with the complex structure of . A class is algebraic when some de Rham class of whose periods over the -cycles swept out by rational vectors equal is a rational combination of cycle classes of irreducible subvarieties of dimension . Cycle classes, de Rham cohomology of a projective variety, -types and Hodge classes are taken from the platform's HodgeConjecture bundle, which formalizes §1 of Deligne's Clay problem description.
The statement fixes neither the field nor the sixfold: it quantifies over every , every polarized abelian sixfold of Weil type of discriminant , and every projective realization of it.
for every imaginary quadratic and every discriminant; this is the use made of Schoen's Proposition 10 (Compositio Math. 114 (1998)) in the paper.
Divisor classes: every Hodge class in of a non-singular projective variety is algebraic. This is an already published platform statement, imported here as a reference, since the reduction in Corollary 1.6.1 uses the algebraicity of divisor classes.
Weil classes are, by the results of Moonen–Zarhin (Duke Math. J. 77 (1995), Math. Ann. 315 (1999)), the only obstruction left in dimension four: for a simple abelian fourfold is spanned by quadratic expressions in divisor classes and by Weil classes, and the non-simple cases reduce to products treated by Ramón Marí (Collect. Math. 59 (2008)) and Moonen–Zarhin. The goal theorem therefore closes the Hodge conjecture for abelian fourfolds, the first dimension in which the conjecture for abelian varieties was open.
Formalizing it produces, first, a reusable Lean model of polarized abelian varieties, of complex multiplication of Weil type, of the Hodge–Weil plane and of the discriminant, tied to an honest notion of algebraic cohomology class through projective realizations. None of these objects exists in Mathlib today. The result itself is proved in the source preprint and has no machine-checked proof; the milestones below are equally unformalized, including the classical statements of Weil and Schoen that the paper's Corollary depends on.
The naive attack — write down subvarieties whose classes span — fails because Weil classes are not expressible through divisors: for a generic abelian variety of Weil type the Néron–Severi group is cyclic while is three-dimensional, so no product of divisor classes reaches the Weil plane. The source constructs instead a reflexive sheaf on , for the Jacobian of a genus- curve, whose characteristic class remains of Hodge type along all deformations of as a polarized abelian sixfold of Weil type, and deforms the pair over that moduli space using a semiregularity theorem for twisted sheaves. Each of these steps — Orlov's derived equivalence, spinor geometry of the Mukai lattice, semiregularity — is itself missing from Mathlib, which is why the milestone list stays on the Hodge-theoretic side of the argument rather than transcribing the sheaf-theoretic core.
Conventions the Lean development commits to:
A complete development needs, beyond what is drafted here: the spin representation of the Mukai lattice of an abelian -fold, pure spinors and -secant lines, Orlov's equivalence, Atiyah classes and semiregularity for twisted sheaves. Contributions establishing any of these, or proving the Hodge-theoretic milestones, are welcome.