Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Chapters 1–3 of Baccelli and Brémaud's Elements of Queueing Theory compute exact quantities: Palm identities, stability criteria, PASTA, Pollaczek–Khinchin. Chapter 4 asks a different question. When you cannot compute a queue, can you at least say it is better than another one?
That requires an order on distributions. The chapter builds a family of them — integral orders
— by choosing a class ℒ of test functions and declaring F ≤_ℒ G when ∫f dF ≤ ∫f dG for all
f ∈ ℒ. Three matter: {i} the non-decreasing functions, giving the strong (stochastic)
order; {cx} the convex functions, giving the convex order; and their intersection {icx}.
An integral order compares two distributions that need not live on the same probability space, and that is both its convenience and its difficulty. Strassen's theorems say each of these orders is secretly a statement about a coupling.
Theorem 4.2.2 (p.278), Strassen's ≤_cx theorem:
F ≤_cx G ⟺ ∃ X ~ F, Y ~ G on one space with E[Y | X] = X a.s.
F ≤_icx G ⟺ the same with E[Y | X] ≥ X a.s.
The convex order holds exactly when G is a martingale dilation of F — obtained by spreading
each point out without moving its conditional mean. That is what makes the order usable: comparison
results for queues become induction arguments on a coupling instead of analytic manipulations of
convolutions of c.d.f.'s.
Its companion Theorem 4.2.1 is the ≤_st version, where the coupling is the simpler X ≤ Y
a.s. In dimension one both are explicit — take X = F⁻¹(U), Y = G⁻¹(U) for a uniform U. In
dimension n there is no such formula, and that is why these are Strassen's theorems. The book
attributes both to Strassen (1965) and proves neither.
§4.1 is a different kind of comparison: not between two queues, but between two service
disciplines for the same queue. The order there is majorization ≺, which compares how
spread out two vectors of the same total are.
The answer is that FIFO minimizes E⁰[f(V)] for every convex f (Property 4.1.3), and the proof
is an interchange argument. Under any non-preemptive discipline that uses no information on the
service times, customer k effectively receives service σ_{γ(k)} for some permutation γ;
Lemma 4.1.3 shows the same queue is produced by FIFO fed with that reordered input, and that
the reordering does not change the law of the input. Lemma 4.1.4 passes to the limit, which
needs ρ < 1. Lemmas 4.1.1 and 4.1.2 then do the combinatorics: undoing one inversion of γ
makes the waiting-time vector less spread out, so the identity permutation — FIFO — is extremal.
§4.4 compares time-stationary queues, and opens with a warning. T_n[P⁰] ≤_i T̃_n[P̃⁰] for
every n does not imply T_n[P] ≤_i T̃_n[P̃]: Example 4.4.1, "Feller's paradox revisited",
exhibits a Poisson process and a renewal process where the Palm order holds and the stationary one
fails. The order does not pass from the Palm probability to the stationary one.
For ≤_cx it does. Lemma 4.4.1 is why: it expands E_P[f(N[0,x))] as a series of second
differences of f against Palm expectations, and a convex f makes every coefficient
non-negative. Lemma 4.4.2 handles the S-orders, built by dividing Palm integrals by the mean
cycle length, and shows that the normalisation does not hide the comparison it normalises by.
≤_i, ≤_cx, ≤_icx on distributions on ℝⁿ are integral orders over the book's
test classes (§4.2.1), with the page's qualification that only test functions with well-defined
integrals count. Majorization ≺ is (4.1.2) with increasing reorderings of both vectors.E[Y | X] = X for ≤_cx, E[Y | X] ≥ X
for ≤_icx, as conditional expectations given σ(X) — and assumes both distributions integrable;
Theorem 4.2.1 has no integrability hypothesis. A one-directional statement (the Jensen half) is
not the theorem.GI/GI input (i.i.d. inter-arrival and service times,
independent), a single work-conserving server started empty, and any non-preemptive discipline
whose choices are measurable in the information the book's σ-field 𝒢_t carries (arrivals,
service times of customers already started) plus external randomisation. FIFO is one such
discipline. The interchange permutations γ_n and their limit γ are built from the schedule
as on pp.268–270; Lemma 4.1.4 assumes ρ = E[σ₀]/E[τ₀] < 1.f, which fails for heavy-tailed counts and
sparse f.S-orders test against {I-ℒ} — primitives ∫_0^t f(u, x) du of test functions —
and apply only to distributions whose first coordinate is a.s. positive with a finite mean.None of it exists. Mathlib has no stochastic order, no convex order, no increasing-convex order, no
majorization, no Schur-convexity and no Strassen theorem; the platform returns zero hits for
q=stochastic ordering. Everything in this chapter is new substrate — and §§4.1–4.2 need nothing
from Palm calculus, so this mission can be read on its own.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds Palm calculus. Chapter 2 settles when a queue has a stationary regime. Chapter 3 is called simply Formulas, and it is what the first two chapters were for: it computes.
The pattern is always the same. A quantity of interest is observed two ways — from a clock fixed in time, and from an arriving customer — and Palm calculus converts between them. Little's law, the Pollaczek–Khinchin formula and the rate conservation principle are all instances.
Theorem 3.3.1 (p.211) is the one that says when the two views coincide.
This classical result of queueing theory states, in rough terms, that if the arrival point process is Poisson, operational characteristics of the system computed just before arrival times and at arbitrary times are the same (Poisson Arrivals See Time Averages). Some care must be exercised in the application of this principle, and we now give a precise statement, in the
θ_t-framework.
E⁰_A[f(Z(0))] = E[f(Z(0))] (3.3.1)
for every F_t-predictable, flow-compatible {Z(t)} and every non-negative measurable f,
whenever A admits the constant F_t-intensity λ; and, under ergodicity,
lim_N (1/N) Σ_{n=1}^N f(Z(T_n)) = lim_T (1/T) ∫_0^T f(Z(s)) ds . (3.3.2)
The "some care" is the word predictable. PASTA is false without it: an arrival that changes the
state it then observes does not see the time average, and that is exactly what predictability —
measurability for the F_t-predictable σ-field, generated by the sets (a,b] × A with A ∈ F_a —
rules out.
The hypothesis is the constant F_t-intensity, not "A is Poisson". By Watanabe's theorem the two
are equivalent, but that equivalence is a remark on the page and not part of this theorem.
§3.4 derives formulas from conservation equations. Applying the rate conservation principle of
Chapter 1 to Y(t) = e^{iuW(t)} in a GI/GI/1/∞ queue gives Takács' formula
iu E[e^{iuW(0)}] = λ E⁰_A[e^{iuW(0−)}] (E[e^{iuσ_0}] − 1) + iu(1 − ρ) , (3.4.44)
an identity between a stationary expectation and a Palm expectation of the workload just before
an arrival. One substitution turns it into a closed form — and that substitution is PASTA. When the
arrivals are Poisson, E⁰_A[e^{iuW(0−)}] = E[e^{iuW(0)}], and
E[e^{iuW(0)}] = iu(1 − ρ) / ( iu − λ(Ψ_σ(u) − 1) ) , (3.4.45)
the Pollaczek–Khinchin characteristic function formula. The most quoted formula in single-server queueing theory is one application of this mission's goal theorem.
§3.1 carries Little's formula to fluid queues. Lemma 3.1.1 is the set identity that turns the fluid workload into an integral against the arrival measure — the same two instants described from the server's side and from the arrivals' side.
§3.2 applies Campbell's formula to rare events. Lemma 3.2.1 gives a closed form, in a
countable-state Markov chain, for the mean time to make an excursion to a rare set and return; its
two expressions count the same cycle rate from the two ends. Theorem 3.2.1 generalizes
Keilson's asymptotic equivalence to a stationary θ_t-compatible process, replacing cycles by
thinnings of the entrance processes of two disjoint sets.
§3.5 applies the stochastic intensity integration formula to a superposition of on-off fluid sources. Lemma 3.5.1 identifies a conditional expectation with a Palm expectation through Papangelou's theorem — the mean workload while a source is idle equals the mean workload that source sees when it wakes. Lemma 3.5.2 measures the gap between the two Palm expectations of the workload taken with respect to a source's start process and its fluid process.
Nothing here is on the platform or in Mathlib. The nearest platform item,
queueing_general_littles_law, is Stidham's deterministic sample-path law; its own docstring
disclaims probability, expectation, stationarity, ergodicity and FIFO. Baccelli's L = λW is the
Palm identity for a stationary ergodic marked point process, derived from the inversion formula
(1.2.25) — an identity between an expectation under P and a Palm expectation under P⁰_N, not a
pathwise limit. Different framework, different hypotheses, and neither implies the other.
Mathlib has filtrations and adapted processes but no predictability in the form this chapter needs, and no stochastic intensity.
(3.3.1) is an equality in [0, ∞] for every non-negative
measurable f. (3.3.2) asserts that, P-almost surely, both averages converge in [0, ∞] to one
common limit, so both limits exist. Predictability is measurability for the predictable σ-field
P(F_t) of p.55. The concrete form Z(t,ω) = v(t, θ_t ω) of (1.8.1) is not used as the hypothesis,
because for a general history it is strictly weaker. The hypothesis is the constant F_t-intensity,
E[A(a,b] | F_a] = λ(b − a), and not "A is Poisson".u, and for
u ≠ 0 respectively. Their hypotheses are the page's: σ_n is independent of W(T_n−) under
P⁰_A, E⁰_A[e^{iuσ_0}] = E[e^{iuσ_0}], P(W(0) = 0) = 1 − ρ, and ρ < 1. The workload is a
measurable, flow-compatible solution of Lindley's equation. (3.4.45) adds PASTA's hypotheses for
{W(t−)}, and it asserts that its denominator is non-zero.E_α R. The chain is irreducible, F is non-empty,
and hitting times are counted from time 0.E⁰_{F_n(→A)}[τ(F_n)] · Λ_n → 1. Its hypotheses are the section's standing ones: P is
flow-invariant, {X(t)} is flow-compatible, and A and every F_n are regular and disjoint.P⁰_{A^i} is the Palm probability of the random measure A^i, and the workload is
the stationary solution of the fluid-queue equation. Lemma 3.5.1 is an identity in [0, ∞].
Lemma 3.5.2 assumes that E⁰_{A^i}[W(0)] and the expectation defining C_i are finite.A formalization that makes Palm probability an opaque measure with the formulas as axioms, or that weakens predictability to adaptedness, trivializes this mission or makes it false, and is out of scope.
Chapter 2 of Baccelli and Brémaud's Elements of Queueing Theory asks when a queue has a stationary regime. §§2.1–2.4 answer it for the single-server and multiserver queues by Loynes' monotone construction. §§2.5 and 2.11 answer it for the general object those constructions are instances of: a stochastic recurrence
W_{n+1} = h(W_n, ξ_n),
driven by a sequence {ξ_n} compatible with an ergodic shift θ. Two questions arise, and this
mission is about both.
§2.5.3 treats the finite-state case. An ergodic transition matrix on E = {1, …, r} has a
stationary law π, and the classical way to sample it is to run the chain and wait. That gives a
sample whose law converges to π and is never equal to it.
Coupling from the past (Propp and Wilson, 1996) does better. Run one chain from every state,
all sharing a single array {ξ_k(i)} of i.i.d. uniforms indexed by time and current state, started
further and further in the past. Once two chains meet they stay together, so eventually all r
coalesce before time 0 — and Theorem 2.5.1 says the common value they reach has the
distribution π exactly. Theorem 2.5.2 makes it practical: if the updating function
preserves a partial order with a least and a greatest state, and a single uniform sequence drives
every chain, the two extremal chains funnel all the others and their coalescence suffices.
Neither theorem is a statement about a program. Each says that a random variable is almost surely
finite, and that another has a distribution equal to π.
§2.5.4 treats the general case, through Borovkov's idea. An event A_n is renovating of length
m when, on it, W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}) — the sequence's value m steps ahead forgets
where it came from. Theorem 2.5.3 turns a condition on how often renovating events occur into
the existence of a finite stationary solution Z with Z ∘ θ = h(Z, ξ), and into strong
backwards coupling: W_n ∘ θ^{-n} is not merely convergent to Z but equal to it after a
finite random index.
Corollary 2.5.1 makes the limit independent of the initial condition — one stationary regime,
reached from every starting point. Theorem 2.5.4 is the converse: for ℝ₊^K-valued recurrences
with a constant initial condition, strong backwards coupling produces renovating events. So the
method characterises stability rather than merely detecting it.
§2.11 treats the multidimensional case, where the state is a vector and the natural models are
monotone and homogeneous. Theorem 2.11.1, due to Crandall and Tartar, is the key that unlocks
it: under homogeneity, monotone and non-expansive are the same property. That is what puts these
models within reach of Kingman's subadditive ergodic theorem, and Theorem 2.11.2 collects the
payoff — asymptotic growth rates γ̄ and γ_ exist, both almost surely and in L¹, and do not
depend on the initial condition.
Queueing folklore has a rule of thumb for the stability of an open network: saturate the queues
fed by the external stream, measure the departure intensity µ of the saturated system, and
declare the network stable when λ < µ. The book is careful that this saturation rule "does
not hold for all systems".
Theorem 2.11.3 (p.166), "the main result on the stability region", proves it for Monotone-Homogeneous-Separable networks:
If lim Z_{[-n,0]} → ∞ a.s., then λ γ(0) ≥ 1. If λ γ(0) > 1, then lim Z_{[-n,0]} → ∞ a.s.
Here γ(c) is the growth rate of the network fed by the scaled process cN, so c = 0 places
every arrival at the origin: γ(0) is exactly the saturated system's rate, and µ = γ(0)⁻¹.
Two implications, with a gap between ≥ 1 and > 1 that the book leaves open — as it leaves open
the critical case ρ = 1 of Loynes' theorem. Closing it would assert more than is proved.
Nothing here is on the platform or in Mathlib. There is no coupling from the past, no theory of
renovating events, and no Crandall–Tartar theorem. Order/Hom/* has monotone maps and
Topology/MetricSpace/* has LipschitzWith 1, which is the right ambient notion for
non-expansiveness in the sup-norm, but the equivalence between them under homogeneity is absent.
(P⁰, θ) is
ergodic and {ξ_n} is compatible with θ. The relation Z ∘ θ = h(Z, ξ) holds P⁰-a.s.{W_n^{[C]}}, the sequence its proof on p.119 builds the renovating
events for. The page prints {W_n^{[0]}} in the conclusion, and that version is false. Corollary
2.5.1 uses the renovating condition of (2.5.14), W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}), where the
page prints W_n.ℝ^K-valued random initial condition Y, under the book's linear lower bound
E[X_n^{[0]}] > −Cn.T_0 = 0,
T_n ∘ θ = T_{n+1} − T_1, ξ_n ∘ θ = ξ_{n+1}, E⁰τ_n = λ^{-1}, E⁰Z_n < ∞. The map X
satisfies (2.11.16) (it depends only on the points and marks in the index window) and the four
framework assumptions for every point process. γ(0) is the a.s. limit of
Z_{[-n,-1]}(0·N)/n. Dropping the marks would reduce the theorem to deterministic service,
and dropping the link between the points and θ makes the second implication false. Neither
is done.≥ 1 and > 1 left
open.Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds a calculus for stationary queues. Chapter 2 asks the prior question: when is there a stationary queue at all?
The G/G/1/∞ queue is one server at unit rate, infinite waiting room, fed by a stationary marked
point process {(T_n, σ_n)} — arrival epochs and required service times. Its workload W(t), the
service still owed by the server, obeys Lindley's equation between arrivals:
W(t) = (W(T_n−) + σ_n − (t − T_n))⁺, t ∈ [T_n, T_{n+1}). (2.1.6)
Nothing in that equation says a solution exists on the whole line, let alone a stationary one. The
answer is a sharp criterion in the traffic intensity ρ = λE⁰_A[σ_0].
Theorem 2.1.1 (p.80), which the book calls "the fundamental result of stability". Under
ρ < 1 there is a unique finite workload process on all of ℝ, compatible with the flow, and
it is given explicitly by the Loynes supremum
W(0) = sup_{n ≤ 0} ( T_n + Σ_{i=n}^{0} σ_i )⁺ , (2.1.12)
with W(T_n−) = 0 for infinitely many negative and infinitely many positive n (2.1.13). If
ρ > 1 there is no finite stationary workload process at all.
Each half earns its place. The supremum is what "the Loynes construction" means: look back from the
origin, take the work brought by customers n, …, 0 less the time −T_n since elapsed, and
maximise over how far back you look. The ρ > 1 half is what turns ρ < 1 from a sufficient
condition into a criterion. The critical case ρ = 1 is an explicit non-result in the book — there
"may or may not" be a stationary workload — and is deliberately absent from the statement.
§2.2 proves the theorem by Loynes' monotone scheme on the Palm space, and two of its steps are worth stating in their own right.
Lemma 2.2.1 (p.87) is the uniqueness engine: a non-negative, a.s. finite Z with
Z − Z∘θ ∈ L¹(P⁰) has E⁰[Z − Z∘θ] = 0. Applied to the difference of two stationary solutions, it
forces that difference to be invariant, and ergodicity then forces it to be zero.
Theorem 2.2.1 (p.90) runs the argument backwards. Its section is titled "Queueing Proof of the Ergodic Theorem", and it is exactly that: the queueing construction yields the pointwise ergodic theorem, in the ratio form
lim_n ( Σ_{i=0}^n σ∘θ^{-i} ) / ( Σ_{i=0}^n τ∘θ^{-i} ) = E⁰[σ]/E⁰[τ], P⁰-a.s.
Mathlib has the mean (von Neumann) ergodic theorem and no pointwise one, so this is absent substrate rather than a restatement.
The multiserver queue (§2.3). With s servers and the least-loaded-server rule, the state is
the ordered workload vector obeying the Kiefer–Wolfowitz recurrence, and the criterion becomes
E⁰[σ] < s E⁰[τ] (Theorem 2.3.1, p.93). Here uniqueness fails: p.94 exhibits a two-point space
with a whole interval of stationary solutions. What survives is that the solution set is bracketed
— M_∞ is minimal, and V^∞_∞ is the largest finite solution (Theorem 2.3.2, p.95).
Coupling (§2.4). Theorem 2.4.1 (p.99) is what "reaches the stationary regime" means: if a
sequence couples with a θ-compatible one, then the law of its whole shifted trajectory converges
in variation to the stationary trajectory's. The proof is one inequality,
|P̃_{X,k} − P̃_{Z,k}| ≤ P(N > k), and the finiteness of the coupling time.
The fluid queue (§2.7). Theorem 2.7.1 (p.131) replaces customers by two θ_t-compatible
random measures, the arrivals A and the service capacity C, and recovers the Loynes supremum
W(t) = sup_{u ≤ t}(A_{u,t} − C_{u,t}) under λ < µ — as the minimal solution, the book
claiming no uniqueness here.
ρ = λE⁰_A[σ_0] takes values in [0, ∞], so an input with E⁰_A[σ_0] = ∞ has ρ = ∞ and
falls under the non-existence half rather than being read as ρ = 0.E⁰[σ]/E⁰[τ] of Theorem
2.2.1, the threshold s E⁰[τ] of Theorem 2.3.1, and the fluid supremum (2.7.7).θ_t-compatible workload processes; maximality
in Theorem 2.3.2 is among measurable finite solutions; the coupling time of Theorem 2.4.1 is a
random variable. A formalization that dropped the explicit supremum, or the ρ > 1 half, would
trivialize the goal and is ruled out.None of it is on the platform or in Mathlib. The nearest platform item,
single_server_queueing_convergence_of_subcritical, presupposes a stationary workload and proves
two-time finite-dimensional convergence to it; Theorem 2.1.1 constructs that workload, proves it
unique, gives it in closed form, and adds the non-existence half. Different conclusion, different
generality, different Mathlib revision.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory has two halves. The first builds
Palm calculus from the Matthes definition of P⁰_N and reaches the Swiss army formula. This
mission is the second: §§1.6, 1.8 and 1.9, which supply the two things the rest of the book runs
on.
§1.6 states, in its own words, "the ergodic theory results to be used later in this book". Five of them, and the book proves none: Birkhoff's pointwise ergodic theorem in discrete (Theorem 1.6.1) and continuous time (Theorem 1.6.4), Kingman's sub-additive ergodic theorem (Theorem 1.6.2), and the extremal characterizations of ergodicity in both settings (Theorems 1.6.3 and 1.6.5) — ergodicity is exactly the impossibility of splitting an invariant probability into two distinct ones.
They are quoted, but they are not decoration. Kingman's theorem is what produces the asymptotic
growth rates of Theorem 2.11.2 and the constant γ(c) on which the saturation rule rests.
Birkhoff's theorem is what makes the time average in PASTA's (3.3.2) a well-defined object, and
what the fluid Loynes theorem invokes for lim_{u→−∞}(A_{u,0} − C_{u,0}) = −∞.
None of the three analytic ones exists in Mathlib. Analysis/InnerProductSpace/MeanErgodic is the
mean (von Neumann, L²) theorem, not almost-everywhere convergence, and there is no sub-additive
ergodic theorem at all. The platform has neither.
§1.8 introduces the stochastic intensity: a point process N admits the (P, F_t)-intensity
{λ(t)} when E[N(a,b] 1_A] = E[(∫_a^b λ(t)dt) 1_A] for A ∈ F_a. Around it sits the notion of a
predictable process — one measurable with respect to the strict past.
Theorem 1.8.1 is the structural fact that makes predictability usable. For the internal history of a marked point process, every predictable process has the concrete form
Z(t, ω) = v(t, θ_t ω), v(t, ·) F_{0−}-measurable. (1.8.1)
That is why mission IV can take this form as PASTA's hypothesis rather than constructing a predictable σ-field: Theorem 1.8.1 says nothing is lost.
Theorem 1.8.2 (p.61), §1.8.4, Watanabe's characterization of Poisson processes. For a
history F_t = F_t^N ∨ G and a G-measurable, locally integrable {λ(t)}, if N admits the
F_t-intensity {λ(t)} then N is a G-conditional Poisson process:
E[ e^{iuN(a,b]} | G ∨ F^N_a ] = exp{ (e^{iu} − 1) ∫_a^b λ(t) dt } . (1.8.12)
A stochastic intensity that carries no information beyond G forces the process to be Poisson
conditionally on G, with the compensator as the parameter — and the conditional characteristic
function is the exact Poisson one, not an approximation. With G trivial and λ constant this is
the ordinary Poisson process, which is the equivalence Remark 3.3.1 of Chapter 3 invokes to explain
the name PASTA. The book: "This result plays a role in queueing theory, especially for proving
that some streams in a queueing network are or are not Poissonian."
§1.9 asks whether the stochastic intensity is the same under P and under P⁰_N — whether the
two probabilities describe the same dynamics. Theorem 1.9.1 says yes, on ℝ₊: the same process
{λ(t)} serves both.
Theorem 1.9.2 is Papangelou's theorem, and it is the deepest statement of the section: N
admits a stochastic intensity if and only if P⁰_N ≪ P on F_{0−}, and then
λ(t) = (μ ∘ θ_t)λ with μ the Radon–Nikodým derivative. A dynamic property and a static one turn
out to be the same thing.
Theorem 1.9.3 is Mecke's characterization: N is Poisson exactly when P ≡ P⁰_N on
F_{0−}. The view from a point of the process and the view from a deterministic instant agree on
the strict past precisely when the process has no memory. It follows in one line from the two
theorems before it.
Four of the five missions in this series import the Chapter 1 substrate; this one adds the two pieces they need from its second half — ergodic theory and the stochastic intensity. Nothing here is on the platform, and Mathlib has filtrations and adapted processes but no predictability in this form, no stochastic intensity, no pointwise ergodic theorem and no Kingman.
Every result is stated in the book's strength, with the book's standing definitions as binders.
A discrete flow is a bijective, measurable, P⁰-preserving map (p.46); a continuous flow is jointly
measurable in (t, ω) (p.3, clause (a)). A history compatible with the flow satisfies
θ_t F_s = F_{s−t} (p.57), and an F_t-intensity is a non-negative, measurable, locally
integrable, adapted process (p.58). The limits of Theorems 1.6.1, 1.6.2 and 1.6.4 are asserted to
exist; Kingman's constant h̄ lies in ℝ ∪ {−∞} and is identified with
inf_n (1/n) E⁰[h_n], the means being extended reals so that E⁰[h_n] = −∞ is not read as 0.
Theorems 1.6.3, 1.6.5, 1.9.2 and 1.9.3 are equivalences, and Theorem 1.9.2 carries the closed form
λ(t) = (μ ∘ θ_t)λ with μ = dP⁰_N/dP on F_{0−}. The goal's conclusion is the exact conditional
characteristic function (1.8.12); a formalization that only asserted some conditional Poisson law,
or conditioned on G alone, would not be this theorem.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds the calculus that the rest
of the book runs on. Its subject is the relation between two ways of looking at the same stationary
system: from a clock fixed in time, and from a customer arriving into it. The two are not the same
— the interval a random instant falls into is longer than a typical interval, a fact every
queueing student meets as the inspection paradox — and the object that makes the difference precise
is the Palm probability P⁰_N.
The chapter defines P⁰_N by the Matthes definition in terms of counting,
λ t P⁰_N(A) = E[ Σ_{n ∈ ℤ} 1_A(θ_{T_n}) 1_{(0,t]}(T_n) ], (1.2.1)
and everything else is a theorem about it. That ordering is deliberate here too: P⁰_N is carried
in the formalization as a predicate satisfying (1.2.1), not as a measure constructed to make
Mecke's formula true. If it were the latter, Mecke's formula would be a definition and the
inversion formula and the goal theorem would inherit that emptiness.
From (1.2.1) the chapter derives, in order: that P⁰_N is invariant under the point shift
(1.2.16); Mecke's formula (1.2.17), which the literature also knows as the generalized Campbell
formula; the inversion formula of Ryll-Nardzewski and Slivnyak (1.2.25), which runs back from
P⁰_N to P; the mean-value formulas (1.3.2)–(1.3.3); the Neveu exchange formula (1.3.4),
which relates two point processes stationary for the same flow; and the Miyazawa rate
conservation principle (1.3.10), which balances the drift of a process between its jumps against
the rate at which it jumps.
§1.3.7 then collects all of them into one identity. Its name is the book's own:
Depending on which blade is selected, a Swiss army knife transforms itself into various useful tools. The formula obtained in this subsection is called the Swiss army formula of Palm calculus because it contains the main formulas of this theory, as well as some new ones.
Theorem 1.3.1 (p.29). For arrivals {T_n} with counting measure A and intensity λ_A,
departures {τ_n} with counting measure D — not assumed ordered — sojourn times
W_n = τ_n − T_n ≥ 0 forming a sequence of marks of A, the number in system {X(t)} with
X(b) − X(a) = A((a,b]) − D((a,b]), a non-decreasing corlol integrator {B(t)} and a non-negative
process {Z(t)}, all compatible with a measurable flow under which P is invariant:
λ_A E⁰_A [ ∫_(0,W_0] Z(s) dB(s) ] = (1/t) E [ ∫_(0,t] X(s−) Z(s) dB(s) ]. (1.3.28)
Selecting the blade Z ≡ 1, B(t) = t turns it into λ_A E⁰_A[W_0] = E[X(0)] — Little's law,
here in its full stationary-ergodic form rather than as a deterministic sample-path identity. Other
choices give the inversion formula, the Miyazawa conservation principle and the rate conservation
law.
P⁰_NOne milestone stands slightly apart. Theorem 1.5.1 (p.45) is what licenses the whole reading of
P⁰_N as "what an arriving customer sees":
lim_{t→0} sup_{A ∈ F} | P⁰_N(A) − P(θ_{T_1} ∈ A | T_1 ≤ t) | = 0. (1.5.3)
The supremum is inside the limit. The convergence is uniform over every measurable event, which is what Dobrushin's estimate of §1.5.1 buys and what a pointwise limit would not give.
Nothing in this chapter exists on the platform or in Mathlib: not stationary marked point processes, not Palm probability, not the Campbell measure. Four of the five missions in this series import the vocabulary built here, and the two definition items — the substrate of §§1.1–1.2 and the setting of §1.3.7 — are as much of the deliverable as the theorems are.
{θ_t} is a one-parameter group with (t, ω) ↦ θ_t ω jointly measurable (p.5 (a)); a
point process is its strictly increasing points {T_n}_{n ∈ ℤ} with T_0 ≤ 0 < T_1, infinitely
many on each side (Hypothesis 1.1.1), with finite non-null intensity λ = E[N((0,1])].P⁰_N is characterized by (1.2.1) for every t > 0, which determines it uniquely; nothing is
axiomatized. A formalization that introduced P⁰_N as any measure satisfying Mecke's formula
would make the milestones and the goal trivial and is ruled out.[0, ∞] with lower Lebesgue integrals, for all such functions, not only bounded
or integrable ones.{B(t)} is θ_t-compatible (the proof uses it, and without it the identity fails);
it is stated for t > 0, the only values at which 1/t and (0, t] give it content; and the
Miyazawa principle assumes Y'(0) ∈ L¹(P), which its E[Y'(0)] presupposes.δ for every A).Anosov flows are the model of uniformly hyperbolic, chaotic continuous-time dynamics: a nonsingular vector field on a closed manifold is Anosov when the tangent bundle splits as , with uniformly contracted and uniformly expanded by the derivative of the flow. They are structurally stable, so one can hope to classify them up to topological equivalence. In dimension three this classification is far from complete: it is not known which closed 3-manifolds carry Anosov flows, nor how many inequivalent Anosov flows a given manifold can carry.
The classical examples — suspensions of hyperbolic toral automorphisms and geodesic flows of hyperbolic surfaces — are rigid (Plante; Ghys). Non-algebraic examples were built by Franks–Williams (a nontransitive Anosov flow, 1980), Handel–Thurston, Goodman, Fried, Bonatti–Langevin, Fenley, Barbot and others. Several of these examples glue together neighbourhoods of hyperbolic sets along their boundaries. Béguin, Bonatti and Yu (Geom. Topol. 21 (2017)) turned this into a general theory, and used it to answer questions of Katok and of Barbot–Fenley.
A plug is a compact 3-manifold with boundary and a nonsingular C¹ vector field transverse to . The boundary splits into the entrance boundary (where points inwards) and the exit boundary . The maximal invariant set consists of the points whose orbit stays in for all times. The plug is hyperbolic if is a hyperbolic set with one-dimensional strong stable and strong unstable bundles. The entrance lamination and the exit lamination are one-dimensional laminations of the boundary surfaces. The plug has filling MS laminations when every component of (and of ) is a strip: a disc whose accessible boundary consists of two leaves asymptotic to each other at both ends.
A diffeomorphism is a strongly transverse gluing map if and are transverse and cut into squares with sides alternately on leaves of the two laminations. Gluing then gives a closed manifold with an induced vector field . Two triples and are strongly isotopic if they are joined by a continuous path of such data.
Theorem 1.5 lets one build Anosov flows on closed 3-manifolds by gluing hyperbolic plugs. Proposition 1.6 gives a combinatorial criterion for the result to be transitive. Together they answer a question of Katok (Theorem 1.9) and questions of Barbot and Fenley on manifolds with several hyperbolic JSJ pieces supporting transitive Anosov flows (Theorem 1.13). They also show that transitive Anosov flows admit no fully canonical decomposition into finitely many transverse tori (Theorem 1.15). The results are proved in the source paper. None of them is formalized, and Mathlib has no theory of hyperbolic sets for flows, stable manifolds or laminations. A formal proof therefore needs a substantial amount of reusable smooth dynamics.
The glued vector field is generally not hyperbolic: perturbing the gluing map can create solid tori of parallel periodic orbits. The difficulty is to choose the gluing map (and the vector field within its topological equivalence class) so that cone fields on are mapped into themselves by the return map. The return map is the composition of the crossing map of the plug with the gluing map. Contraction and expansion must therefore be controlled simultaneously along two transverse invariant foliations. The paper achieves this after reducing to plugs with an affine Markov partition. The naive approach — fixing and trying to verify hyperbolicity — fails in general (Question 1.4 of the paper remains open).
EuclideanHalfSpace 3 with a structure; closed manifolds are compact, Hausdorff and BoundarylessManifold, and connected where the paper's statements concern a single manifold. Orientability is given by an atlas with positive Jacobians.flowMap X t x is when the orbit is undefined.Minimum-cost network flow problems are the largest special class of linear programs met in practice: transportation, distribution, assignment, communication and electric networks, facility location and financial planning all reduce to moving material along the arcs of a directed network from supply nodes to demand nodes at least cost. Chapter 14 of R. J. Vanderbei's Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) develops the network simplex method, and closes with two structural facts that explain why this class is special: simplex bases are spanning trees of the network, and a network problem with integer supplies has integer basic solutions. Vanderbei then uses integrality to prove a classical theorem of combinatorics, König's theorem on regular bipartite graphs. Chapter 15, §5 treats the maximum-flow problem on the same objects and proves the Max-Flow Min-Cut Theorem.
The combinatorial results are older than linear programming. D. König proved in 1916 that every regular bipartite graph has a perfect matching (Math. Ann. 77). The Max-Flow Min-Cut Theorem is due to Ford and Fulkerson (1956, Canad. J. Math. 8) and, independently, Elias, Feinstein and Shannon (1956). The integrality of network bases is the total unimodularity of incidence matrices, known since the 1950s (Hoffman and Kruskal, 1956).
A network has a finite set of nodes and a set of directed arcs . Node carries a supply (negative values are demands) with , and arc carries a cost . The flow on arc is the decision variable. The node–arc incidence matrix has in the column of an entry in row , in row , and elsewhere. The network flow problem (14.1) is
A flow satisfying is balanced; a balanced flow with is feasible. Paths ignore arc directions; the network is connected if every two nodes are joined by a path, which is assumed throughout Chapter 14. A spanning tree is a set of arcs that, on all of and without directions, is connected and has no cycle. Fixing a root node and deleting its row gives the matrix . A set of arcs is a basis if its columns form an invertible square submatrix of , and a basic feasible solution is a feasible flow vanishing off some basis.
For maximum flow, a source , a sink and finite upper bounds are given; all and an extra arc of infinite capacity is added. A feasible flow satisfies , and flow balance. A cut is a node set with , , and its capacity is .
If girls and boys are such that every girl knows exactly boys and every boy knows exactly girls (knowing being symmetric), then there is a bijection from girls to boys with
both extrema attained.
The goal is independent of the network definitions in its statement; the milestones are the book's route to it (14.1, 14.2) and the chapter's other duality theorem on the same objects (15.8, 15.1).
König's theorem is the base case of matching theory: it gives perfect matchings in regular bipartite graphs, hence edge colourings of bipartite graphs with colours, and via Birkhoff–von Neumann-type arguments the decomposition of doubly stochastic matrices. The Integrality Theorem is the reason assignment, transportation and shortest-path problems can be solved as linear programs without an integrality constraint. Theorem 14.1 is the correspondence the network simplex method is built on. Max-Flow Min-Cut is the prototype of combinatorial min–max theorems.
All four theorems are classical and proved. This mission adds machine-checked versions in the book's own formulation: the incidence matrix with Vanderbei's sign convention , bases as square submatrices of with a chosen root, and maximum flow as a circulation through an added return arc. The platform already has network integrality, a tree-solution characterisation and max-flow min-cut in the Bertsimas–Tsitsiklis formulation and a Keller–Trotter max-flow statement; none is stated in this form, and Mathlib has Hall's marriage theorem but no regular-bipartite corollary.
The combinatorial content is small; the difficulty is in the passage between matrices and graphs. Theorem 14.1 needs both directions: the book shows that a spanning tree gives a triangularisable, hence invertible, submatrix and leaves the converse (independent columns form a spanning tree) as an exercise, which requires showing that any cycle, including a pair of antiparallel arcs, yields a linearly dependent set of columns and that acyclic arcs span. The book's proof of König's theorem applies the Integrality Theorem to the girl–boy network, which need not be connected, while Chapter 14 assumes connectedness throughout: the statement of 14.2 does not apply to it verbatim. The step "a feasible problem has a basic optimal solution" is also used and is not stated in the chapter.
Fintype with decidable equality; arcs are a Finset (N × N), so parallel arcs are excluded as in the book, and IsNetwork excludes loops. Flows are real functions on ordered pairs; only their values on arcs matter.Fin n, knowing is one relation between girls and boys, and is a hypothesis: the book's proof divides by , and for the claim is false. No connectedness is assumed.A formalization of the goal as a matching of size in some larger graph, or with the degree conditions on one side only, would be a different theorem; the conclusion is a bijection between exactly the girls and the boys using only acquainted pairs.
Useful infrastructure, reusable beyond this mission: the incidence matrix and its total unimodularity, the undirected graph of an arc set. Proofs of König's theorem through Hall's theorem (Mathlib Finset.all_card_le_biUnion_card_iff_exists_injective) are welcome alongside the book's route.
Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set and redistribute the probability of leaving back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.
A Markov chain with costs on a denumerable state space has transition probabilities with and a finite nonnegative cost at each state. For a set and a start , is the first passage time to . The taboo probability is the probability of moving from to in steps with no intermediate state in . The expected visits count the visits to at times . The mean first passage time is , infinite when is missed with positive probability. The first passage cost is . A state is positive recurrent when , and the steady state probability is . On a positive recurrent class the average cost is . The chain is standard when and for every . Such a chain has one positive recurrent class with , and every other state is transient.
An approximating sequence (AS) consists of increasing nonempty finite sets with and, for each , a chain on with the same costs and transition probabilities . The quantities of are written , , and . An AS is conforming (for a standard ) if, for large , is unichain with in its positive recurrent class, and and for all . It is conforming on if and on .
An augmentation type approximating sequence (ATAS) keeps the original probabilities inside and redistributes the probability of each excluded target according to an augmentation distribution on :
It sends excess probability to if every is concentrated on .
For a standard chain and a finite nonempty ,
and if it is also conforming on . No rate of convergence and no constants are involved, and need not contain .
The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple with . First passage costs can converge to the wrong value even when the steady state probabilities converge.
Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between bounds and limits in explicit, and produces a reusable library of first passage quantities for countable chains.
The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in , a first passage that leaves is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: may have several recurrent classes, or a recurrent class not containing , and ruling this out is part of the conclusion rather than an assumption.
The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, , , and are defined as sums in . is infinite whenever is missed with positive probability. The average cost is the of the Cesàro cost averages.
An AS is a structure carrying , the finite sets (as Finset S) and . is built as an MC on the subtype of , and a set is read in as . Quantities of are lifted to functions of and of states of with the value where they are undefined ( or a state outside ). For fixed states this affects finitely many , and all statements are limits, s or eventual equalities. All convergence is in . The conformity predicate includes the standing assumption that is standard. The positive recurrent class of a standard chain is the communicating class of .
A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class excludes , is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce exactly by (C.27).
A complete development needs first passage decompositions for countable chains, the renewal-reward identity , and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.
Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.
Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the -person game becomes unmanageable as grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.
The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition ; and every splitting set is a union of blocks of . The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.
Let be a finite set of players. A characteristic function is a real number for every subset (every coalition, including the empty set and ). Write . From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying
For with complement , the game is decomposable with respect to and if there are constant-sum games on the players and on the players with for all — formula (41:3). The -constituent is the game on with for (41:4).
A splitting set (43.1) is a satisfying (41:6),
The game is indecomposable if and are its only splitting sets (43.3.1). A minimal splitting set is a splitting set none of whose proper subsets is splitting (43.3.2), and is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. for all , for some reals (the transformation (42:5)).
For every satisfying (42:6:a)–(42:6:c):
The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that is a partition.
In attack order: the criterion (42:G) (decomposability (41:6) (41:7)); the closure properties (43:A) (complements), (43:B) (, ), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ( splits iff every block of lies inside or outside ); and the two extreme cases (43:J) ( = all singletons iff the game is inessential) and (43:K) ( iff the game is indecomposable).
The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of . The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.
The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.
The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that is splitting one cannot simply add the identities (41:6) for and for , since a pair , is not of the form those identities control, and may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of (players of the constituent) and subsets of .
ι with decidable equality (the book's ; in Chapter IX players are also named ). Coalitions are Finset ι, and are the complement Sᶜ in , and is a function Finset ι → ℝ.IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes nonempty ([Nonempty ι], the book's ); every other statement holds without it. (43:E) assumes , since the book's constituent is a game and has at least one player.↥J, ↥Jᶜ; the -constituent is restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives .Finset ι and their atoms, which would shorten (43:F)–(43:H).Hadwiger's conjecture (1943) asserts that for every integer , every graph with no minor is -colourable. It is a far-reaching strengthening of the four-colour theorem, and it is widely described as one of the central open problems of graph theory (Bollobás, Catlin and Erdős called it "one of the deepest unsolved problems in graph theory"). The interest is structural: the four-colour theorem concerns planar graphs, and Hadwiger's conjecture proposes that the only obstruction to -colourability that matters is the presence of a complete graph as a minor.
Timeline.
The case (graphs with no minor are -colourable) is the first open case.
All graphs are finite and simple. A minor of a graph is any graph obtained from a subgraph of by contracting edges. Equivalently, a graph on vertex set is a minor of if there are branch sets , , which are pairwise disjoint, each inducing a connected (nonempty) subgraph of , and such that for every edge of some vertex of is adjacent to some vertex of . has a minor if the complete graph is a minor of , i.e. contains pairwise disjoint connected vertex sets, every two joined by an edge.
A graph is -colourable if its vertices can be coloured with colours so that adjacent vertices receive different colours; is the least such . Write for the statement "every graph with no minor is -colourable". A graph is -degenerate if every nonempty set of vertices contains a vertex with at most neighbours inside the set. The stability number is the largest size of a set of pairwise non-adjacent vertices.
A proof of the conjecture would give a structural explanation of the four-colour theorem that does not depend on planarity, and would settle the chromatic number of every minor-closed class defined by excluding a single complete graph. Partial results already drive the theory of graph minors: bounds on the average degree of -minor-free graphs are the standard input to colouring, and linear Hadwiger-type bounds are used in structural and algorithmic graph theory.
On the formal side, only the smallest cases have Lean proofs: the platform already contains proofs of the cases under a different encoding of minors (namespace Hadwiger), which may be reused after bridging the definitions. The cases , Wagner's bound, the degeneracy lemma, the small extremal bounds and the Duchet–Meyniel theorem have elementary proofs and are realistic targets. The cases depend on the four-colour theorem, whose formal proof exists in Coq but not in Lean; formalizing them here requires either porting that proof or proving the reduction to it. The general conjecture is open.
The natural approach — contracting the colour classes of an optimal colouring — does not produce a minor, because colour classes are independent sets and contraction is only allowed along edges. Degeneracy arguments only give bounds of order , since dense random graphs with no large clique minor have average degree of that order; closing the gap to requires using large chromatic number itself, not just density. Already for the statement is equivalent to the four-colour theorem, so no short proof is expected for any .
Graphs are SimpleGraph V on a finite vertex type V : Type. Minors are encoded by branch sets (IsMinor), complete minors by HasCompleteMinor G t (the complete graph on Fin t is a minor of G), colourability by Mathlib's SimpleGraph.Colorable, and edge counts by the cardinality of the edge set. is the definition HC t. Logarithms are natural logarithms; asymptotic bounds are stated with an explicit existential constant and a ceiling. The case is included; HasCompleteMinor G 0 holds for every graph, so no statement becomes vacuous through a degenerate minor definition.
Useful reusable infrastructure: minor models and their composition, contraction of connected sets, greedy colouring of degenerate graphs, and edge-counting for minor-free graphs. Contributions of intermediate lemmas along the milestones are welcome.
Consider the classical error-correcting problem. An input vector (the plaintext) is encoded as by a coding matrix with , and an unknown, arbitrary vector of errors corrupts the result, so that only is observed. Can be recovered exactly, and by an algorithm whose running time is polynomial in ? Candès and Tao (2005) answer both questions at once: if a matrix annihilating satisfies a restricted orthonormality condition, then is the unique solution of the convex program , which is a linear program, whenever at most entries of are corrupted, whatever their positions and values. Read for the matrix alone, the same theorem says that minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.
Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of and minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order , through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order . Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, , valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition , sharpened the sufficient condition; those later results are not part of this mission.
Let be a real matrix with columns , and let be the linear span of these columns. For an index set and real coefficients , write . A vector is supported on when for all ; with this convention is just the product . Norms are the Euclidean norm and the norm .
Definition 1.1. For an integer , the -restricted isometry constant is the smallest quantity such that
for all of cardinality at most and all real coefficients . The -restricted orthogonality constant is the smallest quantity such that
for all disjoint with and . The paper writes for . These numbers measure how far the columns of are from an orthonormal system when only linear combinations of at most columns are considered.
The two optimization problems are
A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.
Let be a real matrix of full rank with , and a real matrix with . Let satisfy
If where is supported on a set of size at most , then is the unique minimizer of .
Let satisfy (1.10) for , and let be supported on a set with . Then is the unique minimizer of with .
Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the numbers control the numbers), Lemma 1.3 (uniqueness of sparse representations under ), and the two dual sparse reconstruction properties, Lemma 2.1 ( version) and Lemma 2.2 ( version).
The result. The guarantee is deterministic and uniform: one condition on , checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of , and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.
Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of and exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.
The whole proof rests on a dual certificate: a vector with for and for . Given such a , the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is ; this interpolates the signs on and, by restricted orthogonality, its inner products off are small in an sense, but not in the sense required. That is exactly Lemma 2.1: the bound holds only outside an exceptional set of at most indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on fixed, and summing a geometrically convergent series.
Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to () at each step, while the per-step factors it quotes, , are what Lemma 2.1 gives for a set of size ; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with in its bound on the exceptional set, while the inequality (2.3) its proof establishes gives ; the mission states the lemma with , which coincides with the printed form in the case used by Lemma 2.2.
Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on is a vector in Fin m → ℝ supported on the finite set , and is F.mulVec c. The Euclidean and norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. is the span of the columns.
The constants and are the infimum of the set of nonnegative (resp. ) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as . The definitions are total in , and each theorem carries the paper's domain conditions (, and , or as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has , so none of the statements is vacuous.
"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the matrix with is injectivity of ; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant depending only on " is a positive function of the real number , quantified before all other data.
Out of scope, with the reason for each: Theorem 1.6 refers to a threshold "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for and "large enough", with an unspecified threshold and an term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.
Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix and its inverse under , and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to ) belong to a separate mission.
Given a monic polynomial with integer coefficients, one can reduce it modulo each prime and factor it over the finite field . The way factors changes with , and the question of how often each factorization pattern occurs has a precise answer: Chebotarëv's density theorem (1922). It is the common generalization of Dirichlet's theorem on primes in arithmetic progressions (1837) and a theorem of Frobenius (1880, published 1896), and it underlies a large part of algebraic number theory, for example the fact that a Galois extension of a number field is determined by the set of primes that split completely in it. This mission follows the elementary exposition of P. Stevenhagen and H. W. Lenstra, Jr. (Math. Intelligencer 18 (1996)), which states all three theorems over with a minimum of terminology.
Timeline.
Let be monic of degree with nonzero discriminant , so that has distinct complex zeros . Let be its splitting field and its Galois group. Every permutes the zeros; the lengths of the cycles (including cycles of length 1) form the cycle pattern of , a partition of .
For a prime , the degrees of the irreducible factors of over form the decomposition type of modulo , again a partition of .
A Frobenius substitution of is an element such that, for some prime ideal of the ring of integers lying over ,
For these elements form a single conjugacy class of , written .
A set of primes has (analytic, or Dirichlet) density if
and natural density if as .
For every conjugacy class of ,
Chebotarëv's theorem shows that every conjugacy class of the Galois group occurs as a Frobenius class for infinitely many primes, with a predictable frequency. Its standard consequences include: the Frobenius elements are equidistributed; a Galois extension is determined by its completely split primes; if has a zero modulo almost every prime then is linear or reducible; prime ideals are equidistributed over ideal classes. The theorem is the first step in many arguments in arithmetic geometry (e.g. Serre's work on -adic representations).
The theorem is classical and proved; this mission is about formalizing it. Mathlib contains Frobenius elements in Galois extensions of Dedekind domains and Dirichlet's theorem in the form "infinitely many primes in each coprime residue class", but, to our knowledge, neither the density form of Dirichlet's theorem nor Frobenius's or Chebotarëv's density theorem.
The Galois-theoretic parts (milestones 3–6) are standard but require connecting Frobenius elements in with factorization of modulo , including the fact that forces to be unramified in . The analytic core is harder: one needs Dedekind zeta functions and -functions of number fields and their behaviour at . The reduction of the general case to the cyclotomic case (Chebotarëv's "crossing" with cyclotomic extensions) needs the density statement over an arbitrary number field as base, not only over ; in particular, the statement over alone cannot be proved by induction on itself.
All declarations live in the namespace ChebotarevDensity and share one definition file.
SplittingField of viewed in ; is Polynomial.Gal; is Mathlib's Polynomial.discr.IsArithFrobAt at some prime ideal of containing ; "" means that some Frobenius substitution of lies in (for this is equivalent to all of them lying in , by milestone 4).Equiv.Perm.partition of the permutation induced on the complex zeros of ; it includes fixed points.Welcome contributions: Dedekind zeta functions and Hecke -functions at , the density form of Dirichlet's theorem, unramifiedness of primes not dividing the discriminant, and the general number-field version of the theorem.
A classical way to recognize an algebraic function is through the arithmetic of its Taylor coefficients. Eisenstein's theorem (1852) says that if a power series is algebraic over , only finitely many primes occur in the denominators of its coefficients. The converse fails in general: many transcendental power series have integer coefficients. Lam and Litt (arXiv:2501.13175) conjecture that the converse does hold for power series that solve an algebraic differential equation at a non-singular point, and that even a weak control on denominators — primes may appear, but only after roughly coefficients — already forces algebraicity.
For linear differential equations, the conjecture is a strengthening of the Grothendieck–Katz -curvature conjecture, one of the central open problems about algebraic solutions of linear differential equations (arXiv:2501.13175). The bounded-denominator form is Problem 1 on Litt's list of open problems (problemsilike.com/1).
Timeline.
Let be a formal power series with rational coefficients and write for its -th formal derivative. Let be a rational function in variables. The series solves the algebraic ODE defined by if
and is defined at . Concretely, for polynomials with and .
For , is the subring generated by . For a function from the primes to , the coefficients of are -integral if for every prime the numbers lie in (denominators prime to ); is superlinear if .
For solving an algebraic ODE as above, the following are equivalent:
Together the four milestones imply the goal; the last two are the open content of the conjecture.
A proof would give an arithmetic criterion for algebraicity of solutions of arbitrary algebraic differential equations, and, for linear equations, would imply the Grothendieck–Katz -curvature conjecture (arXiv:2501.13175). Lam and Litt draw algebro-geometric consequences from the cases they prove.
For formalization: the conjecture is open, so the goal and the two open milestones are research targets. Eisenstein's theorem is a classical result; formalizing it is concrete, self-contained work. The implication (2)⇒(3) is elementary. The cases proved by Lam and Litt are candidates for further milestones.
Integrality of coefficients alone does not detect algebraicity: there are transcendental power series with integer coefficients that satisfy linear differential equations, such as . Its equation is singular at , which the non-singularity hypothesis on excludes; the conjecture asserts that at non-singular points such examples cannot occur. Even for linear equations the statement contains the Grothendieck–Katz conjecture, which is open in general.
PowerSeries ℚ with the formal derivative; rational functions are the fraction field of MvPolynomial (Fin (n + 1)) ℚ, where variable 0 is and variable i + 1 is .IsAlgebraic (Polynomial ℚ) f, i.e. over (equivalently over ).List.TFAE of the three conditions.Useful infrastructure: formal derivatives and substitution for power series, algebraic power series and their coefficient arithmetic (Eisenstein), and -adic valuations of coefficients. Formalizations of Eisenstein's theorem and of the special cases proved by Lam and Litt are welcome.
FormalConjectures/LittProblems/1.lean. https://github.com/google-deepmind/formal-conjecturesIn a Walrasian pure exchange economy, agents trade a fixed stock of commodities, and a price vector is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).
Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.
There are commodities and agents. Prices are vectors , and the paper's implicit summation is written . Agent has an expenditure function (minimal cost of reaching a fixed utility level), and the market weighs agents with constants ; the aggregate expenditure is
The economy controls the price velocity and minimizes the cost functional (eq. (7))
whose value function is . The Hamiltonian (eq. (8)) is
the optimal policy (eq. (9)) is , and the HJB equation (eq. (10)) reads
Here always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent with . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: .
If is and solves the time-reversed HJB equation, and the price path follows the optimal policy , then on any interval on which
the function is strictly decreasing; if moreover , it is strictly positive on .
The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.
Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.
All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption is kept; positivity of and is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. , , with small on a bounded interval), so the goal is not vacuous.
The mean value problem, also called Smale's mean value conjecture, was posed by Stephen Smale in 1981 in his study of the complexity of root-finding algorithms for polynomials (Smale 1981). For a real differentiable function the mean value theorem produces, between two points, a point where the derivative equals a difference quotient. For a complex polynomial no such point need exist on a segment, and Smale asked for a substitute in which the special point is a critical point of the polynomial (a zero of its derivative). Estimates of this kind control how far Newton-type iterations can move, which is where Smale's original interest came from. The problem appears in lists of unsolved problems in mathematics, including Smale's own list of problems for the next century.
No absolute constant is known that works in every degree.
Let be a polynomial with complex coefficients of degree , and write for its derivative. A critical point of is a complex number with ; since , is a nonconstant polynomial of degree , so has at least one and at most distinct critical points. Fix a complex number that is not a critical point, . For every critical point we then have , and the difference quotient
is well defined. The question is how small this quotient can be made, relative to , by choosing the critical point well.
For every complex polynomial of degree and every with there is a critical point of with
The same with replaced by ; the example shows this constant cannot be lowered.
The result itself. A positive answer gives a sharp, degree-independent mean value inequality for complex polynomials: for every non-critical point, some critical value is reachable along a chord whose slope is at most the local derivative. Bounds of this type feed into the analysis of Newton's method and of path-following root finders, and into the study of how critical values of a polynomial are distributed relative to its values. The conjecture is part of a family of open extremal problems on the geometry of critical points, alongside Sendov's conjecture.
Formalizing it. The goal and the optimal-constant form are open. The milestones are published theorems, none of which is known to have a machine-checked proof. Formalizing Smale's bound and Tischler's special cases would put the classical tools of the subject (critical points of polynomials, univalent function estimates, root location) on a formal footing that later attempts can reuse.
The obvious strategies control the quotient through one critical point at a time: for instance, bounding by integrating along the segment from to . Such estimates lose a constant factor that depends on how the critical points are spread out, and the known uniform arguments all pass through distortion theorems for univalent functions, whose constants lead to close to . Reaching requires using all critical points simultaneously, and no argument doing this in every degree is known. The equality case , in which every critical point is equally bad, shows that any successful argument must be sharp for polynomials with maximally symmetric critical configurations.
Polynomials are elements of ℂ[X] (Mathlib's Polynomial ℂ); the degree is natDegree, the derivative is Polynomial.derivative, evaluation is Polynomial.eval, and the roots of are the multiset P.roots (counted with multiplicity). A critical point is a c : ℂ with P.derivative.eval c = 0. The absolute value is the norm ‖·‖ on ℂ, and the constants and are computed in ℝ from the cast of natDegree.
Every statement assumes . This is the standard normalization and is essential in Lean: division by zero returns , so without it the choice would make the inequality trivially true whenever is itself a critical point. With the hypothesis, every critical point differs from and the quotient is a genuine difference quotient.
Crane's bound is stated as the existence, for each degree , of a constant strictly below that works for all polynomials of degree exactly ; this is equivalent to the best constant in degree being strictly below that value.
A complete development needs basic facts on critical points of complex polynomials (existence, the Gauss–Lucas theorem), and, for the classical bounds, results from the theory of univalent functions such as the Koebe quarter theorem and coefficient estimates. These are reusable well beyond this mission. Contributions of any milestone, of supporting lemmas, and of partial results in fixed small degree are welcome.
Linear programming is usually described as "solvable in polynomial time", but that statement is about rational inputs given exactly. In Smale's list of problems for the 21st century (Smale 1998), Problem 9 asks for a polynomial-time algorithm over the reals deciding the feasibility of , and Smale explicitly calls for "models which process approximate inputs and which permit round-off computations". Real data such as , entries of a discrete cosine transform, or even in floating point can only be accessed approximately.
Bastounis, Hansen and Vlačić pose the extended Smale's 9th problem: in a model where the algorithm can only query approximations of the input to any requested accuracy, can one compute minimisers of linear programming, basis pursuit and Lasso to correct digits? Their Main Theorem I (Theorem 3.4) shows that the answer depends on in a sharp way: for a suitable class of well-conditioned, bounded inputs, no algorithm at all (not only no efficient one) produces correct digits, while digits are computable (but not in bounded time) and digits are computable in polynomial time.
This mission targets the first, impossibility, half of Theorem 3.4(i) for linear programming.
Linear program. For , and , the solution set is
It is a subset of with the norm, . An input is a pair , and the evaluations of are its coordinates and entries .
Extended model (-information). Let . An oracle representation of is a family , indexed by evaluations and accuracies , with and . An algorithm must succeed on every oracle representation of every input.
General algorithm. To make impossibility results independent of the machine model, the paper uses general algorithms (Definition 9.3): a map from inputs to ( = no output) together with a nonempty set of evaluations read on . This set is finite whenever halts. The output is determined by the values read, and any input that agrees on those values reads the same set. Turing machines and BSS machines with an oracle are special cases; general algorithms can even solve the halting problem.
Error and breakdown epsilon. The error is , with distance from . The strong breakdown epsilon is the supremum of all such that every general algorithm has error on some input (Definition 9.17).
For every integer , all dimensions and every there is a nonempty class of inputs with nonempty solution sets, and , such that
The theorem shows that for LP with inexact input, being non-computable in Turing's sense does not rule out a finer complexity theory. The paper builds a " / / digits" classification on this. It also explains why established solvers can return wrong answers with a success flag on small, well-conditioned LPs (§4 of the paper), and it bears on computer-assisted proofs that rely on inexact LP, such as the Flyspeck proof of the Kepler conjecture.
The result is proved on paper. As far as the proposer knows, it has not been machine-checked. This mission formalizes the deterministic impossibility part for LP and puts in place reusable infrastructure: general algorithms, breakdown epsilons and -information. That infrastructure is the base for later missions on the randomised parts of Theorem 3.4(i)–(ii), the weak breakdown epsilon (iii), the exit-flag theorem (Theorem 5.1), and basis pursuit and Lasso.
The obvious objection is that LP is in P for rational inputs, so some rounding scheme ought to work. It fails because an algorithm must halt after reading finitely many approximations. Two inputs that agree to that accuracy but have minimisers far apart then receive the same output. Setting this up needs a notion of algorithm strong enough to cover every computational model, a precise -information model in which the adversary controls the approximations, and explicit LP geometry in which an arbitrarily small perturbation of moves the minimiser by a fixed amount.
PiLp p (Fin N → ℝ).run : Ω → Option M (none = NH) and a read set queried, satisfying the axioms (i)–(iii) of Definition 9.3.ℝ≥0∞), and the error of NH is . The infimum over an empty solution set is . The goal also requires nonempty solution sets, so no junk value enters.ℕ+). An oracle input is stored as a pair (input, oracle family), and algorithms can read only the oracle family.This mission formalizes N. Monod, Groups of piecewise projective homeomorphisms, Proceedings of the National Academy of Sciences 110 (2013) 4524–4527, doi:10.1073/pnas.1218426110: the groups of piecewise projective homeomorphisms of the line are non-amenable and have no free subgroups whenever .
The paper opens with the Banach–Tarski paradox and von Neumann's notion of amenability: "Tarski readily proved that amenability is the only obstruction to paradoxical decompositions. However, the known paradoxes relied more prosaically on the existence of non-abelian free subgroups. Therefore, the main open problem in the subject remained for half a century to find non-amenable groups without free subgroups" (p. 1). That problem, the so-called von Neumann conjecture, was answered by Ol'shanskii around 1980, with Tarski monsters. Monod's groups give "straightforward torsion-free counter-examples", "so simple that many additional properties can be established" (p. 1).
Monod's groups are close relatives of Thompson's groups: Thurston's model identifies Thompson's group with piecewise maps of the line with rational breakpoints (p. 2). Whether is amenable is a notorious open problem, and whether is amenable is Monod's Problem 12 (p. 2).
The projective line is OnePoint ℝ, on which acts through by Möbius transformations (mob, using Mathlib's action on OnePoint). For a subring of (A : Subring ℝ; is ⊥, is ⊤), P A is , the set of fixed points of hyperbolic elements (trace of absolute value greater than ).
A homeomorphism of is piecewise in with breakpoints in (IsPiecewiseProjOn A E f) when, off some finite subset of , it agrees near every point with a Möbius transformation from . Monod's (Gpp) is the group generated by the homeomorphisms piecewise in , with breakpoints anywhere, and (Hpp) is its stabilizer of (fixInf). For a subring , (G A) is the subgroup of generated by its elements that are piecewise in with breakpoints in (IsPiecewiseProj A), and (H A) is its stabilizer of ; is H ⊥. GRat is the subgroup of generated by its elements piecewise in with breakpoints in , and HRat its stabilizer of : the rational-breakpoint variants of and (p. 2).
Amenability is Garrido.IsAmenable (a finitely additive left-invariant probability measure on all subsets), and "no non-abelian free subgroup" is Chou.NoFreeSubgroupOfRankTwo; both are published definitions, in the bundles Garrido_Amenability and Chou_Classes. Co-amenable subgroups (IsCoamenable), inner amenability (IsInnerAmenable) and pointwise stabilizers (fixSubgroup), all on p. 3, are defined in the bundle in the same style.
A relation is amenable for a measure (IsAmenableRel μ R, p. 2) when it has a left invariant mean in the sense of Connes–Feldman–Weiss: a positive, unital map from bounded measurable functions on to functions on , linear up to -null sets and invariant under the partial transformations of . volP1 is the Lebesgue measure class on .
The goal is Theorem 1, "The group is non-amenable if " (p. 1), introduced as "the main result of this article". The proof (p. 2) passes to a countable dense subring of , compares the orbits of and on (Proposition 9), and concludes from two facts about measured equivalence relations: the orbit relation of an amenable group's action is amenable, and, by a theorem of Carrière and Ghys, the orbit relation of on is not.
The milestones are, in the paper's order: consists exactly of the elements of piecewise in with breakpoints in ; ; preserves orientation, is left-orderable and torsion-free; Proposition 9; the countable dense subring; the orbit relation of a measurable action of an amenable group is amenable; the orbit relation of on is not amenable (Carrière–Ghys, external); Lemma 13 and Theorem 14 leading to Theorem 2 ( has no free subgroups); Corollary 3; Proposition 6 (bi-orderability); Lemma 16, Proposition 7 (co-amenability of pointwise stabilizers), Proposition 15 and Proposition 5 (inner amenability); and Thurston's identification of the rational-breakpoint variants of and with and .
The result. Theorem 1 and Theorem 2 together make , for instance , a torsion-free counterexample to the von Neumann conjecture, with finitely generated examples (Corollary 3). The groups are concrete enough to carry many further properties (Propositions 5–7).
Formalizing it. Nothing on amenability of groups of homeomorphisms of the line, or on measured equivalence relations, is in Mathlib. Amenability and Følner's theorem are on this platform from Garrido I, the Banach–Tarski paradox from Garrido II, Brin–Squier's theorem from its own mission, and Thompson's and (CannonFloydParry, CannonFloydParry_T) from the Cannon–Floyd–Parry missions.
The algebraic half, Theorem 2 and Propositions 5–9, follows Brin–Squier and elementary dynamics on the circle. The analytic half is the passage through measured equivalence relations in the proof of Theorem 1. The mission defines amenability of a relation as Connes–Feldman–Weiss do, by an invariant mean valued in , which is the form under which an amenable group's orbit relation is amenable without extra set-theoretic hypotheses. The step taken from the literature, that the orbit relation of on is not amenable for countable and dense, rests on Carrière–Ghys's theorem and on Zimmer's theory of amenable actions (Adams–Elliott–Giordano). The milestone is proved (Monod.not_isAmenableRel_mob) by an elementary route that needs neither: a ping-pong argument in that contradicts an invariant mean directly.
OnePoint ℝ and acts through Matrix.SpecialLinearGroup (Fin 2) A; since acts trivially the orbits are those of .OnePoint ℝ, each defined as the subgroup generated by the maps the paper describes; the milestones state that is exactly its set of such maps and that .volP1).This mission formalizes Geoghegan's conjecture that Thompson's group is not amenable, in the form stated by Cannon, Floyd and Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996), §4, p. 227 (doi:10.5169/seals-87877), together with the landmark results of the literature on the question.
A discrete group is amenable when it carries a finitely additive, translation-invariant probability measure on all of its subsets. Groups containing a non-abelian free subgroup are not amenable, and the question whether every non-amenable group contains one (the von Neumann problem) made Thompson's group the first natural candidate for a counterexample: it contains no non-abelian free subgroup, and it is not elementary amenable. Geoghegan conjectured in 1979 that is not amenable; several announced solutions in each direction did not survive. In 2026 OpenAI released a proof that is not amenable, with a Lean formalization; adapted to this mission's definitions, it is the solution of the goal.
Timeline.
Let UI be the unit interval . Thompson's group (CannonFloydParry.F) is the group, under composition, of the order-preserving homeomorphisms of that are piecewise linear with finitely many breakpoints, every breakpoint a dyadic rational and every slope a power of . It is generated by two elements and finitely presented (Cannon–Floyd–Parry, Corollary 2.6 and Theorem 3.4).
A mean on a set is a function from the subsets of to with , for disjoint , and . A group is amenable (Garrido.IsAmenable G) when it carries a mean with for all and , where . This is equivalent to the definition Cannon, Floyd and Parry give on p. 227, whose means take values in .
The milestones use four further notions, defined precisely in the definitions item and in their own statements:
The question was open until 2026. OpenAI's proof of the conjecture (see the timeline), transferred to CannonFloydParry.F and Garrido.IsAmenable, proves this statement.
The milestones are results from the literature, stated as their sources state them: has no non-abelian free subgroup (Cannon–Floyd–Parry, Corollary 4.9) and is not elementary amenable (Theorem 4.10), and Følner's criterion, all three already proved and linked as references; Moore's tower lower bound on Følner sets of ; Kaimanovich's theorem that random walks on with finitely supported strictly non-degenerate steps are not Liouville; Chornyi's reformulation of amenability of as extensive amenability of its action on the dyadic rationals; Stankov's embedding of into Monod's ; Monod's theorem that is not co-amenable in ; and the theorem of Juschenko, Matte Bon, Monod and de la Salle that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable.
Monod's Problem 12 asks whether is amenable; it is stated as ¬ Garrido.IsAmenable (Monod.H ⊥), where ⊥ is the smallest subring of , namely ; this is parallel to the goal. Through Stankov's embedding, the proof of the goal proves it. By the theorem of Juschenko, Matte Bon, Monod and de la Salle, it is equivalent to the statement that the action of on the line is not extensively amenable; that theorem is proved on this platform, through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn), and for the subgroups of also in a sharper form, with extensive amenability on the set of possible breakpoints only (the breakpoint criterion).
The result. A proof of the conjecture would make a finitely presented, torsion-free, non-amenable group with no non-abelian free subgroup, with a concrete description as a group of homeomorphisms of the interval. A disproof would make an amenable group that is not elementary amenable, and by Moore's theorem one whose Følner sets are at least tower-sized.
Formalizing it. Corollary 4.9 and Theorem 4.10 of Cannon–Floyd–Parry are formalized and proved on this platform and enter as references. Chornyi's corollary is proved here; its "if" direction is proved directly, by establishing the case that Chornyi applies of the Juschenko–Matte Bon–Monod–de la Salle criterion. Moore's theorem is formalized and published together with the lemmas of its proof, and the milestone here has a solution that reduces it to that statement. Kaimanovich's theorem, Stankov's embedding, Monod's 2023 theorem and the theorem of Juschenko, Matte Bon, Monod and de la Salle are proved here as well, the last through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn). The definitions of Følner sets, harmonic functions on groups and extensive amenability are reusable beyond this mission.
The obstructions to amenability that settle the question for most groups are absent here: has no non-abelian free subgroup, and its elementary structure is well understood. In the other direction, the usual constructions of invariant means fail: by Moore's theorem any Følner set of is at least tower-sized, so no explicit search can exhibit one, and by Kaimanovich's theorem the finitely supported random walks on are not Liouville, so the random-walk route to amenability through a trivial Poisson boundary is closed.
Lean representation and conventions.
UI; and are subgroups of the homeomorphisms of OnePoint ℝ. Groups of maps multiply by composition, ; statements from sources that write the product in the other order are restated for this convention, with the equivalence explained in their natural-language statements.What is left out.
What a development needs. Thompson's group and its dyadic action (Cannon–Floyd–Parry §4), its tree diagrams and presentations, and amenability, Følner's criterion and the closure properties of amenable groups (Garrido I) are published and proved on this platform, as are Monod's groups and the isomorphism (Monod.contDiff_and_exists_mulEquiv_HRat_F). Mathlib has Følner filters for measurable groups and Schreier graphs of quivers, but no random walks on groups; the proofs of the landmarks here supply what they need, and the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn) is reusable beyond this mission. Reductions of the goal or of Problem 12 to new, sharper statements are welcome, as is a disproof of either.
A periodic point of a map is a point with for some . A nonwandering point is a much weaker form of recurrence: every neighbourhood of eventually returns to meet itself, for some . Every periodic point is nonwandering, but a nonwandering point need not be periodic, and the orbit of such a point may never come back to exactly.
Pugh's closing lemma asserts that this gap can be closed by an arbitrarily small change of the system: if is nonwandering for a diffeomorphism of a compact manifold, then some diffeomorphism , as close to as desired in the topology, has as a periodic point (Wikipedia, "Pugh's closing lemma"). The result was proved by C. C. Pugh in 1967 (Pugh 1967), in the same paper as the General Density Theorem: for a -generic diffeomorphism the periodic points are dense in the nonwandering set. The source article describes the lemma as establishing a close relationship between chaotic and periodic behaviour and notes that it underlies some autonomous convergence theorems. The article also points to Smale's problems as related material.
Let be a compact smooth manifold of dimension , Hausdorff and without boundary. Write for the set of diffeomorphisms : bijections such that and are continuously differentiable. For , denotes its tangent map on the tangent bundle.
The topology on is the coarsest topology for which is continuous, where the space of continuous self-maps of carries the compact-open topology. Two diffeomorphisms are -close when they, and their derivatives, are uniformly close.
For a map of a topological space:
For every and every ,
Milestones 1–4 are elementary background facts that are not stated in the source article; milestone 5 is the second theorem named in the title of the source's reference.
The result. The closing lemma turns a topological recurrence property into periodicity after a -small perturbation. Combined with genericity arguments it gives the General Density Theorem, so that for generic diffeomorphisms the whole nonwandering set is the closure of the periodic orbits. It is one of the basic perturbation tools of generic dynamics.
Formalizing it. The theorem is classical and proved in the literature. The drafter is not aware of a machine-checked proof. A formalization needs the topology on diffeomorphism groups, local perturbation lemmas in charts and the combinatorics of the closing argument. None of these is currently available in Mathlib as far as the drafter knows.
The first idea is to take the returning piece of orbit near and push it back to with a small local perturbation. This fails in the topology. Moving a point by distance with a bump supported in a ball of radius costs size about , and the return may happen at a distance comparable to the size of the only available ball. The perturbation then fails to be -small. The derivative along the return can also distort any fixed neighbourhood shape without bound. Controlling this distortion is the central difficulty.
BCWCentralizer_Basic. is M ≃ₘ^1⟮𝓡 d, 𝓡 d⟯ M, and the topology is induced by into C(TangentBundle, TangentBundle) with the compact-open topology. On a compact manifold this is the usual topology.PughClosingLemma_nonwandering, shared by all statements. It is reusable for any topological dynamics mission.Welcome contributions: a general theory of the topology on (for example, that it is Baire), local perturbation lemmas, and proofs of the milestones.
Two commuting diffeomorphisms of a manifold share all of their dynamics: permutes the orbits of and preserves every smooth and topological invariant of . The centralizer of ,
always contains the cyclic group , and has trivial centralizer when . S. Smale asked whether diffeomorphisms with trivial centralizer are dense, residual, or even open and dense in (one of Smale's problems for the 21st century).
Timeline: Kopell (1970) answered the question for on the circle; Palis–Yoccoz, Fisher and Burslem obtained results under hyperbolicity or partial hyperbolicity assumptions; Togawa treated generic Axiom A diffeomorphisms in the topology; Bonatti–Crovisier–Vago–Wilkinson showed that trivial-centralizer diffeomorphisms do not contain an open dense set in ; and Bonatti–Crovisier–Wilkinson (this paper, arXiv:0804.1416) proved residuality in for every compact manifold.
is a closed (compact, boundaryless), connected smooth manifold of dimension . is the space of diffeomorphisms of with the topology; a subset is residual if it contains a countable intersection of open dense sets.
There is a residual subset such that for every and every with , one has for some .
Following Section 2 of the paper: the classical upper-semicontinuity lemma used for Proposition 2.5, the wandering part of Theorem A (unbounded distortion is -generic), Proposition 2.5 (density of trivial Lipschitz centralizers implies residuality) and Theorem 2.3 (residuality of trivial Lipschitz centralizers when ).
The theorem answers the second (and hence the first) part of Smale's question in the topology, and exhibits a precise link between dynamical properties of (large derivative and unbounded distortion) and the algebraic structure of inside the group . The result is proved in the literature; it has not been formalized.
The density of trivial centralizers comes from perturbation results (Theorems A and B) that change the derivative without changing the topological dynamics (tidy perturbations in topological towers). Density alone does not give residuality, since the set of diffeomorphisms with the large derivative property is not residual (Appendix); the passage from dense to residual needs the Lipschitz centralizer and a semicontinuity argument.
is a charted space over with a atlas, Hausdorff, compact and connected; is Mathlib's type of diffeomorphisms. The topology is encoded as the topology induced by into the compact-open topology on continuous self-maps of the tangent bundle . Powers , , are taken in the permutation group of . Bi-Lipschitz homeomorphisms are defined chart-locally (equivalent on a compact manifold to bi-Lipschitz for a Riemannian distance). Jacobians are computed with respect to an arbitrary continuous Riemannian metric; the unbounded-distortion property does not depend on this choice.
Contributions welcome: the topology API (Baire property, continuity of composition), the Kupka–Smale and closing-lemma genericity results, and the perturbation machinery of Sections 3–7.
The Thomson problem asks for the configuration of electrons, constrained to the surface of the unit sphere and repelling each other according to Coulomb's law, that minimises the total electrostatic potential energy. J. J. Thomson posed it in 1904 in connection with his "plum pudding" atomic model. The same energy-minimisation question reappears in the arrangement of protein subunits in spherical virus shells, in colloidosomes, in fullerene patterns and in multi-electron bubbles, and it is a special case () of the Riesz -energy problem on the sphere; the logarithmic variant is Smale's 7th problem.
Despite its elementary statement, the minimum is rigorously known only for a handful of values of .
Timeline of exact solutions (as reported in the source).
A configuration of points is a map . It is admissible if every point lies on the unit sphere, , and the points are pairwise distinct. In units with and its Coulomb energy is
An admissible is an energy minimiser (solves the Thomson problem for ) if for every admissible -point configuration .
Explicit candidate configurations are fixed in the definitions file: the antipodal pair (), an equatorial equilateral triangle (), the regular tetrahedron (), the triangular bipyramid (), the regular octahedron (), the pentagonal bipyramid (: the two poles plus a regular pentagon on the equator) and the regular icosahedron ().
This asserts admissibility of the seven points and the inequality against every admissible seven-point configuration . It fixes no numerical value of the minimum and does not assert uniqueness.
The result. Among the values of listed in the source, is the smallest one whose optimum was, until the 2026 claim, supported only by numerical computation; the cases and were settled earlier. Settling extends the short list of rigorously known Thomson minimisers.
Formalizing it. The result reported in the source is recent and described there as a claimed Lean-kernel-checked proof; a formalization on this platform against a public, reviewed statement would corroborate it independently. For the milestones, the source attributes the cases to published proofs (Föppl 1912, Schwartz 2013, Yudin 1992, Andreev 1996); the source does not describe machine-checked proofs of these, and each is a self-contained formalization target.
The energy is a non-convex function on the configuration space with many critical points, so numerical minimisation — which is how most entries of the source's table of smallest known energies were obtained — does not certify global optimality. The case, the most recent classical entry before , was resolved only with a computer-assisted proof (Schwartz 2013).
Points live in EuclideanSpace ℝ (Fin 3); configurations are functions Fin N → EuclideanSpace ℝ (Fin 3). Admissibility requires unit norm and injectivity (distinct points), matching the source's " distinct points". The energy sums over ; Lean's convention is harmless because coincident points are excluded by admissibility. The candidate configurations are fixed in one particular orientation; since the energy is invariant under orthogonal maps and relabelling, this is no loss of generality. The statement " is an energy minimiser" includes admissibility of itself, so the goal cannot be satisfied by a degenerate candidate.
Reusable infrastructure welcome: energy invariance under isometries and permutations, existence of minimisers by compactness, linear-programming (Delsarte–Yudin) bounds on the sphere, and interval-arithmetic tooling for certified numerical bounds.
The second part of Hilbert's 16th problem (Paris, 1900) asks for the maximal number and the relative position of the limit cycles of a planar polynomial differential system
where are real polynomials of degree at most . Smale listed it in 1998 among the mathematical problems for the next century and remarked that, apart from the Riemann hypothesis, it seems the hardest of Hilbert's problems (Smale 1998). Even for it is not known whether the number of limit cycles is uniformly bounded.
J. Llibre's survey Sobre el problema 16 de Hilbert (La Gaceta de la RSME 18 (2015), 543–554) organises the question into seven problems and concentrates on a more tractable restriction: algebraic limit cycles, i.e. limit cycles contained in a real algebraic curve. For this restriction there is an explicit conjecture for the maximal number (Conjecture 1 of the survey, first stated in Llibre–Ramírez–Sadovskaia 2010). This mission formalizes that conjecture as its goal, together with the results of the survey on which it rests.
Timeline (as reported in the survey):
A polynomial vector field is a pair of real polynomials in ; its degree is . A solution is a differentiable curve with for all . A periodic orbit is the image of a non-constant periodic solution. A limit cycle is a periodic orbit that is isolated among periodic orbits: some open set contains no periodic orbit other than .
A limit cycle is algebraic if it is contained in the zero set of a non-zero real polynomial . The algebraic Hilbert number is the supremum, over all polynomial vector fields of degree at most , of the number of algebraic limit cycles (a value in ).
A curve is invariant with cofactor if . A family of irreducible curves is generic if (i) no curve is singular, (ii) the top-degree homogeneous part of each curve is square-free, (iii) distinct curves meet transversally, (iv) no three distinct curves share a point, and (v) the top-degree homogeneous parts of distinct curves are coprime.
The equality asserts both that the number of algebraic limit cycles is bounded by the right-hand side for every field of degree at most , and that the bound is attained.
A proof of the goal would settle Problems 6 and 7 of the survey: it would give a uniform bound, depending only on the degree, for the number of algebraic limit cycles, and identify the sharp value. The conjecture is consistent with every example known to the survey: the generic bound of Theorem 4 is sharp for even , and the known non-generic examples exceed the generic bound only in odd degree and by one. Conjecture 2 () is its first open case.
On the formal side, the milestones require a reusable library of planar dynamics that is currently absent from Mathlib: periodic orbits and limit cycles of planar vector fields, hyperbolicity via the divergence integral, inverse integrating factors, invariant algebraic curves and Darboux-type arguments, and topological configurations of Jordan curves. Theorems 1, 2, 4 and 5, Proposition 3 and the cubic example are proved in the literature but, as far as the proposal author knows, not formalized; the goal and Conjecture 2 are open.
The obvious route bounds the number of ovals of the invariant curve (Harnack's theorem) and relates the degree of the curve to the degree of the field. This fails because a field of degree can have invariant curves of arbitrarily high degree, so no a-priori degree bound on the curve is available; Theorem 4 obtains one only under the genericity conditions (i)–(v), and the degree-3 example shows that non-generic curves behave differently. On the formal side, the dynamical milestones (Theorems 2 and 5, the cubic example) need Poincaré–Bendixson-type planar topology and uniqueness of solutions, which Mathlib does not yet provide.
MvPolynomial (Fin 2) ℝ with variable 0 as and 1 as ; points are ℝ × ℝ. The degree of a field is the maximum of the total degrees of and , and ranges over fields of degree at most , matching equation (1) of the survey.Set.encard values in ℕ∞, so an infinite family is , never silently ; is an iSup in ℕ∞, so the goal also asserts finiteness.HasDerivAt at every real time). A limit cycle is isolated among periodic orbits contained in a neighbourhood. An algebraic limit cycle lies in the zero set of some non-zero polynomial, with no degree restriction on the curve.ℕ∞, not an inequality over a possibly empty family.Contributions welcome: a planar ODE library (uniqueness, flows, Poincaré–Bendixson), Darboux theory of integrability, and proofs of the classical milestones.
A base-stock (order-up-to) policy orders, in every period, exactly enough to bring the inventory position (stock on hand plus stock on order minus backorders) up to a target level. It is the policy used in practice for repairable and consumable service parts, and the analysis of every later chapter of Muckstadt's book assumes it. Its optimality is therefore a foundational question, and there are three classical ways to prove it.
This mission formalizes the third approach, in the finite-horizon single-location form presented in Section 2.2.1 of Muckstadt (2005).
A single item is reviewed in periods . An exogenous, time-homogeneous Markov chain on a finite set is observed at the start of period ; given , the demand has law and is independent of . Excess demand is backordered.
Every unit of demand is a customer, and customers are indexed in arrival order, the initially waiting customers first. A customer's distance is once served, while waiting, and for future customers in the order they will arrive. Units are indexed by location: (used), (on hand), (in transit) and (at the supplier, which holds countably many units). The state is
with the location of unit and the distance of customer . In period : units in transit move one location closer and the released units move from to (so an order is on hand periods later); the demand brings the customers at distances to distance and moves the others steps closer; units on hand serve waiting customers, lowest indices first; then is charged per unit on hand and per waiting customer, with . The criterion is the expected cost over the periods, discounted by .
A policy for the whole system chooses a finite set of units at the supplier to release. It is monotone if it releases lower-indexed units first, and committed if unit only ever serves customer . The subsystem is unit with customer under commitment, with state and actions Release and Hold. The set contains the optimal actions of a subsystem whose unit is at the supplier and whose customer is at distance , and the critical distance is
Every policy that, in each period and Markov state , releases the lowest-indexed units at the supplier to raise the inventory position to
is optimal for among all policies, from every starting state. Such a policy exists. The levels are not fixed numbers but the critical distances of the single-unit problem, so the goal asserts the structure of an optimal policy and identifies its levels, without committing to any constant.
and managing every subsystem independently and optimally is optimal for . 3. Lemma 2 (p. 28): implies . 4. Section 2.2.1.2.2 (p. 29): the critical distance policy, release if and only if , is optimal for every subsystem.
The result shows that under Markov-modulated demand a single-location system is optimally run by a state-dependent base-stock policy. The same unit–customer argument gives echelon base-stock optimality in serial systems with noncrossing stochastic lead times (Sections 2.2.2–2.2.3). The decomposition also yields the levels themselves: they are the critical distances of a two-action problem, which can be solved one customer at a time.
The theorems are proved in the literature (Muharremoglu and Tsitsiklis 2008) and in the book. To our knowledge no machine-checked proof of any base-stock optimality theorem exists, by dynamic programming or by decomposition. The book's proof is informal in three places a formalization has to settle:
A formal development makes each of these precise.
The obvious argument says that costs are linear, so the cost of is the sum of unit–customer costs and everything decouples. That is only half of Theorem 4. The pairing of unit with customer holds only under monotone policies, and a general policy for observes the whole infinite state , not just . The lower bound therefore needs Lemma 1 together with the fact that extra information about the demand history does not help a Markov decision problem. The upper bound needs the lowest-index matching to cost no more than committed matching.
The second difficulty is that the threshold structure is not the obvious consequence of Lemma 2. The set of distances at which releasing is optimal must be shown to be an initial segment when ties are allowed. Unbounded demand makes that set possibly unbounded (it is, in the last periods). Finally, the release decisions of the subsystems must be counted to recover an inventory position, which uses the invariant that future customers occupy consecutive distances.
Everything is in the namespace ServiceParts.UnitDecomp, with three definition files.
Model. Model bundles the chain, the demand law, , , and with the standing assumptions , , , together with the per-unit and per-customer motions and a generic finite-horizon expected-cost recursion. Costs are in .
Subsystem. Subsystem defines a subsystem, its optimal cost, , and the critical distance policy.
System. System defines with lowest-index matching, its policies (finite release sets), monotone and committed policies, starting states, the inventory position and the order-up-to release.
Conventions and pinnings:
Corrections to the book:
Out of scope: stochastic noncrossing lead times (Section 2.2.2), serial systems (Section 2.2.3; compare the disproved platform statement SupplyChainTheory.clark_scarf_sequential), and continuous review (Section 2.2.4, which the book calls intuitive).
Proofs of any milestone are welcome. A reusable by-product would be a general lemma that Markov policies are optimal among history-dependent ones for finite-horizon problems with countable randomness and costs in .
The Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.
This mission extends the best possible constant for complex diagonal matrices from to every real . The result is proved in Lean. The constant and its formula are unchanged from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. For each exponent, it works for every triple of diagonal matrices, whatever their size, and no smaller constant does.
The mission started from a supplied pen-and-paper proof. Lowering the cutoff took more than replacing 256 with 90: several estimates in the original argument had to be strengthened. The research note proves the bound for real entries first, then transfers it to complex entries and shows that the constant cannot be improved. The goal theorem below gives the exact formula and statement.
This is the second step of the sharp diagonal Hlawka campaign, and it reuses the foundation's definitions and supporting results. The campaign invites further improvements below 90, keeping the same formula.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library