Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

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.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ 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 $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

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.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -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 $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

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.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

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.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

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.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Control Theory Functional Analysis Machine Learning·Captain: olivier

Universal Reservoir Computers from Non-Homogeneous State-Affine SystemsResearch Paper

Motivation

A reservoir computer learns a dynamical input/output relation with a recurrent network whose internal weights are fixed once and never trained; only a linear readout on the state is fitted. The method works in practice — it is a standard tool for learning chaotic dynamics — but its justification requires an approximation theorem: the family of reservoirs used must be rich enough to reach any reasonable target system.

The target class is fixed by fading memory, the continuity notion Boyd and Chua introduced in 1985 for the approximation of nonlinear operators: a filter has fading memory when inputs that agree on the recent past produce nearby present outputs, however much they differ long ago. The question is then which reservoir families are dense in that class.

Non-homogeneous state-affine systems are the family that answers it. They are affine in the state, with coefficients depending polynomially on the input, and the density result proved for them is what every later universality theorem for reservoir computing rests on — including the one for echo state networks, whose proof approximates a target filter by a state-affine system first and only then by a network.

Timeline.

1985 — Boyd and Chua identify fading memory as the right continuity notion, and prove a universality result for Volterra series.
2018 — Grigoryeva and Ortega prove that non-homogeneous state-affine systems with linear readouts are universal in the fading memory category, in discrete time and with uniformly bounded inputs.
2018 — The same authors use that density result to prove that echo state networks are universal.

Setting

Time is indexed by the nonpositive integers, so an input has an infinite past and a present. Inputs are real-valued and bounded by one: the set $I^{\mathbb{Z}_-}$ of sequences with $z_t \in [-1,1]$ .

A non-homogeneous state-affine system is the reservoir

x_t = p(z_t)\,x_{t-1} + q(z_t), \qquad y_t = W^{\top} x_t ,

where $p$ is a polynomial with $N \times N$ matrix coefficients, $q$ a polynomial with $N$ -vector coefficients, and $W \in \mathbb{R}^N$ the linear readout. Writing $p(z) = \sum_j z^j P_j$ , the system is affine in the state and polynomial in the input.

Two constants govern it: $M_p = \max_{z \in I} \lVert p(z) \rVert_2$ and $M_q = \max_{z \in I} \lVert q(z) \rVert_2$ . When $M_p < 1$ the state map contracts, the system has the echo state property — exactly one bounded state sequence per input — and the states obey $\lVert x_t \rVert \le M_q/(1 - M_p)$ . The induced map from input history to present output is the SAS functional $H^{p,q}_W$ .

Formalization targets

Goal — state-affine systems are universal

\forall\, H \text{ with fading memory},\ \forall \varepsilon \in (0,1),\ \exists\, p,q,W \text{ with } M_p, M_q < 1-\varepsilon:\quad \sup_{z} \bigl| H(z) - H^{p,q}_W(z) \bigr| < \varepsilon .

Any fading memory filter on uniformly bounded scalar inputs is approximated, uniformly over all such inputs, by a state-affine system read out linearly.

Supporting — the echo state property under a contracting polynomial

\max_{z \in I} \lVert p(z) \rVert_2 < 1 \;\Longrightarrow\; \text{exactly one bounded state sequence, with } \lVert x_t \rVert \le M_q/(1-M_p).

Significance

The result itself. It is the density theorem of reservoir computing. Without it, nothing guarantees that a reservoir family can represent the system one is trying to learn, and the practice of fitting only a linear readout has no theoretical backing. It is also the input to the universality theorem for echo state networks: that proof replaces the target filter by a state-affine system before replacing it by a network, so the present result is a prerequisite rather than a parallel statement.

Formalizing it. The supporting target is a specialization of a result already published on this platform: a state-affine system is a contracting reservoir map, so its echo state property follows from the abstract contraction theorem rather than from a new argument. What this mission adds beyond that is the density statement itself, which is of a different nature — an approximation theorem in a function space, not a fixed point argument.

Difficulty

The obvious approach to the goal is to exhibit an approximating system directly, and it fails: the target is an arbitrary fading memory filter, given by no formula, so no construction can be read off it. The proof is not constructive in that sense. It proceeds instead by showing that the family of SAS functionals is a polynomial algebra which separates points and contains the constants, and by applying a Stone-Weierstrass argument on a space of input sequences made compact by the weighted topology.

Two points resist. The compactness is not that of the supremum norm — the space of uniformly bounded sequences is not compact for it — but of the weighted norm, and it is that topology in which the approximation is obtained. And the algebra property is delicate: the product of two SAS functionals must again be one, which is what forces the non-homogeneous form. The corresponding statement fails for linear reservoirs, whose products leave the family.

Formalization scope

Time is indexed by $\mathbb{N}$ , index $k$ denoting the instant $k$ steps into the past and $k = 0$ the present; the system equation reads $x_k = p(z_k) x_{k+1} + q(z_k)$ . This is a relabelling of the source's indexing, not a weakening.

Inputs are scalar, as in the source's Section 3, where the restriction is made explicit and the multidimensional extension deferred to a remark. Polynomials are given by their coefficient families, and evaluated as $\sum_j z^j P_j$ ; the bounds $M_p$ and $M_q$ are stated as explicit operator and norm bounds valid on $[-1,1]$ rather than through a maximum, so that any valid bound may be supplied.

The fading memory property of the target is the one already published on this platform, stated for a functional rather than a filter: the two are in linear bijection, so nothing is lost and causality and time-invariance need not be formalized separately.

One trivialization is ruled out. The goal quantifies over state sequences satisfying the system equation, and the supporting target is what guarantees such a sequence exists and is unique under the stated bounds; without it, the approximation claim could be read as vacuous.

A complete development needs the Stone-Weierstrass theorem, available in Mathlib, together with compactness of the weighted sequence space, which is not and has to be built. Contributions are welcome on both targets.

Selected references

L. Grigoryeva, J.-P. Ortega, Universal discrete-time reservoir computers with stochastic inputs and linear readouts using non-homogeneous state-affine systems, Journal of Machine Learning Research 19(24) (2018), 1–40. https://jmlr.org/papers/v19/18-020.html · https://arxiv.org/abs/1712.00754
L. Grigoryeva, J.-P. Ortega, Echo state networks are universal, Neural Networks 108 (2018), 495–508. https://doi.org/10.1016/j.neunet.2018.08.025 · https://arxiv.org/abs/1806.00797
S. Boyd, L. Chua, Fading memory and the problem of approximating nonlinear operators with Volterra series, IEEE Transactions on Circuits and Systems 32 (1985), 1150–1161. https://doi.org/10.1109/TCS.1985.1085649

8 thms4 active usersReviewed

Algebra·Captain: mysticflounder

Equational Magmas: E677 → E255 (finite case)Open Problem

Motivation

An equation for a magma constrains a binary operation without assuming that it is associative, commutative, or has an identity. Which laws imply which others, over all magmas or over finite magmas only, is the question the Equational Theories Project studies at scale. Restricting the underlying set to be finite can change the answer: a structural argument may depend on the fact that a surjective self-map of a finite set is injective.

The project's December 2025 paper reports the finite implication from E677 to E255 as unresolved, while reporting a counterexample to the implication when infinite magmas are allowed. The paper also tentatively conjectures that a finite counterexample exists. This mission makes the affirmative implication its formal target and also accepts a rigorous refutation of the complete finite statement.

This mission treats the universal target as open. Supporting structural facts and conditional reductions are separately identified, so that progress on one does not assert completion of the target.

Setting

A magma here is a type $\alpha$ with a total binary operation $\diamond:\alpha\times\alpha\to\alpha$ . Parentheses specify the order of evaluation throughout; no reassociation is permitted. The condition E677 means

\forall x,y\in\alpha,\quad x=y\diamond\bigl(x\diamond((y\diamond x)\diamond y)\bigr).

The condition E255 means

\forall x\in\alpha,\quad x=((x\diamond x)\diamond x)\diamond x.

These are the two laws used in Chapter 13 of the project blueprint. For a fixed element $y$ , the left translation (left multiplication) map is $L_y(x)=y\diamond x$ . A fixer of $x$ is an element $y$ with $y\diamond x=x$ ; it acts on $x$ from the left. This definition concerns one element $x$ ; it does not require $y$ to act as an identity on every element. The left orbit of $x$ is the forward orbit $x,L_x(x),L_x^2(x),\ldots$ of $x$ under its own left translation.

Formalization targets

The supporting targets expose the relevant distinction between a constraint on a possible fixer and the existence of a fixer. For every finite $\alpha$ satisfying E677, the first supporting statement is

\forall y\in\alpha,\quad L_y\text{ is bijective}.

The second supporting statement determines any fixer:

\forall x,y\in\alpha,\quad y\diamond x=x\ \Longrightarrow\ y=(x\diamond x)\diamond x.

The third supporting statement is the backward recurrence

\forall x,y\in\alpha,\quad x=(y\diamond x)\diamond\bigl((y\diamond(y\diamond x))\diamond y\bigr).

These three statements are blueprint Lemma 13.1(i)–(iii) and are Proved on this platform. The following fixer-existence assertion is the same obligation as E255 under E677 and finiteness (blueprint Lemma 13.2); it is a reduction node, not a milestone:

\forall x\in\alpha,\quad\exists y\in\alpha,\quad y\diamond x=x.

The mission goal is

\forall\text{ finite magmas }\alpha,\quad \operatorname{E677}(\alpha)\ \Longrightarrow\ \operatorname{E255}(\alpha).

For finite E677 magmas, E255 at $x$ supplies the fixer $(x\diamond x)\diamond x$ ; from any fixer $y$ of $x$ , Lemma 13.1(ii) gives $y=(x\diamond x)\diamond x$ and hence E255 at $x$ . Each direction is one line, so fixer existence is not a strictly weaker milestone.

Three open sub-goals come from the case split in the accepted reduction sketches for the fixer-existence node. Sub-goal 1 is orbit-local: for a fixed $x$ , if two elements of the left orbit of $x$ have equal right products by $x$ , then they are equal or $x$ has a fixer. Sub-goal 2 concerns the case of exactly one element $A$ outside the left orbit of $x$ , with $x$ having no fixer: a right-translation collision $c\diamond x=A\diamond x$ between an orbit point $c$ and $A$ must propagate to the orbit successor $x\diamond c$ . Sub-goal 3 assumes $x\diamond x\ne x$ and at least two elements outside the left orbit: if right translation by $x$ sends an orbit point outside the orbit, then $x$ has a fixer. Sub-goal 3 is not a smaller case of the goal. If it holds for every finite E677 magma, the mission goal follows by a product construction (milestone "Sub-goal 3 support (a)"), and the mission goal gives Sub-goal 3 because E255 at $x$ supplies the fixer $(x\diamond x)\diamond x$ . So a proof of Sub-goal 3 alone proves the goal, and a route through Sub-goals 1 and 2 still needs Sub-goal 3. The D4 milestones specialize Sub-goal 1 to a left orbit of exact period four; D4.0, D4.1, D4.2 and D4.4a–e are Proved, and the series is open at D4.3 and its five branch closeouts D4.3a–e. One conditional result (E677 together with conjugacy-closed left translations implies E255; Padilla, 2026) is Proved on this platform. The milestone "Alternative resolution — a finite E677 counterexample to E255" (theorem finite_counterexample) is the disproof target. The sixteen milestones "Counterexample structure (a)–(p)" are constraints on a counterexample and rules for a counterexample search, all Proved; (h)–(j) take small-order facts as hypotheses. None of the sixteen is a disproof. None of the displayed statements restricts the cardinality to a tested range.

In the authors' repository, Sub-goal 1 is called Piece 1, the unique-outsider case containing Sub-goal 2 is called Gap 1, and the case of Sub-goal 3 is called Gap ≥ 2; those names appear in some theorem sources and file names.

Significance

A resolution determines whether this particular law gains E255 as a consequence upon restriction to finite carriers. An affirmative proof must cover every finite cardinality, every operation on each carrier, and every assignment of the universally quantified elements. A finite counterexample must supply an operation that satisfies every instance of E677 while failing E255 at some element.

The formal package provides small, reusable statements of the two laws, the left translation property, and the fixer constraint. Keeping these statements separate allows their precise hypotheses and conclusions to be checked individually. In particular, the second supporting result says what a fixer must be when one exists; the fixer-existence formulation records the additional mathematical content needed to ensure existence.

Difficulty

The left translation conclusion concerns maps with the left input fixed. The fixer-existence formulation instead asks about the image of the map $y\mapsto y\diamond x$ , with its right input fixed. No assumption in the formal goal makes these two maps interchangeable. Bijectivity of every left translation map alone does not state that a fixer exists.

Because the implication fails for infinite magmas, E255 is not an equational consequence of E677, so any proof must use finiteness in an essential way. The blueprint's linear and linear-extension constructions cannot produce a finite counterexample (blueprint Lemmas 13.3 and 13.4); community members have formalized on this platform the scalar-coefficient case of the linear lemma, the Type I and Type II affine families, and the linear-extension lemma (see the discussion thread).

Likewise, checking a collection of finite operation tables does not quantify over arbitrary finite cardinalities. Such computation does not discharge the goal submitted here. Any proof must justify every use of finiteness and retain the displayed parenthesization of the laws.

Formalization scope

The representation uses an arbitrary universe-polymorphic type, an explicit binary operation, and a Fintype instance for finite targets. Passing the operation explicitly avoids importing a separate magma package or imposing algebraic typeclass laws. The predicates E677 and E255 themselves do not assume finiteness; each theorem states its own finite-carrier hypothesis.

Empty carriers are included. Both laws hold vacuously on them; the pointwise fixer statement is also vacuous because there is no element $x$ . Consequently an empty carrier cannot refute the main goal. Nonempty carriers of every finite size are included without further assumptions. There is no associativity, commutativity, idempotence, identity element, or cancellation hypothesis hidden in the representation.

The definition bundle FiniteMagmaE677 provides E677, E255, HasFixerAt (existence of a fixer of $x$ ), InLeftOrbit (membership in the left orbit of $x$ ) and OrbitRightCollisionOrFixer. Three further bundles, FiniteMagmaE677_seventh_element_growth, FiniteMagmaE677_d4_first_return and FiniteMagmaE677_sswap_renewal, hold the period-four packet types used by the D4 milestones.

Status (2026-10-22 UTC). Proved on this platform: Lemma 13.1(i)–(iii), the Sub-goal 1, Sub-goal 2 and Sub-goal 3 support lemmas, D4.0, D4.1, D4.2, D4.4a–e, the conditional conjugacy-closure theorem, Counterexample structure (a)–(p), and three further conditional theorems by omegaestable (existential row transport, parametrized row transport, left-parameter transport; see the discussion thread). Open: Sub-goals 1–3, D4.3 with D4.3a–e, and the counterexample target. Community members have also formalized the blueprint's 496-element non-right-cancellative E677 magma (see the discussion thread).

Welcome contributions: a proof of any open sub-goal or D4.3 branch (a proof of Sub-goal 3 proves the goal; see the milestone "Sub-goal 3 support (a)"); a proof sketch that reduces an open leaf to new lemmas; a concrete operation table on Fin n proving finite_counterexample, which would make the main theorem false.

Results in the captain's private repository that are not on this platform

Results that are Proved on this platform are not repeated here. Readers cannot open the captain's private repository, so each statement is given in full. PROVEN means a complete proof, in the form stated. BOUNDED means a SAT-solver result for one encoded finite structure: each UNSAT result used here has a DRAT proof that drat-trim accepted (unverified C code, not a kernel-checked proof). EMPIRICAL means a computation over finite data, with no certificate.

Not ported

A port of these results to this platform is a long job.

1. The finite facts that Counterexample structure (h)–(j) take as hypotheses. BOUNDED. No E677 magma has order 2, 3, 4, 6 or 8, and every E677 magma of order 7 or 9 has an idempotent. Counterexample structure (h) and (j) give the earlier sources and the captain's check. These facts, except those for orders 2 and 3, are hypotheses of theorems that are Proved on this platform, so a port of them would make (h)–(j) unconditional; it needs kernel-checked proofs made from the DRAT certificates. Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/idempotent-free-small-orders-2026-10-21/ and, for order 8, experiments/analysis/ti-groups-2026-10-19/ (section "Order 8").

