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.
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.
Schoolbook matrix multiplication takes n3 operations. The exponent ω is the infimum of all τ such that two n×n matrices can be multiplied in O(nτ) arithmetic operations; trivially ω≥2, and ω=2 is conjectured but open.
Strassen gave the first nontrivial bound, ω<2.81, in 1969, and introduced the laser method in 1986 to reach ω<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 ω<2.371339 in 2025, and the current record is ω<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?
Rudin PMA III: Numerical Sequences and SeriesTextbook
## Motivation
Chapter 3 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) develops the theory of convergence for sequences and series of numbers: subsequential
limits and upper limits, the Cauchy criterion, the comparison, root and ratio tests, power
series, summation by parts, and products of series. Its final section answers a question that
distinguishes analysis from algebra: an infinite sum is not a sum. For a series that converges
only conditionally, the value of the sum depends on the order of the terms, and **Riemann's
rearrangement theorem** (Theorem 3.54) makes the dependence total — by reordering the terms one
can prescribe *any* pair of limit inferior and limit superior for the partial sums, including
divergence to $\pm\infty$.
This mission is the third in a series formalizing Rudin Chapters 1–11. It uses the real and
complex number systems of Mission I and the compactness results of Mission II, and it supplies
the convergence machinery used by Missions VII and VIII.
## Setting
A **series** $\sum a_n$ is the sequence of **partial sums**
$s_n = a_0 + a_1 + \dots + a_{n-1}$; the series **converges to** $s$ when $s_n \to s$, and
**converges absolutely** when $\sum \|a_n\|$ converges. The **upper limit** of a real sequence
is $s^{*} = \limsup_{n} s_n$, taken in the extended real number system
$[-\infty, +\infty]$, and a **subsequential limit** is a limit of a subsequence there. A
**rearrangement** of $\sum a_n$ is a series $\sum a_{\sigma(n)}$ with $\sigma$ a bijection of
the index set onto itself.
The distinction that drives the chapter: for real or complex terms, absolute convergence is
equivalent to convergence of $\sum a_{\sigma(n)}$ for *every* $\sigma$, to the same sum
(Theorem 3.55), whereas mere convergence is not.
## Formalization targets
### Goal — Riemann's rearrangement theorem (Theorem 3.54)
Let $\sum a_n$ be a series of real numbers which converges but not absolutely, and let
$-\infty \le \alpha \le \beta \le +\infty$. Then there is a rearrangement $\sum a_{\sigma(n)}$
with partial sums $s_n'$ such that
$$\liminf_{n \to \infty} s_n' = \alpha, \qquad \limsup_{n \to \infty} s_n' = \beta .$$
### Milestones
$$s^{*} \text{ is a subsequential limit, and } x > s^{*} \Rightarrow s_n < x \text{ eventually; } s^{*} \text{ is unique with these properties} \qquad (3.17)$$
$$\textstyle\sum a_n \text{ converges} \iff \forall \varepsilon>0\ \exists N\ \forall m \ge n \ge N,\ \big|\sum_{k=n}^{m} a_k\big| \le \varepsilon \qquad (3.22)$$
$$\textstyle\sum_{n\ge 0} x^n = \tfrac{1}{1-x}\ (0 \le x < 1), \text{ divergence for } x \ge 1 \qquad (3.26)$$
$$\textstyle\sum n^{-p} \text{ converges} \iff p > 1 \qquad (3.28)$$
$$e = \textstyle\sum 1/n! = \lim_n (1 + 1/n)^n \qquad (3.30,\ 3.31)$$
$$\alpha = \limsup \|a_n\|^{1/n} < 1 \Rightarrow \text{convergence}, \ \alpha > 1 \Rightarrow \text{divergence} \qquad (3.33)$$
$$\text{ratio test} \qquad (3.34)$$
$$\text{radius of convergence of } \textstyle\sum c_n z^n \qquad (3.39)$$
$$\text{bounded partial sums} + b_n \downarrow 0 \Rightarrow \textstyle\sum a_n b_n \text{ converges} \qquad (3.42)$$
$$\text{absolute convergence} \Rightarrow \text{convergence} \qquad (3.45)$$
$$\text{Cauchy product: } \textstyle\sum c_n = AB \text{ when } \sum a_n \text{ converges absolutely} \qquad (3.50)$$
## Significance
The rearrangement theorem is the precise statement of why conditional convergence must be
handled with care, and it is the reason later chapters insist on *uniform* or *absolute*
hypotheses before interchanging limit operations: Theorem 3.50 (Mertens) needs absolute
convergence of one factor, and the Fourier and Lebesgue theories of Chapters 8 and 11 are built
on $L^2$ and $L^1$ convergence rather than pointwise summation. The supporting milestones are
the standard convergence tests, which are used constantly in the rest of the book, and the
characterization of $\limsup$, which is the tool that makes the root test and the radius of
convergence formula precise.
Mathlib's `Summable`/`HasSum` express *unconditional* summability, which over $\mathbb{R}$ and
$\mathbb{C}$ is equivalent to absolute convergence. The conditionally convergent series that
this chapter is about are therefore invisible to that API, and the mission works with partial
sums directly. Some of the classical tests exist in Mathlib in `Summable` form and will need
restating; the rearrangement theorem itself has to be built.
## Difficulty
The goal theorem is a construction, not an estimate: one splits $a_n$ into its positive and
negative parts $p_n, q_n$, observes that $\sum p_n$ and $\sum q_n$ both diverge while
$p_n, q_n \to 0$, and then alternately draws blocks of positive and negative terms to overshoot
targets $\beta_m \to \beta$ and undershoot targets $\alpha_m \to \alpha$. Formalizing the
alternating greedy construction requires defining the permutation recursively together with the
invariant that every index is eventually used — the bookkeeping, not the analysis, is the hard
part. The endpoint cases $\alpha = -\infty$ or $\beta = +\infty$ must be carried through the
same construction rather than treated separately.
## Formalization scope
Conventions fixed by this mission:
* Series convergence is `Rudin.SeriesConvergesTo` / `Rudin.SeriesConverges`, defined through
`Rudin.partialSum a n = ∑_{i<n} a i`. Absolute convergence is `Rudin.SeriesConvergesAbsolutely`.
Mathlib's `Summable` is deliberately *not* used, since it would collapse the distinction the
chapter is about.
* Upper and lower limits are taken in `EReal` via `Filter.limsup`/`Filter.liminf`, so
$\pm\infty$ are allowed as values of $\alpha$ and $\beta$ in the goal.
* Rearrangements are `Equiv.Perm ℕ`, and the rearranged series is `fun k => a (σ k)`.
* Series with complex terms are used where Rudin allows complex terms (3.22, 3.33, 3.34, 3.39,
3.42, 3.45, 3.50); the goal is about real series, as in the book.
* The radius-of-convergence milestone is stated as `α‖z‖ < 1` and `α‖z‖ > 1` rather than
`‖z‖ < 1/α`, to avoid inversion in `EReal`.
The goal is not vacuous: conditionally convergent series exist (the alternating harmonic
series), so the hypotheses are satisfiable, and the conclusion fixes both limit points exactly
rather than merely bounding them.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 3 (pp. 47–78).
- Bernhard Riemann, *Über die Darstellbarkeit einer Function durch eine trigonometrische
Reihe*, Abhandlungen der Königlichen Gesellschaft der Wissenschaften zu Göttingen 13 (1867),
Section 3.
## Motivation
Chapter 5 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) is the differential calculus of one real variable, developed from the definition of the
derivative as a limit of difference quotients. Its organizing result is the **mean value
theorem** and the family of consequences that follow from it: monotonicity criteria,
L'Hospital's rule, and — the chapter's capstone — **Taylor's theorem** (Theorem 5.15), which
approximates a function by a polynomial of degree $n-1$ and expresses the error exactly as a
single $n$-th derivative evaluated at an unspecified intermediate point.
Taylor's theorem is what makes differentiability quantitatively useful. It is the tool that
turns local smoothness into explicit error bounds, and the estimates of Chapter 8 for the
exponential, trigonometric and Gamma functions all rest on it.
This mission is the fifth in a series formalizing Rudin Chapters 1–11; it uses the continuity
and compactness results of Mission IV.
## Setting
Let $f$ be real-valued on $[a,b]$. For $x \in [a,b]$ the **derivative** is
$$f'(x) = \lim_{t \to x} \frac{f(t) - f(x)}{t - x},$$
whenever the limit exists. Higher derivatives $f', f'', \dots, f^{(n)}$ are defined by
iteration; $f^{(n)}$ exists on a set only if $f^{(n-1)}$ exists in a neighbourhood of each of
its points. $f$ has a **local maximum** at $x$ if $f(t) \le f(x)$ for all $t$ near $x$.
Given a positive integer $n$ and a point $\alpha$, the **Taylor polynomial** of $f$ at $\alpha$
of degree $n-1$ is
$$P(t) = \sum_{k=0}^{n-1} \frac{f^{(k)}(\alpha)}{k!}\,(t-\alpha)^k .$$
## Formalization targets
### Goal — Taylor's theorem (Theorem 5.15)
Let $f^{(n-1)}$ be continuous on $[a,b]$, let $f^{(n)}(t)$ exist for $t \in (a,b)$, and let
$\alpha \ne \beta$ be points of $[a,b]$. Then there is a point $x$ strictly between $\alpha$ and
$\beta$ such that
$$f(\beta) \;=\; \sum_{k=0}^{n-1} \frac{f^{(k)}(\alpha)}{k!}\,(\beta-\alpha)^k \;+\; \frac{f^{(n)}(x)}{n!}\,(\beta-\alpha)^n .$$
For $n = 1$ this is exactly the mean value theorem.
### Milestones
$$f \text{ differentiable at } x \Rightarrow f \text{ continuous at } x \qquad (5.2)$$
$$\text{local maximum at an interior } x,\ f'(x) \text{ exists} \Rightarrow f'(x) = 0 \qquad (5.8)$$
$$(f(b)-f(a))\,g'(x) = (g(b)-g(a))\,f'(x) \text{ for some } x \in (a,b) \qquad (5.9)$$
$$f(b) - f(a) = (b-a) f'(x) \text{ for some } x \in (a,b) \qquad (5.10)$$
$$f' \ge 0 \Rightarrow f \text{ increasing}; \quad f' = 0 \Rightarrow f \text{ constant}; \quad f' \le 0 \Rightarrow f \text{ decreasing} \qquad (5.11)$$
$$f'(a) < A < f'(b) \Rightarrow f'(x) = A \text{ for some } x \in (a,b) \qquad (5.12)$$
$$f, g \to 0 \text{ and } f'/g' \to A \Rightarrow f/g \to A \qquad (5.13)$$
$$\|f(b) - f(a)\| \le (b-a)\,\|f'(x)\| \text{ for some } x \in (a,b),\ f \text{ vector-valued} \qquad (5.19)$$
## Significance
The mean value theorem converts a hypothesis about derivatives into a statement about
increments, and everything in the chapter is an application of that conversion. Monotonicity
criteria (5.11) are the basis of every "the function is increasing, hence injective" argument,
including the change of variable in Chapter 6. Darboux's theorem (5.12) shows that derivatives,
though not necessarily continuous, cannot have simple discontinuities — a fact that is easy to
state and impossible to guess from the definition. Theorem 5.19 is the form of the mean value
theorem that survives for vector-valued functions: the equality is lost (there need be no single
point where the vector increment is proportional to the derivative), and only the inequality
remains; the same phenomenon dictates the statements of Chapter 9.
Mathlib contains the mean value theorem, L'Hospital's rule, and a Taylor theorem with various
remainder forms. The value of this mission is a statement of Taylor's theorem in Rudin's exact
formulation — arbitrary distinct endpoints $\alpha, \beta$ in $[a,b]$, hypotheses only on
$f^{(n-1)}$ and $f^{(n)}$, an intermediate point $x$ strictly between them — and the derivation
of the chapter's other results in a form the later missions can quote.
## Difficulty
Taylor's theorem is proved by choosing the constant $M$ so that
$f(\beta) = P(\beta) + M(\beta-\alpha)^n$ and applying Rolle's theorem $n$ times to
$g(t) = f(t) - P(t) - M(t-\alpha)^n$; the bookkeeping is in tracking that $g^{(k)}(\alpha) = 0$
for $k < n$ and that each application produces a new intermediate point strictly inside the
previous interval. In a proof assistant the iteration is the awkward part: the induction is on
$n$ with the interval shrinking, and the statement must be general enough in $\alpha$ and
$\beta$ (either order) for the inductive step to apply. The hypothesis that $f^{(n)}$ exists
only on the *open* interval, while $f^{(n-1)}$ is merely continuous on the closed one, must be
preserved — strengthening it to $C^n$ on $[a,b]$ would make the statement weaker than Rudin's.
## Formalization scope
Conventions fixed by this mission:
* Derivatives are Mathlib's `deriv` and `iteratedDeriv`, which are total functions returning
`0` where the function is not differentiable; every statement therefore carries explicit
differentiability hypotheses exactly where Rudin states them.
* Intervals are `Set.Icc a b` and `Set.Ioo a b`, and "for some $x$ between $\alpha$ and
$\beta$" is stated as an explicit disjunction, since the goal does not assume
$\alpha < \beta$.
* Vector-valued functions in 5.19 take values in `EuclideanSpace ℝ (Fin k)`, and the conclusion
is the inequality, not an equality — the equality version is false, as Rudin notes.
* L'Hospital's rule is formalized in the $0/0$ case at a finite left endpoint, which is the
first case of Rudin's Theorem 5.13; the $\infty$ case and the limits at $\pm\infty$ are not
part of this mission.
* Local maxima in 5.8 are stated with an explicit radius, matching Rudin's Definition 5.7.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 5 (pp. 103–119).
## Motivation
Convergence, continuity and integration are all statements about *nearness*, and Chapter 2 of
Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill, 1976) isolates
the amount of structure needed to talk about nearness: a metric. The chapter's payoff is a
single theorem, **Heine–Borel** (Theorem 2.41), which says that in $\mathbb{R}^k$ — and, as the
chapter's examples show, only in spaces resembling it — three very different-looking finiteness
conditions coincide: being closed and bounded, admitting finite subcovers, and forcing every
infinite subset to accumulate. Nearly every existence theorem in the rest of the book (a
continuous function on $[a,b]$ attains its maximum, is uniformly continuous, is
Riemann-integrable) is an application of that equivalence.
This mission is the second in a series formalizing Rudin Chapters 1–11. It builds on the
number systems of Mission I and supplies the topological input for Missions III–VII.
## Setting
A **metric space** is a set $X$ with a distance $d : X \times X \to \mathbb{R}$ that is
positive for distinct points, symmetric, and satisfies the triangle inequality. The
**neighbourhood** $N_r(p)$ is the set of $q$ with $d(p,q) < r$. A point $p$ is a **limit
point** of $E \subseteq X$ if every neighbourhood of $p$ contains a point of $E$ different
from $p$; $E$ is **closed** if it contains all its limit points, **open** if each of its points
has a neighbourhood inside $E$, and its **closure** $\bar E$ is $E$ together with its limit
points. $E$ is **perfect** if it is closed and every point of $E$ is a limit point of $E$, and
**bounded** if it is contained in some neighbourhood.
An **open cover** of $E$ is a family of open sets whose union contains $E$; $K$ is **compact**
if every open cover of $K$ has a finite subcover. A **$k$-cell** is a product
$\{x \in \mathbb{R}^k : a_j \le x_j \le b_j \text{ for all } j\}$. Two sets $A, B$ are
**separated** if $\bar A \cap B = A \cap \bar B = \varnothing$, and $E$ is **connected** if it
is not the union of two nonempty separated sets.
## Formalization targets
### Goal — Heine–Borel (Theorem 2.41)
For $E \subseteq \mathbb{R}^k$, the following are equivalent:
$$
\text{(a) } E \text{ closed and bounded} \quad\Longleftrightarrow\quad
\text{(b) } E \text{ compact} \quad\Longleftrightarrow\quad
\text{(c) every infinite } S \subseteq E \text{ has a limit point in } E .
$$
### Milestones
$$\textstyle\bigcup_n E_n \text{ countable when each } E_n \text{ is} \qquad (2.12)$$
$$\{0,1\}^{\mathbb{N}} \text{ is uncountable} \qquad (2.14)$$
$$\text{arbitrary unions of open sets, finite intersections of open sets, and the closed duals} \qquad (2.24)$$
$$\bar E = E \cup E', \quad \bar E \text{ closed}, \quad \bar E = E \Leftrightarrow E \text{ closed}, \quad E \subseteq F \text{ closed} \Rightarrow \bar E \subseteq F \qquad (2.27)$$
$$\sup E \in \bar E \qquad (2.28)$$
$$\text{open-cover compactness} \Leftrightarrow \text{compactness} \qquad (2.32)$$
$$F \subseteq K,\ F \text{ closed},\ K \text{ compact} \Rightarrow F \text{ compact} \qquad (2.35)$$
$$\text{finite intersection property for compact sets} \qquad (2.36)$$
$$\text{infinite } E \subseteq K \text{ compact} \Rightarrow E \text{ has a limit point in } K \qquad (2.37)$$
$$\text{nested } k\text{-cells have a common point} \qquad (2.39)$$
$$\text{every } k\text{-cell is compact} \qquad (2.40)$$
$$\text{nonempty perfect } P \subseteq \mathbb{R}^k \text{ is uncountable} \qquad (2.43)$$
$$E \subseteq \mathbb{R} \text{ connected} \Leftrightarrow (x,y \in E,\ x<z<y \Rightarrow z \in E) \qquad (2.47)$$
## Significance
Heine–Borel is the bridge between the order completeness of $\mathbb{R}$ established in
Chapter 1 and the analytic theorems of Chapters 3–7: the bisection argument that proves
$k$-cells compact is the same argument that produces convergent subsequences (Bolzano–Weierstrass,
Theorem 2.42), and compactness is what converts local information into global statements.
Theorem 2.43 supplies the standard source of uncountable sets of measure zero — the Cantor set
is the running example — which matters again in Chapter 11. Theorem 2.47, characterizing the
connected subsets of the line as the order-convex ones, is the topological content of the
intermediate value theorem proved in Chapter 4.
Mathlib has an extensive metric-space and compactness library, so much of this chapter exists
there in some form. What this mission adds is the explicit correspondence with Rudin's
formulations: his open-cover definition of compactness against the library's filter-based
`IsCompact` (a milestone in its own right), his $\varepsilon$-style limit points against
`closure`, and his $k$-cells against the library's boxes. The resulting dictionary is what the
remaining missions in the series use when they need a compactness argument.
## Difficulty
The mathematics is standard, and the difficulty is almost entirely in the translation layer.
Two places bite. First, Rudin's compactness quantifies over arbitrary open covers, so the
statement is a $\Pi$-type over families of sets, while Mathlib's `IsCompact` is a statement
about filters; the equivalence is available in the library but only after the cover is
presented in the right indexed form. Second, "limit point" in Rudin's sense is *not*
`p ∈ closure E`: the point must be approached by points of $E$ *other than* $p$, so isolated
points of $E$ are excluded, and statements such as 2.27(a) and 2.41(c) are false if the two
notions are conflated.
## Formalization scope
Conventions fixed by this mission:
* Metric spaces are Mathlib's `[MetricSpace X]`; `IsOpen`, `IsClosed`, `closure`, `Perfect`,
`IsCompact`, `Bornology.IsBounded` and `IsPreconnected` are used for Rudin's corresponding
notions.
* Rudin's limit points are `Rudin.IsLimitPoint p E`, defined with the explicit $\varepsilon$
and the condition $q \ne p$, and his open-cover compactness is `Rudin.IsCoverCompact`.
* $k$-cells are `Rudin.kCell k a b` inside `EuclideanSpace ℝ (Fin k)`; the case where some
$a_j > b_j$ gives the empty set, which is why the nested-cell milestone assumes each cell is
nonempty, exactly as Rudin's construction does.
* Connectedness is `IsPreconnected`, which admits the empty set, matching Rudin's convention
that a set is connected unless it splits into two *nonempty* separated pieces.
* The Heine–Borel goal is stated as a `TFAE` list in Rudin's order (a), (b), (c).
The equivalence is not vacuous: all three conditions are satisfied by any $k$-cell and all
three fail for $\mathbb{R}^k$ itself when $k \ge 1$.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 2 (pp. 24–55).
- The mathlib Community, *The Lean Mathematical Library*, CPP 2020.
https://doi.org/10.1145/3372885.3373824
Rudin PMA I: The Real and Complex Number SystemsTextbook
## Motivation
Every course in analysis begins by fixing what a real number is, because the theorems that
follow — the intermediate value theorem, the convergence of monotone bounded sequences, the
compactness of closed bounded intervals — are false over the rationals and true over the reals
for exactly one reason: the **least-upper-bound property**. Walter Rudin opens *Principles of
Mathematical Analysis* (3rd edition, McGraw-Hill, 1976) with this point. His Example 1.1
exhibits the gap concretely: the set of rationals $p$ with $p^2 < 2$ has no least upper bound
in $\mathbb{Q}$. Chapter 1 then constructs an ordered field in which no such gap occurs, and
derives from that single axiom the archimedean property, the density of $\mathbb{Q}$, and the
existence of $n$-th roots.
This mission is the first in a series formalizing Rudin Chapters 1–11. It covers the chapter's
number-system foundations: the ordering axioms, the real field, the complex field, and
euclidean space $\mathbb{R}^k$.
## Setting
An **ordered set** is a set $S$ with a transitive relation $<$ such that for $x, y \in S$
exactly one of $x < y$, $x = y$, $y < x$ holds. If $E \subseteq S$ and there is $\beta \in S$
with $x \le \beta$ for all $x \in E$, then $E$ is **bounded above** and $\beta$ is an **upper
bound**. A **least upper bound** (supremum) of $E$ is an upper bound $\alpha$ such that no
$\gamma < \alpha$ is an upper bound. The ordered set $S$ has the **least-upper-bound property**
if every nonempty $E \subseteq S$ that is bounded above has a least upper bound in $S$.
An **ordered field** is a field $F$ carrying an order such that $x + y < x + z$ whenever
$y < z$, and $xy > 0$ whenever $x > 0$ and $y > 0$. Rudin's Theorem 1.19 asserts that an
ordered field $\mathbb{R}$ with the least-upper-bound property exists and contains $\mathbb{Q}$
as a subfield; the members of $\mathbb{R}$ are the **real numbers**. The **complex field**
$\mathbb{C}$ is the set of ordered pairs $(a,b)$ of reals with the usual operations, written
$a + bi$, with $|z| = (z\bar z)^{1/2}$; **euclidean $k$-space** $\mathbb{R}^k$ is the set of
$k$-tuples with the inner product $x \cdot y = \sum_{j} x_j y_j$ and norm
$|x| = (x\cdot x)^{1/2}$.
## Formalization targets
### Goal — the real field is the unique complete ordered field (Theorem 1.19)
$$
\text{$K$ an ordered field with the least-upper-bound property}
\;\Longrightarrow\;
\exists!\, e : K \xrightarrow{\ \sim\ } \mathbb{R} \text{ an order-preserving field isomorphism.}
$$
Existence of such a field is witnessed in Lean by $\mathbb{R}$ itself; what carries the content
of Rudin's theorem, and what the goal asks for, is that the least-upper-bound property pins the
field down up to a unique isomorphism of ordered fields. Uniqueness of $e$ also gives Rudin's
second assertion for free: any embedding of $\mathbb{Q}$ is the canonical one, so $K$ contains
$\mathbb{Q}$ as an ordered subfield.
### Milestones
$$\neg\,\exists p \in \mathbb{Q},\ p^2 = 2 \qquad (\text{Example } 1.1)$$
$$\text{LUB property} \Rightarrow \text{GLB property, with } \inf B = \sup(\text{lower bounds of } B) \qquad (1.11)$$
$$x>0 \Rightarrow \exists n \in \mathbb{N},\ nx > y; \qquad x<y \Rightarrow \exists p \in \mathbb{Q},\ x<p<y \qquad (1.20)$$
$$x>0,\ n>0 \Rightarrow \exists!\, y>0,\ y^n = x \qquad (1.21)$$
$$|\bar z| = |z|,\quad |zw| = |z||w|,\quad |\operatorname{Re} z| \le |z|,\quad |z+w| \le |z|+|w| \qquad (1.33)$$
$$\Big|\sum_{j} a_j \overline{b_j}\Big|^2 \le \sum_j |a_j|^2 \sum_j |b_j|^2 \qquad (1.35)$$
$$|x \cdot y| \le |x|\,|y|, \quad |x+y| \le |x|+|y|, \quad |x-z| \le |x-y|+|y-z| \qquad (1.37)$$
## Significance
The least-upper-bound property is the only non-algebraic input to the whole of single-variable
analysis, and the chapter shows how much follows from it alone: the archimedean property, which
rules out infinitesimals; the density of $\mathbb{Q}$, which makes approximation arguments
possible; and the existence of $n$-th roots, which repairs precisely the defect exhibited by
$\sqrt{2}$. The uniqueness statement is what licenses the common practice of treating "the"
real numbers as a single object regardless of the construction used (Dedekind cuts, as in
Rudin's appendix, or Cauchy sequences).
Mathlib already contains $\mathbb{R}$, $\mathbb{C}$, and a uniqueness theorem for conditionally
complete linearly ordered fields, and several of the milestones are available there in some
form. The work this mission asks for is therefore bridging work: stating Rudin's hypotheses in
his own terms — an order with the least-upper-bound property as a *hypothesis on a set*, not as
a typeclass whose data includes a chosen supremum operator — and deriving the standard library
form from them. That bridge is what later missions in the series reuse.
## Difficulty
The individual statements are elementary, and the mathematical difficulty is genuinely low;
what makes the chapter non-mechanical in a proof assistant is the mismatch between hypothesis
and structure. Mathlib's completeness is packaged as `ConditionallyCompleteLinearOrder`, a
structure carrying `sSup` and `sInf` as data; Rudin's is a proposition about an arbitrary
ordered field. Turning the proposition into the structure (in order to invoke the library's
uniqueness theorem) is the one step where the obvious "just apply the Mathlib lemma" move does
not typecheck.
## Formalization scope
Conventions fixed by this mission:
* Rudin's least-upper-bound property is the predicate `Rudin.HasLeastUpperBoundProperty`, using
Mathlib's `IsLUB`, `BddAbove`, `lowerBounds`; no completeness typeclass is assumed of `K`.
* Ordered fields are `[Field K] [LinearOrder K] [IsStrictOrderedRing K]`, which is exactly
Rudin's Definition 1.17.
* Order-field isomorphisms are Mathlib's `≃+*o` (`OrderRingIso`), so "unique isomorphism"
is stated as `∃ e, ∀ e', e' = e`.
* $\mathbb{C}$ is Mathlib's `ℂ` and $|z|$ is the norm `‖z‖`; euclidean $k$-space is
`EuclideanSpace ℝ (Fin k)` with the inner product `inner ℝ x y`, so Rudin's $\mathbb{R}^k$
facts are norm and inner-product inequalities.
* Statements bundling several of Rudin's conclusions (1.33, 1.37) are stated as a single
conjunction, in the order the book lists them.
Nothing here is vacuous: the goal quantifies over an arbitrary ordered field satisfying the
property, and `ℝ` itself is such a field, so the hypothesis is satisfiable and the conclusion
is not automatic.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 1 (pp. 1–21) and its Appendix.
- The mathlib Community, *The Lean Mathematical Library*, CPP 2020.
https://doi.org/10.1145/3372885.3373824
Superlinear or exact bounds for planar distinct distancesOpen Problem
# Superlinear or exact bounds for planar distinct distances
## Motivation
This mission asks how restrictions on collinear and cocircular points limit
the reuse of distances in the plane. Its central question is
[Erdős Problem 98](https://www.erdosproblems.com/98): must the minimum number
of distances grow faster than the number of points?
## Setting
For each positive integer n, let h(n) be the minimum number of distinct
positive Euclidean distances determined by an n-point set in the plane with
no three collinear points and no four cocircular points. Write D(P) for the
number of distinct positive Euclidean distances determined by P.
## Target
The mission is to establish a superlinear lower bound, or determine this
extremal function exactly. The superlinear target is Erdős Problem 98:
$$\lim_{n\to\infty} h(n)/n=\infty.$$
Concretely, for every real A > 0, prove that there is an integer n_A such
that every general-position configuration P with |P| = n >= n_A satisfies
D(P) > A n. A fixed improvement of the coefficient 1/3, or an additive
sublinear improvement above n/3, does not complete this objective.
The alternative completion target is an exact determination of h(n), proved
by a universal lower bound and general-position constructions attaining that
bound. State the range of n explicitly. An asymptotic estimate or a
counterexample to superlinearity alone must be labeled with its actual scope;
neither is an exact determination of h(n).
## Significance and supporting results
The current strongest internally audited
[prose result in this project](https://github.com/flound1129/esgk-on3/blob/main/docs/results/esgk-n14-atomic-proof-2026-09-13.md) is
$$D(P)\ge n/3+c n^{1/4}$$
for some absolute c > 0 and all sufficiently large n. Its full Lean
formalization remains open. The n^(1/4), n^(1/5), and n^(1/6) theorem targets
and their existing milestones are supporting results, not the mission's
terminal goal. Resolving the superlinear target would establish a lower bound
above every fixed linear coefficient. Determining h(n) exactly would settle
the corresponding extremal problem with matching constructions.
## Difficulty and research priorities
The n^(1/4) route constructs a deficiency--Newton carrier, proves pair
separation, and applies one polynomial partition to obtain the curve bound
D(S) >= c d^(-4/3) |S|^(4/3). Its current final calculation yields an additive
n^(1/4) term. Stronger additive bounds count as intermediate progress; they
must not be reported as a superlinear lower bound.
- Develop an argument that excludes D(P) <= A n for every fixed A > 0.
The repository's fixed-A distance-energy gap is one sufficient route.
- Investigate additional structure of the Newton carriers and interactions
between their factors, or another geometric or combinatorial route that
can control the superlinear target.
- Investigate constructions and universal lower bounds together when
pursuing an exact extremal determination.
- Preserve and formalize useful intermediate theorems while keeping their
statements and remaining premises explicit.
## Formalization scope
Configurations are finite subsets of the Euclidean plane, represented in the
project by injective maps from `Fin n` to the plane. Both general-position
hypotheses apply to the image. D(P) counts distinct positive distance values,
not pairs or ordered multiplicities. The superlinear quantifier ranges over
every real A > 0 and every sufficiently large general-position configuration.
The superlinear target and exact-determination target remain open here.
Distinguish conjectures, conditional reductions, audited prose proofs, and
kernel-checked Lean results. A completed supporting formalization does not
by itself complete this mission.
## Selected references
- [Erdős Problem 98](https://www.erdosproblems.com/98) — extremal question and
bibliography.
- [Project overview](https://github.com/flound1129/esgk-on3/blob/main/README.md)
— fixed-A target and current theorem status.
- [Atomic proof of the ESGK n^(1/4) additive bound](https://github.com/flound1129/esgk-on3/blob/main/docs/results/esgk-n14-atomic-proof-2026-09-13.md),
project manuscript, revised 2026-09-14.
- [Full-proof audit](https://github.com/flound1129/esgk-on3/blob/main/docs/audits/esgk-n14-strengthened-full-audit-2026-09-14.md),
internal adversarial review, 2026-09-14.
Birkhoff's Retrograde Global-Section Conjecture in the Planar Circular Restricted Three-Body ProblemOpen Problem
## Motivation and historical timeline
In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit ([Birkhoff 1915](https://doi.org/10.1007/BF03015982); [Liu--Salomão, Section 1.4](https://arxiv.org/abs/2506.17867v2)). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics ([Joung--van Koert, Introduction](https://arxiv.org/abs/2407.19159v3)).
In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 ([Joung--van Koert, Theorem 1.3](https://arxiv.org/abs/2407.19159v3); [Hryniewicz](https://arxiv.org/abs/0812.4076v8)). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for \(0\leq\mu\leq 1/2\) and \(2.1\leq c\leq 2.1+10^{-6}\) ([Theorems 1.2 and 1.5](https://arxiv.org/abs/2407.19159v3)). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to \(1/2\), in fact obtaining rational open books bound by every retrograde orbit in that regime ([Theorem 1.16](https://arxiv.org/abs/2506.17867v2)). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem ([Liu--Salomão 2026](https://arxiv.org/abs/2606.12912)). These results leave the universal finite-mass, all-subcritical statement below as the open target.
## Setting
Two primaries of masses \(1-\mu\) and \(\mu\), with \(0<\mu<1\), are fixed in rotating coordinates at \((-\mu,0)\) and \((1-\mu,0)\). For a massless particle with phase coordinates \((q_1,q_2,p_1,p_2)\), the Hamiltonian is
$$
H_\mu(q,p)=\frac{p_1^2+p_2^2}{2}+q_1p_2-q_2p_1
-\frac{1-\mu}{\sqrt{(q_1+\mu)^2+q_2^2}}
-\frac{\mu}{\sqrt{(q_1-1+\mu)^2+q_2^2}}.
$$
This is equation (1.1) of [Joung--van Koert](https://arxiv.org/abs/2407.19159v3). Let \(h_1(\mu)=H_\mu(L_1)\) be the smallest collision-free critical value, where \(L_1\) lies between the primaries. The subcritical range is \(H_\mu=-c<h_1(\mu)\); there are then two bounded physical components, one around each primary ([Liu--Salomão, Section 4](https://arxiv.org/abs/2506.17867v2)).
The mission labels the primary at \((-\mu,0)\). With complex Levi-Civita variables \(z=z_1+iz_2\) and \(w=w_1+iw_2\), the inverse position map is \(q+\mu=2z^2\), and the regularized Hamiltonian is
$$
\begin{aligned}
K_{\mu,c}(z,w)={}&\frac{|w|^2}{2}+c|z|^2-\frac{1-\mu}{2}
+2|z|^2(z_1w_2-z_2w_1)\\
&-\mu(z_1w_2+z_2w_1)
-\frac{\mu|z|^2}{|2z^2-1|}.
\end{aligned}
$$
On the collision-free domain, \(K_{\mu,c}=|z|^2(H_\mu+c)\), and its zero level regularizes collision with the labeled primary ([Joung--van Koert, equation (2.2)](https://arxiv.org/abs/2407.19159v3)). The selected component \(\Sigma_{\mu,c}\) is anchored at \((z,w)=(0,\sqrt{1-\mu})\). Below \(h_1\), it is a star-shaped three-sphere, invariant under the free antipodal deck map \((z,w)\mapsto(-z,-w)\), and it double-covers the corresponding Moser-regularized \(\mathbb{R}P^3\) component ([Joung--van Koert, Proposition 2.4](https://arxiv.org/abs/2407.19159v3)).
## Target
For every \(0<\mu<1\), every \(-c<h_1(\mu)\), and every complete flow \(\varphi\) on \(\Sigma_{\mu,c}\) generated by \(X_{K_{\mu,c}}\) and commuting with the antipodal map, prove
$$
\exists\,\delta\quad
\operatorname{GeometricRetrograde}(\delta)\ \land\
\operatorname{RationalGSS}(\operatorname{DoubleLift}(\delta)).
$$
Here \(\delta\) consists of \(x\in\Sigma_{\mu,c}\) and a quotient period \(P>0\) with \(\varphi_P(x)=-x\), with no earlier positive time reaching either \(x\) or \(-x\). Its physical projection is required to be a \(q_2\)-symmetric, simple, collision-free loop of winding \(+1\) around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in [Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3](https://arxiv.org/abs/2407.19159v3).
The rational page is encoded by a smooth immersive disk lift \(\widetilde f:D^2\to\Sigma_{\mu,c}\). Its lift is embedded, its interior is transverse to \(X_{K_{\mu,c}}\), and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section ([Hryniewicz, Definition 1.1](https://arxiv.org/abs/0812.4076v8)).
## Significance
A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences ([Birkhoff 1915](https://doi.org/10.1007/BF03015982); [Joung--van Koert, Introduction](https://arxiv.org/abs/2407.19159v3)). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.
## Difficulty
Existence of a \(q_2\)-symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every \(0<\mu<1\) and every energy below \(L_1(\mu)\) ([Liu--Salomão, Theorem 5.1](https://arxiv.org/abs/2506.17867v2)). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges ([Joung--van Koert, Theorem 1.5](https://arxiv.org/abs/2407.19159v3); [Liu--Salomão, Theorem 1.16](https://arxiv.org/abs/2506.17867v2)).
## Formalization scope
The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual `Flow` together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.
The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.
All theorem rows are Lean declarations ending in `by sorry`. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.
## Selected references
- G. D. Birkhoff, *The restricted problem of three bodies*, Rendiconti del Circolo Matematico di Palermo 39 (1915), 265--334. [DOI](https://doi.org/10.1007/BF03015982).
- U. Hryniewicz, *Fast finite-energy planes in symplectizations and applications*, Trans. Amer. Math. Soc. 364 (2012), 1859--1931. [arXiv:0812.4076v8](https://arxiv.org/abs/0812.4076v8).
- C. Joung and O. van Koert, *Computational symplectic topology and symmetric orbits in the restricted three-body problem*, Nonlinearity 38 (2025), 025015. [arXiv:2407.19159v3](https://arxiv.org/abs/2407.19159v3).
- L. Liu and P. A. S. Salomão, *Finite energy foliations and global dynamics in the restricted three-body problem*, arXiv:2506.17867v2 (25 May 2026). [Preprint](https://arxiv.org/abs/2506.17867v2).
- L. Liu and P. A. S. Salomão, *Birkhoff conjecture and finite energy foliations in Hill's lunar problem*, arXiv:2606.12912 (2026). [Preprint](https://arxiv.org/abs/2606.12912).
Circle packing in a square: exact constantsTextbook
## Motivation
Packing congruent circles into a square is a classical problem in discrete geometry: for each natural number $n$, choose a common radius as large as possible while keeping all disks inside the square and preventing overlap. Every exact value requires two logically distinct achievements: an explicit configuration attaining the proposed radius and a proof that no configuration can do better.
The character of those proofs changes sharply with $n$. The first cases admit short geometric arguments; later cases use contact-graph analysis, specialized case divisions, or computer-assisted global optimization with interval arithmetic. Formalizing the resulting constants therefore provides a growing benchmark for extremal geometry, real algebra, finite configurations, and verified computation in Lean.
This is an **open-ended formalization mission**. It begins with the exact constants currently represented by theorem-backed milestones, but it is not restricted to a fixed terminal value of $n$. Further milestones may be added whenever an exact packing value and its rigorous optimality argument are identified and stated precisely enough for formalization.
## Setting
A point is a pair of real coordinates. For points $p=(x,y)$ and $q=(x',y')$, squared Euclidean distance is
$$
\operatorname{sqDist}(p,q)=(x-x')^2+(y-y')^2.
$$
For a real radius $r$, a point lies in the inner square when both coordinates belong to the closed interval $[r,1-r]$. This is exactly the coordinate condition saying that a closed disk of radius $r$, centered at that point, is contained in the unit square.
The predicate $\operatorname{Packable}(n,r)$ requires $0\le r\le \tfrac12$ and a family of $n$ centers in the inner square such that the squared distance between every two distinctly indexed centers is at least $(2r)^2$. Equality is allowed, so tangent disks are admitted. Radius zero is also admitted.
Define
$$
r_n=\sup\{r\in\mathbb R:\operatorname{Packable}(n,r)\}
$$
and define the optimal covered-area fraction by
$$
c_n=n\pi r_n^2.
$$
It is often convenient to use the equivalent point-separation constant $d_n$, the greatest possible minimum pairwise distance among $n$ points in the unit square. The conversion is
$$
r_n=\frac{d_n}{2(1+d_n)},
\qquad
c_n=n\pi\left(\frac{d_n}{2(1+d_n)}\right)^2.
$$
The Lean definitions use a supremum rather than assuming in advance that an optimal packing is attained.
## Current exact-value milestones
The mission currently contains theorem-backed milestones for the following values:
| $n$ | Exact separation or area value | Proof character in the supplied notes |
|---:|---|---|
| $2$ | $d_2=\sqrt2$, hence $c_2=\pi(3-2\sqrt2)$ | diagonal bound |
| $3$ | $d_3=\sqrt6-\sqrt2$ | minimum enclosing square of a triangle |
| $4$ | $d_4=1$, hence $c_4=\pi/4$ | convex hull and perimeter |
| $5$ | $d_5=1/\sqrt2$ | four-cell pigeonhole argument |
| $6$ | $d_6=\sqrt{13}/6$ | case-specific geometric proof |
| $7$ | $d_7=4-2\sqrt3$ | hand proof and later computer verification |
| $8$ | $d_8=\sqrt{2-\sqrt3}$ | case-specific geometric proof |
| $9$ | $d_9=1/2$, hence $c_9=\pi/4$ | classical geometric proof |
| $16$ | $d_{16}=1/3$, hence $c_{16}=\pi/4$ | theoretical grid-optimality proof |
| $25$ | $d_{25}=1/4$, hence $c_{25}=\pi/4$ | theoretical grid-optimality proof |
| $36$ | $d_{36}=1/5$, hence $c_{36}=\pi/4$ | theoretical grid-optimality proof |
For rows stated using $d_n$, the corresponding milestone for $c_n$ uses the conversion formula above. The equalities are claims about the supremum-defined packing constants, not merely about the displayed candidate configurations.
## An extensible mission
The milestone list is intended to grow. The supplied survey notes classify $n=2,\ldots,33$ and $n=36$ as rigorously solved in the cited literature, while distinguishing $n=34$ and $n=35$ as not rigorously closed in the cited 2021 account. Many of the computer-assisted cases do not have a simple radical expression in the supplied notes. Before such a case is linked to a Lean theorem, its primary source must provide a precise candidate value, algebraic characterization, certified enclosure, or optimal-configuration certificate that can be stated faithfully.
A new milestone should identify:
1. the precise value or exact characterization being formalized;
2. an attaining configuration or a certified existence argument;
3. a universal upper bound or global-optimality certificate;
4. the primary source and exact theorem, equation, or certificate location;
5. any trusted computational artifact and the arithmetic guarantees it requires.
Numerical evidence and strong bounds are valuable, but they must be labeled as bounds rather than exact-value milestones. Conversely, newly published exact results for larger $n$ may be added without changing the underlying definitions.
## Proof obligations
Every exact-value milestone must connect the proposed value to `Packable`, `r_n`, and `c_n`. Constructing a configuration establishes only a lower bound. An upper-bound argument without attainability also does not establish equality. A complete proof must bridge both directions through the supremum definition.
The proof methods may include:
- elementary diameter, pigeonhole, convexity, or enclosing-shape arguments;
- normalization between disk centers and point-separation configurations;
- contact-graph and boundary-constraint analysis;
- finite case decompositions;
- interval arithmetic and formally checked branch-and-bound certificates;
- exact algebraic identities needed to convert $d_n$ into $r_n$ and $c_n$.
Shortcuts that redefine $r_n$, $d_n$, or $c_n$ to equal a desired answer are excluded. The constants must remain consequences of the common geometric model.
## Mission structure
The root theorem `CirclePackingConstants.c_all` is the conjunction of the eleven exact-value milestones currently in the mission, covering $n=2,3,4,5,6,7,8,9,16,25,36$. Its proof sketch reduces the root directly to those milestone theorems, so the mission remains open until every current exact value is proved.
The milestone theorems remain separately reusable and independently auditable. When further exact values are added, a successor aggregate theorem can extend the conjunction and become the new root without replacing the shared definitions or invalidating earlier results.
This structure allows elementary cases, historical hand proofs, and computer-assisted certificates to progress independently while remaining part of one cumulative library of exact circle-packing constants.
## Formalization scope
The Lean model uses `ℝ × ℝ` for points and an explicit coordinate formula for squared Euclidean distance. Disk containment is represented by inclusive coordinate inequalities. Nonoverlap is represented by a weak squared-distance inequality, so tangency is permitted. The indexing type is `Fin n`, and the definitions apply to every natural number, including zero.
The definition bundle contains only `Point`, `sqDist`, `InInnerSquare`, `Packable`, `r_n`, and `c_n`. Solvers may introduce normalization maps, separation bounds, explicit configurations, supremum lemmas, contact structures, certificate checkers, and radical or polynomial identities as auxiliary declarations.
## Selected references
- User-supplied notes, *Circles in squares: constants, proofs, and what is actually known*, supplied September 12, 2026. The notes summarize the exact small-$n$ formulas, grid cases, historical proof taxonomy, and computer-assisted frontier used to organize this mission.
- J. Schaer and A. Meir, “On a geometric extremum problem,” *Canadian Mathematical Bulletin* 8 (1965), 21–27.
- J. Schaer, “The densest packing of nine circles in a square,” *Canadian Mathematical Bulletin* 8 (1965), 273–277.
- B. L. Schwartz, “Separating points in a square,” *Journal of Recreational Mathematics* 3 (1970), 195–204.
- J. B. M. Melissen, “Densest packing of six equal circles in a square,” *Elemente der Mathematik* 49 (1994), 27–31.
- M. C. Markot, “Improved interval methods for solving circle packing problems in the unit square,” *Journal of Global Optimization* 81 (2021), 773–803.
- Erich Friedman, *Circles in Squares*, Erich's Packing Center, for background tables and diagrams of candidate packings.
Erdős Problem 142: Asymptotics for Sets Free of k-Term Arithmetic ProgressionsOpen Problem
## Motivation
Erdős asked, repeatedly and with a rising price tag, for an asymptotic formula for the largest subset of $\{1,\dots,N\}$ that contains no arithmetic progression of a given length. He offered 1000 dollars for it in [Er97c] and 10000 dollars in [Er81, p.4], where he called the question "probably enormously difficult"; elsewhere he described it as "probably unattackable at present". Most of modern additive combinatorics — the density increment method, the triangle removal lemma, Gowers uniformity norms, the arithmetic regularity lemma — grew out of attempts on this single question, and the answer is still unknown, even in the first non-trivial case $k=3$.
**Timeline.**
- 1936: Erdős and Turán conjecture that $r_k(N)=o(N)$ for every $k$.
- 1946: Behrend constructs large progression-free sets, giving $r_3(N)\ge N\exp(-c\sqrt{\log N})$.
- 1953: Roth proves $r_3(N)=o(N)$, with the quantitative form $r_3(N)\ll N/\log\log N$.
- 1961: Rankin generalises Behrend, giving $r_k(N)\ge N\exp(-c_k(\log N)^{1/(k-1)})$.
- 1969, 1975: Szemerédi proves $r_4(N)=o(N)$ and then $r_k(N)=o(N)$ for all $k$, settling Erdős–Turán.
- 1977: Furstenberg reproves Szemerédi's theorem ergodically, with no effective bound.
- 1998, 2001: Gowers introduces uniformity norms and obtains $r_k(N)\ll N(\log\log N)^{-c_k}$, the first effective bound for general $k$.
- 2017: Green and Tao obtain $r_4(N)\ll N(\log N)^{-c}$.
- 2020: Bloom and Sisask obtain $r_3(N)\ll N(\log N)^{-1-c}$, the first bound past the $N/\log N$ barrier.
- 2023: Kelley and Meka obtain $r_3(N)\le N\exp(-c(\log N)^{1/12})$.
- 2024: Leng, Sah and Sawhney obtain $r_k(N)\ll N\exp(-(\log\log N)^{c_k})$ for $k\ge5$.
Every upper bound in this list is still astronomically far from Behrend's lower bound, and no candidate asymptotic formula has been proposed for any $k\ge3$.
## Setting
Fix an integer $k$. A **non-trivial $k$-term arithmetic progression** is a list $a,\,a+d,\,a+2d,\dots,a+(k-1)d$ of natural numbers with common difference $d>0$; the requirement $d>0$ is what "non-trivial" means, and it forces the $k$ terms to be distinct. A finite set $A\subseteq\mathbb N$ is **$k$-AP-free** if it contains no such progression. Write
$$r_k(N)\;=\;\max\bigl\{\,|A| \;:\; A\subseteq\{1,\dots,N\},\ A\ \text{is}\ k\text{-AP-free}\,\bigr\}.$$
The mission takes its formal definition of $r_k$ **verbatim from the [formal-conjectures](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.lean) entry for this problem**, so that the goal below is literally the statement recorded there. In that development a set is called *free of progressions of length $l$* when every subset of it that **is** an arithmetic progression of length $l$ forces $l\le1$. Progressions of length $0$ and $1$ count as trivial, so under that convention every set is free of them and $r_0(N)=r_1(N)=N$; the interesting range begins at $k\ge2$. Every statement in this mission that depends on the convention carries an explicit hypothesis on $k$.
On that range, $r_k(N)$ is non-decreasing in both $N$ and $k$, satisfies $r_k(M+N)\le r_k(M)+r_k(N)$, and hence, by Fekete's subadditivity lemma, $r_k(N)/N$ converges. Szemerédi's theorem is the statement that the limit is $0$; the whole difficulty of this mission lies in *how fast* it goes to $0$.
## Formalization targets
### Goal
$$r_k(N)\;=\;o_k\!\left(\frac{N}{\log N}\right)\qquad\text{for every }k>1 .$$
This is `erdos_142.variants.lower` of the [formal-conjectures file for Erdős 142](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.lean), reproduced binder for binder, over that file's own definition of $r_k$.
The headline theorem in that file, `erdos_142`, states $r_k(N)=\Theta(f)$ with the comparison function left as an `answer(sorry)` placeholder, and the same is true of its `variants.upper` and `variants.three`. Those are not closed propositions and cannot serve as a mission goal: the literal request of Erdős Problem #142 — "prove an asymptotic formula for $r_k(N)$" — has no known right-hand side for any $k\ge3$, which is exactly why the file leaves a hole there. `variants.lower` is the one formalizable target in the file, and it is also the strongest precisely-stated form the problem page attaches to #142: Erdős offered 5000 dollars for (essentially) exactly it, as recorded under Erdős Problem #3. It is known for $k=3$ — it follows from Bloom–Sisask 2020, and a fortiori from Kelley–Meka 2023 — trivial for $k=2$, where $r_2(N)=1$, and open for every $k\ge4$. It fixes no constants, so no future improvement can invalidate it.
### A weaker open question
$$\frac{r_k(n)}{r_{k+1}(n)}\longrightarrow 0\qquad\text{for some }k\ge3 .$$
Erdős remarked in [Er80, p.92] that even this separation between consecutive progression lengths is not known. Here `[Er80]` is the erdosproblems.com bibliography key for Erdős's 1980 paper; it is a citation, not a pointer to Erdős Problem #80, which is an unrelated question about books in graphs. This statement has no counterpart in formal-conjectures: the file for #142 contains only the $\Theta$, $o$ and $O$ variants above, and the only two files in that repository that mention $r_k$ at all are the ones for #142 and #139.
## Significance
Proving $r_k(N)=o_k(N/\log N)$ for all $k$ yields, by a standard summation argument, Erdős's conjecture that every $A\subseteq\mathbb N$ with $\sum_{a\in A}1/a=\infty$ contains arbitrarily long arithmetic progressions — the 5000-dollar Erdős Problem #3, of which the Green–Tao theorem on primes is the best-known special case. Below that threshold, quantitative bounds on $r_k$ control the density at which progressions must appear in any concrete set, and are the input to results on progressions in the primes, in sumsets, and in sparse random subsets of the integers.
Formalization status is uneven, and this mission is designed around that gap. Mathlib already contains the $k=3$ theory in a usable form: the predicate `ThreeAPFree`, the Roth number `rothNumberNat`, its subadditivity, and a complete formalization of Behrend's construction (`Behrend.roth_lower_bound`). Mathlib does **not** contain Roth's theorem, Szemerédi's theorem, or any of the modern upper bounds; to the best of current knowledge none of Roth, Szemerédi, Gowers, Green–Tao, Kelley–Meka or Leng–Sah–Sawhney has a machine-checked proof anywhere. The formal-conjectures entry states the problem but proves nothing: every declaration in it is a `sorry`. Two of this mission's targets are taken from that repository — the goal from its file for #142, and the Szemerédi milestone from its file for #139, which uses the same $r_k$; those are the only two files there that mention $r_k$. The milestones therefore split cleanly: the first six are reachable now on top of Mathlib, and the last five are open formalization projects of independent value.
## Difficulty
Every known upper bound for $r_k$ runs a **density increment**: if $A\subseteq\{1,\dots,N\}$ of density $\delta$ has no $k$-term progression, find a long subprogression on which $A$ has density $\delta(1+c(\delta))$, and iterate. The bound this produces is governed entirely by two quantities — how large the increment $c(\delta)$ is, and how much of the interval survives one step. For $k\ge4$ the increment is extracted from an inverse theorem for the Gowers $U^{k-1}$-norm, and the best available correlation bounds there are quasipolynomial in $\delta$; iterating a quasipolynomial increment cannot do better than $N\exp(-(\log\log N)^{c})$, which is nowhere near $N/\log N$. Reaching $N/\log N$ requires an increment with *polynomial* dependence on $\delta$ together with a subprogression of polynomial length, and that combination is currently available only for $k=3$, through the sifting and almost-periodicity machinery of Kelley–Meka. No soft or averaging argument can substitute: Behrend's construction shows the truth at $k=3$ is $N\exp(-\Theta(\sqrt{\log N}))$, so the answer is not a power of $\log N$ and cannot be produced by any argument whose output has that shape.
## Formalization scope
The mission's definition file `Erdos142Basic` carries two layers, and every statement in the mission is written against them.
1. **The source definitions, ported verbatim.** `IsAPOfLengthWith`, `IsAPOfLength`, `IsAPOfLengthFree` and `r` are the declarations of the formal-conjectures entry, transcribed unchanged into the mission's namespace: a set is an arithmetic progression of length $l$ with first term $a$ and difference $d$ when it has exactly $l$ elements and equals $\{a+nd : n<l\}$; it is free of length-$l$ progressions when every progression of length $l$ inside it forces $l\le1$; and $r_k(N)$ is the supremum of $|S|$ over subsets $S\subseteq\{1,\dots,N\}$ free of length-$k$ progressions. The ground set is `Finset.Icc 1 N`, and the supremum is `sSup` over $\mathbb N$; the file proves the two facts that make it a genuine maximum (`le_r` and `r_le`).
2. **An elementary handle.** `HasAP k A` is `∃ a d, 0 < d ∧ ∀ i < k, a + i * d ∈ A`, and `APFree k A` its negation. This form carries no cardinality side condition in $\mathbb N\cup\{\infty\}$ and is what a solver actually wants to induct on. The first milestone is exactly the bridge between the two layers.
Two consequences of the source convention are worth stating plainly, because the prose is silent about them. Length-$0$ and length-$1$ progressions are trivial, so every set is free of them and $r_0(N)=r_1(N)=N$; monotonicity of $r_k$ in $k$ therefore holds only from $k\ge2$ onward, and the corresponding milestone carries that hypothesis. Asymptotic statements use `Asymptotics.IsLittleO` and `Filter.atTop` over $\mathbb N$ with real-valued casts, and real division is Lean's, so `(N : ℝ) / Real.log N` is $0$ at $N=1$; this is invisible to `atTop`.
A trivializing formalization is ruled out by construction: one milestone asserts $r_3(N)=$ `rothNumberNat N`, pinning this development against Mathlib's independently written definition of the Roth number, so a vacuous or mis-quantified notion of progression-freeness cannot survive. That milestone, the bridge milestone above it, and the monotonicity milestone have all been checked to be provable before this proposal was drafted.
A full development needs: discrete Fourier analysis on $\mathbb Z/N\mathbb Z$, Bohr sets and their regularity, the arithmetic regularity lemma, Gowers uniformity norms and the inverse theorem for them, and — for the lower bounds — sphere-counting in high-dimensional boxes (already in Mathlib via `Behrend`). All of this is reusable well beyond this mission. Contributions of any kind are welcome, including partial results: quantitative bounds weaker than the cited ones, the $k=3$ case of a general-$k$ milestone, and reusable Fourier-analytic infrastructure are all valuable even when they do not close a milestone.
## Selected references
- Erdős Problem #142. <https://www.erdosproblems.com/142>
- Erdős Problem #3. <https://www.erdosproblems.com/3>
- Erdős Problem #139 (Szemerédi's theorem in the $r_k$ formulation), linked from #142. <https://www.erdosproblems.com/139>
- Google DeepMind, *formal-conjectures*, `FormalConjectures/ErdosProblems/142.lean` — the source of the goal statement and of the definition of $r_k$. <https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.lean>
- F. A. Behrend, *On sets of integers which contain no three terms in arithmetical progression*, Proc. Nat. Acad. Sci. USA 32 (1946), 331–332. <https://doi.org/10.1073/pnas.32.12.331>
- K. F. Roth, *On certain sets of integers*, J. London Math. Soc. 28 (1953), 104–109. <https://doi.org/10.1112/jlms/s1-28.1.104>
- R. A. Rankin, *Sets of integers containing not more than a given number of terms in arithmetical progression*, Proc. Roy. Soc. Edinburgh Sect. A 65 (1961), 332–344.
- E. Szemerédi, *On sets of integers containing no $k$ elements in arithmetic progression*, Acta Arith. 27 (1975), 199–245. <https://doi.org/10.4064/aa-27-1-199-245>
- W. T. Gowers, *A new proof of Szemerédi's theorem*, Geom. Funct. Anal. 11 (2001), 465–588. <https://doi.org/10.1007/s00039-001-0332-9>
- B. Green and T. Tao, *New bounds for Szemerédi's theorem, III: A polylogarithmic bound for $r_4(N)$*, Mathematika 63 (2017), 944–1040. <https://arxiv.org/abs/1705.01703>
- T. F. Bloom and O. Sisask, *Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions*, arXiv:2007.03528. <https://arxiv.org/abs/2007.03528>
- Z. Kelley and R. Meka, *Strong bounds for 3-progressions*, arXiv:2302.05537. <https://arxiv.org/abs/2302.05537>
- J. Leng, A. Sah and M. Sawhney, *Improved bounds for Szemerédi's theorem*, arXiv:2402.17995. <https://arxiv.org/abs/2402.17995>
# Proofs from THE BOOK: verified results and open formalization tasks
This Textbook project develops a reusable Lean library around Martin Aigner and Günter M. Ziegler's *Proofs from THE BOOK*. It combines results imported from the existing `proof_in_the_book` repository with precise contribution targets from the sixth edition (2018). The aim is to preserve mathematical meaning, reuse existing proofs, and make the remaining work accessible to other contributors.
## What is already verified
The original import contains 156 distinct platform-accepted results. Euclid, the original main theorem, is retained as a completed milestone when the project goal moves to the sixth-edition extension. Every one of the repository's 40 chapter topics has accepted results. Each result certifies its actual Lean statement, including its hypotheses; this does not certify every argument or every theorem in a chapter. Some proofs reuse Mathlib, while others were developed in the repository. Their source and proof notes retain that distinction.
The imported source snapshot is `873d52e0c88cd351f594221e70c3c5b3559777a9`. Imported results use Lean 4.30.0 and Mathlib `c5ea00351c28e24afc9f0f84379aa41082b1188f`. Immutable public source links are used only where the linked source matches the verified artifact. Compatibility changes, unsuccessful attempts, and verification evidence are retained in the integration project.
The live goal is the explicit conjunction of the 21 linked sixth-edition extension targets. Its reduction connects these targets to the goal, so proving the remaining children advances the project. This goal is deliberately narrower than “every theorem and every proof in the book”; the unlinked topology tasks below are additional formalization work.
## Sixth-edition contribution targets
New milestones explicitly marked **6th ed.** cover Chapters 7 (spectral theorem and determinants), 15 (round circles and links), 35 (finite Kakeya), 37 (permanents and entropy), and 45 (probabilistic counting). They include the precise definitions and boundary conditions needed to state the results. Compiled Open targets are requests for proofs, not proved results. The spectral theorem has a direct Mathlib proof; community results are reused under their actual statements and with attribution.
Two Chapter 15 tasks intentionally remain unlinked mathematical milestones: the full non-equivalence assertion for the depicted Borromean, Tait, and trivial links, and the Fox-coloring invariance bridge for equivalent link diagrams. These invite formalization of the diagrams and the topology bridge as well as proof. The separate modular Fox calculations do not by themselves establish ambient non-equivalence.
The crossing-lemma target is the universal good-drawing form: actual injective edge arcs and exact finite intersection records appear in its interface. It does not assume the desired crossing bound. The Ramsey target preserves the real exponent for odd k. The related public Erdős–Ramsey result with a rounded exponent is identified as a supporting result, not as proof of that full target.
## Chapter numbering and statement scope
Older milestones use the repository's chapter labels. Repository Chapters 1–21 match the bundled fourth edition; Chapter 22 inserts Van der Waerden's permanent theorem, and Chapters 23–40 correspond to fourth-edition Chapters 22–39. The sixth edition has 45 chapters, so these organizational labels are not sixth-edition chapter numbers. New milestones give sixth-edition numbers and printed source pages explicitly.
Some existing formalizations preserve narrower statements or additional premises. Examples include repository Chapter 13's dihedral-angle conclusion, Chapter 28's Dilworth lower-bound result, and the geometric premises in Chapter 36. Read the actual linked theorem and its description before reusing it. A chapter title or the former Euclid main theorem is not a completion certificate for the collection.
## How to contribute
Choose an Open linked theorem and inspect its definitions, exact binders, Mathlib revision, and prior attempts. Reuse a compatible existing result when it proves that statement; preserve the original contributor's attribution. Submit a matching proof for verification. For an unlinked milestone, first formalize and review the source statement and its definitions. These are known textbook results awaiting formalization or proof in this project, rather than claims of new unresolved mathematics.
Source repository: https://github.com/xiangyazi24/proof_in_the_book
Book: Aigner and Ziegler, *Proofs from THE BOOK*, Sixth Edition (2018), https://doi.org/10.1007/978-3-662-57265-8
Algorithmic Game Theory III: Arrow and Gibbard–SatterthwaiteTextbook
# Algorithmic Game Theory III: Arrow and Gibbard–Satterthwaite
## Motivation
Before a mechanism can pay anyone, it must decide something — and the impossibility theorems of social choice say that deciding honestly is already hard. Arrow's theorem (1951) showed that any method of aggregating individual rankings into a social ranking that respects unanimity and independence of irrelevant alternatives must be a dictatorship; Gibbard (1973) and Satterthwaite (1975) showed the voting analogue: any non-dictatorial voting rule onto three or more candidates can be strategically manipulated. These two results frame all of mechanism design — they are the reason Chapter 9 of Nisan–Roughgarden–Tardos–Vazirani (eds.), *Algorithmic Game Theory* (Cambridge, 2007), this mission's source, introduces money and quasilinear utilities immediately after proving them: without transfers, incentive compatibility is an impossibility, not a design constraint.
A timeline: Arrow proved the aggregation impossibility in his 1951 monograph *Social Choice and Individual Values*; Gibbard (1973) established the manipulability of non-dictatorial voting schemes via game forms, Satterthwaite (1975) independently via a direct argument; the derivation of Gibbard–Satterthwaite as a corollary of Arrow's theorem, which the book follows and this mission adopts as its attack path, is standard since the 1970s.
## Setting
Fix a finite set $A$ of **alternatives** (candidates) and a finite set $\iota$ of **voters**. A **preference** is a strict total order on $A$; we write the relation as $r(a,b)$, read "$a$ is strictly preferred to $b$" (the book writes $b \prec a$). A **preference profile** assigns a preference to each voter. A **social welfare function** $F$ maps profiles to a social preference; a **social choice function** $f$ maps profiles to a single chosen alternative (Definition 9.1).
The properties at stake (Definitions 9.2, 9.4, 9.5, 9.7):
- $F$ satisfies **unanimity** if on every profile where all voters hold the identical preference $r$, the social preference is $r$.
- $F$ satisfies **independence of irrelevant alternatives (IIA)** if the social preference between $a$ and $b$ depends only on the voters' preferences between $a$ and $b$.
- Voter $i$ is a **dictator** in $F$ if the social preference always equals $i$'s; in $f$, if $f$ always elects $i$'s top alternative.
- $f$ is **incentive compatible** if no voter, by misreporting, can obtain an outcome they strictly prefer (under their true preference) to the truthful outcome; $f$ is **monotone** if whenever a single voter's change of vote moves the outcome from $a$ to $a' \ne a$, that voter ranked $a$ above $a'$ before and $a'$ above $a$ after.
- $f$ is **onto** if every alternative is elected on some profile.
## Formalization targets
### Goal (capstone) — Theorem 9.8, Gibbard–Satterthwaite
$$|A| \ge 3,\ f \text{ incentive compatible and onto } A \implies f \text{ is a dictatorship.}$$
### Theorem 9.3 — Arrow
$$|A| \ge 3,\ F \text{ a social welfare function satisfying unanimity and IIA} \implies F \text{ is a dictatorship.}$$
### Proposition 9.6 — incentive compatibility = monotonicity
$$f \text{ is incentive compatible} \iff f \text{ is monotone},$$
with no cardinality or finiteness assumptions: the two properties are quantifier-for-quantifier the same data viewed twice.
## Significance
These are the two foundational impossibility theorems of social choice, and the pivot of the whole mechanism-design part of this series: the VCG mission that follows exists because Gibbard–Satterthwaite closes the door on non-trivial strategyproof choice without money. The chapter derives Gibbard–Satterthwaite from Arrow through the top-set extension (Definition 9.9, Lemmas 9.10–9.11), so a solver of the capstone gets Arrow as a stepping stone, not a detour.
Formalizing them produces the platform's first social-choice library: preference profiles as strict total orders, the aggregation vocabulary, and the impossibility pair. Arrow's theorem has been formalized before in other proof assistants (Nipkow's Isabelle formalization, 2009; a Mizar formalization by Wiedijk), which is evidence the statement shapes here are the standard ones — but no Lean 4/mathlib formalization exists, and none on this platform.
## Difficulty
The proofs are short on paper and famously slippery in the details. Arrow's proof (the book gives Geanakoplos's pairwise-neutrality route) is a sequence of profile surgeries: each step swaps one voter's ranking of a pair and tracks the social outcome through IIA; the formal cost is constructing the intermediate profiles and proving they remain strict total orders — pure bookkeeping, but a lot of it. The hybrid-profile argument needs, over three or more alternatives, custom orders placing chosen pairs at chosen positions; building these on an abstract finite type is where most of the work lies. For the capstone, the book's route through the top-set extension $\prec^S$ (move $S$ to the top, Definition 9.9) requires proving the extension is again a strict total order (Lemma 9.10) and inherits unanimity, IIA, and non-dictatorship (Lemma 9.11); a solver may equally take any direct proof of Gibbard–Satterthwaite — the statement fixes no route. Proposition 9.6 is a genuine warm-up: unfolding both definitions and rearranging quantifiers.
## Formalization scope
Preferences are relations `A → A → Prop` carrying `IsStrictTotalOrder`; `r a b` means "$a$ is strictly preferred to $b$", the reverse of the book's $\prec$ — every definition's docstring states this orientation. Aggregators are total functions on all relation-valued profiles; every property quantifies only over genuine preference profiles, so behavior on invalid inputs is irrelevant, and nothing can be smuggled through junk inputs. Unanimity is the book's identical-profile form (Definition 9.2), which together with IIA yields the pairwise form used in proofs. Both alternatives and voters are finite types; `|A| ≥ 3` enters as `2 < Fintype.card A`. Arrow's theorem carries `Nonempty ι`, matching the book's setting of $n \ge 1$ voters; it is not needed for truth — with zero voters the identical-profile unanimity is already unsatisfiable over three or more alternatives, so that case is vacuous either way. Gibbard–Satterthwaite deliberately omits it: with zero voters ontoness onto three alternatives is unsatisfiable, and the statement holds vacuously. Dictatorship for choice functions is Definition 9.7 exactly: whenever some alternative is the dictator's unique maximum, it is elected.
## Selected references
- K. J. Arrow, *Social Choice and Individual Values*, Wiley, 1951 (2nd ed. 1963). [Link](https://cowles.yale.edu/sites/default/files/2022-09/m12-2-all.pdf)
- A. Gibbard, *Manipulation of voting schemes: a general result*, Econometrica 41 (1973), 587–601. [DOI](https://doi.org/10.2307/1914083)
- M. A. Satterthwaite, *Strategy-proofness and Arrow's conditions*, Journal of Economic Theory 10 (1975), 187–217. [DOI](https://doi.org/10.1016/0022-0531(75)90050-2)
- J. Geanakoplos, *Three brief proofs of Arrow's impossibility theorem*, Economic Theory 26 (2005), 211–215. [DOI](https://doi.org/10.1007/s00199-004-0556-7)
- T. Nipkow, *Social choice theory in HOL: Arrow and Gibbard–Satterthwaite*, J. Automated Reasoning 43 (2009), 289–304. [DOI](https://doi.org/10.1007/s10817-009-9147-4)
- N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), *Algorithmic Game Theory*, Cambridge University Press, 2007, Chapter 9, §9.2. [DOI](https://doi.org/10.1017/CBO9780511800481)
Algorithmic Game Theory II: No-Regret Learning and Correlated EquilibriaTextbook
## Motivation
Equilibrium concepts are static; play is dynamic. The bridge between the two is **regret minimization**: simple adaptive rules that, against arbitrary — even adversarial — opponents, perform nearly as well as the best fixed alternative in hindsight. The subject begins with Hannan (1957) and Blackwell (1956), whose consistency theorems predate most of computational learning theory; the modern multiplicative-weights style bounds are due to Littlestone–Warmuth (1994) and Freund–Schapire (1997); the reduction from external to swap regret, and with it the algorithmic route to correlated equilibria, is Blum–Mansour (2005), following Foster–Vohra (1997) and Hart–Mas-Colell (2000). Chapter 4 of Nisan–Roughgarden–Tardos–Vazirani (eds.), *Algorithmic Game Theory* (Cambridge, 2007), written by Blum and Mansour, is the source text of this mission.
The punchline of the chapter, and of this mission, is that a *computationally trivial* form of rationality — each player privately running a no-swap-regret algorithm — drives the empirical play of any finite game into an approximate **correlated equilibrium** (Aumann, 1974). No coordination, no knowledge of the game, no fixed-point computation: the equilibrium concept that Chapter 1 of the series defines through a correlating device is reached by decentralized learning.
## Setting
The online model (§4.2): there are $N$ actions. At each time $t$ an **online algorithm** selects a distribution $p^t$ over actions, as a function of the loss vectors observed so far; then the adversary reveals a loss vector $\ell^t \in [0,1]^N$ and the algorithm suffers $\sum_i p^t_i \ell^t_i$. Cumulatively, $L_H^T = \sum_{t \le T} \sum_i p^t_i \ell^t_i$ and $L_k^T = \sum_{t \le T} \ell^t_k$ for a fixed action $k$. The **external regret** of $H$ is $L_H^T - \min_k L_k^T$. A **modification rule** $F : \{1,\dots,N\} \to \{1,\dots,N\}$ rewires the algorithm's play, giving the modified loss $L_{H,F}^T = \sum_t \sum_i p^t_i\, \ell^t_{F(i)}$; the **swap regret** is $L_H^T - \min_F L_{H,F}^T$ over all $N^N$ rules.
A finite game (the vocabulary of Mission I of this series, in loss form): players $\iota$, finite action sets $S_i$, cost functions $c_i : \prod_j S_j \to \mathbb{R}$. A joint distribution $Q$ on action vectors is an **$\varepsilon$-correlated equilibrium** (Definition 4.11) if for every player $i$ and every switching rule $F : S_i \to S_i$,
$$\mathbb{E}_{s \sim Q}\big[c_i(s)\big] \;\le\; \mathbb{E}_{s \sim Q}\big[c_i(F(s_i), s_{-i})\big] + \varepsilon.$$
## Formalization targets
### Goal (capstone) — Corollary 4.16, explicit form
$$\forall N, T\ \exists H:\quad \text{swap regret of } H \text{ on every } [0,1]\text{-loss sequence} \;\le\; 2N\sqrt{T \ln N}.$$
An online algorithm with vanishing per-round swap regret, with the constant the chapter's own route produces.
### Theorem 4.6 — Polynomial Weights
$$L_{PW}^T \;\le\; L_k^T + \eta\, Q_k^T + \frac{\ln N}{\eta}, \qquad Q_k^T = \sum_{t\le T} (\ell^t_k)^2, \quad 0 < \eta \le \tfrac12.$$
### Theorem 4.9 — external regret in constant-sum games
A player with external regret $R$ over $T$ rounds has average loss at most $v_i + R/T$, where $v_i$ is the game value — no-regret play guarantees the minimax value against any opponent.
### Theorem 4.15 — external-to-swap reduction
Any algorithm with external regret $\le R$ on all $[0,1]$-loss sequences yields one with swap regret $\le N R$.
### Theorem 4.12 — swap regret bounds distance from correlated equilibrium
If every player's swap regret over $T$ steps of mixed play is at most $R$, the empirical joint distribution is an $(R/T)$-correlated equilibrium.
### Theorem 4.3 — deterministic algorithms fail
Every deterministic algorithm has a $\{0,1\}$-loss sequence forcing loss $T$ while some action loses at most $\lfloor T/N \rfloor$: randomization is necessary, not a convenience.
## Significance
Correlated equilibrium is the equilibrium concept with a defensible dynamic foundation: Nash equilibria are PPAD-hard to find, but the capstone plus Theorem 4.12 exhibit polynomial-time decentralized dynamics whose empirical play is an $\varepsilon$-correlated equilibrium after $T = O(N^2 \ln N / \varepsilon^2)$ rounds. Later missions in this series lean on this machinery: the price-of-anarchy chapters bound the cost of *no-regret play* (not just of exact equilibria), and the routing-game chapter uses precisely the convergence result formalized here.
Formalizing it produces the platform's first online-learning library: the adversarial protocol, regret in both external and swap forms, the multiplicative-weights analysis, and correlated equilibria. The regret vocabulary is directly reusable for the bandit-flavored missions already on the platform. All results are classical, with textbook proofs; the work requested is machine-checked proof, not new mathematics.
## Difficulty
The Polynomial Weights bound is a potential-function argument: the total weight $W^t$ falls geometrically with the algorithm's loss and is bounded below by the weight of action $k$; the formal work is inequalities for $\ln(1-x)$ on $[0, 1/2]$ and careful bookkeeping of the recursion. The reduction (Theorem 4.15) is the structurally interesting step: the master algorithm runs $N$ copies of the external-regret procedure, feeds copy $i$ the true losses scaled by the master's own probability $p^t_i$, and — the crux — plays the *stationary distribution* $p^t = p^t Q^t$ of the column-stochastic matrix assembled from the copies' outputs. Existence of that fixed point is exactly the existence of a stationary distribution of a finite Markov chain, available on this platform as the goal of *Markov Chains and Mixing Times I* — or provable directly. Theorem 4.12 is an averaging argument, deliberately easy; Theorem 4.3 is an adversary construction; Theorem 4.9 combines the regret bound with the security level the minimax theorem of Mission I supplies, through the opponent's empirical mixture. The capstone is the composition of 4.6 (tuned at $\eta = \min\{\sqrt{\ln N / T}, 1/2\}$) with 4.15, plus the arithmetic that turns $N \cdot 2\sqrt{T \ln N}$ into the stated bound.
## Formalization scope
An online algorithm is a deterministic function from the observed history (the list of past loss vectors) to the mixed action played next — the standard formal reading of the full-information model; randomization lives in the mixed action, and losses are expected losses. Boundedness of losses ($[0,1]$) is a hypothesis on theorems, never part of a definition. The Polynomial Weights algorithm is defined concretely by its weight recursion, and its learning rate carries the hypothesis $0 < \eta \le 1/2$: the book writes only $\eta \le 1/2$, but at $\eta = 0$ the bound's $\ln N / \eta$ term degenerates and the claim is false, so positivity is explicit. Action sets are `Fin (n+1)`, keeping them nonempty. The number of steps $T$ is a known parameter (the book's convention; guess-and-double is out of scope). Correlated equilibria use the switching-rule form of Definition 4.11, over the game vocabulary (`IsLottery`, `IsMixedProfile`, `profileProb`) published with Mission I of this series. In Theorem 4.12 the empirical distribution is the average of product distributions of the played profiles, $T \ge 1$ is required (at $T = 0$ there is no empirical distribution), and costs are not assumed bounded — the averaging is scale-free.
Trivializing readings are ruled out: the existential algorithms in Theorem 4.15 and the capstone are quantified *before* the loss sequence and the modification rule, so a witness must work uniformly against every adversary — nothing may be chosen with hindsight.
## Selected references
- A. Blum, Y. Mansour, *From external to internal regret*, JMLR 8 (2007), 1307–1324. [Link](https://www.jmlr.org/papers/v8/blum07a.html)
- N. Littlestone, M. K. Warmuth, *The weighted majority algorithm*, Information and Computation 108 (1994), 212–261. [DOI](https://doi.org/10.1006/inco.1994.1009)
- D. P. Foster, R. V. Vohra, *Calibrated learning and correlated equilibrium*, Games and Economic Behavior 21 (1997), 40–55. [DOI](https://doi.org/10.1006/game.1997.0595)
- S. Hart, A. Mas-Colell, *A simple adaptive procedure leading to correlated equilibrium*, Econometrica 68 (2000), 1127–1150. [DOI](https://doi.org/10.1111/1468-0262.00153)
- N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), *Algorithmic Game Theory*, Cambridge University Press, 2007, Chapter 4. [DOI](https://doi.org/10.1017/CBO9780511800481)
Erdős Problem 287: Gaps Between Unit-Fraction DenominatorsOpen Problem
## Motivation
A **unit fraction** is the reciprocal $1/n$ of a positive integer. The number $1$ can be written as a sum of distinct unit fractions in infinitely many ways — $1 = \tfrac12+\tfrac13+\tfrac16$, $1 = \tfrac12+\tfrac14+\tfrac16+\tfrac1{12}$, and so on — and the combinatorics of such representations is one of the oldest recurring themes in Erdős's problem lists. Most questions in the area concern *size*: how many terms are needed, how small the largest denominator can be, how large the smallest one must be. Erdős Problem 287 asks instead about the *shape* of a representation: how tightly can the denominators be packed?
Order the denominators increasingly and look at their consecutive differences. For $1 = \tfrac12+\tfrac13+\tfrac16$ the differences are $1$ and $3$. The question is whether a difference of at least $3$ must always occur, in every representation of $1$, no matter how many terms it has. The problem is recorded in Erdős and Graham's 1980 problem book ([ErGr80, p. 33](https://mathweb.ucsd.edu/~ronspubs/80_11_number_theory.pdf)) and was selected for the booklet of favourite problems prepared for the 1999 Budapest conference on Erdős's mathematics ([Va99, 1.15]). It remains [open](https://www.erdosproblems.com/287).
**Timeline.** The weaker statement that *some* difference must be at least $2$ — equivalently, that $1$ is never the sum of the reciprocals of a block of consecutive integers — is classical. Theisinger (1915) proved that the harmonic number $H_n$ is not an integer for $n \ge 2$, using Bertrand's postulate. Kürschák (1918) introduced the $2$-adic argument that proves the general block statement: for $m \le n-2$, the difference $H_n - H_m$ is not an integer. Erdős's 1932 paper [Er32], whose title translates as *"A generalisation of an elementary number-theoretic theorem of Kürschák"*, extends the result from blocks of consecutive integers to arithmetic progressions; the erdosproblems.com entry for Problem 287 cites it for the difference-$\ge 2$ bound. Nothing stronger appears to be known: the passage from $2$ to $3$ is the open part, and no partial result is recorded in the entry beyond a conditional one, namely that the conjecture would follow for all but finitely many exceptions if it were known that for every large $N$ there is a prime $p \in [N, 2N]$ with $(p+1)/2$ also prime.
## Setting
Fix an integer $k \ge 2$ and integers
$$1 < n_1 < n_2 < \cdots < n_k$$
with
$$1 \;=\; \frac{1}{n_1} + \frac{1}{n_2} + \cdots + \frac{1}{n_k},$$
the sum taken in $\mathbb{Q}$. Call such a tuple a **representation of length $k$**. The denominators are strictly increasing, hence distinct, and all exceed $1$: the value $n_1 = 1$ is excluded because $1/1$ already exhausts the total. The **gaps** of the representation are the $k-1$ consecutive differences $n_{i+1} - n_i$ for $1 \le i \le k-1$, and its **maximal gap** is $\max_i (n_{i+1} - n_i)$.
Representations exist for every $k \ge 3$, and for $k = 1$ only the excluded $n_1 = 1$; no representation of length $2$ exists. Examples: $(2,3,6)$ with gaps $1, 3$; $(2,4,6,12)$ with gaps $2,2,6$; $(3,4,6,10,12,15)$ with gaps $1,2,4,2,3$.
## Formalization targets
### Goal — Erdős Problem 287
$$\text{every representation } 1 < n_1 < \cdots < n_k \ (k \ge 2) \text{ of } 1 \text{ satisfies } \max_{1 \le i < k} (n_{i+1} - n_i) \;\ge\; 3.$$
This is the open conjecture, stated with no bound on $k$ and no restriction on the denominators beyond those in **Setting**. It is the weakest form that captures the question: asserting a bound for one particular $k$, or for denominators in some range, would be a different and strictly easier statement.
### Milestone — the gap-two bound (Kürschák; Erdős [Er32])
$$\text{every representation satisfies } \max_{1 \le i < k}(n_{i+1} - n_i) \;\ge\; 2.$$
Equivalently: no block of two or more consecutive integers has reciprocals summing to $1$. This is closed mathematics and the natural first target.
### Milestone — the classical block theorem (Kürschák)
$$\text{for } n \ge 1 \text{ and } k \ge 2, \qquad \sum_{i=0}^{k-1} \frac{1}{n+i} \notin \mathbb{Z}.$$
The gap-two bound is an immediate consequence, since a representation all of whose gaps equal $1$ is exactly a block of consecutive integers.
### Milestone — sharpness
$$1 = \tfrac12+\tfrac13+\tfrac16 \text{ is a representation all of whose gaps are at most } 3.$$
So the constant $3$ in the goal is optimal and cannot be replaced by $4$.
## Significance
*The result itself.* A positive answer would say that a representation of $1$ by unit fractions can never have all its denominators within distance $2$ of each other — a structural constraint of a kind that the size-based results in this area do not provide. The conditional route recorded on the problem page is instructive about where the difficulty sits: it reduces the conjecture, up to finitely many exceptions, to the existence of primes $p$ in $[N,2N]$ with $(p+1)/2$ prime, a statement of Bertrand-with-extra-structure type that is itself out of reach of current technology. A direct proof would therefore either bypass that route or resolve the conjecture for the remaining cases by different means.
*Formalizing it.* The gap-two bound and the block theorem behind it are closed mathematics, so the honest description of that part of this mission is formalization, not research. It is nevertheless not already available: Mathlib proves Theisinger's case `harmonic_not_int`, that $H_n \notin \mathbb{Z}$ for $n \ge 2$, but not Kürschák's block version $H_n - H_m \notin \mathbb{Z}$, which is the form Problem 287 needs. Supplying it is a genuine strengthening of the library's existing development and is reusable for any question about reciprocal sums over intervals. The goal itself is open, and this mission does not claim otherwise: it is registered with an open proof, and the milestones are what a solver can realistically close today.
## Difficulty
The obvious first idea — bound the number of terms, then check finitely many cases — fails immediately, because $k$ is unbounded: representations of $1$ exist with arbitrarily many terms, so no finite computation can settle the conjecture. The second idea, extending the $2$-adic argument that gives the gap-two bound, also fails, and instructively. That argument works because a block of consecutive integers contains exactly one element of maximal $2$-adic valuation, which leaves the total with negative valuation. Once gaps of size $2$ are permitted the denominators may be chosen to avoid that configuration — for instance all even, as in $(2,4,6,12)$ — and the valuation obstruction disappears. There is no evident replacement prime or weighting that rules out all gap-$\le 2$ configurations simultaneously, and the conditional result quoted above suggests why: the known routes pass through the distribution of primes in short intervals with a multiplicative side condition, rather than through a congruence obstruction.
## Formalization scope
A representation is encoded as a function $f : \mathbb{N} \to \mathbb{N}$ together with the hypotheses `∀ i < k, 1 < f i` and `∀ i j, i < j → j < k → f i < f j`, and the requirement `∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1`. Only the values of $f$ below $k$ are constrained; the function is not required to be monotone or bounded elsewhere, and nothing outside the window is used. The conclusion is `∃ i, i + 1 < k ∧ 3 ≤ f (i + 1) - f i`, the existential form of "the maximal gap is at least $3$"; the subtraction is natural-number subtraction, which is harmless because $f$ is increasing on the window, so no truncation can occur. The sum is a rational equality, not an approximation.
The statement admits no trivializing reading. The hypothesis `1 < f i` is essential and is not vacuous — dropping it would admit $f\,0 = 1$, $k = 1$; the strict monotonicity is what makes the gaps well defined and the denominators distinct; and `k ≥ 2` guarantees that at least one gap exists, so the conclusion is not an empty existential. Asserting *exactly* $3$ rather than *at least* $3$ would be false, as $(2,4,6,12)$ has a gap of $6$.
Infrastructure: the block theorem is proved from Mathlib's `padicNorm` and `padicValNat` API — `padicNorm.add_eq_max_of_ne`, `padicNorm.sum_lt'`, `padicNorm.not_int_of_not_padic_int`, `pow_padicValNat_dvd` and `pow_succ_padicValNat_not_dvd` — and needs no new definitions. That development is reusable beyond this mission and is a candidate for upstreaming to Mathlib alongside `harmonic_not_int`. Contributions are welcome on any milestone independently; a formalization of the conditional reduction to primes $p$ with $(p+1)/2$ prime would also be a valuable addition, and is not included as a milestone here only because the problem page states it too briefly to formalize faithfully without consulting a primary source.
## Selected references
- P. Erdős, *Egy Kürschák-féle elemi számelméleti tétel általánosítása* (A generalisation of an elementary number-theoretic theorem of Kürschák), Mat. és Phys. Lapok **39** (1932), 17–24.
- P. Erdős and R. L. Graham, *Old and new problems and results in combinatorial number theory*, Monographies de L'Enseignement Mathématique, Geneva, 1980, p. 33. [scan](https://mathweb.ucsd.edu/~ronspubs/80_11_number_theory.pdf)
- Various, *Some of Paul's favorite problems*, booklet for the conference "Paul Erdős and his mathematics", Budapest, July 1999, item 1.15.
- K. Conrad, *The $p$-adic growth of harmonic sums*, expository notes (Theorem 2 is Kürschák's block theorem, with the $2$-adic proof). [pdf](https://kconrad.math.uconn.edu/blurbs/gradnumthy/padicharmonicsum.pdf)
- T. F. Bloom, *Erdős Problem #287*, [erdosproblems.com/287](https://www.erdosproblems.com/287).
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
The Erdős–Straus Conjecture (Erdős Problem 242)Open Problem
## Egyptian fractions and the Erdős–Straus question
A **unit fraction** is the reciprocal of a positive integer. The Erdős–Straus conjecture asks whether the particularly simple rational number $4/n$ always admits an expansion with three such terms. Its difficulty lies in obtaining a fixed number of terms for every denominator: general algorithms for Egyptian fractions do not give this three-term guarantee.
The conjecture is open. This mission adopts the exact statement maintained as [Erdős Problem 242](https://www.erdosproblems.com/242). It aims to formalize established reductions and provide a precise frontier for further work; it does not present a proof of the universal conjecture.
The historical formulations vary. [Erdős’s 1950 paper, pp. 193–195](https://www.renyi.hu/~p_erdos/1950-02.pdf), discusses distinct unit fractions and attributes the conjecture jointly to himself and Straus. [His 1961 problem I.32, p. 238](https://www.renyi.hu/~p_erdos/1961-22.pdf), allows positive denominators without specifying distinctness, while [the 1979 statement, problem 9, p. 70](https://www.renyi.hu/~p_erdos/1979-22.pdf), explicitly orders distinct denominators. The earliest published discussion may be Obláth’s 1950 paper, submitted in 1948; it attributes the question to Erdős, as explained by [Bloom–Elsholtz, pp. 238–239](https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf).
The main developments relevant here are:
- **1950:** Obláth’s sufficient condition using a prime divisor of $n+1$ congruent to $3$ modulo $4$.
- **1965–1969:** Yamamoto’s congruence analysis and Mordell’s exposition reduce the remaining prime cases to six classes modulo $840$.
- **1970–1971:** Vaughan bounds the density of possible exceptions; Terzi develops a stronger congruence sieve modulo $120120$.
- **2013–2022:** Elsholtz–Tao analyze representation counts and soluble polynomial congruences; Bloom–Elsholtz give an explicit equivalent covering formulation.
- **2025:** Computational verification is reported through $10^{18}$. Pomerance–Weingartner study the more general Erdős–Straus–Schinzel problem, including quantitative dependence on a variable numerator.
## The exact property
For a natural number $n$, write $\mathrm{IsErdosStraus}(n)$ for the following literal property:
$$\exists x,y,z\in\mathbb N,\qquad 1\le x<y<z,\qquad \frac4n=\frac1x+\frac1y+\frac1z.$$
Every fraction is evaluated in $\mathbb Q$. The predicate contains only these witnesses, inequalities, and equality. The required range of the conjecture is $n>2$; distinctness is part of the mathematical target. In particular, the prime $2$ cannot simply be imported from a formulation permitting repeated denominators. The boundary value $n=3$ is included, with denominators $1,4,12$.
## Formalization targets
The unresolved root goal is
$$\forall n\in\mathbb N,\quad n>2\Longrightarrow\mathrm{IsErdosStraus}(n).$$
The supporting milestones concern established mathematics. Denominator clearing relates the rational equation to $4xyz=n(yz+xz+xy)$ under strict positivity. Positive scaling transports a solution for $n$ to one for $kn$ while preserving the strict order. An explicit even-number family supplies the case needed for the prime reduction.
The elementary families cover $3\mid n$, $n\equiv2\pmod3$, $n\equiv3\pmod4$, and $n\equiv5\pmod8$, with the displayed witnesses and their integrality and strict ordering recorded in separate statements. Together with the even case, they solve every $n>2$ outside $1\pmod{24}$. The useful reduction is an equivalence between the root goal and its restriction to primes $p\equiv1\pmod{24}$; the ordinary prime reduction is also stated separately. The classical scaling and residue observations are discussed in [Bloom–Elsholtz, p. 239](https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf).
Obláth’s milestone says that $\mathrm{IsErdosStraus}(n)$ holds for $n>2$ whenever $n+1$ has a prime divisor $q\equiv3\pmod4$. This condition is explicitly recorded in the introduction of [Pomerance–Weingartner](https://math.dartmouth.edu/~carlp/ESS-ExceptionsV9.pdf), which identifies the original Obláth reference. The exact distinctness requirement is retained in this mission.
The **Mordell–Yamamoto milestone** asks for a decomposition for every prime $p>2$ satisfying
$$p\bmod840\notin\{1,121,169,289,361,529\}.$$
The actual existence claim is the theorem to prove. It has no hypothesis asserting that these classes are covered. [Yamamoto’s original paper, §§3–4, pp. 42–46](https://www.jstage.jst.go.jp/article/kyushumfs/19/1/19_1_37/_pdf/-char/en), supplies the congruence framework and prints this residual list. The same list appears in the current Erdős Problems record. The list printed on p. 239 of Bloom–Elsholtz instead contains $49$ and omits $529$; that discrepant list is not used here. The historical papers often permit repeated denominators, so producing distinct ordered witnesses is an explicit part of the formalization obligation.
## What these results provide
The elementary infrastructure gives reusable certificates and transports for exact rational decompositions. The reductions identify a mathematically meaningful remaining domain without assuming the conjecture. Completion of the modulo-$840$ milestone would leave the prime cases in its six residual classes as the classical research frontier; those classes are not asserted to consist of counterexamples.
Later targets include [Terzi’s 1971 sieve](https://doi.org/10.1007/BF01934370), whose publisher abstract reports 198 residual classes modulo $120120$, and [Vaughan’s density theorem](https://doi.org/10.1112/S0025579300002886), bounding the exceptional count by $X\exp(-c(\log X)^{2/3})$ for a positive constant $c$. Neither is a core Lean statement in this draft. No unaudited list of 198 classes is supplied.
[Elsholtz–Tao](https://arxiv.org/abs/1107.1010) provide counting results and a classification of polynomially soluble congruences. [Bloom–Elsholtz, Theorem 1, pp. 239–240](https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf), characterize their conjecture by coverage of all primes by classes
$$-a/c\pmod{4acd-1}\quad(a,c,d\ge1),$$
or
$$-(4c^2d+1)/k\pmod{4cd}\quad(c,d,k\ge1,\ k\mid4c^2d+1).$$
Here division by $c$ denotes a modular inverse; division by $k$ is exact integer division. The authors are **Bloom and Elsholtz**, not Bradford and Elsholtz. This is a later formalization target: an initial core theorem is not included until the translation between that paper’s denominator convention and the present strict convention is separately formalized. [Pomerance–Weingartner](https://math.dartmouth.edu/~carlp/ESS-ExceptionsV9.pdf) address growing numerators in the generalized problem; their exceptions are not counterexamples to the fixed numerator $4$ conjecture.
## The remaining difficulty
Congruence identities prove infinite families only when the identities and their arithmetic hypotheses are established for arbitrary parameters. Checking finitely many representatives with a search program does not prove that all future values in an arithmetic progression work. Density estimates also allow an exceptional set and therefore do not settle the universal statement.
The current record cites [Mihnea–Bogdan (2025)](https://arxiv.org/abs/2509.00128) for computational verification through $10^{18}$. This is reported computational evidence, not a Lean-certified theorem in this mission. No universal conclusion or periodicity assertion is inferred from it.
## Formalization scope
The development uses natural-number denominators, exact rational arithmetic, integer polynomial identities, divisibility, primality, and natural-number remainders. Definitions are transparent. The root is not hidden in a typeclass, structure field, certificate, or extra assumption, and its quantifier is not bounded. The existing [Google DeepMind transcription](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/242.lean) is a statement reference, not an imported proof.
The draft targets Mathlib `0df444a360eaa60ab8c11dca51a86af692955474` with Lean `4.33.1`. Every proposed statement has been locally elaborated and supplied with an independent read-back. Statement elaboration with `sorry` is not proof verification. The accompanying local proof audit distinguishes the proved supporting results from the open root and the remaining modulo-$840$ formalization task.
## Selected references
- Erdős, *Az … egyenlet egész számú megoldásairól*, Mat. Lapok **1** (1950), 192–210; [original scan](https://www.renyi.hu/~p_erdos/1950-02.pdf).
- Erdős–Graham, *Old and New Problems and Results in Combinatorial Number Theory* (1980), chapter IV; [author’s institutional scan](https://mathweb.ucsd.edu/~ronspubs/80_11_number_theory.pdf).
- Obláth, *Sur l’équation diophantienne $4/n=1/x_1+1/x_2+1/x_3$*, Mathesis **59** (1950), 308–316; [bibliographic record](https://www.erdosproblems.com/bibs/Ob50), also cited in Pomerance–Weingartner.
- Yamamoto, *On the Diophantine Equation $4/n=1/x+1/y+1/z$*, Mem. Fac. Sci. Kyushu Univ. A **19** (1965), 37–47; [original paper](https://doi.org/10.2206/kyushumfs.19.37).
- Mordell, *Diophantine Equations*, Academic Press (1969), chapter 30, pp. 287–290; [publisher record](https://shop.elsevier.com/books/diophantine-equations/mordell/978-0-12-506250-3).
- Terzi (1971), Vaughan (1970), Elsholtz–Tao (2013), Bloom–Elsholtz (2022), Mihnea–Bogdan (2025), and Pomerance–Weingartner (2025/2026): primary sources linked at their statements above.
## Motivation
Let $G=(V,E)$ be a finite connected graph. In **Bernoulli bond percolation** each edge is independently retained with probability $P$ and deleted otherwise, and one writes $\mathbb{P}_P[u \leftrightarrow v]$ for the probability that vertices $u$ and $v$ lie in the same component of the resulting random subgraph. Comparing such connection probabilities is a basic and genuinely hard problem: computing them exactly is $\#\mathsf{P}$-hard.
The **bunkbed graph** is built from two copies of $G$, joined by vertical edges called *posts* above a chosen set $T \subseteq V$ of *transversal* vertices. Percolation is performed on the two copies while every post is retained. Writing $v$ for a vertex in the lower copy and $v'$ for its counterpart upstairs, Kasteleyn conjectured in 1985 that being connected within a level is always at least as likely as crossing between levels.
The conjecture is intuitively compelling — crossing levels appears to require "using up" a post — and it resisted proof for forty years. A short timeline:
- **1985** — Kasteleyn formulates the conjecture; it is recorded as Remark 5 of van den Berg–Kahn (2001), which is how the source cites it.
- Positive results accumulate for special cases: wheels, complete graphs, complete bipartite graphs, graphs symmetric with respect to an automorphism exchanging $u$ and $v$, one or two transversal vertices, and in the $P \uparrow 1$ limit.
- **2024** — [Hollom](https://arxiv.org/abs/2406.01790) refutes the $3$-uniform **hypergraph** analogue. This alone does not settle the graph case: it is impossible to simulate a single $3$-hyperedge by bond percolation on a gadget graph.
- **2025** — [Gladkov, Pak and Zimin](https://doi.org/10.1073/pnas.2420725122) disprove the conjecture outright, with an explicit counterexample and *without* computer assistance.
Section 7 of the source is a candid account of a large-scale machine-learning-guided search that **failed** to find a counterexample, and of why the problem is unusually ill-suited to experimental testing.
## Setting
Fix a finite graph with vertex set $V$ and edge set $E$, and a retention function $w : E \to [0,1]$ (the uniform case is $w \equiv P$). A **configuration** is a subset $S \subseteq E$ of open edges, occurring with probability
$$\mathbb{P}(S) \;=\; \prod_{e \in S} w(e) \prod_{e \in E \setminus S} \bigl(1 - w(e)\bigr),$$
and $\mathbb{P}[u \leftrightarrow v]$ is the total probability of those $S$ for which $u$ and $v$ are connected in $(V, S)$.
Given $T \subseteq V$, the **bunkbed graph** has vertex set $V \times \{0,1\}$. Its edges are a copy of $E$ in each level together with a post $\{(t,0),(t,1)\}$ for every $t \in T$. In **bunkbed percolation** the two level-copies are percolated independently while all posts are retained; $\mathbb{P}^{\mathrm{bb}}$ denotes the resulting connection probabilities.
## Formalization targets
### Goal — the bunkbed conjecture is false
$$\neg\;\Bigl(\forall\,G \text{ connected},\ \forall\,T \subseteq V,\ \forall\,0<P<1,\ \forall\,u,v \in V:\quad \mathbb{P}^{\mathrm{bb}}_P[u \leftrightarrow v] \;\ge\; \mathbb{P}^{\mathrm{bb}}_P[u \leftrightarrow v'] \Bigr)$$
### Supporting target — the explicit counterexample (Theorem 1.2)
$$\exists\, G,\ |V| = 7{,}222,\ |E| = 14{,}442,\ |T| = 3,\ \exists\, u,v:\qquad \mathbb{P}^{\mathrm{bb}}_{1/2}[u \leftrightarrow v] \;<\; \mathbb{P}^{\mathrm{bb}}_{1/2}[u \leftrightarrow v']$$
### Supporting target — hyperedge simulation (Lemma 4.1)
For the gadget $G_n$ on $n+1$ vertices,
$$P_{abc}\,P_{a|b|c} \;-\; P_{ab|c}\,P_{ac|b} \;>\; \Bigl(n\tfrac{1-P}{1+P} - 1\Bigr) P_{a|bc}.$$
## Significance
*The result itself.* A forty-year-old conjecture in percolation theory is false, and prior positive results are thereby sharpened rather than superseded: it becomes interesting to delimit exactly which families of graphs do satisfy the inequality. The refutation also settles the Counting, Weighted, Alternative and Computational variants listed in §8.1, and shows the random-cluster analogue cannot be pushed from $q=2$ down to $q=1$.
*Formalizing it.* Nothing here is open; the mission produces machine-checked versions of published results, and as a by-product the first percolation theory in Lean. Mathlib currently contains **no percolation of any kind** — no connection probabilities, no bunkbed graph, no hypergraph percolation. That infrastructure is reusable far beyond this mission. The source itself notes (§8.2) that its central combinatorial lemma was independently verified by computer; a formal proof would replace that check with a certificate.
## Difficulty
The obvious approach — exhibit a small graph and compute both probabilities — is hopeless, and the source explains why at length. A graph with $m$ edges has $2^m$ configurations; for the counterexample here the probability gap is on the order of $10^{-4331}$, so no sampling argument can detect it, and exact enumeration is out of reach. Section 7 records a substantial computational search that found nothing and, in hindsight, could not have.
The proof is instead structural, and its difficulty is concentrated in one place. Hollom's refutation of the hypergraph version cannot be transferred directly, because a single $3$-hyperedge **cannot** be simulated by bond percolation on any gadget graph. The source's answer is to prove a *robust* version of Hollom's lemma (Lemma 3.3) which survives the inexact simulation that gadget graphs do provide, and this robustness is what Lemma 4.1's inequality quantifies. Lemma 3.3 is proved by constructing a weight-preserving involution on a refined configuration space — the technical heart, and the milestone a solver should expect to spend the most effort on.
## Formalization scope
The development commits to the following conventions.
- Everything is **finite and rational-valued**, hence computable: connection probabilities are `ℚ` and evaluate by `#eval`, and small instances close by `decide`.
- A graph is given by an explicit edge `Finset` and realised through `SimpleGraph.fromEdgeSet`; connectivity is Mathlib's `SimpleGraph.Reachable`.
- Percolation is a **sum over the powerset of the edge set**, weighted as displayed above, of a reachability indicator. Edge weights are per-edge (`Sym2 V → ℚ`), since the gadget $G_n$ genuinely needs two different weights: its spokes are retained with probability $1-P$ and its path edges with probability $P$.
- In the bunkbed, level `0` is the lower copy; posts over `T` are **unconditionally present** and are not percolated. The two levels are percolated independently.
- ⚠️ **Planarity is omitted from the goal.** Theorem 1.2 asserts the counterexample is planar, and Mathlib has no notion of a planar graph — no `IsPlanar`, no Euler formula, no Kuratowski. Building one is a larger project than this mission. The formalized statement of Theorem 1.2 is therefore strictly weaker than the published one, and the goal is instead the negation of the conjecture, which is exactly the source's own "In particular, the BBC is false." Contributions adding planarity are welcome and would strengthen the milestone.
- Ruling out a trivializing reading: the conjecture must be negated as stated, over *all* connected graphs, transversal sets and $0<P<1$. Weakening it to a fixed graph, or to $P \in \{0,1\}$, or dropping connectivity, would make the refutation vacuous.
**Infrastructure.** Mathlib supplies `SimpleGraph`, `boxProd`, `Reachable` with a `DecidableRel` instance, `fromEdgeSet`, `edgeFinset` and `Finset.powerset`. It supplies no percolation, so this mission ships two definition files: Bernoulli bond percolation with the bunkbed construction and the five triple-partition probabilities, and hypergraph percolation with Hollom's hypergraph and the Wierman–Ziff five-state model. One known gap: Mathlib's `Reachable` decision procedure enumerates walks and is far too slow to evaluate the $64$-configuration check of Lemma 3.1 by `decide`. A solver will want a linear-time reachability procedure together with a proof that it agrees with `Reachable`; that is itself a worthwhile reusable contribution.
## Selected references
- J. van den Berg and J. Kahn, *A correlation inequality for connection events in percolation*, Ann. Probab. **29** (2001), 123–126 — Kasteleyn's conjecture appears as Remark 5.
- T. Hollom, *A new proof of the bunkbed conjecture in the $p \uparrow 1$ limit*, Discrete Math. **347** (2024), 113711.
- T. Hollom, *The bunkbed conjecture is not robust to generalisation*, [arXiv:2406.01790](https://arxiv.org/abs/2406.01790) (2024).
- T. Hutchcroft, P. Nizić-Nikolac, A. Kent, *The bunkbed conjecture holds in the $p \uparrow 1$ limit*, Comb. Probab. Comput. **32** (2023), 363–369.
- N. Gladkov, I. Pak, A. Zimin, *The bunkbed conjecture is false*, Proc. Natl. Acad. Sci. USA **122** (2025), no. 24, e2420725122. [doi:10.1073/pnas.2420725122](https://doi.org/10.1073/pnas.2420725122); preprint [arXiv:2410.02545](https://arxiv.org/abs/2410.02545).
- J. C. Wierman and R. M. Ziff, *Self-dual planar hypergraphs and exact bond percolation thresholds*, Electron. J. Combin. **18** (2011).
- G. R. Grimmett, *Percolation*, 2nd ed., Springer, 1999.
Counterexamples to the Zeng–Pryadko Homological-Distance ConjectureResearch Paper
## Background and main question
The tensor product of chain complexes is a basic construction in homological algebra and in the theory of quantum CSS codes. If $A$ and $B$ are finite based chain complexes over a finite field, their tensor product is graded by total degree,
$$
(A\otimes B)_j=\bigoplus_{i=0}^{j} A_i\otimes B_{j-i}.
$$
Each complex carries a basis-dependent homological distance: $d_j(A)$ is the least Hamming weight of a degree-$j$ cycle that is not a boundary, with $d_j(A)=\infty$ when the degree-$j$ homology vanishes. A natural candidate for the distance of the tensor product is therefore
$$
m_j(A,B)=\min_{0\le i\le j} d_i(A)d_{j-i}(B).
$$
Every nonzero pair of homology classes in complementary degrees gives a pure-tensor class of the corresponding product weight, so one always has $d_j(A\otimes B)\le m_j(A,B)$. The substantive question is whether this upper bound is always sharp.
In the preprint [*Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates*](https://arxiv.org/abs/1810.01519), posted in 2018 and subsequently [published in *Physical Review Letters*](https://link.aps.org/doi/10.1103/PhysRevLett.122.230501), Zeng and Pryadko proved that the bound is sharp when one factor is a binary one-complex. Their exact formula is Eq. (13) of the arXiv version and is the capstone theorem of the Prove2Me mission [*Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates*](https://prove2.me/missions/Higher-Dimensional%20Quantum%20Hypergraph-Product%20Codes%20with%20Finite%20Rates). The present formalization is a direct sequel: it retains the same definitions and degree conventions while examining what happens when the one-complex restriction is removed.
Zeng and Pryadko later considered arbitrary finite chain complexes over arbitrary finite fields in [*Minimal distances for certain quantum product codes and tensor products of chain complexes*](https://link.aps.org/doi/10.1103/PhysRevA.102.062402), published in 2020. In [the corresponding arXiv preprint](https://arxiv.org/abs/2007.12152), Conjecture 18 asserts the unrestricted equality
$$
d_j(A\otimes B)=m_j(A,B).
$$
The conjecture is appealing because it would make tensor-product distance completely compositional: the degreewise distances of the two factors would determine the distance of their product. The obstruction is that a homology class in $A\otimes B$ need not have a minimum-weight representative supported in a single bidegree. A representative spread across several summands of the total complex can be lighter than every pure-tensor representative. The purpose of this formalization is to turn that observation into a concrete, machine-checked counterexample to Conjecture 18 while preserving the valid one-complex theorem as a sharply delimited special case.
## The counterexample mechanism
The common foundation is recorded in the Prove2Me entry [*Based binary chain complexes and homological distance*](https://prove2.me/theorems/9d65f1ac-c78c-4540-8ac4-38597548a9ff). In particular, the boundary in degree $j$ is a map $\partial_j:A_j\to A_{j-1}$, and
$$
d_j(A)=\inf\{\operatorname{wt}(x):x\in\ker\partial_j,\ x\notin\operatorname{im}\partial_{j+1}\}.
$$
The one-complex result is separately available as [*Eq. (13) — Exact distance with a one-complex*](https://prove2.me/theorems/4f4006fe-af5b-42ba-a936-bb49e92c92b6). The construction below uses exactly the same notion of distance, but both tensor factors are genuine three-term complexes.
Begin with binary CSS check maps
$$
H_X:\mathbb F_2^n\longrightarrow\mathbb F_2^{r_X},
\qquad
H_Z:\mathbb F_2^n\longrightarrow\mathbb F_2^{r_Z},
$$
assumed surjective and satisfying $H_XH_Z^T=H_ZH_X^T=0$. Suppose there are logical vectors $x,z\in\mathbb F_2^n$ such that
$$
H_Zx=0,\qquad H_Xz=0,\qquad x\cdot z=1.
$$
The check maps determine two dual three-term complexes
$$
A:\quad \mathbb F_2^{r_X}\xleftarrow{H_X}\mathbb F_2^n
\xleftarrow{H_Z^T}\mathbb F_2^{r_Z},
\qquad
B:\quad \mathbb F_2^{r_Z}\xleftarrow{H_Z}\mathbb F_2^n
\xleftarrow{H_X^T}\mathbb F_2^{r_X}.
$$
Their degree-two tensor space has three bidegree summands, corresponding to $(2,0)$, $(1,1)$, and $(0,2)$. Under the natural matrix identifications, consider the element whose three blocks are
$$
(I_{r_Z},I_n,I_{r_X}).
$$
The CSS orthogonality relations make this element a cycle. Its pairing with the chosen logical vectors certifies that it is not a boundary. Its Hamming weight is exactly $r_Z+n+r_X$, whereas the componentwise candidate in degree two reduces to
$$
m_2(A,B)=d_1(A)d_1(B).
$$
Consequently, any CSS datum satisfying
$$
r_Z+n+r_X<d_1(A)d_1(B)
$$
produces the strict inequality $d_2(A\otimes B)<m_2(A,B)$. For orientation, a binary quantum Golay CSS presentation with parameters $[[23,1,7]]$ has $r_X=r_Z=11$, giving the numerical comparison $45<49$. The formal proof must supply an explicit CSS instance and verify its algebraic and distance properties, rather than relying on the parameter notation alone.
## Formalization objectives
The first milestone proves the general certificate: for every CSS datum satisfying the hypotheses above, the element $(I_{r_Z},I_n,I_{r_X})$ is a nontrivial degree-two cycle of weight $r_Z+n+r_X$, and the componentwise minimum is $d_1(A)d_1(B)$.
The second milestone constructs and verifies one explicit CSS datum for which $r_Z+n+r_X<d_1(A)d_1(B)$. This is the step that turns the general mechanism into an actual counterexample.
The capstone packages the construction as the direct existential statement
$$
\exists\,A,B\qquad d_2(A\otimes B)<\min_{0\le i\le 2}d_i(A)d_{2-i}(B).
$$
Thus the final theorem is not conditional on the existence of suitable code data: it exhibits finite based binary chain complexes for which the equality proposed in Conjecture 18 fails.
## Relation to prior work
The counterexample concerns only the unrestricted passage from a one-complex factor to two arbitrary bounded complexes. It does not conflict with Zeng and Pryadko's Eq. (13), whose one-complex hypothesis rules out the three-bidegree interaction used here.
The broader literature also indicates why additional structure matters. [Bravyi and Hastings](https://dl.acm.org/doi/10.1145/2591796.2591870) introduced homological-product codes and analyzed logical representatives in product constructions; [Audoux and Couvreur](https://www.numdam.org/articles/10.4171/aihpd/71/) developed tensor products of CSS codes through chain-complex methods. More recently, [Akhmechet et al.](https://arxiv.org/abs/2410.11252) discussed the Zeng–Pryadko conjecture in the structured setting of complexes derived from Khovanov homology, while [Berthusen et al.](https://arxiv.org/abs/2508.04794) restated it as Conjecture 5.1 in their study of automorphism gadgets. [Golowich and Guruswami](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.25) obtained strong distance guarantees for iterated homological products under expansion and local-testability hypotheses. These results are compatible with the proposed counterexample: they concern special families or impose hypotheses that are absent from Conjecture 18.
Besides settling the unrestricted statement, the formalization isolates a reusable obstruction. It shows precisely how a low-weight class assembled across several bidegrees can evade a formula based only on the degreewise distances of the factors. This distinction should help guide corrected formulations in which an exact product formula, or a useful lower bound, is recovered from additional geometric, expansion, or local-testability assumptions.
The main formal issues are mathematically substantive rather than presentational: the proof must respect the endpoint conventions for the boundary maps, distinguish a cycle from a non-boundary, compare finite weights with $\infty$-valued distances, and verify a concrete strict-gap instance. Making each of these points explicit is especially important here, because an indexing shift or a merely conditional existence statement would no longer constitute a refutation of the conjecture as stated.
## References
- W. Zeng and L. P. Pryadko, [*Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates*](https://link.aps.org/doi/10.1103/PhysRevLett.122.230501), *Physical Review Letters* 122, 230501 (2019); [arXiv:1810.01519 (2018), Eq. (13)](https://arxiv.org/abs/1810.01519).
- W. Zeng and L. P. Pryadko, [*Minimal distances for certain quantum product codes and tensor products of chain complexes*](https://link.aps.org/doi/10.1103/PhysRevA.102.062402), *Physical Review A* 102, 062402 (2020); [arXiv:2007.12152, Conjecture 18](https://arxiv.org/abs/2007.12152).
- S. Bravyi and M. B. Hastings, [*Homological Product Codes*](https://dl.acm.org/doi/10.1145/2591796.2591870), STOC 2014; [arXiv:1311.0885](https://arxiv.org/abs/1311.0885).
- B. Audoux and A. Couvreur, [*On tensor products of CSS codes*](https://www.numdam.org/articles/10.4171/aihpd/71/), *Annales de l'Institut Henri Poincaré D* 6 (2019); [arXiv:1512.07081](https://arxiv.org/abs/1512.07081).
- R. Akhmechet et al., [*Khovanov homology and quantum error-correcting codes*](https://arxiv.org/abs/2410.11252), arXiv:2410.11252 (2024).
- N. Berthusen et al., [*Automorphism gadgets in homological product codes*](https://arxiv.org/abs/2508.04794), arXiv:2508.04794 (2025).
- L. Golowich and V. Guruswami, [*Quantum LDPC Codes of Almost Linear Distance via Iterated Homological Products*](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.25), CCC 2025; [full version](https://arxiv.org/abs/2411.03646).
## Motivation
A quantum circuit of depth $d$ built from gates of fan-in at most two cannot let an output
wire depend on more than $2^d$ input wires. The argument is folklore and takes a paragraph on
paper: the *causal cone* of the measured wire grows by at most a factor of two per layer.
Formalizing it exposes a subtlety that the paper argument hides, and that is what this mission
is about.
## The subtlety
Define the backward cone step of a wire set $S$ through a layer $l$ by adjoining the support of
every gate of $l$ that meets $S$. There is a choice here: test each gate against the **incoming**
set $S$, or against the **partially accumulated** cone. Testing against the accumulator
over-approximates, and the doubling bound fails. Testing against the incoming set gives the
bound — but is only *correct* when the gates within a layer act on pairwise disjoint wires.
Without that hypothesis (`LayerOk`) the semantic statement is false, and the counterexample is
small: on three wires, the single layer `[cnot 2 1, cnot 1 0]` has cone $\{0,1\}$ around wire
$0$, yet wire $0$ ends up holding $x_0 \oplus x_1 \oplus x_2$. So the cone under-approximates
the true dependence. This mission's development carries `LayerOk` throughout, and the
counterexample is recorded in the source.
## What is formalized
Layered circuits over $\{H, S, T, \mathrm{CNOT}\}$ on $n$ wires, with states as amplitude
functions on bit-strings and no tensor products anywhere. On top of that:
- the combinatorial half — one layer at most doubles the cone, hence $|\mathrm{cone}| \le 2^{d}\,|S|$;
- norm preservation, so that `acceptProb` is a genuine probability in $[0,1]$;
- the semantic half — inputs agreeing on the causal cone of the output wire are accepted with
*equal probability*.
The semantic half is proved in the Heisenberg picture. The measurement observable is conjugated
backwards through the circuit and its support tracked: a gate meeting the support enlarges it by
that gate's own wires, and a gate missing it **commutes** with the observable and cancels against
its own adjoint. That cancellation is the reason the non-cascading cone step is correct, and it is
why unitarity of the gate set is needed at the $2^n$-dimensional level rather than gate by gate.
Supporting this is a small reusable algebra of local operators: locality is monotone, closed under
adjoint and product, and disjointly supported operators commute.
## The frontier
The published depth bound assumes each input wire lies in the *syntactic* cone of the output. That
is weaker than saying the wire *matters*. Milestone 1 asks for the semantically honest version,
stated in terms of genuine functional dependence; the bridge is the semantic cone theorem already
in the development.
Beyond that, the natural continuations are the same argument for fan-in-$k$ gates
($|\mathrm{cone}| \le k^{d}$), for geometrically local circuits where cone growth is linear
rather than exponential, and ultimately the Bravyi–Gosset–König separation
$\mathrm{QNC}^{0} \not\subset \mathrm{NC}^{0}$ — which needs machinery (non-local games, magic
squares) that this development deliberately does not build.
Oracle-Parameterized Convergence Rates: SPIDER, Q-SPIDER, and the Exact CrossoverResearch Paper
## Motivation
Quantum algorithms for stochastic optimization are usually presented one paper at a time: a schedule is fixed, a quantum mean estimator is substituted for a classical minibatch, and a new rate is derived from scratch. The derivations are near-identical, and the step that actually differs — the price of one gradient query — is buried inside each proof rather than exposed as a parameter.
This mission publishes a Lean 4 development in which **the oracle is a parameter, not an assumption**. One rate theorem, instantiated at different oracle contracts and cost models, yields the classical rate, the inexact-gradient rate, and the quantum rate. All constants are explicit; nothing is asymptotic.
The published results it reproduces or corrects:
- **Ghadimi--Lan (2013)**, the $\varepsilon^{-4}$ rate for smooth nonconvex SGD.
- **Fang et al.**, the classical SPIDER variance-reduction schedule and its $\varepsilon^{-3}$ query complexity.
- **Sidford--Zhang**, *Quantum speedups for stochastic optimization* ([arXiv:2308.01582](https://arxiv.org/abs/2308.01582)) — Theorem 6's $\tilde O(\Delta\ell\sigma\sqrt{d}\,\varepsilon^{-3})$ and Theorem 8's $\tilde O(\ell\Delta\sqrt{d\sigma}\,\varepsilon^{-5/2})$, both obtained here from *one* schedule evaluated at two cost exponents.
## Setting
Let $E$ be a real inner-product space, $f:E\to\mathbb{R}$ an objective, and $g:E\to E$ a map supplied as a parameter in place of the gradient. The smoothness hypothesis is the descent-lemma inequality
$$f(y)\;\le\;f(x)+\langle g(x),y-x\rangle+\tfrac{L}{2}\|y-x\|^{2},$$
written $\mathrm{QuadUpper}\,f\,g\,L$; this is exactly what rate proofs consume, and it is implied by a Lipschitz gradient. Write $\Delta_0=f(x_0)-f^{\star}$ for the initial gap, $\varepsilon$ for the target accuracy, $\sigma$ for the gradient-noise scale, $\ell$ for the mean-squared smoothness constant, and $d$ for the ambient dimension.
A **cost model** converts a target accuracy into a query count as a power law with exponent $p$. Its $p=2$ member is the classical minibatch bill, scaling as $\sigma^{2}/\varepsilon^{2}$; its $p=1$ member is the quantum mean-estimation bill, scaling as $\sigma/\varepsilon$. That single exponent is where classical and quantum part company.
## Target
The goal theorem is the exact crossover between the two SPIDER bills. Writing $Q$ and $C$ for the dominant terms of the quantum and classical query totals,
$$Q=\frac{64000\,\ell\Delta\sqrt{d}\sqrt{10\sigma}}{\varepsilon^{2}\sqrt{\varepsilon}},\qquad C=\frac{25\,728\,000\,\ell\Delta\sigma}{\varepsilon^{3}},$$
the target asserts, for $\ell,\Delta,\sigma,\varepsilon>0$ and $d\ge0$,
$$Q<C\quad\Longleftrightarrow\quad d\,\varepsilon<16000\,\sigma .$$
Every supporting rate is also published and proved: the two SPIDER query totals, SPIDER's correctness, the SGD and PL rates, the exact and inexact gradient-descent rates, the two variance-purchase bills, and the two query counts.
## Significance
*The results.* The crossover makes the dimension-versus-accuracy trade-off of quantum stochastic optimization quantitative rather than folkloric. Two readings follow directly: at fixed $d$ the quantum advantage disappears as $\varepsilon\to0$, so the speedup lives at moderate accuracy, not asymptotically; and at fixed $\varepsilon$ the advantage requires $d<16000\sigma/\varepsilon$. Note what cancels — $\ell$, $\Delta$ and the $\varepsilon$-exponent all drop out, leaving only $d\varepsilon$ against $\sigma$.
*The formalization.* Because the oracle and the cost exponent are parameters, the classical and quantum rates are one theorem evaluated twice rather than two proofs. This mission is unusual in that its frontier is already closed: every node arrives with a machine-checked proof, transplanted from a green build. What it offers the platform is a reusable, fully-proved layer for first-order convergence analysis — function classes, cost models, a one-step descent recursion, accumulation laws including a stopped-time version, and the SPIDER schedule — on which further rates can be built by instantiation.
## Difficulty
The apparent difficulty is not where a newcomer expects. Deriving a rate from the one-step recursion is routine telescoping. What is delicate is keeping the constants honest while the oracle varies: a rate proof that quietly assumes an exact gradient, or a global lower bound on $f$, will produce the right-looking exponent from the wrong hypotheses.
Two specific places carry real content. Evaluating an error recursion at a **random return time** breaks the unconditional variance bound, because conditioning on $\tau=k$ destroys independence; the stopped-time accumulation law is what repairs it. And reproducing a published constant exactly — rather than up to $\tilde O(\cdot)$ — is what certifies that the parametrized machinery has not silently degraded the bound it generalizes.
## Formalization scope
Smoothness is `QuadUpper` on an explicitly supplied `g`; no differentiability or convexity is assumed anywhere, and the only lower-bound hypothesis is $f^{\star}\le f(x_K)$ at the terminal iterate rather than globally. Cost models are an inductive family with a power-law member, so the classical and quantum instances are $p=2$ and $p=1$ of one definition. Half-integer powers are written with `Real.sqrt`, so no real exponentiation appears in any statement. Stochastic results use a genuine `Filtration` and a conditional oracle contract; the tower property is derived, not assumed.
Two honesty notes. Several statements carry hypotheses that Lean marks unused; these are recorded as such in the individual nodes rather than presented as load-bearing. And the library records a discrepancy in Sidford--Zhang's Algorithm 7 parameter block, documented in its own STATUS notes; the formalization follows the corrected parameters.
## Selected references
- S. Bubeck-style descent machinery aside, the rates reproduced here are: S. Ghadimi and G. Lan, *Stochastic first- and zeroth-order methods for nonconvex stochastic programming*, SIAM J. Optim. 23(4) (2013).
- C. Fang, C. J. Li, Z. Lin, T. Zhang, *SPIDER: Near-optimal non-convex optimization via stochastic path-integrated differential estimator*, NeurIPS 2018.
- A. Sidford and C. Zhang, *Quantum speedups for stochastic optimization*, [arXiv:2308.01582](https://arxiv.org/abs/2308.01582).
- Source development: `lean-optrates`, [github.com/shiy1022/lean-optrates](https://github.com/shiy1022/lean-optrates) at commit `4c0b8498`, Apache-2.0, by Yueheng Shi. The platform copy renames the root namespace `OptRates` to `ShiOptRates`; no statement or proof is otherwise altered.
Dynamic Programming and Optimal Control VI: Lookahead and RolloutTextbook
## Motivation
When exact dynamic programming is intractable, practice runs on approximations: one-step and multistep lookahead with a cost-to-go surrogate, open-loop feedback control, and rollout — the algorithm that improved backgammon programs and became a conceptual ancestor of Monte-Carlo tree search and modern policy improvement schemes. Chapter 6 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) gives the basic guarantees: performance bounds for limited lookahead (Props. 6.3.1–6.3.2), superiority of open-loop feedback control over open-loop control (Prop. 6.2.1), and the cost-improvement theory of rollout on discrete deterministic problems (Props. 6.4.1–6.4.3). These are the theorems that make "approximate DP" more than a heuristic.
## Setting
Two frameworks. For the stochastic bounds (§6.2–6.3): the basic finite-horizon model of Mission I of this series (`BertsekasDPModel`), its policy cost recursion, and the open-loop cost of a fixed control sequence (`BertsekasDPOpenLoopCost`). For rollout (§6.4.1): a **graph search problem** — a finite digraph with destination set and terminal costs $g(i)$ on destinations (`BertsekasGraphSearch`); a **base heuristic** $\mathcal{H}$ producing from every node a path to a destination (`BertsekasBaseHeuristic`), with projection $p(i)$ and heuristic cost $H(i) = g(p(i))$; the **rollout algorithm** $R\mathcal{H}$ repeatedly moves to a neighbor $j$ minimizing $H(j)$ (`BertsekasIsRolloutRun`). $\mathcal{H}$ is *sequentially consistent* if its paths have the tail property (Def. 6.4.1), *sequentially improving* if $\min_{j \in N(i)} H(j) \le H(i)$ (Def. 6.4.2).
## Target
For sequentially improving $\mathcal{H}$ and any terminating rollout run $(i_1, \dots, i_{\bar m})$:
$$g(i_{\bar m}) \;\le\; H(i_1), \qquad g(i_{\bar m}) \;=\; \min\Big\{ H(i_1),\ \min_{j \in N(i_1)} H(j),\ \dots,\ \min_{j \in N(i_{\bar m - 1})} H(j) \Big\},$$
— `BertsekasDP.rollout_sequential_improvement` (goal, Prop. 6.4.2). Milestones: Props. 6.4.1 (termination under sequential consistency with the book's tie-breaking), 6.4.3 (exact cost identity via the defects $\delta_i$), 6.3.1, 6.3.2 (lookahead bounds), 6.2.1 (OLFC).
## Significance
Prop. 6.4.2 is the "rollout never hurts" theorem — the formal warrant for policy improvement by simulation, with Prop. 6.3.1 its stochastic counterpart (via Example 6.3.1 the rollout of any policy improves that policy). Prop. 6.3.2 is the robustness version that quantifies the cost of inexact minimization, used for CEC bounds. Formalizing the chapter yields a reusable graph-search + base-heuristic vocabulary and connects it to the Mission I stochastic model. Everything here is proved in the book; the formal versions are new.
## Difficulty
The rollout proofs are elementary but exact: the min formula (6.37) requires tracking the running minimum along the run, and the `IsLeast` membership half forces identifying which neighbor value is attained. Termination under sequential consistency (6.4.1) is the delicate one — it fails without the tie-breaking convention (the book gives a cycling counterexample), so the formal statement carries the convention explicitly and the proof must extract a termination measure from "strict decreases are finitely many, plateaus shorten the heuristic path". The stochastic bounds are clean backward inductions over the Mission I recursion.
## Formalization scope
Graph search: finite node type, arcs as ordered pairs, vertex costs only (no arc costs — the book's reduction absorbs them into destination costs); heuristic paths as lists; rollout runs as lists (finite, complete runs) except 6.4.1, where the run is an infinite sequence absorbed at destinations so that termination is a genuine claim. Ties in neighbor selection are allowed everywhere except where 6.4.1's convention pins them. Stochastic side: state-independent constraint sets for OLFC (as in §6.2); restricted lookahead sets $\bar U_k(x) \subseteq U_k(x)$ per Eq. (6.19); all statements at the level of the Mission I model.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (§6.2–6.4.) http://www.athenasc.com/dpbook.html
- G. Tesauro, G. R. Galperin, On-line policy improvement using Monte-Carlo search, *NIPS* 1996. https://papers.nips.cc/paper/1302
- D. P. Bertsekas, J. N. Tsitsiklis, C. Wu, Rollout algorithms for combinatorial optimization, *J. Heuristics* 3 (1997), 245–262. https://doi.org/10.1023/A:1009635226865
Rothvoß Discrepancy Notes I: Spencer's Theorem via the Entropy MethodTextbook
## Motivation
**Discrepancy theory** asks how unbalanced a two-coloring of a combinatorial structure must be in the worst case. Concretely: given $n$ sets over an $n$-element ground set, color each element $+1$ or $-1$ so that every set is as close to balanced as possible. The question is classical (Beck–Fiala 1981; Spencer 1985) and the answer for general (dense) set systems is one of the sharpest gaps between a naive probabilistic bound and the truth known in combinatorics: assigning colors uniformly at random only guarantees discrepancy $\Theta(\sqrt{n\log n})$, yet a coloring with discrepancy $O(\sqrt n)$ always exists — the logarithmic factor is an artifact of the naive argument, not of the problem. This mission formalizes that removal, following T. Rothvoß's lecture-note exposition of J. Spencer's **entropy method** ([MIT 18.095, "Discrepancy theory"](https://math.mit.edu/classes/18.095/lect6/notes.pdf)), the standard modern presentation of the technique (see also Matoušek, *Geometric Discrepancy*, Ch. 4). The entropy method is the ancestor of the whole "partial coloring" family of arguments used throughout discrepancy theory and combinatorial algorithm design, so a machine-checked account of its base case is reusable well beyond this one theorem.
## Setting
Fix $n\ge 1$ and an $n\times n$ matrix $A$ with entries in $\{0,1\}$, thought of as the incidence matrix of $n$ sets $S_1,\dots,S_n$ over an $n$-element ground set: $A_{ij}=1$ iff element $j$ lies in set $S_i$. A **coloring** is a map $\varepsilon:\{1,\dots,n\}\to\{-1,+1\}$, and the **discrepancy of row $i$ under $\varepsilon$** is $\bigl|\sum_j A_{ij}\varepsilon_j\bigr|$, the signed imbalance of set $S_i$. The **discrepancy of the matrix** is the value achieved by the best coloring, minimizing the worst row.
The entropy method bounds this via the **partial coloring lemma**: rather than coloring all $n$ elements at once, one repeatedly colors a constant fraction of the *currently uncolored* elements while keeping every row's contribution small, then recurses on what remains. Each round is itself produced by an entropy/pigeonhole argument: quantize each row's signed sum (under a uniformly random coloring) into $O(1)$ "shells" of width $\Theta(\sqrt m)$ (where $m$ is the number of active elements); a short computation shows this quantization carries very little **Shannon entropy** $H(Z)=\sum_x \Pr[Z=x]\log_2\frac{1}{\Pr[Z=x]}$ once the shell width exceeds a threshold; subadditivity of entropy across the $n$ rows then bounds the *joint* quantization entropy, which by pigeonhole forces an exponentially large set of colorings landing in the same joint shell; Kleitman's theorem on the diameter of a large subset of the Hamming cube then extracts two such colorings that are far apart in Hamming distance, and their difference is the sought partial coloring.
## Formalization targets
**Goal.**
$$
\exists\, C\in\mathbb R,\ \forall n\ge 1,\ \forall A\in\{0,1\}^{n\times n},\ \exists\,\varepsilon\in\{-1,1\}^n,\ \forall i,\ \Bigl|\sum_{j=1}^n A_{ij}\varepsilon_j\Bigr|\le C\sqrt n.
$$
This is the qualitative, constant-suppressed form of Spencer's theorem: it asserts $O(\sqrt n)$ discrepancy with a single universal constant, and deliberately leaves that constant unspecified. This is the right goal for this mission because it is the weakest statement that is still stable: any future improvement to the constant (down to Spencer's sharp $6$, or beyond) refines this theorem rather than invalidating it.
## Significance
The removal of the $\sqrt{\log n}$ factor is the entire content of Spencer's theorem: it is what separates discrepancy theory from a corollary of concentration inequalities, and the partial-coloring/entropy method it introduced underlies later results throughout the field (Beck–Fiala-type bounds, the Komlós conjecture literature, and constructive/algorithmic discrepancy minimization). Formalizing it is formalizing the base case that every later partial-coloring argument specializes.
This mission's goal theorem, `spencer_discrepancy_sqrt_n_bound`, is **already proved** (zero `sorry`s), by a from-scratch entropy-method development: the per-row shell-entropy bound, the joint pigeonhole-and-Kleitman assembly for one round, and the outer geometric iteration and induction combining rounds into a full coloring. What remains open in this mission is `shannonEntropy_shellFin_le` (Lemma 9 in Rothvoß's notes) — the per-row entropy bound is currently imported as an assumption by the one-round lemma `lemma8_partial_coloring_round`, which is therefore only conditionally proved pending it. A separate, harder mission on this platform (`Komlos.spencer_six_deviations`) targets Spencer's *sharp* constant $6$ via a tighter, non-standard numeric derivation; that is a distinct, substantially harder target and this mission does not duplicate it.
## Difficulty
The obvious argument is: fix a target bound $t=\lambda\sqrt n$, use a Chernoff/Hoeffding bound to show each row fails with probability at most $2e^{-\lambda^2/2}$, union-bound over the $n$ rows, and take a coloring outside the bad event. This works to prove a *single* good coloring exists — but it is not strong enough to survive being iterated to remove the entire uncolored set, because a per-row union bound loses a factor of $n$ that a fixed $\lambda$ cannot always absorb once the active column count $m$ is close to $n$: for the *scaling family* where the row count and the active set shrink together, the naive union bound's failure probability grows *linearly* in $m$, not exponentially, exactly canceling the exponential decay one is trying to exploit. The fix is to bound the *joint* entropy of all $n$ rows' quantizations at once (subadditivity of Shannon entropy), rather than union-bounding row-by-row failure events; this is genuinely a different technique, not a tightening of the same one, and it is the reason the entropy method is presented as its own tool rather than a Chernoff-bound corollary.
## Formalization scope
Matrices are `Fin n → Fin n → ℝ` with an explicit `∀ i j, A i j = 0 ∨ A i j = 1` hypothesis; colorings are represented two ways in this development — `Fin m → Bool` internally (via the platform definition `RSign` converting to $\pm1$) during the entropy/Kleitman argument, and directly as `Fin n → ℝ` constrained to $\{-1,1\}$ pointwise in the goal theorem's statement, matching the usual $\{\pm1\}$-coloring convention. The row-sum shell quantization is the platform definitions `rowSumB`, `shellIdx`, `shellFin` (an integer-valued "round to nearest shell" construction, packaged into a fixed `Fin (2m+3)` type for entropy purposes). The active column set during the outer iteration is tracked as a shrinking `Finset (Fin n)` of the *original* index type throughout, rather than moving between different `Fin m` types round to round, which keeps the induction free of type-level bookkeeping.
Reusable, already-Proved infrastructure this development builds on: `shannonEntropy_pi_le` (subadditivity across independent rows), `shannonEntropy_pigeonhole`, `choose_sum_le_exp_mul_binEntropy`, and `kleitman_diameter`, all already Proved on the platform independent of this mission. The one genuinely open piece — and the mission's standing invitation — is `shannonEntropy_shellFin_le` (Lemma 9): a self-contained Shannon-entropy computation about the `shellFin` quantization that does not depend on anything else in this mission and can be attempted independently.
## Selected references
- J. Spencer, *Six standard deviations suffice*, Trans. Amer. Math. Soc. 289 (1985), 679–706. [DOI](https://doi.org/10.1090/S0002-9947-1985-0784009-0)
- T. Rothvoß, *Discrepancy theory, or: how much balance is possible?*, MIT 18.095 lecture notes. [PDF](https://math.mit.edu/classes/18.095/lect6/notes.pdf)
- J. Matoušek, *Geometric Discrepancy: An Illustrated Guide*, Algorithms and Combinatorics 18, Springer, 1999.
- J. Beck, T. Fiala, *"Integer-making" theorems*, Discrete Appl. Math. 3(1) (1981), 1–8.
Higher-Dimensional Quantum Hypergraph-Product Codes with Finite RatesResearch Paper
## Motivation
Quantum low-density parity-check codes encode quantum information using sparse
parity constraints. A standard way to construct them is to translate binary
chain complexes into Calderbank--Shor--Steane codes and to combine complexes by
tensor product. Homology identifies the logical operators of the resulting
code, while the smallest Hamming weight of a nontrivial homology class controls
one of its distances. Determining how this distance behaves under a tensor
product is therefore a basic structural question, not merely a parameter
calculation.
Weilei Zeng and Leonid P. Pryadko studied products in which one factor is an
arbitrary finite binary chain complex and the other is the one-complex induced
by a binary matrix. Their paper was published as [“Higher-Dimensional Quantum
Hypergraph-Product Codes with Finite Rates,” *Physical Review Letters* 122,
230501 (2019)](https://doi.org/10.1103/PhysRevLett.122.230501). Its main
distance result is Eq. (13) in the [arXiv version](https://arxiv.org/abs/1810.01519):
for this particular tensor factor, the usual product upper bound is always
exact. The result extends the familiar two-complex setting of quantum
hypergraph-product codes to the local structure occurring in complexes of any
dimension.
## Setting
A **based binary chain complex** consists of finite-dimensional vector spaces
$A_i$ over $\mathbb F_2$, each equipped with a specified coordinate basis, and
linear boundary maps
$$
\cdots\longrightarrow A_{i+1}\xrightarrow{\partial_{i+1}}A_i
\xrightarrow{\partial_i}A_{i-1}\longrightarrow\cdots
$$
such that $\partial_i\partial_{i+1}=0$. Its degree-$i$ homology is
$H_i(\mathcal A)=\ker\partial_i/\operatorname{im}\partial_{i+1}$. The
**homological distance** is measured in the chosen basis:
$$
d_i(\mathcal A)=
\min\{\operatorname{wt}(x):x\in\ker\partial_i\setminus
\operatorname{im}\partial_{i+1}\}.
$$
Following the paper, the minimum of an empty set is $\infty$. Thus
$d_i(\mathcal A)=\infty$ when $H_i(\mathcal A)$ is trivial.
The endpoint convention is also the one stated explicitly after Eq. (1). For
an $m$-complex, $\partial_0:A_0\to\{0\}$ is the zero $0\times n_0$ matrix and
$\partial_{m+1}:\{0\}\to A_m$ is the zero $n_m\times0$ matrix. Consequently
$$
d_0(\mathcal A)=\min\{\operatorname{wt}(x):
x\in A_0\setminus\operatorname{im}\partial_1\}
$$
and
$$
d_m(\mathcal A)=\min\{\operatorname{wt}(x):
0\ne x\in\ker\partial_m\}.
$$
For an $r\times c$ binary matrix $P$, the **one-complex**
$\mathcal K(P)$ has $\mathbb F_2^c$ in degree one,
$\mathbb F_2^r$ in degree zero, and boundary $P$. Its two distances are
$$
d_1(\mathcal K(P))=
\min\{\operatorname{wt}(x):Px=0,\ x\ne0\}
$$
and
$$
d_0(\mathcal K(P))=
\min\{\operatorname{wt}(y):y\notin\operatorname{im}P\}.
$$
In particular, $d_0=1$ unless $P$ has full row rank, in which case
$d_0=\infty$. The degree-$j$ chain group of
$\mathcal A\times\mathcal K(P)$ is
$$
(A_j\otimes\mathbb F_2^r)\oplus
(A_{j-1}\otimes\mathbb F_2^c),
$$
with the standard tensor-product boundary. Over $\mathbb F_2$ the usual sign
in that boundary has no effect.
## Formalization targets
### Tensor-product upper bound for arbitrary complexes
The first milestone is Eq. (11) for two arbitrary finite-length based binary
chain complexes:
$$
d_j(\mathcal A\times\mathcal B)\le
\min_i d_i(\mathcal A)d_{j-i}(\mathcal B).
$$
### Rank-sensitive lower bound
Let $u=\operatorname{rank}P$ and
$\delta=d_1(\mathcal K(P))$. The second milestone is Theorem 1, including
both of its cases:
$$
u<r\Longrightarrow
d_j(\mathcal A\times\mathcal K(P))\ge
\min\!\left(d_j(\mathcal A),d_{j-1}(\mathcal A)\delta\right),
$$
and
$$
u=r\Longrightarrow
d_j(\mathcal A\times\mathcal K(P))\ge
d_{j-1}(\mathcal A)\delta.
$$
### Exact distance with a one-complex
The goal is Eq. (13):
$$
d_j(\mathcal A\times\mathcal K(P))=
\min\!\left(
d_{j-1}(\mathcal A)d_1(\mathcal K(P)),
d_j(\mathcal A)d_0(\mathcal K(P))
\right).
$$
No full-rank hypothesis is imposed on $P$.
## Significance
The equality determines the product distance exactly from four component
distances. General tensor-product arguments immediately provide the upper
bound, but an exact formula requires ruling out lower-weight homology classes
that mix the two direct-sum blocks. Once established, the formula can be
applied repeatedly to tensor products of one-complexes, which is the step used
in the paper to obtain higher-dimensional quantum hypergraph-product code
families and to compute their distances.
For formalization, the mission contributes reusable definitions of finite
based binary chain data, homological distance valued in
$\mathbb N\cup\{\infty\}$, the one-complex of a binary matrix, and the relevant
tensor-product boundary maps. Mathlib contains Hamming weight and general
homological-algebra infrastructure, while QECLean contains a closely related
based length-three homological-code interface. Neither the selected Mathlib
environment nor the inspected QECLean development currently supplies this
rank-sensitive exact distance theorem.
## Difficulty
The central issue is that Hamming weight depends on the chosen bases and is not
preserved by arbitrary homological isomorphisms. A Künneth isomorphism
describes the product homology and readily produces low-weight representatives,
which is enough for the upper bound, but it does not by itself exclude a still
lighter representative obtained by cancellation between the two tensor
blocks. The lower bound must also remain valid at the endpoints of the complex
and in singular cases where one or more homology groups vanish and the relevant
distance is $\infty$.
The theorem cannot be reduced to a dimension calculation. It must reason
about supports and Hamming weights of based representatives while respecting
the quotient by boundaries, and it must cover both $\operatorname{rank}P<r$
and $\operatorname{rank}P=r$.
## Formalization scope
The Lean development works over `ZMod 2`. A finite basis in degree $i$ is
represented by `Fin (dimension i)`, and a chain group is the function space
from that coordinate type to `ZMod 2`. `BasedBinaryChainComplex` stores the
dimension and boundary in every nonnegative degree, the chain condition, and a
finite length above which all dimensions are zero. Thus the first milestone
quantifies over genuinely arbitrary finite lengths for both $\mathcal A$ and
$\mathcal B$, rather than over a local window or a one-complex specialization.
If the stored length is $m$, the zero-dimensional source in degree $m+1$
makes $\partial_{m+1}:\{0\}\to A_m$ the unique zero map, just as the
zero-dimensional target below degree zero makes
$\partial_0:A_0\to\{0\}$ the unique zero map. Hence both singular endpoint
cases in Eqs. (1) and (4) are represented directly.
Distances use `WithTop ℕ`. Their definitions are actual minima of Hamming
weights of nontrivial representatives, with `⊤` produced by the empty-set
case; infinite distance is not an extra hypothesis or a separately hard-coded
branch. Coordinate types may be empty, which covers missing endpoint blocks.
The binary matrix $P$ is represented as a linear map between two finite based
function spaces. Its row and column coordinate types need not be nonempty,
and no injectivity or surjectivity assumption is added.
The degree-$j$ product group is indexed by the disjoint union of all coordinate
products $A_i\times B_{j-i}$ for $0\le i\le j$. Consequently its Hamming norm
is the sum of the weights of all tensor-degree blocks. The product boundary is
the standard signed tensor boundary; its sign disappears over $\mathbb F_2$.
A formal proof verifies that every pair of consecutive product boundaries
composes to zero; the cancellation of the two mixed terms uses characteristic
two. Thus the product distance is taken from an actual chain complex, rather
than from unrelated adjacent linear maps.
A basis-free tensor product or an abstract homology group alone is insufficient
for the target, because either would discard the weight data on which the
statement depends.
The mission does not formalize the asymptotic code-family construction later
in the paper, the transposed cohomological distance, or the CSS-code parameter
translation. Those are natural downstream missions; they should reuse rather
than alter the present based-chain definitions.
## Selected references
- Weilei Zeng and Leonid P. Pryadko, [“Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,”](https://doi.org/10.1103/PhysRevLett.122.230501) *Physical Review Letters* 122, 230501 (2019). [arXiv:1810.01519](https://arxiv.org/abs/1810.01519).
- Benjamin Audoux and Alain Couvreur, [“On Tensor Products of CSS Codes,”](https://arxiv.org/abs/1512.07081) arXiv:1512.07081 (2015), especially Proposition 1.13 and Corollary 2.14 as cited by Zeng--Pryadko.
- Jean-Pierre Tillich and Gilles Zémor, [“Quantum LDPC Codes With Positive Rate and Minimum Distance Proportional to the Square Root of the Blocklength,”](https://doi.org/10.1109/TIT.2013.2292061) *IEEE Transactions on Information Theory* 60 (2014), 1193--1202.
Irrationality and transcendence of Euler's constantOpen Problem
## What the constant is
Euler's constant $\gamma$ measures the gap between the harmonic numbers and the logarithm:
$$\gamma \;=\; \lim_{n\to\infty}\left(\sum_{k=1}^{n}\frac{1}{k} \;-\; \log n\right) \;=\; 0.5772156649\ldots$$
It appears wherever the harmonic series is compared against an integral, and it is the value at $1$ of the digamma function, $\psi(1) = -\gamma$, equivalently $\gamma = -\Gamma'(1)$. Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown.
## What is being asked
For $\pi$ and $e$ the arithmetic questions were settled long ago: both are irrational and transcendental. For $\gamma$, **neither is known**. It is not known whether $\gamma$ is irrational, and a fortiori not whether it is transcendental, though it is universally expected to be both.
The goal theorem of this mission is transcendence,
$$\gamma \notin \overline{\mathbb{Q}},$$
with irrationality carried as a separate, weaker target — a proof of transcendence yields irrationality immediately, but not conversely, and irrationality alone would already be a landmark.
## What is actually known
Progress has come in three forms, and the milestones below formalize each.
**Conditional bounds on a putative denominator.** If $\gamma$ were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing $\gamma$ to $30{,}000$ places by an algorithm built on modified Bessel functions, showed any denominator exceeds $10^{15000}$; a continued-fraction analysis by Papanikolaou (1997) pushed this past $10^{244663}$. These are not steps toward a proof so much as a measurement of how far brute computation can go.
**Disjunctive results.** The strongest unconditional statements pair $\gamma$ with the Euler–Gompertz constant
$$\delta \;=\; \int_0^{\infty} \frac{e^{-u}}{1+u}\, du \;=\; 0.5963473623\ldots$$
Aptekarev, building on work of Mahler and Shidlovskii, observed that **at least one of $\gamma$ and $\delta$ is irrational**. Rivoal later strengthened this to **at least one of them is transcendental**. Neither argument isolates which, and that is precisely the obstruction: the Padé-approximation machinery that controls the pair does not separate them.
**Irrationality criteria.** Sondow, adapting Beukers' treatment of Apéry's theorem for $\zeta(3)$, gave criteria equivalent to the irrationality of $\gamma$ in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it.
## Timeline
- **1734** — Euler introduces the constant and computes it to six decimals.
- **1790s–1800s** — Mascheroni computes further digits; the constant acquires its second name.
- **1873** — Hermite proves $e$ transcendental; **1882** — Lindemann does the same for $\pi$. The methods do not reach $\gamma$.
- **1980** — Brent and McMillan: if $\gamma = p/q$ then $q > 10^{15000}$.
- **1997** — Papanikolaou: the same denominator exceeds $10^{244663}$.
- **2009** — Aptekarev: at least one of $\gamma$, $\delta$ is irrational.
- **2012** — Rivoal: at least one of $\gamma$, $\delta$ is transcendental.
- **2010s** — Murty, Saradha and others obtain transcendence results for generalized Euler–Lehmer constants, again leaving $\gamma$ itself untouched.
## Formalization notes
Mathlib provides the constant as `Real.eulerMascheroniConstant`, defined as the limit of $\sum_{k\le n} 1/k - \log n$, together with the identifications $\psi(1) = -\gamma$ and $\gamma = -\Gamma'(1)$ and the numeric bounds $1/2 < \gamma < 2/3$. `Irrational` and `Transcendental ℚ` are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.
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. Determining which equations force other equations separates the consequences of a single law from familiar properties that require additional assumptions. 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 Equational Theories Project studies these implications systematically. Its [December 2025 paper](https://arxiv.org/html/2512.07087v2) 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 $A$ with a total binary operation $\diamond:A\times A\to A$. Parentheses specify the order of evaluation throughout; no reassociation is permitted. The condition **E677** means
$$\forall x,y\in A,\quad x=y\diamond\bigl(x\diamond((y\diamond x)\diamond y)\bigr).$$
The condition **E255** means
$$\forall x\in A,\quad x=((x\diamond x)\diamond x)\diamond x.$$
These are the two laws used in [Chapter 13 of the project blueprint](https://teorth.github.io/equational_theories/blueprint/677-chapter.html). For a fixed element $y$, the **left multiplication map** is $L_y(x)=y\diamond x$. A **fixer** for $x$ is an element $y$ satisfying $y\diamond x=x$. This definition concerns one element $x$; it does not require $y$ to act as an identity on every element.
## 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 $A$ satisfying E677, the first supporting statement is
$$\forall y\in A,\quad L_y\text{ is bijective}.$$
The second supporting statement specifies any fixer:
$$\forall x,y\in A,\quad y\diamond x=x\ \Longrightarrow\ y=(x\diamond x)\diamond x.$$
The third supporting statement is the backward recurrence
$$\forall x,y\in A,\quad x=(y\diamond x)\diamond\bigl((y\diamond(y\diamond x))\diamond y\bigr).$$
These supporting statements come from ETP blueprint Lemma 13.1(i)–(iii); local direct proof files accompany their statements. The following universal fixer-existence assertion is retained as an explicit equivalent reformulation:
$$\forall x\in A,\quad\exists y\in A,\quad y\diamond x=x.$$
The mission goal is
$$\forall\text{ finite magmas }A,\quad \operatorname{E677}(A)\ \Longrightarrow\ \operatorname{E255}(A).$$
For finite E677 magmas, fixer existence is equivalent to E255: E255 supplies the fixer $(x\diamond x)\diamond x$, and Lemma 13.1(ii) converts any fixer into E255. Thus it is not presented as a strictly weaker milestone.
The active open milestone is an orbit-local producer statement. For a fixed $x$, if two elements in the forward orbit $x,L_x(x),L_x^2(x),\ldots$ have equal right products by $x$, they must be equal unless $x$ has a fixer. This isolates a genuine structural step without asserting a fixer for every element. None of the displayed statements restricts the cardinality to a tested range.
## 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 multiplication 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 multiplication 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 multiplication map alone does not state that a fixer exists.
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.
## Selected references
- Matthew Bolan et al., *The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale*, arXiv:2512.07087v2 (December 16, 2025), [paper](https://arxiv.org/html/2512.07087v2).
- The Equational Theories Project contributors, *Equational Theories*, online proof blueprint, Chapter 13, equations (1)–(2) and Lemmas 13.1–13.2, [chapter](https://teorth.github.io/equational_theories/blueprint/677-chapter.html), accessed September 7, 2026.
Speculative Actions: Cost-Latency Analysis for Agentic SpeculationResearch Paper
## Motivation
An LLM agent acting in an environment spends most of its wall-clock time waiting. Each
step — a model call, a tool or MCP request, a browser action, sometimes a human reply —
must complete before the next can be issued, and the round trips dominate end-to-end
latency: a chess game between two reasoning agents runs for hours, and an
operating-system tuning task for tens of minutes. When a training or prompt-optimization
loop repeats such a run thousands of times, the waiting is the cost.
*Speculative actions* ([Ye, Ahuja, Liargkovas, Lu, Kaffes, Peng, ICLR 2026](https://arxiv.org/abs/2510.04371))
transplants a classical systems idea — speculative execution in microprocessors, and
speculative decoding for LLM inference — to the agent's environment loop. A cheap, fast
**speculator** guesses the action a slow, authoritative **actor** is about to produce,
the guess is used to launch the *next* environment call early, and the work is committed
only when the actor's real action confirms the guess. The interface stays sequential and
lossless; the internals run in parallel.
What makes this a formalization target rather than an engineering report is the paper's
§5 cost–latency analysis. Speculating more branches buys hit probability but costs
tokens, and the paper derives closed-form expressions for both sides of that trade — a
self-contained piece of applied probability sitting underneath a systems paper. This
mission asks for those expressions, machine-checked.
## Setting
Fix a horizon $T$ and index steps $t = 0, 1, \dots, T-1$. At each step a policy maps the
state to an API call; the **actor** executes it with latency $\mathrm{Exp}(\beta)$, while
the **speculator** proposes candidate actions with latency $\mathrm{Exp}(\alpha)$, where
$\beta < \alpha$ (the speculator is faster in expectation). A speculative branch
**hits** when the action it guesses implies the same next call the actor's true action
would have implied; branches hit independently across steps with probability $p$.
Two knobs define the two regimes analyzed. **Breadth** $k$: at each step, launch $k$
independent one-step speculations in parallel, each immediately followed by a real call.
At least one of the $k$ succeeds with probability
$$p(k) \;=\; 1 - (1-p)^k .$$
**Depth**: follow a single branch, extending it whenever a speculative or real call
returns and pruning subtrees the actor contradicts.
The quantity driving both results is $S_n$, the expected number of hits by round $n$. A
hit consumes the following step's speculation window — after a correct guess the next
call is already cached, so no new speculation is launched there — which yields the
two-term recursion
$$S_0 = 0, \qquad S_1 = p, \qquad S_n = p\,(1 + S_{n-2}) + (1-p)\,S_{n-1}.$$
Write $T_{\mathrm{seq}}, M_{\mathrm{seq}}$ for the latency and token cost of strictly
sequential execution, and $T_{\mathrm{spec}}, M_{\mathrm{spec}}$ for their speculative
counterparts. In the depth regime latencies are taken deterministic: $a$ for a real call,
$b < a$ for a speculative one.
## Target
The goal theorem is the finite-horizon latency ratio for breadth-focused speculation
(Proposition 1), with $p(k)$ abbreviated $p_k$:
$$\frac{\mathbb{E}[T_{\mathrm{spec}}]}{\mathbb{E}[T_{\mathrm{seq}}]}
= 1 - \frac{1}{T}\,\frac{\alpha}{\alpha+\beta}
\left[\frac{(T-1)p_k}{1+p_k} + \frac{p_k^2}{(1+p_k)^2}
- \frac{p_k^2}{(1+p_k)^2}(-p_k)^{T-1}\right].$$
The supporting targets, ordered as the analysis builds them:
1. the closed form $S_n = \frac{p}{1+p}n + \frac{p^2}{(1+p)^2}\bigl(1 - (-p)^n\bigr)$ solving the recursion;
2. the per-hit saving $\mathbb{E}[(B-A)^+] = \frac{\alpha}{\beta(\alpha+\beta)}$ for independent $A \sim \mathrm{Exp}(\alpha)$, $B \sim \mathrm{Exp}(\beta)$;
3. the $T \to \infty$ limit $1 - \frac{p_k}{1+p_k}\cdot\frac{\alpha}{\alpha+\beta}$, and the resulting **50% ceiling**: the latency reduction is strictly below $\tfrac12$ for every $p_k \le 1$;
4. the cost counterpart (Theorem 4), finite-horizon and in the limit, with $\tilde k$ the number of *distinct* actions across the $k$ branches;
5. the depth-focused time and cost identities (Theorem 6), whose latency coefficient is $p$ rather than $\frac{p}{1+p}$ — raising the speedup ceiling from $\tfrac12$ to $1$;
6. the structure of confidence-aware selective speculation (Theorem 3 and Corollary 5): with sorted per-branch confidences, the marginal hit-probability gain is non-increasing, so the optimal breadth is the greedy threshold rule "add a branch while $\Delta^\star \delta q(m) \ge c$".
## Significance
The analysis is what turns speculation from a trick into a tunable system. Proposition 1
and Theorem 4 are governed by the *same* quantity $p_k$, so a practitioner who can
estimate hit probability can choose $k$ offline against a latency/cost budget rather than
by trial. The 50% ceiling is a genuine negative result — it says breadth alone cannot do
better, and motivates the depth regime, where the ceiling becomes 1. Theorem 3 explains
why confidence-based branch selection is cheap in practice: the whole dynamic program
collapses to one scalar continuation value, so a runtime system sorts confidences and
adds branches greedily in $O(k)$ per step.
The paper's proofs are pen-and-paper and, as far as we are aware, none of these results
has a machine-checked proof. Three parts reward formalization specifically. The
recursion's closed form is derived by a characteristic-equation argument with a
particular solution that collides with the homogeneous part — routine but error-prone.
The per-hit saving is an honest two-dimensional integral over independent exponentials.
And Theorem 6's cost expression is stated in the paper with a floor function and then
immediately replaced by an approximation, so formalizing it forces a decision about which
claim is actually being asserted (see *Formalization scope*).
## Difficulty
The obvious first move on the recursion — guess a constant particular solution — fails,
because $r = 1$ is a root of the characteristic polynomial $r^2 - (1-p)r - p$ and a
constant trial collides with the homogeneous family; the particular solution is linear in
$n$, and the $\frac{p^2}{(1+p)^2}$ coefficient comes out of matching *both* initial
conditions, not one.
The interesting hypothesis is the one the recursion's shape encodes and the prose states
only in passing: a hit at round $t$ removes the speculation window at round $t+1$. Drop
it and the recursion becomes one-term and the answer changes.
For the per-hit saving, the difficulty is analytic rather than algebraic: the inner
antiderivative of $(b-a)\alpha e^{-\alpha a}$ must be handled, and the outer integral runs
over an unbounded interval, so integrability has to be established rather than assumed.
The asymptotic statements need the oscillating term $(-p_k)^{T-1}$ controlled uniformly —
it is bounded, not vanishing termwise in an obvious way — before the $\tfrac1T$ prefactor
can be taken to zero.
## Formalization scope
Everything is over $\mathbb{R}$. The model lives in one definition bundle,
`Def_SpecActions_model`, in namespace `SpecActions`; the mission's Lean names match the
prose symbols ($S_n$ is `hits`, $p(k)$ is `phit`, $\tilde k$ is `kt`).
The model is formalized at the level the paper's own proofs use: $\mathbb{E}[T]$ and
$\mathbb{E}[M]$ are *defined* by the expressions Appendix A derives for them
(`specTime`, `specCost`, and their depth analogues), and the theorems assert the
algebraic and asymptotic identities relating those quantities. Deriving those
expressions from a measure-theoretic model of the execution trace is deliberately **not**
in scope — with one exception: milestone 2 states the per-hit saving as a genuine
iterated integral against the exponential densities, so the one probabilistic step the
paper actually computes is formalized as an integral rather than assumed.
Conventions a solver should know before starting:
- Statements are quantified over $\alpha, \beta > 0$ and $0 \le p_k \le 1$; the standing
assumption $\beta < \alpha$ is *not* imposed, since none of the identities need it.
- Finite-horizon statements carry $1 \le T$, and $T-1$ is natural-number subtraction —
the $T = 0$ case is excluded rather than silently truncated.
- `hits` takes $p_k$ (the per-*step* hit probability $p(k)$), not the per-branch $p$;
`phit` relates the two, and `Thm_SpecActions_phit_bounds` supplies the
$0 \le p(k) \le 1$ range facts the other statements assume.
- **Theorem 6's cost is stated as the exact identity, not the paper's approximation.**
The paper gives an exact expression involving $\lfloor a/b \rfloor$ and then an
$\approx$ form with $\frac{a}{2b} - \frac12$; these coincide only when $a/b$ is an
integer. The milestone asserts the exact floor version, which is what the proof
establishes.
- The 50% ceiling is stated as the strict bound
$\frac{p_k}{1+p_k}\cdot\frac{\alpha}{\alpha+\beta} < \frac12$, which holds for all
admissible parameters; the paper's "upper bound of 50%, occurring when $p=1$ and
$\alpha = \infty$" describes an unattained supremum.
- Theorem 3's dynamic program is formalized as the two facts that carry its content —
diminishing marginal returns, and optimality of the greedy threshold breadth — rather
than as a Bellman recursion over a mode process, which would require a full MDP
development.
Reusable beyond this mission: the two-term linear recursion solved in milestone 1, and
the $\mathbb{E}[(B-A)^+]$ computation for independent exponentials, which is a standard
fact absent from Mathlib. Contributions extending the model toward an actual measure on
execution traces — deriving `specTime` rather than defining it — are welcome as
follow-on work.
## Selected references
- Naimeng Ye, Arnav Ahuja, Georgios Liargkovas, Yunan Lu, Kostis Kaffes, Tianyi Peng. *Speculative Actions: A Lossless Framework for Faster Agentic Systems.* ICLR 2026. [arXiv:2510.04371](https://arxiv.org/abs/2510.04371) — Proposition 1 (p. 4), Appendix A (pp. 13–14), Theorem 3 (p. 10), Theorem 4 (p. 19), Corollary 5 (p. 22), Theorem 6 (p. 23).
- Yaniv Leviathan, Matan Kalman, Yossi Matias. *Fast Inference from Transformers via Speculative Decoding.* ICML 2023. [arXiv:2211.17192](https://arxiv.org/abs/2211.17192) — the speculate-verify pattern at token level.
- Wenyue Hua, Mengting Wan, Shashank Vadrevu, Ryan Nadel, Yongfeng Zhang, Chi Wang. *Interactive Speculative Planning.* 2024. [arXiv:2410.00079](https://arxiv.org/abs/2410.00079) — depth-oriented speculation on a single planning branch.
- Yilin Guan et al. *Dynamic Speculative Agent Planning.* 2025. [arXiv:2509.01920](https://arxiv.org/abs/2509.01920) — online RL for choosing speculation depth under a cost-latency trade-off.
- Robert M. Tomasulo. *An Efficient Algorithm for Exploiting Multiple Arithmetic Units.* IBM Journal of Research and Development, 1967. [DOI:10.1147/rd.111.0025](https://doi.org/10.1147/rd.111.0025) — speculative execution in hardware.
## Motivation
This mission seeks a Lean proof that every odd natural number greater than 1 is the sum of at most three primes. It follows from Helfgott's ternary Goldbach theorem for odd numbers greater than 5, together with the small cases 3 and 5, each of which is itself prime.
## Setting and goal
For every natural number n with Odd n and 1 < n, construct a multiset of at most three prime natural numbers whose sum is n. Repetition is allowed and order is irrelevant. Examples include 3 = 3, 5 = 5, 7 = 2 + 2 + 3, and 9 = 3 + 3 + 3. The primes need not all be odd.
## Relationship to the five-primes mission
The goal uses the same Multiset ℕ representation and the same hypothesis 1 < n as [Every Odd Number Greater Than 1 is the Sum of at Most Five Primes](https://prove2.me/missions/Every%20Odd%20Number%20Greater%20Than%201%20is%20the%20Sum%20of%20at%20Most%20Five%20Primes). The cardinality bound changes from s.card ≤ 5 to s.card ≤ 3. No custom definitions are needed.
## Formalization scope
The target is unconditional and covers every odd natural number greater than 1. At most three is essential: 3 and 5 cannot be sums of exactly three primes. All summands must satisfy Nat.Prime, and multiplicities count toward the cardinality bound. The initial proposal contains the goal with an open proof, ready for formalization.
## Proof approach
A proof may combine a formalization of Helfgott's theorem, which supplies exactly three primes for odd n > 5, with singleton multisets for n = 3 and n = 5. Establishing Helfgott's result requires verified proofs of the analytic and computational ingredients of the chosen argument.
## Reference
H. A. Helfgott, [The ternary Goldbach conjecture is true](https://arxiv.org/abs/1312.7748), 2013, revised 2014. The mission's at-most-three formulation also includes the elementary cases n = 3 and n = 5.