2. Period-four refinements of D4.2. PROVEN (Lean; axioms propext, Classical.choice, Quot.sound). A repository theorem refines the five branches of the D4.2 first-return packet and keeps every case. Write $q=c_2\diamond x$ . In the R-through-one branch (the repository's name), each outcome is a fixer of $x$ , a strict decrease of a finite contact budget, a new $L_x$ -cycle disjoint from the elements already accounted for (with its exact size), or a closed trace of $L_q^{-1}$ that is reduced to two phase-contact families. In the two unswapped S branches, each outcome is a fixer of $x$ , a decrease by one of the number of unmarked phases on the $L_x$ -cycle of $q$ , or a new disjoint $L_x$ -cycle with its exact size. These results do not close D4.3 or any of D4.3a–e, because the outcomes are not yet combined into one state with a strictly decreasing well-founded measure. A port needs the repository's library of period-four packets. Source: the captain's private repository, revision 4100763b, lean/E677/Spine/Piece1D4RefinedFirstReturn.lean, e677_d4_q_refinedFirstReturnPacket_of_firstReturnPacket.

Not formalized

These results have only solver or computation evidence, and no Lean proof, and no milestone on this platform uses them as hypotheses.

3. A counterexample has at least 11 elements. BOUNDED. Every E677 magma with at most 10 elements satisfies E255. By item 1, no E677 magma has order 2, 3, 4, 6 or 8. Every E677 magma of order 5, 7 or 9 is right-cancellative; then each right translation $y\mapsto y\diamond x$ is a bijection, so $x$ has a fixer, and Lemma 13.1(ii) gives E255 at $x$ . At order 10, a point $x$ at which E255 fails has no fixer, so $x$ is not in its own column $\{y\diamond x\}$ ; a search for such a table, split into 67 cases by the cycle type of $L_x$ (the length $l\ge 2$ of the left orbit of $x$ , and the cycle lengths of $L_x$ on the other $10-l$ elements), is UNSAT in each case. Earlier reports: the sources listed in Counterexample structure (h)–(j) for the E677 magmas of orders 2–4 and 6–9, among them a Lean proof for order 6 by J. Hyun. Without certificates (ETP Zulip thread "FINITE: 677 -> 255"): J. Brox (Mace4) reports no counterexample of order 9 (2024-12-10), none of order at most 10 (2025-01-10), no E677 magma of order 10 (2025-01-12) and no counterexample of order 11 (2025-03-12); B. Le Floch (2024-12-22, Mace4) reports none of order at most 9; J. Hyun (2025-01-09, CaDiCaL) none of order 5 to 8; S. Chuks-Onah (2026-05-01, Z3) none of order 5 or 6; R. Schneider (2026-05-15, own search program) and B. Subercaseaux (2026-05-15, SAT) none of order at most 11. The new content here is the DRAT certificates. Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/rc-small-orders-2026-10-19/ and experiments/analysis/rc-cubes-2026-10-19/.

4. Order 35 over the quotient $x\diamond y=4x+3y$ on $\mathbb{F}_7$ . With the order-7 fact of item 1, Counterexample structure (i) gives: if a minimum counterexample $M$ has order 35 and a non-universal congruence $\theta$ that relates $z$ and $q(z)$ , then $M/\theta$ has 7 elements and an idempotent, and the classes have 5 elements. By the classification of J. Brox (ETP Zulip thread "FINITE: 677 -> 255", 2025-03-26, Mace4, no certificate; not checked by the captain), $M/\theta$ is then isomorphic to $4x+3y$ or to $4x+y$ on $\mathbb{F}_7$ . Take $Q$ : $x\diamond y=4x+3y$ on $\mathbb{F}_7$ (0 is its only idempotent), write the elements of $M$ as pairs $(a,s)$ with $a\in\mathbb{F}_7$ and $s\in\mathbb{F}_5$ , and call the map $(s,t)\mapsto$ (second coordinate of $(a,s)\diamond(b,t)$ ) the block over $(a,b)$ . Results, each for an E677 magma of this form:

If at most five blocks other than the block over $(0,0)$ do not have the form $(s,t)\mapsto s+f_{ab}(t-s)$ with a permutation $f_{ab}$ of $\mathbb{F}_5$ , then E255 holds. BOUNDED (two short paper lemmas reduce it to 48 patterns of non-cyclic blocks, each UNSAT). This includes the case where every block has this form.
If every block has the form $(s,t)\mapsto A\,t+B$ with $A\in\{1,4\}$ (with $A$ and $B$ chosen for each block and each $s$ ), then E255 holds. BOUNDED.
With all blocks free, the solver runs did not finish, so there is no result. The quotient $4x+y$ was not tested.

The only known E677 magma of order 35 with this quotient and classes of 5 elements is isomorphic to $Q\times M_5$ , where $M_5$ is $s\diamond t=2s-t$ on $\mathbb{F}_5$ (EMPIRICAL). T. Tao (ETP Zulip thread "FINITE: 677 -> 255", 2024-12-13) proposed the extensions $(x,s)\diamond(y,t)=(4x+3y,\ s\diamond_{x,y}t)$ , and (same thread, 2024-12-22) the fibre operations $s+f_{x,y}(t-s)$ of the first result. The second result is a case of the form $(x\diamond y,\ b_{x,y,s}t+c_{x,y,s})$ for which B. Reinke (same thread, 2026-06-11) expected E255 to lift, without a proof. Source: the captain's private repository, revision dd2ee3e5, docs/current/e677-coverage-matrix-2026-10-19.md (the rows for this quotient) and experiments/analysis/pro-counterexample-audit-2026-10-20/.

5. Extensions and row changes of the order-31 magma $x\diamond y=5x-4y+1$ on $\mathbb{F}_{31}$ . Call it $Q_{31}$ . It has no idempotent, and it is the smallest known E677 magma without an idempotent; every known E677 magma without an idempotent has order divisible by 31 (EMPIRICAL). So $Q_{31}$ is the smallest known candidate quotient in Counterexample structure (j). BOUNDED results:

No E677 magma has a congruence with quotient $Q_{31}$ and classes of 2 or 3 elements.
No E677 magma with a congruence with quotient $Q_{31}$ and classes of 4 elements fails E255.
In the family $(u,s)\diamond(w,t)=(5u-4w+1,\ s+h_{w-u}(t-s))$ on $\mathbb{F}_{31}\times\mathbb{F}_5$ , with permutations $h_d$ of $\mathbb{F}_5$ , no E677 member fails E255.
An E677 operation on $\mathbb{F}_{31}$ that fails E255 differs from $Q_{31}$ in at least 20 rows and at least 40 cells.

B. Le Floch (ETP Zulip thread "FINITE: 677 -> 255", 2024-12-13) found $5x-4y+c$ mod 31 as the one linear E677 model in which $c$ cannot be removed, and R. Schneider (same thread, 2025-11-21) noted that $Q_{31}$ has no idempotent. T. Tao (same thread, 2024-12-13) proposed the extensions $(x,s)\diamond(y,t)=(x\diamond y,\ s\diamond_{y-x}t)$ of $Q_{31}$ . B. Reinke (same thread, 2025-11-07) encoded them for z3 and wrote that he thought he could exclude classes of fewer than 4 elements (no certificate). The first result above covers all extensions with classes of 2 or 3 elements, not only these; the third result is the case of Tao's extensions with fibre operations $s+h(t-s)$ . Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/gap2-monolith-m3-2026-10-17/ (§2, §6), experiments/analysis/pro-counterexample-audit-2026-10-20/ (cyclic-section-19375/, construction-19350/) and experiments/analysis/idempotent-free-2026-10-19/.

6. Tables with an automorphism of prime order, orders 12–21. BOUNDED, incomplete. Let $\alpha$ be an automorphism of prime order $p$ of an E677 magma of order $n$ , $12\le n\le 21$ , with $f$ fixed points, and let $z$ be a point with no fixer. The fixed points of $\alpha$ form a submagma, so an E677 magma of order $f$ ; by item 1, $f\notin\{2,3,4,6,8\}$ . The search covers $f\in\{0,1,5,7,9,11\}$ . If $\alpha$ fixes $z$ , the fixed points form an E677 magma of order $f$ that fails E255 at $z$ ; this is excluded for $f\le 9$ by item 3, and for $f=11$ 4 shapes $(n,p,f)$ are UNSAT and 7 were not run. If $z$ is in a cycle of $\alpha$ , 26 shapes are UNSAT (all 9 shapes with $p\ge 11$ , and 17 shapes with $p\le 7$ ); 14 shapes are UNKNOWN after 3600 s, and 40 were not run. Not covered: the shapes with $f=0$ and one cycle ( $n=p\in\{13,17,19\}$ , translation-invariant tables on $\mathbb{Z}_n$ ), fixed-point count 10, and fixed-point counts of at least 12. Earlier searches without certificates (ETP Zulip thread "FINITE: 677 -> 255"): R. Schneider (2025-11-20 and 2025-11-21) searched the tables with the automorphism $(0)(1\,2\,\dots\,n-1)$ up to $n=31$ and found only right-cancellative ones (the shapes with $f=1$ and one cycle); B. Reinke (2025-11-21) noted that the fixed points form a submagma and found no table with one cycle and 5 fixed points of order at most 25 other than order 5 (the shapes with $f=5$ and one cycle), and (2025-11-26) noted that in a minimum counterexample only the identity automorphism fixes the failing point. Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/symmetric-simple-2026-10-20/.

7. A refuted intermediate statement. EMPIRICAL (exhaustive check of one explicit table, run twice with independent encodings; not kernel-checked). Let $S(x)$ be the closure of the left orbit of $x$ under $z\mapsto z\diamond x$ . The repository's gate CP asserted: in a finite E677 magma, if the hypotheses of Sub-goal 3 hold at $x$ and $z\mapsto z\diamond x$ is not injective on $S(x)$ , then the left orbit of $x$ has minimal period $7$ . Let $K$ be the 7-element E677 magma of Sub-goal 3 support (a) (file db/7/1 of the public collection memoryleak47/eq677), and let $M$ be the E677 magma of order $77$ in file db/77/65 of the same collection. In $M\times K$ (order $539$ ; E677 checked on all $539^2$ pairs), the point $(0,0)$ satisfies these hypotheses, and its left orbit has minimal period $\operatorname{lcm}(7,6)=42$ . The point $(0,0)$ has the fixer $(76,4)$ , so this is not a counterexample to E255, and it refutes CP only in the form without a no-fixer hypothesis. Source: the captain's private repository, revision 4100763b, docs/current/dead-ends/gap-ge-2.md, entry D7-6.

8. $\Phi(x)=(x\diamond x)\diamond x$ is not injective in general. EMPIRICAL. In the 2026-09-27 snapshot of the community database (4091 tables), every table satisfies E255, and $\Phi$ is not injective in 1107 of them; the smallest such order is $7$ . In one table of order 7, row 6 is the identity row, so $6$ is a fixer of every $x$ and Lemma 13.1(ii) gives $\Phi(x)=6$ for every $x$ . So global injectivity of $\Phi$ is not a usable intermediate target. Source: the captain's private repository, revision 4100763b, docs/professor-phi-injectivity.md, correction of 2026-10-14.

Selected references

Matthew Bolan et al., The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale, arXiv:2512.07087v2 (December 16, 2025), paper.
The Equational Theories Project contributors, Equational Theories, online proof blueprint, Chapter 13, equations (1)–(2) and Lemmas 13.1–13.4, chapter, accessed September 7, 2026 and October 13, 2026.
J. I. Padilla (GitHub: omegaestable), Prove E677 implies E255 under left translation conjugacy closure, Equational Theories Project pull request #1518, 2026 (closed without merge by its author on 2026-10-13; the theorem is Proved on this platform), pull request.
Lean Zulip, channel "Equational", thread "FINITE: 677 -> 255", thread.

54 thms4 active usersReviewed

Computational Geometry Discrete Geometry Graph Theory·Captain: hao jia

Uniform Obstacle Bounds for Planar Graphs (OPG-37357)Open Problem

Motivation

An obstacle representation turns a graph into a visibility system: vertices are points in the plane, and nonedges are blocked by polygonal obstacles. The obstacle number asks for the minimum number of obstacles needed. OPG-37357 records two different questions for planar graphs. The first asks whether one obstacle can ever be insufficient. The second asks whether some universal constant bounds the ordinary obstacle number of every planar graph.

The status of the two parts is different. Berman, Chappell, Faudree, Gimbel, Hartman, and Williams proved in 2017 that explicit planar graphs, including the icosahedron and their graphs $X_4$ and $X_6$ , have ordinary obstacle number two. Thus the first question has a published positive answer. The universal-constant question remains the research target here. A separate invariant called planar or plane obstacle number requires a crossing-free visibility drawing; results for that invariant must not be substituted for the ordinary obstacle number used by this mission.

Setting

A finite simple graph $G$ has a $k$ -obstacle drawing when its vertices are placed injectively as points in $\mathbb R^2$ and there are $k$ pairwise disjoint closed connected polygonal obstacles such that

uv\in E(G) \quad\Longleftrightarrow\quad [p(u),p(v)]\text{ meets no obstacle}.

Graph vertices lie outside every obstacle. The ordinary obstacle number $\operatorname{obs}(G)$ is the least such $k$ . The drawing itself may contain crossings between visible graph edges; planarity is a property of the abstract input graph, not an extra constraint on the obstacle drawing.

The Lean model represents a polygonal obstacle as a connected finite union of closed filled triangles. This gives a compact polygonal region with exact real-coordinate segment incidence. Straight-line planarity of the abstract graph is represented separately.

Formalization targets

The two-part OPG record

The source records both

\exists\text{ finite planar }G,\ \operatorname{obs}(G)>1

and

\exists k\in\mathbb N\ \forall\text{ finite planar }H, \ \operatorname{obs}(H)\le k.

The first assertion is known in the literature and appears as a published-result milestone. The second is open and is therefore the mission's main theorem. Together they preserve the two-part source without presenting the whole record as unresolved.

Published first part

A milestone formalizes the stronger published statement

\exists\text{ finite planar }G, \qquad \operatorname{obs}(G)\le2 \quad\text{and}\quad \operatorname{obs}(G)\not\le1.

This captures ordinary obstacle number exactly two without hard-coding one graph before its adjacency data and lower-bound certificate are formalized.

Universal bound

The open milestone asks for a single natural number $k$ , chosen before the graph, that works for every finite planar graph. The number of obstacle corners is not bounded by this theorem; only the number of connected polygonal obstacles is.

Significance

The published first part establishes that planarity alone does not force a one-obstacle representation. The second part asks whether planar graphs nevertheless have uniformly bounded visibility complexity. A positive answer would produce a common finite obstacle budget independent of graph order; a negative answer would require a family of planar graphs with unbounded ordinary obstacle number.

Formalization is especially useful because several nearby notions differ by one word but have different known bounds: ordinary versus plane obstacle number, arbitrary polygonal versus convex obstacles, and fixed-placement versus freely chosen drawings. The mission's definitions make those choices explicit and provide reusable segment-obstacle semantics for later geometric graph formalizations.

Difficulty

A finite combinatorial graph does not come with a canonical visibility drawing. Even when one starts with an arbitrary connected blocking set, replacing it by one bounded simple polygon requires compactness, component, incidence, and polygonal-neighborhood arguments. Conversely, lower bounds must quantify over every possible placement and obstacle, not merely refute a selected coordinate drawing.

Counting results for unrestricted graphs do not automatically preserve planarity. Bounds for planar obstacle number impose a crossing-free drawing and therefore answer a different question. The known two-obstacle examples close only the existential first part and give no universal $k$ .

Formalization scope

All graph vertex types are finite. Obstacles are closed connected polygonal regions represented by finite triangle unions; they are pairwise disjoint and avoid graph vertices. Visibility uses the full closed segment, so tangency or boundary contact blocks a nonedge. The planarity witness is independent of the obstacle drawing. Empty and one-vertex graphs remain in the universal quantifier and should be handled without division or nonemptiness assumptions.

The repository's fixed-placement polygonization argument and finite arrangement code are candidate_only. They may motivate supporting lemmas, but they neither prove the unrestricted obstacle-drawing completeness theorem nor settle the universal bound. Contributions are welcome on exact geometry primitives, the published two-obstacle construction and lower bound, conversions between connected blockers and polygonal obstacles, and the universal root. A proof for the plane invariant, convex invariant, one fixed drawing, or a finite order cutoff must be labeled at that narrower scope.

Selected references

L. W. Berman, G. G. Chappell, J. R. Faudree, J. Gimbel, C. Hartman, and G. I. Williams, Graphs with Obstacle Number Greater than One, JGAA 21(6), 2017. https://doi.org/10.7155/jgaa.00452
J. Gimbel, P. Ossona de Mendez, and P. Valtr, Obstacle Numbers of Planar Graphs, Graph Drawing 2017. https://arxiv.org/abs/1706.06992
M. Balko, S. Chaplick, R. Ganian, S. Gupta, M. Hoffmann, P. Valtr, and A. Wolff, Bounding and Computing Obstacle Numbers of Graphs, SIAM Journal on Discrete Mathematics 38(2), 2024. https://arxiv.org/abs/2206.15414
Open Problem Garden / UnsolvedMath, OPG-37357. https://www.unsolvedmath.com/problems/OPG-37357

6 thms4 active usersReviewed

Combinatorics Graph Theory Optimization·Captain: hao jia

Clique Partitions of Chordal Graphs (Erdos Problem 81)Open Problem

Motivation

An edge partition into cliques compresses the adjacency structure of a graph into complete pieces without allowing any edge to be counted twice. Erdős Problem 81 asks for the asymptotically sharp upper bound on the number of pieces needed when the graph is chordal. Chordal graphs have strong elimination structure, but that structure does not make the partition parameter additive under arbitrary edge deletion, and obtaining a linear error term remains substantially stronger than identifying the leading quadratic coefficient.

Erdős, Ordman, and Zalcstein studied clique partitions of chordal graphs in 1993. Their examples already exhibit the $n^2/6$ scale, while their general upper estimate had a larger quadratic coefficient. Later dense-packing results of Haxell–Rödl and Yuster compare fractional and integer triangle packings with an $o(n^2)$ gap. The project candidate combines that interface with chordal elimination arguments to formulate a uniform $n^2/6+o(n^2)$ milestone. It does not supply the $O(n)$ remainder asked for by the root.

Setting

A finite simple graph is chordal when it has no induced cycle of length greater than three. The Lean definition uses the equivalent perfect-elimination form: vertices admit an injective ranking such that the later neighbors of every vertex form a clique.

An edge partition into cliques is a finite family $\mathcal P$ of complete vertex sets such that every edge of $G$ belongs to exactly one member of $\mathcal P$ . Members may share vertices but may not share edges. Write $\operatorname{cp}(G)$ for the minimum possible number of pieces.

The asymptotic notation

\frac{n^2}{6}+O(n)

means that there are constants $C>0$ and $n_0\ge1$ , chosen independently of $G$ and $n$ , such that every chordal $n$ -vertex graph with $n\ge n_0$ has a clique partition with at most $n^2/6+Cn$ pieces.

Formalization targets

Erdős Problem 81

The root theorem is

\exists C>0\ \exists n_0\ge1\ \forall n\ge n_0\ \forall G\text{ chordal on }n\text{ vertices}, \qquad \operatorname{cp}(G)\le \frac{n^2}{6}+Cn.

The quantifier order is essential: $C$ and $n_0$ are universal and cannot depend on the graph.

Leading-coefficient milestone

The supporting target records the weaker uniform statement

\forall\varepsilon>0\ \exists n_0\ \forall n\ge n_0\ \forall G\text{ chordal on }n\text{ vertices}, \qquad \operatorname{cp}(G)\le \left(\frac16+\varepsilon\right)n^2.

This is the precise $n^2/6+o(n^2)$ form. It is not equivalent to the root: choosing $\varepsilon=1/n$ is invalid because the cutoff may depend on the fixed value of $\varepsilon$ .

Significance

The root would determine the clique-partition extremum for chordal graphs up to a linear remainder, matching the scale of the complete-split examples that motivate the coefficient $1/6$ . It would refine a leading-order asymptotic theorem into a uniform estimate strong enough to distinguish second-order behavior.

Formalization creates a clean interface among perfect elimination orderings, exact edge partitions, fractional edge-and-triangle decompositions, and integer triangle packings. It also forces the proof to distinguish a partition from a cover and original graph order from the order of any auxiliary hypergraph. These definitions can support other decomposition problems on chordal and split graphs.

Difficulty

Perfect elimination does not by itself give the sharp partition count. Greedily taking maximal cliques may overlap in edges or accumulate too many singleton pieces. Similarly, a fractional edge-and-triangle partition can achieve the right leading coefficient while integer rounding loses $o(n^2)$ pieces; the root requires that loss to be only $O(n)$ .

The dense-packing theorem has quantifiers of the form “for every fixed $\varepsilon>0$ there exists $N(\varepsilon)$ .” It therefore yields a uniform subquadratic error but no linear error. Any proof of the root must add a chordal-specific rounding or extremal reduction rather than treating the general packing theorem as if its $\varepsilon$ could vary with $n$ .

Formalization scope

Graphs are finite and simple. Chordality is encoded by existence of a perfect-elimination ranking, including disconnected and edgeless graphs. A clique piece is a finite vertex set that spans a complete subgraph. Exactness means every actual edge occurs in exactly one piece; no nonedge can occur inside a piece. Bounds are compared in $\mathbb R$ so the displayed asymptotic expressions retain their conventional form, while the number of parts remains a natural number.

The candidate derivation of the leading coefficient imports finite linear-programming duality and the Haxell–Rödl/Yuster fixed-triangle packing approximation. It is candidate_only, not an admitted result or kernel proof. Contributions may formalize the perfect-elimination lemmas, the fractional compression, the uniform packing interface, complete-split lower examples, or the root linear rounding theorem. A result for edge-and-triangle pieces only, a fractional partition, or one fixed order must not be presented as the unrestricted integer clique-partition theorem.

Selected references

P. Erdős, E. T. Ordman, and Y. Zalcstein, Clique Partitions of Chordal Graphs, Combinatorics, Probability and Computing 2(4), 1993. https://doi.org/10.1017/S0963548300000808
P. E. Haxell and V. Rödl, Integer and Fractional Packings in Dense Graphs, Combinatorica 21, 2001. https://doi.org/10.1007/s004930170003
R. Yuster, Integer and fractional packing of families of graphs, 2003. https://arxiv.org/abs/math/0305350
Erdős Problems, Problem 81. https://www.erdosproblems.com/81

16 thms4 active usersReviewed

Partial Differential Equations Pure Mathematics·Captain: korbonits

Formalize Navier-StokesOpen Problem

Motivation

The incompressible Navier–Stokes equations are the standard model for the motion of a viscous fluid such as water or air, used daily in engineering, meteorology and oceanography. Yet the most basic mathematical question about them is open: starting from smooth initial data in three dimensions, does a smooth solution exist for all time? This is one of the seven Millennium Prize Problems of the Clay Mathematics Institute. Its official formulation is Charles Fefferman's problem description, Existence and smoothness of the Navier–Stokes equation (2000), which offers a prize for a proof of any one of four statements: global existence and smoothness on $\mathbb{R}^3$ (statement (A)) or on the torus $\mathbb{R}^3/\mathbb{Z}^3$ (statement (B)), or a counterexample to either (statements (C) and (D)). This mission formalizes statement (A), together with the classical partial results that Fefferman lists as known.

Timeline.

1822–1845: Navier and Stokes write down the equations of a viscous incompressible fluid.
1934: Jean Leray, Sur le mouvement d'un liquide visqueux emplissant l'espace (Acta Math. 63), proves on $\mathbb{R}^3$ that smooth solutions exist for a positive time depending on the data, that they exist for all time when the data is small compared with the viscosity, and that global weak solutions with finite energy always exist. Their smoothness and uniqueness are left open.
1933–1969: the two-dimensional problem is settled (Leray for the plane; Olga Ladyzhenskaya's monograph The Mathematical Theory of Viscous Incompressible Flow, 2nd ed. 1969, for bounded domains): smooth solutions exist for all time and are unique.
1984: Tosio Kato, Strong $L^p$ -solutions of the Navier–Stokes equation in $\mathbb{R}^m$ (Math. Z. 187), gives global solutions for initial data small in $L^3(\mathbb{R}^3)$ .
1976–1998: partial regularity. Scheffer, then Caffarelli, Kohn and Nirenberg (Comm. Pure Appl. Math. 35, 1982), show that the singular set of a suitable weak solution has one-dimensional parabolic Hausdorff measure zero.
2000: the Clay Mathematics Institute adopts Fefferman's formulation as a Millennium Prize Problem. It remains open.

Setting

Fix a dimension $n \ge 1$ and write $\mathbb{R}^n$ for Euclidean $n$ -space with its Euclidean norm $|x|$ ; in Lean this is NavierStokes.Vec n. A velocity field assigns to each time $t \in \mathbb{R}$ and point $x \in \mathbb{R}^n$ a vector $u(x,t) \in \mathbb{R}^n$ ; in Lean $u\,t$ is the field at time $t$ and $u\,t\,x$ is Fefferman's $u(x,t)$ . A pressure is a real function $p(x,t)$ . The viscosity $\nu$ is a positive constant. The external force of Fefferman's equation (1) is identically zero throughout, as in statement (A).

For a vector field $v : \mathbb{R}^n \to \mathbb{R}^n$ the divergence is

\operatorname{div} v = \sum_{i=1}^n \frac{\partial v_i}{\partial x_i},

in Lean NavierStokes.div, computed from the Fréchet derivative $Dv(x)$ as $\sum_i (Dv(x)\,e_i)_i$ . The Laplacian $\Delta v = \sum_i \partial^2 v/\partial x_i^2$ acts componentwise (Mathlib's Laplacian on inner product spaces). The gradient $\nabla p$ is Mathlib's gradient. The convective term $\sum_j u_j\,\partial u/\partial x_j$ is the derivative of $u(\cdot,t)$ at $x$ in the direction $u(x,t)$ . Finally $|\nabla v|^2 = \sum_{i,j} (\partial v_i/\partial x_j)^2$ is NavierStokes.gradNormSq.

Admissible initial data (Fefferman's condition (4), NavierStokes.IsInitialData): a $C^\infty$ , divergence-free vector field $u^0$ that decays together with all its derivatives faster than any power,

|\partial_x^\alpha u^0(x)| \le C_{\alpha K}\,(1+|x|)^{-K} \quad \text{on } \mathbb{R}^n, \text{ for every } \alpha \text{ and } K.

In Lean the bound is $(1+|x|)^K\,\|D^k u^0(x)\| \le C_{kK}$ on the $k$ -th Fréchet derivative, an equivalent family of conditions. These are exactly the divergence-free Schwartz functions.

A physically reasonable solution on a set $S$ of times (NavierStokes.IsSolutionOn; $S = [0,\infty)$ for NavierStokes.IsSolution) is a pair $(u,p)$ such that

(Fefferman (6)) $u$ and $p$ are $C^\infty$ on $S \times \mathbb{R}^n$ , up to the boundary of $S$ ;
(Fefferman (1), $f \equiv 0$ ) for every $t \in S$ with $t > 0$ and every $x$ ,

\frac{\partial u}{\partial t} + \sum_{j=1}^n u_j \frac{\partial u}{\partial x_j} = \nu\,\Delta u - \nabla p;

(Fefferman (2)) $\operatorname{div} u(\cdot,t) = 0$ for every $t \in S$ ;
(Fefferman (3)) $u(x,0) = u^0(x)$ ;
(Fefferman (7), bounded energy) $\int_{\mathbb{R}^n} |u(x,t)|^2\,dx < C$ for all $t \in S$ , for some constant $C$ .

Formalization targets

Goal: Fefferman's statement (A)

Take $\nu > 0$ and $n = 3$ . For every admissible initial datum $u^0$ there exist a velocity field $u$ and a pressure $p$ forming a physically reasonable solution on $\mathbb{R}^3 \times [0,\infty)$ :

\forall\, \nu > 0,\ \forall\, u^0 \text{ satisfying (4)},\ \exists\, (u,p) \text{ satisfying (1), (2), (3), (6), (7) on } \mathbb{R}^3 \times [0,\infty).

This is NavierStokes.existence_and_smoothness_R3. It is open; a proof would settle the Millennium Prize Problem in the affirmative.

Milestones: what Fefferman lists as known

Local existence (NavierStokes.local_existence_R3): for $n = 3$ and every admissible $u^0$ there are $T > 0$ and a physically reasonable solution on $\mathbb{R}^3 \times [0,T)$ . Fefferman: "(A) and (B) hold ... if the time interval $[0,\infty)$ is replaced by a small time interval $[0,T)$ , with $T$ depending on the initial data."
Global existence for small data (NavierStokes.small_data_global_existence_R3): there is an absolute constant $c > 0$ such that, for $n = 3$ , (A) holds for every admissible $u^0$ with

\|u^0\|_{L^2}^2\,\|\nabla u^0\|_{L^2}^2 \le c\,\nu^4.

Fefferman: "(A) and (B) hold provided the initial velocity $u^0$ satisfies a smallness condition." The scale-invariant product is Leray's form of the condition; it implies smallness of $\|u^0\|_{L^3}/\nu$ , so Kato's theorem also applies. 3. The two-dimensional case (NavierStokes.existence_and_smoothness_R2): statement (A) with $n = 2$ . Fefferman: "In two dimensions, the analogues of assertions (A) and (B) have been known for a long time (Ladyzhenskaya)."

A bridging lemma, NavierStokes.isInitialData_iff_schwartz, identifies the admissible data with the divergence-free elements of Mathlib's Schwartz space.

Significance

The result itself. Statement (A) asks whether the basic model of viscous flow is well posed in the classical sense, i.e. whether smooth finite-energy flows can develop singularities in finite time. A positive answer shows the equations never leave the classical regime; a negative one shows the model predicts its own breakdown. Fefferman: "since we don't even know whether these solutions exist, our understanding is at a very primitive level."

Formalizing it. None of the results in this mission has a machine-checked proof, and Mathlib contains no theory of the Navier–Stokes or Euler equations. The milestones are all proved in the literature; formalizing them requires building, on Mathlib's calculus, measure theory and Schwartz space, the heat semigroup on $\mathbb{R}^n$ , the pressure equation $\Delta p = -\sum_{i,j} \partial_i\partial_j(u_i u_j)$ or the Leray projection, energy estimates, and a fixed-point construction of solutions, most of which is reusable for other evolution equations. The goal is open and expected to remain so; its role is to fix in Lean the exact statement the prize asks for, so partial results are formalized against it.

Difficulty

The energy identity $\frac{d}{dt}\int|u|^2 = -2\nu\int|\nabla u|^2$ controls $u$ in $L^2$ and $\nabla u$ in $L^2_{t,x}$ , but in three dimensions this control is supercritical: under the scaling $u_\lambda(x,t) = \lambda u(\lambda x, \lambda^2 t)$ that preserves the equations, the energy of $u_\lambda$ shrinks as $\lambda \to \infty$ , so bounded energy does not prevent concentration at small scales. Every known continuation criterion (Leray, Prodi–Serrin, Beale–Kato–Majda, Escauriaza–Seregin–Šverák) needs a quantity at or above critical scaling, none of which the energy controls. The obvious first idea, an ordinary differential inequality for $\|\nabla u(t)\|_{L^2}$ , gives $\frac{d}{dt}\|\nabla u\|_{L^2}^2 \le C\nu^{-3}\|\nabla u\|_{L^2}^6$ , which closes only for small data or short time. That is exactly why milestones 1 and 2 are theorems and the goal is not.

The formalization adds a second difficulty: the solutions of the literature live in Sobolev or Besov spaces, with pointwise smoothness of $u$ and $p$ recovered afterwards by regularity theory, and Mathlib has neither Sobolev spaces on $\mathbb{R}^n$ nor the heat semigroup in usable form.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure; the dimension is a parameter, the goal fixes $n = 3$ and the 2D milestone $n = 2$ .
A velocity field is a function of all real times, but every condition is imposed only on the time set $S$ ; values at negative times are unconstrained.
Smoothness on $\mathbb{R}^n \times [0,\infty)$ is Mathlib's ContDiffOn of the uncurried map on the closed half-space, i.e. all derivatives extend continuously to $t = 0$ . The momentum equation is imposed at interior times $t > 0$ with two-sided derivatives; by continuity of the derivatives this is equivalent to Fefferman's " $t \ge 0$ ".
Derivatives are Mathlib's total functions (fderiv, deriv, iteratedFDeriv, gradient, Laplacian) with junk value $0$ at non-differentiable points; the smoothness hypotheses make every derivative in the statements honest.
The energy is a Lebesgue integral in $[0,\infty]$ , equal to $\infty$ when $u(\cdot,t) \notin L^2$ , so bounded energy cannot hold vacuously. The $L^2$ norms in the small-data hypothesis are Bochner integrals, genuine for Schwartz data.
No normalization is imposed on the pressure, as in Fefferman's text.

No trivializing formalization. The zero field solves the equations only for $u^0 = 0$ ; for any other admissible $u^0$ the initial condition, smoothness, the equation on $t > 0$ and bounded energy must all hold.

Infrastructure needed and welcome contributions. The heat kernel on $\mathbb{R}^n$ with Schwartz bounds; the Riesz-transform representation of the pressure or the Leray projection; energy identities for smooth decaying solutions; local existence by Picard iteration; the two-dimensional vorticity equation and its maximum principle. Theorems in the NavierStokes namespace, decompositions of the milestones, and Mathlib lemmas about ContDiffOn on half-spaces are all welcome. Statements (B), (C), (D) and the Euler equations ( $\nu = 0$ ) are out of scope.

Selected references

C. L. Fefferman, Existence and smoothness of the Navier–Stokes equation, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf
J. Leray, Sur le mouvement d'un liquide visqueux emplissant l'espace, Acta Mathematica 63 (1934), 193–248. https://doi.org/10.1007/BF02547354
O. A. Ladyzhenskaya, The Mathematical Theory of Viscous Incompressible Flow, 2nd ed., Gordon and Breach, 1969. https://archive.org/details/mathematicaltheo0000lady
T. Kato, Strong $L^p$ -solutions of the Navier–Stokes equation in $\mathbb{R}^m$ , with applications to weak solutions, Mathematische Zeitschrift 187 (1984), 471–480. https://doi.org/10.1007/BF01174182
L. Caffarelli, R. Kohn, L. Nirenberg, Partial regularity of suitable weak solutions of the Navier–Stokes equations, Communications on Pure and Applied Mathematics 35 (1982), 771–831. https://doi.org/10.1002/cpa.3160350604
A. J. Majda, A. L. Bertozzi, Vorticity and Incompressible Flow, Cambridge University Press, 2002. https://doi.org/10.1017/CBO9780511613203
J. C. Robinson, J. L. Rodrigo, W. Sadowski, The Three-Dimensional Navier–Stokes Equations: Classical Theory, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781139095143

20 thms4 active usersReviewed

Completed

Information Theory·Captain: Elsie66

Shannon's Source Coding TheoremResearch Paper

Motivation

How short can a code for a data source be, if the code must still be uniquely decodable — if every string of concatenated codewords can be unambiguously split back into the original symbols? Shannon's 1948 source coding theorem answers this exactly: the entropy of the source is a hard lower bound on the average codeword length of any uniquely decodable code, and it is also achievable up to a one-symbol slack. Entropy is not just a measure of "average surprise" — it is the literal, tight answer to a combinatorial question about how densely symbols can be packed into strings without losing decodability. This is the theorem that gives Shannon's entropy its operational meaning, and it underlies every practical lossless compression scheme (Huffman coding, arithmetic coding, Lempel–Ziv) as the benchmark they approach.

Timeline.

1948 — Claude Shannon, "A Mathematical Theory of Communication" (Bell System Technical Journal), introduces entropy and proves the source coding theorem.
1949 — Leon Kraft's MIT master's thesis proves the combinatorial inequality (for prefix codes) that makes the theorem's achievability half constructive.
1956 — Brockway McMillan extends Kraft's inequality's necessity direction from prefix codes to the strictly larger class of uniquely decodable codes, giving the theorem its full generality.

Setting

A source has a finite alphabet of symbols $\iota$ , with at least two symbols, and probability distribution $p:\iota\to\mathbb R$ ( $p_i>0$ , $\sum_i p_i=1$ ). A code assigns to each symbol $i$ a codeword $c(i)$ , a finite string over a $D$ -ary code alphabet $\alpha$ ( $D=|\alpha|\ge 2$ ); the code is uniquely decodable if every finite sequence of codewords is determined by its concatenation. The entropy of $p$ in base $D$ is

H_D(p) = -\sum_i p_i \log_D p_i.

The expected codeword length of $c$ under $p$ is $L(c) = \sum_i p_i \, |c(i)|$ .

Formalization targets

Goal — Shannon's source coding theorem

\forall \text{ injective, uniquely decodable } c,\quad H_D(p) \le L(c), \qquad \exists \text{ such } c,\quad L(c) < H_D(p) + 1.

(For a source with $|\iota| \ge 2$ symbols — see Formalization scope for why the single-symbol case must be excluded.)

Significance

The result itself. This theorem is the reason entropy is called entropy in an information-theoretic sense at all: it converts a quantity defined by an abstract formula ( $-\sum p_i\log p_i$ ) into the exact answer to an operational question (minimum achievable expected code length), with a slack no worse than one symbol. It is the founding theorem of lossless source coding and the benchmark every practical compressor is measured against.

Formalizing it. Mathlib recently gained genuine information-theoretic coding content: InformationTheory.UniquelyDecodable and the necessity direction of the Kraft–McMillan inequality (McMillan's 1956 result: a uniquely decodable code's lengths satisfy $\sum_w D^{-|w|}\le 1$ ) are already proved, via a counting argument on concatenations of $r$ codewords. This mission builds directly on that foundation rather than duplicating it. What Mathlib does not have — and what this mission's milestones supply — is Kraft's original 1949 sufficiency direction (existence of a uniquely decodable code realizing any length assignment satisfying the Kraft sum bound), any notion of Shannon entropy for a general finite distribution, and the source coding theorem itself.

Difficulty

The lower bound ( $H_D(p)\le L(c)$ ) is the easier half: it follows from the Kraft–McMillan inequality (already in Mathlib) via Gibbs'/Jensen's inequality applied to the two probability-like sequences $p_i$ and $D^{-\ell_i}/K$ (where $K=\sum_j D^{-\ell_j}\le1$ is the Kraft sum) — a short, self-contained convexity argument.

The achievability half is the genuine construction. Given the ideal (generally non-integer) lengths $-\log_D p_i$ , one rounds up to $\ell_i=\lceil -\log_D p_i\rceil$ (Shannon–Fano–Elias lengths); a one-line estimate shows $D^{-\ell_i}\le p_i$ , so the Kraft sum of the rounded lengths is still $\le\sum_i p_i=1$ , and the bound $\ell_i<-\log_D p_i+1$ gives $L(c)<H_D(p)+1$ immediately once a code with exactly these lengths is shown to exist. Producing that code is Kraft's sufficiency direction, and it needs an explicit construction: order the lengths, and assign to symbol $i$ the first $\ell_i$ digits of the $D$ -ary expansion of the cumulative sum $\sum_{j<i} D^{-\ell_j}$ . Verifying this assignment is injective, has the prescribed lengths, and is uniquely decodable (indeed prefix-free) is a careful but standard combinatorial argument — the main open piece of this mission.

Formalization scope

The source alphabet $\iota$ must have at least two symbols ( $|\iota|\ge 2$ ), not merely be nonempty. A single-symbol source forces $p\equiv 1$ and entropy $H_D(p)=0$ , so the achievability conjunct would demand a codeword of length $0$ — but a uniquely decodable code can never contain the empty codeword (InformationTheory.UniquelyDecodable.epsilon_not_mem, provable from the definition: the empty string decodes ambiguously as zero or two copies of itself), so no admissible code exists and the theorem would be false, not merely hard, at $|\iota|=1$ . The same defect breaks Kraft's sufficiency direction (Milestone 2) whenever any prescribed length is $0$ , independent of $|\iota|$ ; that milestone accordingly requires every length strictly positive. With $|\iota|\ge2$ and full support, every $p_i<1$ strictly, so the Shannon–Fano lengths $\lceil-\log_D p_i\rceil$ are automatically all $\ge1$ , and the achievability construction only ever needs Milestone 2 at positive lengths. The code alphabet $\alpha$ is likewise an arbitrary finite type (matching Mathlib's own Fintype/Nonempty conventions for the Kraft–McMillan file), with $|\alpha|\ge2$ required to keep Real.logb non-degenerate. The source distribution is required strictly positive ( $p_i>0$ ) — the standard simplifying assumption (zero-probability symbols can always be dropped without loss). Unique decodability is stated exactly as Mathlib's InformationTheory.UniquelyDecodable, not re-derived from a "prefix code" definition, so the mission's results transport directly onto Mathlib's existing Kraft–McMillan file. A trivializing route to rule out: proving only the lower bound (citing Mathlib's inequality) while leaving the existential achievability half unaddressed would not be Shannon's theorem — the sandwich $H_D(p)\le L^*<H_D(p)+1$ is the theorem's actual content, and the lower bound alone (already essentially free from Mathlib) is not a novel contribution on its own.

Reusable output: the Kraft sufficiency construction (Milestone 2) is directly reusable for any future formalization of Huffman coding optimality, arithmetic coding, or the general "Kraft-inequality-achieving code exists" fact used throughout coding theory. Contributions are welcome starting from Milestone 2 (the open construction) or Milestone 3 (the Gibbs'-inequality lower bound, which only needs Milestone 1, already available via Mathlib).

Selected references

C. E. Shannon, "A Mathematical Theory of Communication," The Bell System Technical Journal 27 (1948), 379–423, 623–656.
T. M. Cover and J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006, Chapter 5 ("Data Compression"), §5.2 ("Kraft Inequality") and §5.4 ("Bounds on the Optimal Code Length," Theorem 5.4.1).
L. G. Kraft, A Device for Quantizing, Grouping, and Coding Amplitude-Modulated Pulses, M.S. thesis, MIT, 1949.
B. McMillan, "Two Inequalities Implied by Unique Decipherability," IRE Transactions on Information Theory 2:4 (1956), 115–116.
Mathlib, Mathlib.InformationTheory.Coding.UniquelyDecodable and Mathlib.InformationTheory.Coding.KraftMcMillan (2026).

7 thms4 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: Goku

Stabilizer Rank of Magic StatesOpen Problem

Motivation

Quantum circuits built from Clifford gates alone are classically simulable in polynomial time. Universality is recovered by adding copies of a magic state, and the fastest known classical simulators of such circuits work by writing the magic-state input as a short linear combination of stabilizer states. The length of the shortest such combination -- the stabilizer rank -- is therefore the exponent governing classical simulation of quantum computation in this model, and lower bounds on it are among the very few unconditional obstructions to classical simulation available at all.

A timeline of what is established for the standard magic state $|H\rangle$ :

2016. Bravyi, Smith and Smolin exhibit a decomposition giving $\chi(|H^{\otimes 6}\rangle)\le 7$ , hence $\chi(|H^{\otimes n}\rangle)\le 7^{\,n/6}\le 2^{\,0.468n}$ , and prove a lower bound of order $\sqrt{n}$ .
2020. Huang, Newman and Szegedy show that hardness assumptions stronger than $\mathrm{P}\neq\mathrm{NP}$ , such as the exponential time hypothesis, imply $\chi(|H^{\otimes n}\rangle)=2^{\Omega(n)}$ (arXiv link).
2022. Peleg, Shpilka and Volk improve the unconditional lower bound to $\Omega(n)$ and give the first non-trivial bound for the approximate rank (arXiv:2106.03214).
2024. A quadratic lower bound is obtained for the approximate stabilizer rank (arXiv:2305.10277).

Between the linear unconditional lower bound and the $2^{0.468n}$ upper bound lies the open problem this mission targets.

Setting

Index the computational basis of an $n$ -qubit system by bit strings $x\in\{0,1\}^n$ , so a state is a vector $\psi\in\mathbb{C}^{2^n}$ with coordinates $\psi(x)$ .

The Pauli operators are $X^aZ^b$ for $a,b\in\{0,1\}^n$ , acting by $X^aZ^b|x\rangle=(-1)^{\,b\cdot x}|x\oplus a\rangle$ , where $b\cdot x$ counts the coordinates on which both are $1$ and $\oplus$ is bitwise addition; the Pauli group is the set of $4\cdot 4^n$ operators $i^cX^aZ^b$ . A unitary $U$ is a Clifford unitary when $UPU^\dagger$ lies in the Pauli group for every Pauli group element $P$ , and a stabilizer state is a vector $U|0\cdots0\rangle$ for some Clifford $U$ . There are $2^n\prod_{k=1}^{n}(2^k+1)$ of them up to phase -- six for a single qubit.

The stabilizer rank $\chi(\psi)$ is the least $r$ admitting coefficients $c_1,\dots,c_r\in\mathbb{C}$ and stabilizer states $\varphi_1,\dots,\varphi_r$ with $\psi=\sum_{j\le r}c_j\varphi_j$ .

The magic state is $|H\rangle=\cos(\pi/8)|0\rangle+\sin(\pi/8)|1\rangle$ , and $|H^{\otimes n}\rangle$ its $n$ -fold tensor power, with coordinates $\cos(\pi/8)^{\,n-|x|}\sin(\pi/8)^{\,|x|}$ where $|x|$ is the Hamming weight of $x$ .

Target

The goal is a super-polynomial lower bound: for every exponent $d$ and constant $C$ there exists $n$ with

\chi\bigl(|H^{\otimes n}\rangle\bigr)\;>\;C\,n^{d},

equivalently, $\chi(|H^{\otimes n}\rangle)$ is not $O(n^d)$ for any fixed $d$ .

Stronger statements are expected but are deliberately not the goal. An exponential bound $\chi=2^{\Omega(n)}$ is believed and follows from hardness assumptions, but a goal naming a specific growth rate would be superseded by the next improvement; super-polynomiality is the weakest statement that settles the question of principle.

Significance

The result itself. A super-polynomial lower bound would unconditionally rule out efficient classical simulation of Clifford-plus-magic-state circuits by stabilizer decomposition, currently the leading such technique. The converse direction shows how much is at stake: a polynomial upper bound on $\chi(|H^{\otimes n}\rangle)$ would imply $\mathrm{BPP}=\mathrm{BQP}$ , and via postselection $\mathrm{P}=\mathrm{NP}$ . There is also a purely classical payoff -- improving the known bound even to super-linear would produce a Boolean function computable in polynomial time requiring a super-linear number of summands in any decomposition into exponentials of quadratic forms over $\mathbb{F}_2$ , resolving a separate open question.

Formalizing it. The goal is open, so no known proof is being transcribed. What the mission produces is a machine-checked statement of the problem together with formalizations of the established bounds, none of which has a machine-checked proof anywhere. It also produces the first Pauli/Clifford/stabilizer layer in Lean: no existing Lean library contains the $n$ -qubit Pauli group, the Clifford group, or stabilizer states, and that layer is reusable for stabilizer error correction, magic monotones, and Clifford simulation generally.

Difficulty

Counting settles the problem for random states: the stabilizer states are too few for short combinations to cover a generic state, so almost every state has exponential stabilizer rank. This says nothing about $|H^{\otimes n}\rangle$ , which is a single explicit, highly structured vector, and the entire difficulty is that lower bounds must be proved for that specific state rather than for a typical one. Every newcomer proposes the counting argument; it does not apply.

The known techniques reduce the question to statements about decompositions of explicit Boolean functions into quadratic-form exponentials, and the barrier is quantitative: the available arguments lose a factor that caps them at linear bounds. The source of the current record documents explicitly why its method cannot pass super-linear, and the fact that going beyond linear would resolve an independent open problem in Boolean function complexity indicates the obstruction is not merely technical.

Formalization scope

State vectors are functions $\{0,1\}^n\to\mathbb{C}$ and are not required to be normalised; normalisation does not affect the rank, and stabilizer states are unit vectors automatically as Clifford images of $|0\cdots0\rangle$ . The Pauli group is given by the explicit parametrisation $i^cX^aZ^b$ rather than an abstract presentation, and the Clifford group is characterised as its unitary normaliser, equivalent to the usual generated-by- $H,S,\mathrm{CNOT}$ description. Because $e^{i\theta}U$ normalises the Pauli group whenever $U$ does, the stabilizer states are closed under global phase; this is harmless, as the coefficients are arbitrary complex numbers.

One trivialising reading must be excluded. The rank is defined as an infimum over a set of natural numbers, and Lean gives the empty infimum the value $0$ ; if no decomposition existed the rank would be $0$ for every state and the goal would be false rather than merely unproved. The milestone $\chi(\psi)\le 2^n$ is what certifies the set is nonempty, making the rank a genuine minimum, and it should be proved first. Separately, the goal quantifies $C$ over all reals including negative values, for which the inequality is trivially satisfiable; the content lies in large positive $C$ .

A complete development needs, beyond the published definitions, the correspondence between stabilizer states and affine subspaces carrying quadratic phase functions, on which all known lower-bound arguments rest. Contributions of any milestone are welcome, as are function-level reformulations of the rank and the equivalent characterisation of stabilizer states via maximal abelian Pauli subgroups.

Selected references

S. Peleg, A. Shpilka, B. L. Volk, Lower Bounds on Stabilizer Rank, Quantum 6 (2022) 652; arXiv:2106.03214.
S. Bravyi, G. Smith, J. Smolin, Trading Classical and Quantum Computational Resources, Phys. Rev. X 6 (2016) 021043; arXiv:1506.01396.
C. Huang, M. Newman, M. Szegedy, Explicit Lower Bounds on Strong Quantum Simulation, IEEE Trans. Inf. Theory 66(9) (2020) 5585--5600.
Quadratic Lower Bounds on the Approximate Stabilizer Rank: A Probabilistic Approach, STOC 2024; arXiv:2305.10277.

5 thms4 active usersReviewed

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: Shuze Chen

Dynamic Programming and Optimal Control V: LQG and Certainty EquivalenceTextbook

Motivation

The separation theorem — certainty equivalence for linear-quadratic control with imperfect state information — is one of the celebrated structural results of stochastic control: the optimal controller splits into a least-squares estimator and the deterministic LQR actuator, designed independently. It underlies every LQG autopilot and Kalman-filter-based regulator. Section 5.2 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) proves it from the DP algorithm over information vectors, with Lemma 5.2.1 supplying the key fact that the estimation error is beyond the controller's influence. No formal analogue exists in Mathlib.

Setting

Linear dynamics and measurements

x_{k+1} = A_k x_k + B_k u_k + w_k, \qquad z_k = C_k x_k + v_k,

with quadratic cost $\mathbb{E}\big[x_N^\top Q_N x_N + \sum_{k<N}(x_k^\top Q_k x_k + u_k^\top R_k u_k)\big]$ , $Q_k \succeq 0$ , $R_k \succ 0$ . The initial state and the zero-mean disturbances/noises are independent with finite ranges; independence is structural — the sample space is the product of an initial-state coordinate and per-stage noise coordinates (BertsekasLQGModel, BertsekasLQGSample, BertsekasLQGProb). A policy maps the realized measurement history $(z_0,\dots,z_k)$ to $u_k$ ; the closed-loop process is BertsekasLQGTraj, the expected cost BertsekasLQGCost. The estimator $\mathbb{E}[x_k \mid I_k]$ is an explicit conditional average (BertsekasCondExpVec, BertsekasLQGEstimate); the gains $L_k$ come from the time-varying Riccati recursion (BertsekasLQGRiccati, BertsekasLQGGain).

Target

\pi^*(I_k) = L_k\, \mathbb{E}[x_k \mid I_k] \ \text{ along its own trajectories} \quad\Longrightarrow\quad J(\pi^*) \le J(\pi)\ \ \forall \pi,

— BertsekasDP.lqg_certainty_equivalence (goal). Milestone: Lemma 5.2.1 in pointwise form — the error $x_k - \mathbb{E}[x_k \mid I_k]$ is the same under any two policies, outcome by outcome (lqg_estimation_error_policy_independent).

Significance

This is the theorem that justifies designing estimator and controller separately — remove it and the entire LQG methodology loses its warrant. The formalization also yields the first machine-checked instance of the informational decomposition (control-dependent part + policy-independent error) that recurs throughout imperfect-information control. Notably the result needs no Gaussian assumption — only zero mean and independence — and the finite-support model makes that generality exact. The result is classical (Joseph–Tou 1961, Gunckel–Franklin 1963; the book's §5.2); the formal proof is new.

Difficulty

The heart is Lemma 5.2.1: showing the estimation error coincides, sample by sample, with the error of the control-free system — which requires proving that the observation-history σ-events under any policy coincide with those of the control-free system (controls are determined by the history, so they shift observations by a known amount). Then the DP argument over information histories must carry the quadratic decomposition through the backward recursion. Bookkeeping over histories-as-lists is the main formal burden; probability theory stays finite.

Formalization scope

Finite-support randomness (all expectations are finite sums); conditional expectation with the explicit junk value 0 on zero-probability events — the goal's hypothesis is accordingly restricted to outcomes of positive probability. Policies are functions of the measurement list only (equivalent to the book's information vector for deterministic policies, since past controls are recoverable from past measurements). Matrices are time-varying; positive definiteness of $R_k$ makes every matrix inverse in the gains genuine. Measurement noise covariance is not assumed positive definite — the estimator is the abstract conditional expectation, not the Kalman filter (whose recursive form, §5.2.1, would be a natural follow-up mission).

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§5.2, Lemma 5.2.1.) http://www.athenasc.com/dpbook.html
P. D. Joseph, J. T. Tou, On linear control theory, Trans. AIEE 80 (1961), 193–196. https://doi.org/10.1109/TAI.1961.6371743
T. L. Gunckel, G. F. Franklin, A general solution for linear sampled-data control, J. Basic Eng. 85 (1963), 197–201. https://doi.org/10.1115/1.3656559

5 thms4 active usersReviewed

Completed

Graph Theory Operations Research·Captain: Shuze Chen

Dynamic Programming and Optimal Control II: Label Correcting MethodsTextbook

Motivation

Label correcting methods are the workhorse family of shortest-path algorithms — Dijkstra's method, Bellman–Ford, SLF/LLL variants and A* all fit the template analyzed in §2.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005), where shortest paths appear as the purely deterministic face of dynamic programming. The correctness proof (Prop. 2.3.1) is short on paper but genuinely nondeterministic — any node may be removed from the candidate list, children processed in any order — so a formal proof certifies a whole family of concrete algorithms at once.

Setting

A finite directed graph with arc set $\mathcal{A}$ , real arc lengths $a_{ij}$ , origin $s$ and destination $t \ne s$ (BertsekasSPGraph). Walks are nonempty node lists whose consecutive pairs are arcs (BertsekasIsWalkFrom), with length the sum of arc lengths (BertsekasWalkLength); the shortest distance is the infimum of walk lengths in the extended reals, $+\infty$ if no walk exists (BertsekasShortestDistance). The standing assumption of §2.3: every cycle has nonnegative length (negative arcs allowed).

The algorithm state (BertsekasLCState) carries labels $d_j \in \overline{\mathbb{R}}$ , the scalar UPPER, and the candidate list OPEN. Initially $d_s = 0$ , all other labels $\infty$ , UPPER $= \infty$ , OPEN $= \{s\}$ . One iteration (BertsekasLCStep, nondeterministic): remove any $i$ from OPEN; for each child $j$ of $i$ in any order, if $d_i + a_{ij} < \min\{d_j, \text{UPPER}\}$ set $d_j := d_i + a_{ij}$ , and put $j$ in OPEN if $j \ne t$ , or update UPPER if $j = t$ . The algorithm terminates when OPEN is empty.

Target

\text{OPEN} = \varnothing \implies \text{UPPER} = \operatorname{dist}(s, t) \in \overline{\mathbb{R}},

for every execution, under the nonnegative arc length assumption of §2.3 ( $a_{ij} \ge 0$ for every arc) — BertsekasDP.label_correcting_correctness_of_nonneg_arcs (goal). Milestones: termination — no infinite execution exists, which needs only the weaker nonnegative-cycle assumption (label_correcting_terminates) — and the workhorse invariant that every finite label is the length of an actual walk from $s$ , which needs neither (label_correcting_invariant).

The nonnegative-arc hypothesis is essential and not a formalization artifact: the algorithm prunes with the test $d_i + a_{ij} < \min\{d_j, \mathrm{UPPER}\}$ , and with a negative arc a longer prefix can still reach $t$ more cheaply, so the pruned node is never entered into OPEN. An earlier version of this mission's goal carried only the nonnegative-cycle assumption of §2.1 and was disproved by the counterexample $s=0$ , $t=2$ , $a_{02}=1$ , $a_{01}=2$ , $a_{12}=-2$ (a graph with no cycles at all), where the algorithm terminates with $\mathrm{UPPER}=1$ while the shortest distance is $0$ . Exercise 2.7 of the source treats the nonnegative-cycle case, which requires a modified algorithm.

Significance

Prop. 2.3.1 certifies simultaneously breadth-first search, Dijkstra (best-first), depth-first and small-label-first variants — every removal discipline is one refinement of the nondeterministic relation. Formally, the development contributes a reusable small-step framework for label-setting/correcting algorithms on which sharper results (Dijkstra's single-pass property, A* admissibility, §2.3.3) can later be built. The result is classical; the formal content is the induction along the nondeterministic step relation.

Difficulty

Termination is the subtle half: labels do not decrease monotonically along the run in an obvious well-founded way; the book's argument counts the finitely many distinct walk lengths below a bound — this needs the nonnegative-cycle assumption and a careful bound relating labels to simple-path lengths. The invariant proof must thread through the fold over children within a single step.

Formalization scope

Finite node type with decidable equality; arcs as a Finset of ordered pairs; lengths total on $V \times V$ (only arc values matter). The step relation is fully nondeterministic in pivot choice and child order (a permutation quantifier); correctness quantifies over all reachable terminal states — there is no fixed schedule to exploit. Distances live in EReal, so the no-path case is the honest empty infimum, not a sentinel. The trivializing risk of restricting to nonnegative arcs is avoided: only cycles are constrained.

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 2.3.1, §2.3.) http://www.athenasc.com/dpbook.html
E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
R. Bellman, On a routing problem, Quart. Appl. Math. 16 (1958), 87–90. https://doi.org/10.1090/qam/102435

6 thms4 active users

Differential Geometry Geometry & Topology·Captain: xuanji

Strong Whitney embedding in dimension 2nResearch Paper

Motivation: an intrinsic manifold in a fixed Euclidean space

A smooth manifold is a space that can be described locally by real coordinates, even when no single coordinate chart describes the whole space. Differential geometry works with these local descriptions, whereas an embedding realizes the entire space inside one Euclidean space without losing either its topology or its infinitesimal geometry. The strong Whitney embedding theorem supplies a dimension bound depending only on the dimension of the manifold. This mission targets the precise version selected by LeanEval v1, rather than a substitute formulation.

The benchmark attributes the strong result to Hassler Whitney's 1944 paper and distinguishes it from the earlier bound of $2n+1$ . The result is a known mathematical theorem; the remaining task here is its formal proof in Lean. The exact benchmark declaration is authoritative for the target and its hypotheses, not a reconstruction from the historical literature (source and attribution).

Setting: topology, smoothness, and the differential

Let $n$ be a natural number satisfying $1\le n$ . Let $M$ carry a topology and a smooth atlas modeled on $\mathbb R^n$ , with the usual model having no boundary. The topology is Hausdorff: distinct points admit disjoint neighborhoods. It is second countable: there is a countable collection of open sets from which every open set can be assembled as a union. These are explicit hypotheses, alongside the chosen charted-space and smooth-manifold structures, in the Lean statement.

A topological embedding is a map that is a homeomorphism onto its image, where the image has the subspace topology inherited from the codomain. An immersion has an injective differential at every point. For a smooth map $e$ , write $d e_x$ for the induced linear map on tangent spaces at $x$ . These are separate requirements: the target asks for global topological embedding and pointwise injectivity of the differential together, as well as infinite differentiability. Their precise Lean meanings are the existing Mathlib predicates used directly by the benchmark, not new mission-specific definitions.

Formalization target: the single root theorem

For every $n\ge1$ and every $M$ with the structures and hypotheses just stated, establish

\exists e:M\longrightarrow\mathbb R^{2n},\qquad e\in C^\infty(M,\mathbb R^{2n}) \ \land\ e\text{ is a topological embedding} \ \land\ \forall x\in M,\ d e_x\text{ is injective}.

The codomain has dimension exactly $2n$ . The quantifier ranges over all such manifolds, including noncompact ones. There is exactly one goal theorem and no auxiliary theorem items, definition items, or milestones. The declaration is LeanEval.Geometry.WhitneyEmbeddingProblem.whitney_embedding, with the binders and conclusion preserved from the benchmark source.

Significance: the full theorem rather than an easier restriction

The result realizes the given manifold in a Euclidean space with a uniform dimension bound. Its value in this formulation is the simultaneous control of topology, smoothness, and the differential, without a compactness assumption. Replacing the image-topology condition with mere injectivity would omit part of the requested conclusion; replacing $2n$ with an unspecified dimension would omit the quantitative constraint. Both distinctions are explicit in the benchmark's explanation.

A completed formalization would supply a reusable strong embedding theorem on top of Mathlib's manifold language. This is a long-term infrastructure task, not a claim that a short proof is available. The September 5, 2026 LeanEval v1 snapshot supplied for this task records no accepted benchmark credit for this target. That dated benchmark status is not a claim about all formalization projects, and preparing an open theorem statement does not establish the theorem or earn benchmark credit.

Difficulty: the dimension bound and the noncompact scope

The existing compact embedding result discussed by the benchmark provides an embedding into some finite-dimensional Euclidean space. That does not settle the present goal: it assumes compactness and does not supply the $2n$ bound. Consequently, simply invoking that result cannot discharge the unrestricted benchmark statement. The source identifies substantial differential-topological infrastructure behind the strong theorem; this proposal does not advertise an easy proof or prescribe a decomposition (benchmark discussion).

All positive dimensions remain in scope, including $n=1$ and $n=2$ . Noncompactness is not a later extension or optional strengthening. The absence of an assumption must not be replaced by an implicit restriction in a new definition or an easier surrogate theorem.

Formalization scope: unchanged Mathlib predicates

The source model is EuclideanSpace ℝ (Fin n), and the target is EuclideanSpace ℝ (Fin (2 * n)). Smoothness is expressed by ContMDiff (𝓡 n) (𝓡 (2 * n)) ∞ e; the other two conjuncts are IsEmbedding e and pointwise Function.Injective of mfderiv. The type $M$ remains universe-polymorphic. No compactness, connectedness, orientability, or nonemptiness hypothesis is added. The empty manifold is included; dimension zero is excluded. Neither properness nor closedness of the image is demanded by the conclusion (exact declaration).

Mathlib already provides the vocabulary needed to state the goal: Euclidean spaces, charts, manifold smoothness, topological embeddings, and manifold derivatives. No custom definition item is necessary. Future proof work may develop reusable infrastructure, but this draft contains only the root theorem and intentionally imposes no supporting targets. A proof must establish that exact statement, not the compact-only, immersion-only, or weak $2n+1$ alternative.

Selected references

LeanEval contributors, Whitney embedding theorem (strong form, sharp dimension 2n), LeanEval v1 source declaration and manifest, statement revision 1, pinned source and manifest. These specify the exact formal target.
H. Whitney, The self-intersections of a smooth n-manifold in 2n-space, Annals of Mathematics (2) 45 (1944), 220–246, DOI. Historical attribution as recorded in the LeanEval manifest; no alternate statement from this reference replaces the benchmark goal.

16 thms4 active usersReviewed

Completed

Functional Analysis Pure Mathematics·Captain: wenxinzhang

Equality case for compressed convex functional calculusOpen Problem

Motivation and history

Compressing an operator to a closed subspace keeps the information visible within that subspace but can discard interactions with its orthogonal complement. The compression-rigidity question asks whether a particular equality detects that no such interactions were present. Its inputs are two commuting positive contractions and an ordinary strictly convex function of two real variables. The issue is the equality case, not the existence of a general operator inequality for every convex function.

The question was contributed by Boris Bilich to the CUHK-Shenzhen AI Math Problems collection and added on June 1, 2026. The original problem asks about operators on a Hilbert space without imposing finite dimension. The first formal target in this mission treated matrices with supplied joint spectral data. That finite-dimensional declaration has a verified proof on Prove2Me, but it does not settle the unrestricted Hilbert-space question. The September 2026 correction restores arbitrary complex Hilbert spaces as the main target and preserves the earlier result as a supporting artifact.

Setting

Let $H$ be a complete complex Hilbert space, and let $\mathcal B(H)$ be its algebra of bounded complex-linear operators. The multiplication $AB$ means composition, with $B$ acting first, and $A^*$ denotes the adjoint. A positive contraction $A$ is self-adjoint, satisfies $\operatorname{Re}\langle v,Av\rangle\geq0$ for every $v\in H$ , and has operator norm at most one. Both zero and the identity are permitted.

Write $S=[0,1]^2$ . Let $X,Y\in\mathcal B(H)$ be positive contractions satisfying $XY=YX$ . Their joint continuous functional calculus assigns an operator $g(X,Y)$ to each continuous real function $g$ on $S$ . It is characterized as a continuous unital real star-algebra homomorphism from $C(S,\mathbb R)$ to $\mathcal B(H)$ that maps the two coordinate functions to $X$ and $Y$ . The domain has the uniform norm and the codomain the operator norm. The existence and uniqueness of this calculus follow from the standard joint spectral theorem; the relevant source is Dereziński, Lemma 6.6, printed page 43.

An orthogonal projection is an operator $P$ satisfying $P^*=P$ and $P^2=P$ . The compressed operators $PXP$ and $PYP$ are still viewed as operators on the original space $H$ , not as operators on a separately chosen finite-dimensional range. The question includes the additional hypothesis that these compressed operators commute. The original commutation of $X$ and $Y$ does not remove the need to state this hypothesis.

Formalization targets

The main target is the entire compression implication from the source. Let $f:S\to\mathbb R$ be continuous and strictly convex: for distinct $x,y\in S$ and $0<t<1$ , its value at $tx+(1-t)y$ is strictly less than $t f(x)+(1-t)f(y)$ . For $X,Y,P$ as above, the question is whether

P f(X,Y)P=P f(PXP,PYP)P \quad\Longrightarrow\quad PX=XP\ \text{and}\ PY=YP.

Both outer projections on the right are part of the original assertion. There is no hypothesis that $f(0,0)=0$ . Commutation of $P$ with each coordinate operator is exactly the reducing-subspace conclusion asked for in the source.

The accompanying standard infrastructure target asserts that, for every commuting pair of positive contractions on $H$ ,

\exists!\,\Phi:C(S,\mathbb R)\longrightarrow\mathcal B(H),\qquad \Phi(x\mapsto x_0)=X,\quad\Phi(x\mapsto x_1)=Y,

where $\Phi$ is continuous, unital, real-linear, multiplicative and star-preserving. This is the unit-square, real-valued-function specialization of Lemma 6.6, not a claim that this known theorem is a new research conjecture. Its Lean proof is a separate supporting obligation. The earlier two-dimensional milestone and the proved finite-dimensional capstone remain available; neither replaces the new main target.

Significance

A positive resolution would show that exact preservation of one strictly convex functional-calculus value, under the specified commuting-compression hypothesis, forces both operators to preserve the projection's range and its orthogonal complement. A negative resolution would require an actual Hilbert space, operators and strictly convex function satisfying every hypothesis while at least one of the two reducing identities fails.

The formal development separates this research question from the standard spectral infrastructure needed to express it. The new main declaration is an open proof obligation. The joint-calculus existence-and-uniqueness declaration is also unproved in this contribution, although mathematically standard. Local compilation and server publication check the declarations' well-formedness; they are not proofs of either statement. Only the earlier finite-dimensional result is being reported here as already proved.

Difficulty

Arbitrary bounded commuting self-adjoint operators need not have a joint eigenbasis. Consequently a matrix formulation that records finitely many joint spectral atoms cannot serve as the general operator model. The compressed pair may also have different spectral data from the original pair. The equality involves these two different functional calculi, with a projection on either side of each value.

Strict convexity in this question is ordinary scalar strict convexity on the square. Operator convexity, finite rank of the projection, compactness of the coordinate operators, and a multivariable operator Jensen inequality are not additional assumptions. Introducing any of them would change the requested question. The general formulation must also retain boundary cases rather than exclude them to simplify an argument.

Formalization scope

The Lean model uses actual bounded complex-linear maps on an arbitrary complete inner-product space. It imposes no finite-dimensionality, separability, common-eigenbasis or nonzero-space assumption. It includes $P=0$ , $P=I_H$ and the zero Hilbert space. The scalar field convention is complex; a real-Hilbert-space transfer is not separately formalized here.

The function is stored on the ambient real plane, but continuity, strict convexity and evaluation use only its restriction to $S$ . Values outside $S$ are irrelevant, and continuity outside the square is not required. Thus storing an ambient function does not exclude any continuous function originally defined only on the square.

Joint evaluation is a total definition. If a representing continuous unital real star-algebra homomorphism exists, it chooses one for the operator pair and then evaluates the supplied function. Otherwise it returns zero. The separate existence-and-uniqueness target establishes that this fallback is inapplicable to commuting positive contractions and that the choice is immaterial. No field in the model assumes the compression-rigidity conclusion. The supporting standard theorem must also apply to the compressed pair using the original projection and positivity hypotheses, without adding representation existence as a new restriction on the main question.

The replacement definition and both statements were built at Lean 4.30.0 with supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, and their final versions received independent blind readbacks. Published older declarations and their proof identities are preserved. They should be cited with their finite-dimensional scope, not described as a solution of the arbitrary-Hilbert-space target.

Selected references

Boris Bilich, Equality case for compressed convex functional calculus, CUHK-Shenzhen AI Math Problems, Problem 2, added June 1, 2026. Original statement.
Jan Dereziński, Bounded operators, Warsaw University lecture notes, January 2007, Lemma 6.6, printed page 43. Joint continuous functional calculus.

5 thms4 active users

Completed

Algebraic Topology Pure Mathematics·Captain: korbonits

Hatcher Algebraic Topology I: The Fundamental Group of the CircleTextbook

Motivation

The fundamental group $\pi_1(X, x_0)$ is the first algebraic invariant a student of topology meets, and $\pi_1(S^1)\cong\mathbb{Z}$ is the first computation of it that carries real content. Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; freely available at pi.math.cornell.edu/~hatcher/AT/AT.pdf) is the standard text on the subject. Its Chapter 1 opens with exactly this computation (Theorem 1.7, p. 29) and immediately draws three classical consequences from it: the Fundamental Theorem of Algebra (Theorem 1.8), the Brouwer fixed point theorem for the disk (Theorem 1.9), and the Borsuk–Ulam theorem for the sphere (Theorem 1.10).

This mission is the opening entry in a series that formalizes Hatcher's book capstone by capstone. It covers the subsection "The Fundamental Group of the Circle" of Section 1.1 (pp. 29–33): the covering-space lifting properties that drive the proof, the theorem itself, and its three applications. Later entries in the series (van Kampen's theorem, the classification of covering spaces, simplicial and singular homology) will build on the declarations introduced here, which all live in the shared Lean namespace Hatcher.

Setting

A path in a topological space $X$ is a continuous map $f : I \to X$ , where $I = [0,1]$ . A homotopy of paths is a family $f_t : I \to X$ , $0 \le t \le 1$ , such that the endpoints $f_t(0) = x_0$ and $f_t(1) = x_1$ are independent of $t$ and the associated map $F : I \times I \to X$ , $F(s,t) = f_t(s)$ , is continuous. A loop at a basepoint $x_0$ is a path with $f(0) = f(1) = x_0$ . The set of homotopy classes $[f]$ of loops at $x_0$ is the fundamental group $\pi_1(X, x_0)$ ; its product is $[f][g] = [f\cdot g]$ , where $f\cdot g$ traverses $f$ and then $g$ , each at double speed (Hatcher, Proposition 1.3).

The circle $S^1 \subset \mathbb{R}^2$ is realised as the unit circle of $\mathbb{C}$ , so the point $(\cos\theta, \sin\theta)$ is $e^{i\theta}$ and the basepoint $(1,0)$ is $1$ . Hatcher's map

p : \mathbb{R} \to S^1, \qquad p(s) = (\cos 2\pi s, \sin 2\pi s) = e^{2\pi i s}

is Hatcher.circleCover. The loops

\omega_n(s) = (\cos 2\pi n s, \sin 2\pi n s) = p(ns), \qquad n \in \mathbb{Z},

based at $(1,0)$ are Hatcher.omegaLoopN n, and $\omega = \omega_1$ is Hatcher.omegaLoop; its class $[\omega] \in \pi_1(S^1, 1)$ is Hatcher.omegaClass.

A covering space of $X$ is a space $\tilde X$ together with a map $p : \tilde X \to X$ such that every $x \in X$ has an open neighbourhood $U$ for which $p^{-1}(U)$ is a disjoint union of open sets each mapped homeomorphically onto $U$ by $p$ (Hatcher's condition $(\ast)$ , p. 29; such a $U$ is evenly covered). A lift of a map $f : Y \to X$ is a map $\tilde f : Y \to \tilde X$ with $p \circ \tilde f = f$ .

Formalization targets

Goal (Theorem 1.7)

$\pi_1(S^1, 1)$ is an infinite cyclic group generated by $[\omega]$ . In the form stated in Lean:

\forall\, g \in \pi_1(S^1, 1)\quad \exists!\, n \in \mathbb{Z}:\quad [\omega]^n = g.

Surjectivity of $n \mapsto [\omega]^n$ says $[\omega]$ generates; uniqueness of $n$ says the group is infinite cyclic rather than finite.

Milestones on the road to the goal

$p(s) = e^{2\pi i s}$ is a covering space of $S^1$ (Hatcher, p. 29).
Homotopy lifting property (c): for a covering space $p : \tilde X \to X$ , a map $F : Y \times I \to X$ and a lift of $F|_{Y \times \{0\}}$ extend uniquely to a lift of $F$ (p. 30).
Path lifting property (a): a path $f$ starting at $x_0$ and a point $\tilde x_0 \in p^{-1}(x_0)$ determine a unique lift $\tilde f$ starting at $\tilde x_0$ (p. 29).
Lifting homotopies of paths (b): a homotopy of paths $f_t$ starting at $x_0$ lifts uniquely to a homotopy of paths $\tilde f_t$ starting at $\tilde x_0$ (p. 29).
Every loop in $S^1$ at $(1,0)$ is homotopic to $\omega_n$ for a unique $n \in \mathbb{Z}$ (the reformulation of Theorem 1.7 that Hatcher actually proves, p. 29).
$[\omega]^n = [\omega_n]$ for every $n \in \mathbb{Z}$ (Hatcher's remark after Theorem 1.7, p. 29).

Applications (Theorems 1.8–1.10)

\text{Every nonconstant } f \in \mathbb{C}[z] \text{ has a root in } \mathbb{C}.

\text{Every continuous } h : D^2 \to D^2 \text{ has a fixed point.}

\text{Every continuous } f : S^2 \to \mathbb{R}^2 \text{ satisfies } f(x) = f(-x) \text{ for some } x \in S^2.

Significance

The result itself. The computation $\pi_1(S^1) \cong \mathbb{Z}$ assigns to every loop in the circle an integer, its winding number, and shows that this integer is the only homotopy invariant of the loop. It is the seed of degree theory, and in Hatcher's text it is the starting point for every later computation of fundamental groups (products, van Kampen, covering spaces). The three applications are the standard demonstration that a single algebraic invariant can settle purely geometric or algebraic existence questions.

Formalizing it. Mathlib (revision 0df444a) already contains the covering-space infrastructure: IsCoveringMap, path lifting (IsCoveringMap.liftPath, eq_liftPath_iff'), homotopy lifting (IsCoveringMap.liftHomotopy, eq_liftHomotopy_iff'), monodromy, and the fact that Circle.exp is a covering map (Circle.isCoveringMap_exp). It also has FundamentalGroup X x as the endomorphism group of the fundamental groupoid. It does not contain the computation $\pi_1(S^1) \cong \mathbb{Z}$ , nor the two-dimensional Brouwer and Borsuk–Ulam theorems. The Fundamental Theorem of Algebra is in Mathlib as Complex.exists_root (proved by Liouville's theorem rather than by Hatcher's argument); it is kept as a milestone because it is one of the section's stated theorems, and a solver may close it directly from Mathlib. Milestones 2–4 are also within reach of the existing lifting API, but they are the lemmas Hatcher states and uses, and a faithful record of them in the mission's own namespace is what later entries in the series will import.

Difficulty

The obvious first idea for the goal is to define the winding number of a loop through the complex argument. That fails because $\arg$ is discontinuous on $S^1$ ; the integer has to be produced by lifting the loop through $p$ and reading off the endpoint of the lift, which is only well defined because of the uniqueness in the path lifting property. The second difficulty is uniqueness of $n$ : this needs lifting of homotopies (milestone 4), not just of paths, together with the observation that a lifted homotopy of paths has constant endpoints.

Connecting the concrete loops to Mathlib's abstract $\pi_1$ is its own obstacle. FundamentalGroup Circle 1 multiplies by composing morphisms of the fundamental groupoid, so identifying $[\omega]^n$ with the class of the explicit loop $\omega_n$ (milestone 6) requires reparametrization arguments for concatenated paths, for negative $n$ as well as positive.

For Theorem 1.9 the difficulty is the construction and continuity of the retraction $r : D^2 \to S^1$ from a fixed-point-free map, and then the non-existence of a retraction, which uses that $\pi_1(S^1) \neq 0$ . For Theorem 1.10 Hatcher's proof lifts a loop $g(s) = f(\cos 2\pi s, \sin 2\pi s)/\lvert \cdots \rvert$ through $p$ and shows the lift changes by an odd integer over half a turn; making that parity argument rigorous in Lean is the substance of the milestone.

Formalization scope

$S^1$ is Circle (the unit circle in $\mathbb{C}$ ) with basepoint 1; $D^2$ is Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1; $S^2$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1, with $-x$ the antipodal point.
A covering space is Mathlib's IsCoveringMap p. This agrees with Hatcher's condition $(\ast)$ ; neither requires $p$ to be surjective.
Paths are continuous maps C(I, X) or Mathlib Paths; for homotopies of paths, the square is written I × I with Hatcher's coordinate order $F(s,t) = f_t(s)$ : the first coordinate is the path parameter, the second the homotopy parameter. In the general homotopy lifting property the domain is Y × I with $Y$ an arbitrary topological space, as in Hatcher.
$\pi_1(S^1, 1)$ is Mathlib's FundamentalGroup Circle 1, and $[\omega]$ is FundamentalGroup.fromPath ⟦omegaLoop⟧. Because the goal quantifies over integer powers of a single element, the order of multiplication in FundamentalGroup is immaterial to its truth.
The goal is stated as $\forall g\, \exists! n,\ [\omega]^n = g$ rather than as an abstract isomorphism with $\mathbb{Z}$ , so that the generator is pinned to Hatcher's explicit loop; an isomorphism FundamentalGroup Circle 1 ≃* Multiplicative ℤ sending $[\omega]$ to $1$ is an immediate corollary and a welcome contribution.
"Nonconstant polynomial" is 0 < f.degree, which excludes both the zero polynomial and nonzero constants.

Contributions welcome: proofs of the milestones from Mathlib's lifting API, a degree homomorphism $\pi_1(S^1,1) \to \mathbb{Z}$ packaged for reuse, and any lemma about concatenation and reparametrization of loops in Circle that later chapters of the series can import.

Selected references

A. Hatcher, Algebraic Topology, Cambridge University Press, 2002. Section 1.1, "The Fundamental Group of the Circle", pp. 29–33. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
L. E. J. Brouwer, Über Abbildung von Mannigfaltigkeiten, Mathematische Annalen 71 (1911), 97–115. https://doi.org/10.1007/BF01456931
K. Borsuk, Drei Sätze über die n-dimensionale euklidische Sphäre, Fundamenta Mathematicae 20 (1933), 177–190. https://doi.org/10.4064/fm-20-1-177-190
Mathlib, Mathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting for covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean
Mathlib, Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean (the fundamental group). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

11 thms4 active usersReviewed

Completed

Algorithmic Game Theory Theoretical Computer Science·Captain: Shuze Chen

Algorithmic Game Theory I: Existence of Nash EquilibriumTextbook

Motivation

The strategic-form game is the basic object of noncooperative game theory, and the Nash equilibrium — a profile of randomized strategies from which no player benefits by deviating unilaterally — is its central solution concept. Nash proved in 1951 that every game with finitely many players and finite strategy sets has such an equilibrium (Nash, Non-cooperative games, Ann. Math. 54 (1951)); this single existence theorem is the reason the concept organizes the rest of the field, from the computational complexity of finding equilibria to the price of anarchy. The theorem is stated as Theorem 1.8 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), the source text of this mission series, whose first chapter (Tardos–Vazirani) also treats the two special cases that admit direct algorithmic proofs: two-person zero-sum games, where equilibria are exactly the optimal solutions of a dual pair of linear programs (von Neumann 1928; Theorem 1.11), and a simple linear market, where equilibrium prices are computed by an ascending tight-set algorithm (Theorem 1.17).

A timeline of the existence theorem: von Neumann (1928) proved the minimax theorem for two-person zero-sum games; Nash (1950, 1951) extended existence to arbitrary finite games, first via Kakutani's fixed-point theorem and then via Brouwer's. All known proofs of the general theorem pass through a fixed-point principle, and this is not an artifact: computing a Nash equilibrium is PPAD-complete (Daskalakis–Goldberg–Papadimitriou 2009; Chen–Deng–Teng 2009), and PPAD is precisely the complexity class of the fixed-point arguments.

Setting

A finite strategic-form game consists of a finite set $\iota$ of players, for each player $i$ a finite nonempty set $S_i$ of pure strategies, and for each player a payoff function $u_i : \prod_j S_j \to \mathbb{R}$ ; all players are utility maximizers. A mixed strategy for player $i$ is a probability distribution on $S_i$ , represented as a weight function $\sigma_i : S_i \to \mathbb{R}$ with $\sigma_i \ge 0$ and $\sum_{s} \sigma_i(s) = 1$ (a lottery). Players randomize independently, so a mixed profile $\sigma = (\sigma_i)_{i}$ induces the product distribution on pure strategy vectors, and player $i$ 's expected payoff is

U_i(\sigma) \;=\; \sum_{s \in \prod_j S_j} \Big(\prod_j \sigma_j(s_j)\Big)\, u_i(s).

A mixed profile $\sigma$ is a (mixed) Nash equilibrium if for every player $i$ and every lottery $\tau$ on $S_i$ , replacing $\sigma_i$ by $\tau$ does not increase $U_i$ .

A two-person zero-sum game is given by a matrix $A \in \mathbb{R}^{m \times n}$ : the row player picks a row distribution $p$ , the column player a column distribution $q$ , and the column player pays the row player $p^{\mathsf T} A q$ in expectation.

The market of §1.8.1 of the source has finitely many divisible goods, good $a$ in $s_a$ units, and finitely many buyers, buyer $j$ bringing budget $m_j > 0$ and interested in a nonempty set of goods; utilities are linear 0/1, so a buyer wants any goods from her interest set and none other. Market-clearing prices are positive prices under which each buyer can spend her whole budget on cheapest goods in her interest set while every good sells out exactly.

Formalization targets

Goal (capstone) — Theorem 1.8

\text{Every finite strategic-form game has a mixed Nash equilibrium.}

Stated for an arbitrary finite family of finite nonempty strategy types; no bound on the number of players, no genericity assumptions.

Supporting — Brouwer fixed-point theorem

K \subseteq E \text{ nonempty compact convex},\ E \text{ finite-dimensional},\ f : K \to K \text{ continuous} \implies \exists x,\ f(x) = x.

Mathlib currently has no form of Brouwer's theorem; every known proof of Theorem 1.8 needs it (or an equivalent), so it enters the mission as an explicit milestone rather than an assumed library fact.

Theorem 1.11 — zero-sum games

\exists\, p^\ast, q^\ast:\quad \forall p,\ p^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q^\ast, \quad \forall q,\ {p^\ast}^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q, \quad\text{and}\quad (p^\ast, q^\ast) \text{ is a mixed Nash equilibrium}

of the explicit two-player game with payoffs $A_{xy}$ to the row player and $-A_{xy}$ to the column player. The source states the result as: optimal solutions of a dual pair of LPs form a Nash equilibrium of the zero-sum game; the first two conjuncts are the saddle point that LP optimality amounts to, and the third states the Nash-equilibrium clause against the mission's own game vocabulary, so "zero-sum" is formal (the two payoffs sum to zero) rather than implicit in the shape of the statement.

Theorem 1.17 (existence form)

\text{The 0/1-utilities linear market admits market-clearing prices and allocations.}

The source proves this by an ascending-price algorithm and also bounds its running time; the complexity half has no formal counterpart in this mission.

Significance

The capstone is the foundation of the whole mission series: correlated equilibria, price-of-anarchy bounds, and mechanism-design characterizations in later missions all quantify over or compare against Nash equilibria, and the series inherits its game vocabulary (IsLottery, IsMixedProfile, expectedPayoff, IsMixedNash) from this mission.

Formalizing it produces the first Brouwer fixed-point theorem in this environment — a well-known gap in mathlib with reuse value far beyond game theory (every degree-theoretic and equilibrium-existence argument needs it). The zero-sum milestone yields the minimax theorem, reusable for the learning-dynamics mission that follows. All results here are classical and proved on paper; the work requested is machine-checked proof, not new mathematics.

Difficulty

The central difficulty is Brouwer. The standard routes are (i) Sperner's lemma plus a limit argument, which needs a formal theory of simplicial subdivisions that does not exist in mathlib; (ii) algebraic topology (no retraction of the ball onto the sphere), for which mathlib has singular homology but not yet the homology of spheres in usable form; (iii) analytic proofs (Milnor–Rogers). None is short; the milestone is deliberately stated for a general nonempty compact convex set in a finite-dimensional normed space so that any route serves, and so the lemma lands in reusable generality.

Given Brouwer, Theorem 1.8 still requires Nash's gain-function construction on the product of simplices and the verification that fixed points are equilibria — bookkeeping-heavy but standard. Theorem 1.11 does not need Brouwer: mathlib's Sion minimax theorem (Mathlib.Topology.Sion) applies to the bilinear payoff on the product of standard simplices, or one can argue by LP duality directly. Theorem 1.17 needs the tight-set/max-flow argument of Lemmas 1.15–1.16 or any direct construction of the equilibrium.

Formalization scope

Games are presented concretely: players form a finite index type, strategies a finite type per player, payoffs are functions into $\mathbb{R}$ ; mixed strategies are weight functions with a IsLottery predicate, not measure-theoretic distributions. Deviations in the equilibrium definition range over all lotteries (not only pure strategies): the pure-deviation reduction is a lemma a solver may prove, not part of the definition. Strategy sets are assumed nonempty in the capstone; the player set need not be. In the zero-sum milestone both dimensions are positive (Fin (m+1), Fin (n+1)), payoffs flow from the column player to the row player, stdSimplex plays the role of the mixed-strategy space, and the Nash-equilibrium conjunct is stated for the Boolean-indexed two-player game built by matrixGameStrat/zeroSumPayoff/matrixGameProfile from the definitions bundle. In the market milestone all supplies and budgets are positive, every buyer's interest set is nonempty, and every good has an interested buyer, matching the standing assumptions of §1.8.1; allocations are recorded as money spent, so the clearing condition is $\sum_j x_{ja} = p_a s_a$ with no division anywhere.

Trivializing readings are ruled out: the empty simplex has no lotteries, so nonemptiness hypotheses appear exactly where their absence would make an existence claim false (Brouwer on the empty set, games with an empty strategy set, zero-dimensional matrix games).

Selected references

J. F. Nash, Non-cooperative games, Annals of Mathematics 54 (1951), 286–295. DOI
J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100 (1928), 295–320. DOI
N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 1. DOI
C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, The complexity of computing a Nash equilibrium, SIAM J. Computing 39 (2009), 195–259. DOI

10 thms4 active usersReviewed

Completed

Theoretical Computer Science·Captain: marwahaha

Schönhage–Pan–Winograd Bound: omega < 2.522Research Paper

Motivation

The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound $\omega<c$ means that, over the field under consideration, $N\times N$ matrices can be multiplied using $O(N^{c+\varepsilon})$ arithmetic operations for every $\varepsilon>0$ . Improvements to $\omega$ are a central benchmark in algebraic complexity because matrix multiplication is also a basic subroutine in linear algebra, graph algorithms, and symbolic computation.

The existing Prove2Me mission formalizes Schönhage's bound $\omega<2.55$ from a concrete two-summand tensor degeneration. The present mission advances the same formal development to the next clean historical construction. Pan and Winograd found a simultaneous approximate algorithm for three matrix products; Romani recorded its tensor form and the parameter choice $n=11$ , $k=5$ , which gives $\omega\le 2.5218127\ldots$ . Schönhage's 1981 paper reports the equivalent bound $3\log 52/\log 110$ in the arbitrary-field setting. The exact formal target here is the slightly weaker rational inequality $\omega<1261/500=2.522$ .

Setting

For a field $K$ , the matrix-multiplication tensor $\langle a,b,c\rangle_K$ encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix:

\langle a,b,c\rangle_K =\sum_{i<a}\sum_{j<b}\sum_{\ell<c} e_{ij}\otimes e_{j\ell}\otimes e_{\ell i}.

A direct sum places several such tensors in disjoint coordinate blocks. A tensor $T$ has border rank at most $r$ when it is a polynomial degeneration of the diagonal tensor $I_r=\sum_{s<r}e_s\otimes e_s\otimes e_s$ . In the Lean development this relation is Degenerates T (TensorObj.diagObj K 3 r). The argument order matters: the first tensor is the target and the diagonal tensor is the source.

The platform already defines ordinary tensor rank, asymptotic tensor rank, the tensor-rank exponent matMulExp K, the equivalent Strassen-preorder exponent matMulExp_strassen K, and Schönhage's asymptotic sum inequality. This mission reuses those declarations. No alternative definition of $\omega$ is introduced.

Formalization targets

The goal has exactly the same quantified proposition as the existing $2.55$ mission, with only the rational endpoint changed:

\forall K\;[\mathrm{Field}(K)],\qquad \operatorname{matMulExp}(K)<\frac{1261}{500}.

The source construction to be formalized is

\underline R\!\left( \langle1,5,22\rangle_K\oplus \langle11,2,5\rangle_K\oplus \langle10,11,1\rangle_K \right)\le156.

Each summand has volume $110$ :

1\cdot5\cdot22=11\cdot2\cdot5=10\cdot11\cdot1=110.

The milestone chain records the degeneration, its asymptotic-rank consequence, the exact numerical implication

3\cdot110^{\omega^{\mathrm{Str}}_K/3}\le156 \quad\Longrightarrow\quad \omega^{\mathrm{Str}}_K<\frac{1261}{500},

and the resulting Strassen-form exponent bound. The public goal then transfers the bound to matMulExp K through the already established equality of the two exponent definitions.

Significance

Mathematically, this construction improves the concrete exponent certified by the existing mission from $2.55$ to $2.522$ without changing the surrounding theory. It isolates the first genuinely new ingredient after the accepted Schönhage example: a larger simultaneous tensor degeneration rather than a sharper numerical estimate for the old witness.

For formalization, the mission tests whether the current polynomial-degeneration API can express a historically important trilinear aggregation at realistic scale. Once the explicit witness is available, the remaining declarations form a reusable template for later bounds: a source tensor degeneration, an asymptotic-rank bound, a specialization of the asymptotic sum inequality, and a final exponent transfer. This creates a trustworthy stepping stone toward the Coppersmith--Winograd tensor and later laser-method analyses.

The $2.522$ theorem is known mathematically; the open work is its machine-checked Lean formalization. The exact numerical endpoint and every downstream bridge from the degeneration have already been checked locally. The explicit Pan--Winograd degeneration remains the substantive open milestone.

Difficulty

The central difficulty is not the logarithmic comparison. It is constructing and verifying the polynomial family whose leading nonzero coefficient is exactly the tagged direct sum of the three matrix-multiplication tensors and whose earlier coefficients vanish. The family has $156$ diagonal source slots and many indexed target coordinates. A proof must account for all mixed-coordinate terms and all cancellations uniformly over an arbitrary field.

Romani's published summary states the approximate-rank inequality but does not spell out a Lean-ready map between its trilinear forms and the platform's TensorObj.bigAdd coordinate spaces. A solver must therefore recover the source indexing carefully and prove that the resulting modewise linear maps have the required coefficients. Reversing the degeneration direction, conflating tensor rank with asymptotic rank, or silently assuming a characteristic-zero scalar identity would invalidate the result.

Formalization scope

All theorems quantify over an arbitrary type $K$ with [Field K], matching the existing Schönhage goal and the arbitrary-field statement of the source bound. Tensor spaces are finite-dimensional function spaces already packaged by MMObj; the three products are combined with TensorObj.bigAdd. Border rank is represented by the existing finitely supported polynomial-family predicate Degenerates. Because the source summary specifies approximate rank but not a leading order, the main degeneration milestone existentially quantifies that order instead of hard-coding one.

The mission includes no placeholder laser-value definition and makes no claim about the later $2.376$ analysis. It also excludes Schönhage's additional microscopic symmetrization improvement beyond $3\log52/\log110$ . A valid solution must construct the stated degeneration itself; a vacuous hypothesis or a redefinition of matMulExp is outside scope.

Reusable contributions include coefficient lemmas for polynomial tensor families, finite-index equivalences for direct sums, and generic aggregation identities that specialize to the $n=11$ , $k=5$ witness. Contributions that merely restate the target under stronger field hypotheses do not close the arbitrary-field milestone.

Selected references

A. Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981, pp. 434--455. DOI 10.1137/0210032.
Francesco Romani, Some Properties of Disjoint Sums of Tensors Related to Matrix Multiplication, CNR Nota Interna B80-4, February 1980, printed p. 6; journal version, SIAM Journal on Computing 11(2), 1982. Archived preprint and DOI 10.1137/0211020.
Avi Wigderson and Jeroen Zuiddam, Asymptotic Spectra: Theory, Applications and Extensions, 2023, for the tensor-preorder and asymptotic-rank framework reused by the Lean development. Author manuscript.

27 thms4 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times VIII: Path Coupling and Approximate CountingTextbook

Motivation

The coupling method of Mission III asks for a coupling of two copies of a chain from every pair of starting states — often painful to construct globally. Chapter 14 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) replaces that global demand by a local one. The path coupling technique of Bubley and Dyer says: put a connected graph structure on the state space, and couple one step of the chain only across edges; if each edge contracts in expectation, contraction propagates automatically along paths to arbitrary pairs of distributions. The bookkeeping runs through the transportation metric (Kantorovich distance) between distributions, whose theory — attainment by an optimal coupling, the triangle inequality — is developed on the way. The chapter's payoff is the sharpest elementary bound for sampling proper colorings (Theorem 14.8: the Glauber dynamics mixes in $O(n\log n)$ steps once $q>2\Delta$ ), and, through the sampling-to-counting reduction of Jerrum–Valiant–Vazirani, a polynomial-time approximation algorithm for counting colorings — the paradigm of the Markov chain Monte Carlo method as an algorithmic tool.

Setting

All chains live on a finite state space $V$ with a transition matrix $P$ ; $P^t(x,\cdot)$ is the time- $t$ distribution from $x$ , $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ the total variation distance, $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$ the worst-case distance to the stationary distribution $\pi$ , and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ the mixing time. A coupling of distributions $\mu,\nu$ is a distribution $q$ on $V\times V$ with marginals $\mu$ and $\nu$ .

Given a metric-like cost $\rho$ on pairs of states, the transportation metric between two distributions is the cheapest expected cost of moving one onto the other:

\rho_K(\mu,\nu)=\min\Bigl\{\sum_{x,y}\rho(x,y)\,q(x,y)\;:\;q\ \text{a coupling of}\ \mu,\nu\Bigr\}.

Given a connected graph structure $G$ on the state space with edge lengths $\ell\ge1$ , the path metric $\rho(x,y)$ is the least total length of a $G$ -path from $x$ to $y$ .

For the colorings application: a $q$ -coloring of the vertices of a graph is proper when adjacent vertices receive distinct colors, and the Glauber dynamics on proper colorings picks a uniform vertex and re-samples its color uniformly among the colors legal there; its stationary distribution is uniform on the proper colorings. Throughout, $n$ is the number of vertices and $\Delta$ the maximum degree of the graph being colored.

Formalization targets

Goal

Theorem 14.8, the capstone of Chapter 14: for the Glauber dynamics on proper $q$ -colorings, if $q>2\Delta$ then

t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{q-\Delta}{q-2\Delta}\;n\,\bigl(\log n-\log\varepsilon\bigr)\Bigr\rceil.

Milestones

Lemma 14.3 and Remark 14.2 — the transportation distance is attained by an optimal coupling, and satisfies the triangle inequality (so it is a genuine metric on distributions).
Theorem 14.6, path coupling (Bubley–Dyer) — if for every edge $\{x,y\}$ of a connected graph structure there is a coupling of the one-step distributions $P(x,\cdot),P(y,\cdot)$ contracting the path metric by $e^{-\alpha}$ in expectation, then one step of the chain contracts the transportation metric of arbitrary distribution pairs by $e^{-\alpha}$ .
Corollary 14.7 — under the same hypotheses, $d(t)\le e^{-\alpha t}\,\mathrm{diam}(V)$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil(\log\mathrm{diam}(V)-\log\varepsilon)/\alpha\rceil$ , where $\mathrm{diam}(V)$ is the largest path-metric distance between two states.
Theorem 14.12, approximate counting — for $q>2\Delta$ there is a randomized estimator, computed from an explicit polynomial number of independent uniform random seeds, which with probability at least $1-\eta$ estimates the number of proper $q$ -colorings within a $(1\pm\varepsilon)$ factor: rapid sampling yields rapid approximate counting.

Significance

The results. Path coupling converted the coupling method from an art into a calculus: one bounds a single-edge contraction constant, and the machinery does the rest. It is the standard tool for Glauber dynamics on colorings, independent sets, and other constraint-satisfaction models, and the $q>2\Delta$ colorings bound is its flagship application. Theorem 14.12 is the discrete embodiment of the Jerrum–Valiant–Vazirani equivalence between approximate counting and sampling — the conceptual foundation of the entire MCMC approach to $\#\mathrm P$ -hard counting problems.

Formalizing them. Mathlib has no transportation/Kantorovich metric in the finite setting, no path coupling, and nothing on approximate counting. The transportation-metric layer (optimal couplings, triangle inequality) is reusable far beyond this mission — it is the finite Wasserstein distance. The path-coupling theorem feeds directly into Mission IX (Ising) and is quoted throughout modern mixing literature.

Difficulty

The transportation metric asks for minimization over the (compact) polytope of couplings: attainment is a finite-dimensional compactness argument, and the triangle inequality requires gluing two optimal couplings along their common marginal — the classic construction that must be carried out with explicit finite sums here. Path coupling itself is an induction along geodesics of the path metric, with the subtlety that the composite coupling produced along a path need not be optimal, only admissible; the bookkeeping of the contraction constant through the induction is exactly the kind of argument Lean keeps honest. Theorem 14.8 instantiates the machinery: the single-edge coupling for colorings needs a careful case analysis of the proposed recolorings at the two endpoints (matching legal colors bijectively), and the contraction constant $(q-2\Delta)/(q-\Delta)$ emerges from counting disagreeing proposals. Theorem 14.12 layers a probabilistic-amplification argument (medians of means over independent runs) on top of the mixing bound; its combinatorial core — expressing $|\Omega|^{-1}$ as a telescoping product of marginal probabilities — is elementary but notation-heavy, and the formal statement quantifies over explicit seed spaces, so the whole estimator is a finite object.

Formalization scope

The transportation metric is an sInf over coupling costs (the coupling polytope is nonempty for genuine distributions, and attainment is part of the milestone, so the junk value never propagates); the path metric is an sInf over walk lengths in a connected graph. The Glauber dynamics on colorings is the restriction to proper colorings of the single-site heat-bath chain of Mission II, matching §3.3 of the book; its state space is the subtype of proper colorings, nonempty whenever $q>2\Delta$ (a fact the hypotheses of the goal supply). Mixing-time upper bounds are stated with the book's explicit ceilings, so no rounding slack is hidden. In Theorem 14.12 the estimator is presented concretely as a function of finitely many uniform seeds, and "with probability $\ge1-\eta$ " is a counting inequality over the seed space — no measure theory enters. Contributions of intermediate lemmas (optimal-coupling gluing, geodesic decompositions, colorings edge-coupling) are welcome and will be reused by Mission IX.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
R. Bubley, M. Dyer, Path coupling: a technique for proving rapid mixing in Markov chains, FOCS 1997. https://doi.org/10.1109/SFCS.1997.646111
M. Jerrum, A very simple algorithm for estimating the number of k-colorings of a low-degree graph, Random Structures Algorithms 7 (1995). https://doi.org/10.1002/rsa.3240070205
M. Jerrum, L. Valiant, V. Vazirani, Random generation of combinatorial structures from a uniform distribution, Theoret. Comput. Sci. 43 (1986). https://doi.org/10.1016/0304-3975(86)90174-X

9 thms4 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times VI: Networks, Hitting Times, and Cover TimesTextbook

Motivation

A reversible Markov chain is an electrical network: states are nodes, and the conductance $c(x,y)=\pi(x)P(x,y)$ turns hitting probabilities into voltages and hitting times into resistances. This dictionary, going back to Kakutani and popularized by Doyle and Snell, converts probabilistic estimates into the physical laws of circuits — series/parallel reduction, energy minimization, monotonicity under edge removal. Chapters 9–11 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the dictionary and its two crown results: the commute time identity of Chandra–Raghavan–Ruzzo–Smolensky–Tiwari, $\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)=c_G\,R(a\leftrightarrow b)$ , and the Matthews method bounding cover times by hitting times with harmonic-number precision.

Setting

A network is a symmetric nonnegative conductance function $c$ on pairs of vertices; the associated walk moves with probabilities

P(x,y)=c(x,y)/c(x)

where $c(x)=\sum_y c(x,y)$ , and $c_G=\sum_x c(x)$ . A function $h$ is harmonic at $x$ if $h(x)=\sum_y P(x,y)h(y)$ . The voltage with boundary values $1$ at $a$ and $0$ at $z$ is $W(x)=\mathbb P_x\{\tau_a<\tau_z\}$ , the harmonic extension of its boundary data; the current flowing out of $a$ has strength $\|I\|=\sum_y c(a,y)\,[W(a)-W(y)]$ , and the effective resistance is $R(a\leftrightarrow z)=\|I\|^{-1}$ . A flow from $a$ to $z$ is an antisymmetric edge function obeying the node law off $\{a,z\}$ ; its energy is $\mathcal E(\theta)=\sum_e\theta(e)^2/c(e)$ . Hitting times $\tau_S=\min\{t\ge0:X_t\in S\}$ , their expectations, the Green's function $G_{\tau_z}(a,x)$ , the maximal hitting time $t_{\mathrm{hit}}$ , and the cover time $t_{\mathrm{cov}}$ (expected time to visit every state, maximized over starts) all use the trajectory calculus of Mission I.

Formalization targets

Goal

\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)\;=\;c_G\,R(a\leftrightarrow b).

This is Proposition 10.6, the commute time identity — the exact bridge between the probabilistic and electrical sides, and the engine of the transience/recurrence theory of Mission XII.

Milestones

Reversibility and stationarity of the network walk with $\pi(x)=c(x)/c_G$ (§9.1); Proposition 9.1 (existence and uniqueness of harmonic extensions with given boundary values, $h(x)=\mathbb E_x f(X_{\tau_B})$ ); Lemma 9.6 (the Green's function identity $G_{\tau_z}(a,a)=c(a)R(a\leftrightarrow z)$ ); Theorem 9.10 (Thomson's principle: $R(a\leftrightarrow z)$ is the minimal energy of a unit flow, attained); Theorem 9.12 (Rayleigh monotonicity: lowering conductances raises effective resistance); Lemma 10.1 (the random target lemma: $\sum_y\mathbb E_a(\tau_y)\pi(y)$ does not depend on $a$ ); Corollary 10.8 (the resistance triangle inequality); Theorem 11.2 (Matthews: $t_{\mathrm{cov}}\le t_{\mathrm{hit}}\,(1+\tfrac12+\dots+\tfrac1n)$ ); Proposition 11.4 (the matching Matthews lower bound over subsets).

Significance

The results. The commute time identity computes hitting times from circuit reductions — this is how hitting times on trees, tori and glued graphs are actually evaluated — and, through Thomson and Rayleigh, makes them monotone under graph operations, something invisible probabilistically. The Matthews bounds pin cover times up to a $\log n$ factor in complete generality; they are the tool behind cover-time results for lamplighter groups in Mission XI's sequel. Green's function identities feed Mission XII's recurrence theory, where $R(a\leftrightarrow\infty)$ decides transience.

Formalizing them. Mathlib has graph Laplacians but no electrical network theory: no effective resistance, no flows, no energy, no Thomson/Rayleigh, no hitting or cover times. This mission publishes that layer over the trajectory calculus of Mission I. It is the most reusable single block of the series outside Missions I–II: effective resistance on finite networks is of independent interest to combinatorics (spanning trees, spectral sparsification) well beyond mixing times.

Difficulty

The identity chain behind the goal runs: Green's function of the stopped walk $\to$ escape probability $\mathbb P_a\{\tau_z<\tau_a^+\}=\bigl(c(a)R(a\leftrightarrow z)\bigr)^{-1}$ (via harmonic uniqueness) $\to$ the Aldous–Fill occupation identity $G_\tau(a,x)=\mathbb E_a(\tau)\pi(x)$ for stopping times with $X_\tau=a$ — each step is a manipulation of infinite series of trajectory sums whose exchange steps (splitting a path at its first visit, last-exit decompositions) need summability from Mission I's Lemma 1.13. Thomson's principle is a finite-dimensional convex minimization: existence of the minimizer needs a compactness or completing-the-square argument, and the identification of the minimizer with the current flow needs the cycle law; the naive "differentiate the energy" route must be made exact. Matthews' method is a clean but genuinely clever argument — a uniformly random ordering of targets and the harmonic-number telescoping; the formal cost is the exchangeability of the randomized order against the chain, handled combinatorially.

Formalization scope

Networks are functions $c:V\times V\to\mathbb R$ with a symmetry-and-nonnegativity predicate; loops are permitted; connectivity enters as irreducibility of the induced walk. The voltage is defined probabilistically as $\mathbb P_x\{\tau_a<\tau_z\}$ (the book's harmonic characterization is Proposition 9.1); $R(a\leftrightarrow z)$ is the reciprocal of the explicit current strength, with total division junk when $a,z$ are disconnected — statements carry irreducibility so this does not arise. Energy counts each undirected edge once, formalized as half the ordered double sum, and $0^2/0=0$ handles absent edges. Cover times are tail sums of the explicit event "some state unvisited". The Matthews lower bound is stated with an arbitrary lower bound $m$ for the pairwise hitting times of the subset $A$ — equivalent to the book's min over pairs and easier to instantiate.

Welcome contributions: series/parallel reduction laws, the cycle and node law API for flows, escape-probability lemmas — all reused in Mission XII's infinite-network arguments.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
P. G. Doyle, J. L. Snell, Random Walks and Electric Networks, MAA, 1984. https://arxiv.org/abs/math/0001057
A. K. Chandra, P. Raghavan, W. L. Ruzzo, R. Smolensky, P. Tiwari, The electrical resistance of a graph captures its commute and cover times, STOC 1989. https://doi.org/10.1145/73007.73062
P. Matthews, Covering problems for Markov chains, Ann. Probab. 16 (1988). https://doi.org/10.1214/aop/1176991894

15 thms4 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary DistributionTextbook

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary Distribution

Motivation

Finite Markov chains are the basic model for memoryless random dynamics: card shuffles, random walks on graphs and groups, Monte Carlo samplers, and queueing systems are all chains on a finite state space. The single most used fact about them is that an irreducible chain has exactly one stationary distribution — a probability vector $\pi$ with $\pi = \pi P$ — and that this $\pi$ is strictly positive and encodes the long-run behaviour of the chain through the return-time identity $\pi(x) = 1/\mathbb{E}_x(\tau_x^+)$ . Every later result in the theory of mixing times (convergence theorems, coupling bounds, spectral methods, cutoff) is a statement about the distance of the chain from this $\pi$ , so nothing in the subject can be formalized before this mission is.

This mission is the first in a series formalizing D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times (AMS, 2009), covering Chapters 1–2: the basic vocabulary of finite chains (stochastic matrices, irreducibility, period, reversibility, time reversal, random walks on graphs and groups) and the classical examples of Chapter 2 (gambler's ruin, coupon collecting, the reflection principle for simple random walk on $\mathbb{Z}$ ). Later missions in the series build on the definitions published here.

Setting

A chain on a finite state space $\Omega$ is presented by its transition matrix, a matrix $P \in \mathbb{R}^{\Omega\times\Omega}$ with nonnegative entries whose rows sum to $1$ . A distribution is a row vector $\mu$ with nonnegative entries summing to $1$ ; one step of the chain carries $\mu$ to $\mu P$ , and the $t$ -step transition probabilities are the entries of the matrix power $P^t$ .

The chain is irreducible if for all states $x, y$ there is a $t$ with $P^t(x,y) > 0$ . The period of a state $x$ is $\gcd\,\mathcal{T}(x)$ where $\mathcal{T}(x) = \{t \ge 1 : P^t(x,x) > 0\}$ , and the chain is aperiodic if every state has period $1$ . A distribution $\pi$ is stationary if $\pi P = \pi$ , and $\pi$ and $P$ are in detailed balance (the chain is reversible) if $\pi(x)P(x,y) = \pi(y)P(y,x)$ for all $x,y$ .

Trajectory events over a finite horizon are finite sums of path weights: a length- $t$ trajectory is a function $\omega : \{0,\dots,t\} \to \Omega$ , with weight $\prod_{i<t} P(\omega_i, \omega_{i+1})$ conditional on its starting state. The tail probability $\mathbb{P}_x\{\tau_z^+ > t\}$ of the first hitting time $\tau_z^+ = \min\{t \ge 1 : X_t = z\}$ is the sum of the weights of the trajectories from $x$ that avoid $z$ at times $1,\dots,t$ , and expectations of hitting times are recovered by the tail-sum formula $\mathbb{E}(Y) = \sum_{t\ge0} \mathbb{P}\{Y > t\}$ , formalized as a tsum over $t$ .

Formalization targets

Goal

$\text{$P$ stochastic and irreducible on a finite nonempty $\Omega$} \;\Longrightarrow\; \exists!\, \pi,\ \pi = \pi P .$

This is Corollary 1.17 of the book. It asserts only existence and uniqueness, leaving the finer structure of $\pi$ to the milestones; it is the weakest statement on which the rest of the series can stand, which is why it is the goal.

Milestones toward and around the goal

The milestone list follows the book's own route: well-definedness of the period (Lemma 1.6), positivity of some matrix power for irreducible aperiodic chains (Proposition 1.7), finiteness of expected hitting times (Lemma 1.13), existence of a positive stationary distribution together with

\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1

(Proposition 1.14), constancy of harmonic functions (Lemma 1.16), stationarity from detailed balance (Proposition 1.19), the stationary and reversible measure $\pi(x) = \deg(x)/2|E|$ of simple random walk on a graph (Examples 1.12 and 1.20), the time reversal $\hat P$ and its path-reversal identity (Proposition 1.22), and the random walks on finite groups of Section 2.6 (Propositions 2.12–2.14). From Chapter 2 the list adds the gambler's ruin formulas $\mathbb{P}_k\{X_\tau = n\} = k/n$ and $\mathbb{E}_k(\tau) = k(n-k)$ (Proposition 2.1), the coupon collector expectation $n\sum_{k\le n} 1/k$ and tail bound $e^{-c}$ (Propositions 2.3 and 2.4), and the reflection principle and the bound $\mathbb{P}_k\{\tau_0 > r\} \le 12k/\sqrt{r}$ for simple random walk on $\mathbb{Z}$ (Lemma 2.18 and Theorem 2.17).

Significance

The result itself. Existence and uniqueness of $\pi$ is the pivot on which the entire quantitative theory turns: it defines the target of convergence, and the identity $\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1$ ties the stationary measure to return times, which later missions use for hitting-time and cover-time results. Detailed balance is the practical tool by which stationary measures of graph and group walks are computed, and the Chapter 2 examples (gambler's ruin, coupon collecting, reflection) are the standard building blocks reused throughout the book — the coupon collector bound, for instance, is exactly the estimate behind the $n \log n + cn$ analysis of the top-to-random shuffle in a later mission of this series.

Formalizing it. Mathlib currently has no theory of finite Markov chains: no stochastic-matrix predicate, no stationary distribution, no periodicity, no hitting times. Everything proved in this mission is new formal mathematics, and the definition layer published here (mm_basic, mm_path, mm_classical) is the shared foundation that all twelve subsequent missions of the series import. All results are classical and have textbook proofs; none has a machine-checked proof.

Difficulty

The delicate point is the existence proof. The natural first idea — extract $\pi$ from an eigenvector of $P^{\mathsf T}$ for eigenvalue $1$ , or invoke a fixed-point theorem — either does not give positivity and nonnegativity without further work, or uses compactness machinery (Brouwer) that is unavailable. The book's proof instead builds $\tilde\pi(y) = \mathbb{E}_z(\text{visits to } y \text{ before } \tau_z^+)$ and verifies $\tilde\pi P = \tilde\pi$ by reindexing trajectory sums; formalizing it requires managing infinite series of path sums (summability from the geometric tail bound of Lemma 1.13, exchanging tsum with finite sums, splitting a trajectory at its last step). The uniqueness half is linear algebra via constancy of harmonic functions (Lemma 1.16), which is elementary but requires a maximum-principle argument over a finite state space. The reflection principle and Theorem 2.17 are finite combinatorics on $\pm 1$ paths — the bijection is easy to describe and fiddly to implement.

Formalization scope

States form a Fintype with decidable equality; chains are Matrix V V ℝ with the row-stochasticity predicate IsStochastic; distributions are functions V → ℝ with the predicate IsDist. Everything is distribution-side: no probability space or measure theory is used. The period is formalized as $\sup\{d : d \mid t \text{ for all } t \in \mathcal{T}(x)\}$ , which equals $\gcd \mathcal{T}(x)$ when $\mathcal{T}(x) \neq \varnothing$ and takes the junk value $0$ otherwise. Expectations of hitting times are tsums of tail probabilities, with the usual junk value $0$ for non-summable families — the statements are arranged (e.g. multiplicatively, $\pi(x)\cdot\mathbb{E}_x(\tau_x^+) = 1$ ) so that junk values cannot make them vacuously true. Existence statements carry a Nonempty V hypothesis; irreducibility on the empty space is vacuous, and without nonemptiness the goal would be false, not trivial. The coupon collector and the walk on $\mathbb{Z}$ are presented directly by their driving randomness (uniform draws Fin t → Fin n, uniform sign strings Fin r → Bool), so those probabilities are elementary counting; in particular the reflection principle is stated as an equality of cardinalities of sets of sign strings — this is equivalent to the probabilistic statement because all $2^r$ strings are equally likely.

Contributions welcome beyond the milestone list: simp lemmas for the definition layer, the taboo-matrix representation of avoidance probabilities (useful for Lemma 1.13), and any interface lemmas connecting pathWeight sums to matrix powers — these will be reused by every later mission in the series.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
J. R. Norris, Markov Chains, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9780511810633
D. Aldous, J. A. Fill, Reversible Markov Chains and Random Walks on Graphs, 2002 (unfinished monograph). https://www.stat.berkeley.edu/~aldous/RWG/book.html

20 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: Shuze Chen

Introduction to Linear Optimization XIII: Lagrangean Duality and Integer ProgrammingTextbook

Linear programming has a complete duality theory; integer programming does not — and the Lagrangean dual measures exactly how far duality reaches. This mission formalizes the duality theory of integer programming from Section 11.4 of Bertsimas–Tsitsiklis, built on the general linear programming duality of Section 4.10. For the integer program

Z_{IP} = \min\{c'x : Ax \ge b,\ Dx \ge d,\ x \text{ integer}\}

with integer data, the complicating constraints $Ax \ge b$ are dualized with multipliers $p \ge 0$ over the tractable set $X = \{x \text{ integer} \mid Dx \ge d\}$ : the dual function is

Z(p) = \min_{x \in X}\big(c'x + p'(b - Ax)\big)

and the Lagrangean dual is $Z_D = \max_{p \ge 0} Z(p)$ . Weak duality $Z_D \le Z_{IP}$ (Theorem 11.2) always holds, but strong duality can fail. The convex hull $CH(X)$ of the integer points of a polyhedron with integer data is itself a polyhedron (Theorem 11.3, Meyer's theorem), and the capstone — Theorem 11.4, the central result of Section 11.4 — identifies the Lagrangean dual exactly: $Z_D$ equals the optimal cost of the linear program

\min\{c'x : Ax \ge b,\ x \in CH(X)\}

. This is the geometric explanation of the strength of Lagrangean relaxation, yields the bound ordering $Z_{LP} \le Z_D \le Z_{IP}$ , and Corollary 11.1 characterizes exactly when the bounds collapse. The polyhedral engine is the general weak/strong duality pair (Theorems 4.17/4.18) over a primal $\min c'x$ s.t. $Ax \ge b$ , $x \in P = \{x \mid Dx \ge d\}$ , and the formulation-strength comparison $P_{sub} \subseteq P_{cut}$ of Theorem 10.1 supplies the motivating principle that tighter relaxations of the same integer set give sharper bounds.

18 thms4 active usersReviewed