Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The iteration of a rational map of the Riemann sphere is the model problem of holomorphic dynamics. The subject was founded by Fatou and Julia around 1918–1920, who split the sphere into a region of stable behaviour and a region of chaotic behaviour, and it was revived in the 1980s by Douady, Hubbard, Sullivan and Thurston. John Milnor's textbook Dynamics in One Complex Variable (3rd ed., Princeton, 2006) is the standard graduate introduction. This mission, the first of a series on the book, formalizes the chain of results that leads from Montel's theorem on normal families to Sullivan's theorem that rational maps have no wandering domains.
Timeline of the results formalized here:
The Riemann sphere is , the one-point compactification of , with the two coordinates (near finite points) and (near ). A rational map is with coprime complex polynomials, ; it acts on in the usual way, and its degree is . Write for the -th iterate.
A family of maps from an open set to is normal if every sequence in it has a subsequence converging locally uniformly in the spherical (chordal) metric. The Fatou set is the set of points having a neighbourhood on which the iterates form a normal family; the Julia set is its complement . A Fatou component is a connected component of . A periodic point of minimal period has multiplier , computed in a local coordinate; it is repelling if and attracting if .
A Fatou component with is a Siegel disk (resp. Herman ring) if is conformally conjugate to an irrational rotation of the unit disk (resp. of a round annulus ).
For a rational map of degree and every Fatou component there are , with
The results. Montel's theorem is the engine of the Fatou–Julia theory: nonemptiness of , density of iterated preimages and density of repelling cycles all rest on it. Theorem 14.1 identifies the non-normality locus with the closure of the repelling cycles, the form in which the Julia set is usually computed and pictured. Sullivan's theorem, combined with Theorem 16.1, gives a complete qualitative picture of the dynamics on the Fatou set; it is used throughout the later theory, e.g. to show that the Julia set of a postcritically finite map without superattracting cycles is the whole sphere (Milnor, Corollary 16.5).
Formalizing them. All results here are classical theorems with published proofs; none is open. A text search of Mathlib at the platform's pinned revision (0df444a) finds no Montel theorem for families of holomorphic maps, no Fatou or Julia sets and no wandering-domain results; it does contain the Schwarz lemma and the hyperbolic metric on the upper half-plane. The remaining work is to formalize the known proofs.
The early milestones need the uniformization-type input that is covered by the disk (via the modular function or an equivalent construction) and Schwarz–Pick-type estimates on hyperbolic surfaces; Mathlib has the Schwarz lemma and the hyperbolic metric of the upper half-plane, but not the Poincaré metric of general hyperbolic domains or covering-space uniformization. Theorem 14.1 requires a quantitative use of Montel's theorem around points of that are not critical values. Theorem 16.1 needs the Denjoy–Wolff-type classification of self-maps of hyperbolic surfaces and the Snail Lemma for parabolic points. The goal is substantially harder: Sullivan's proof uses the measurable Riemann mapping theorem (Morrey–Ahlfors–Bers) to build an infinite-dimensional family of quasiconformal deformations of , contradicting the finite dimensionality of the space of rational maps of degree . The theory of quasiconformal maps and Beltrami equations is absent from Mathlib, and no elementary argument avoiding it is known.
All declarations live in the book-wide namespace MilnorDynamics and build on the published definition files MilnorDynamics_NormalFamilies, MilnorDynamics_RationalMaps and MilnorDynamics_PeriodicPoints; one new definition file, MilnorDynamics_FatouComponents, adds Fatou components, immediate basins, Siegel disks and Herman rings.
OnePoint ℂ; a rational map is a structure of coprime polynomials with , acting on OnePoint ℂ via RationalMap.toFun; the degree is .IsHolomorphicOn). Normality is locally uniform subconvergence in the chordal metric (IsNormalFamily); the Fatou set is defined through the standard charts of .Welcome contributions: the Poincaré metric and Schwarz–Pick on hyperbolic domains, the modular covering of , the degree theory of rational maps, quasiconformal maps and the measurable Riemann mapping theorem. These are reusable far beyond this mission.
The diagonal Ramsey number is the least such that every red/blue colouring of the edges of the complete graph contains a monochromatic copy of . Ramsey's theorem guarantees that is finite; the question of how fast it grows is one of the central problems of extremal and probabilistic combinatorics. Erdős asked repeatedly ([Er88], [Er93]; see erdosproblems.com/77) for the value of
It is not even known whether this limit exists.
Timeline.
So today, if the limit exists, it lies in .
For consider simple graphs on the vertex set . A red/blue colouring of the edges of is the same as such a graph (the red edges) together with its complement (the blue edges). A -clique of is a set of exactly vertices, any two of which are adjacent in . Define
In the Lean development this is Erdos77.diagonalRamsey k. Small values: , , , , .
The original problem asks for the value of the limit, which is unknown; a goal with a hard-coded value cannot be stated honestly. The goal therefore asserts only that the limit exists (as a real number). Determining remains the ultimate aim; any proof of a specific value would in particular prove this goal.
The result itself. Existence of the limit would say that diagonal Ramsey numbers have a well-defined exponential growth rate — a regularity statement that is currently unknown in either direction. Even the bounds and are the products of decades of work, and the lower bound base has resisted improvement since 1947.
Formalizing it. The goal is open. The milestones are proved results in the literature; the classical ones (Erdős–Szekeres, Erdős 1947) are natural first formalization targets, and the recent upper bounds (CGMS, GNNW) are substantial formalization projects in their own right. The status of existing machine-checked formalizations of these results is not asserted here.
There is no known sub- or super-multiplicativity for that would give existence of the limit via Fekete's lemma: the natural product constructions relate to and only with losses that are too large, and the best lower and upper bounds come from entirely different methods (random colourings versus the book algorithm), so neither side controls the other.
sInf of an empty set of naturals is ; the Erdős–Szekeres milestone shows the set is nonempty, so the infimum is the genuine Ramsey number.atTop filter on ; "" in GNNW is encoded as "for every , eventually with exponent ".Fin n, binomial estimates, the probabilistic method for the lower bounds (Spencer uses the Lovász Local Lemma), and the CGMS book algorithm for the upper bounds. All of these are reusable beyond this mission.A sunflower (also called a -system) with petals is a family of sets whose pairwise intersections are all equal to one common set, the kernel. In 1960 Erdős and Rado proved the sunflower lemma: every sufficiently large family of -element sets contains a sunflower with petals, and they asked how large "sufficiently large" must be (Erdős–Rado 1960). The conjecture that the threshold is only exponential in is one of Erdős' best-known problems in extremal combinatorics; it is listed as Erdős Problem 20, and Erdős offered a $1000 prize for it. Sunflower bounds are used, for example, in Razborov's monotone circuit lower bounds and in the study of set systems with restricted intersections.
Timeline.
The conjecture itself remains open, even for .
Fix natural numbers (the uniformity) and (the number of petals). A family of sets is -uniform if every member of has exactly elements. A subfamily is a -sunflower if and there is a set with for all distinct .
The sunflower threshold is the least natural number such that every -uniform family (over any ground set) with contains a -sunflower.
The constants are left unspecified; only the exponential shape in is asked for. A disproof (the negation of this statement) would equally settle the problem.
A supporting sanity check, , is taken from the source formalization.
A positive answer would show that sunflower-free -uniform families have at most exponential size, the correct order of magnitude by the Erdős–Rado lower bound; this would sharpen every application that currently loses a factor per coordinate, including monotone circuit lower bounds. A negative answer would show the -type bounds of 2019–2021 are essentially the truth.
On the formal side, the Erdős–Rado upper bound has a Lean formalization recorded in the source file; the lower-bound construction and the spread-family / coding arguments behind the Rao and Bell–Chueluecha–Warnke bounds are, as far as this proposal records, not yet formalized. Formalizing them produces reusable infrastructure on spread families and random-subset (or entropy) arguments.
The classical induction on (pick a maximal family of pairwise disjoint members; if it is small, some element lies in many members, recurse on the link) loses a factor of about at each of steps, which is where comes from. The modern arguments replace the recursion by an analysis of spread families, but each still loses a factor per level, and no known technique removes it. The case is already open.
Set (Set α) and sizes are measured with Set.ncard, which returns on infinite sets. Consequently, for only finite members can be "-element", and the condition with only applies to finite families. All targets assume (except the sanity check), so the quirks do not affect them.answer(·) statement.Contributions of general lemmas on sunflowers, spread families and the Erdős–Rado construction are welcome and reusable beyond this mission.
Every generalization bound presented so far in this series is for classification, where the
error of a prediction is binary (correct or not). Regression asks a different question:
predictions are real-valued, and error is measured by the magnitude of the deviation from
the true label, via a loss function L. Chapter 11 develops generalization theory for bounded
regression, showing that the same two complexity measures used for classification —
Rademacher complexity and a VC-dimension analogue — extend naturally, once the loss function
itself is folded into the machinery via a Lipschitz-contraction argument (Rademacher route) or
a reduction to classification via level-set thresholding (pseudo-dimension route).
A regression hypothesis h:X→ℝ is scored by a loss L:ℝ×ℝ→ℝ against a joint distribution D
on X×ℝ (the stochastic scenario, since regression labels are rarely exactly reproducible);
R(h) = E_{(x,y)~D}[L(h(x),y)] (Eq. 11.1) and R̂_S(h) = (1/m)∑L(h(x_i),y_i) (Eq. 11.2). For
a finite hypothesis set, Theorem 11.1 gives a Hoeffding/union-bound guarantee directly, the
regression analogue of chunk 02-pac's finite-hypothesis bound. For infinite H, §11.2.2
develops a Rademacher-complexity route: Proposition 11.2 shows that if L is µ-Lipschitz in
its first (predicted-value) argument, the Rademacher complexity of the loss-composed family
G = {(x,y)↦L(h(x),y) : h∈H} is controlled by µ times H's own Rademacher complexity, via
Talagrand's contraction lemma (chunk 05-svm's Lemma 5.7); Theorem 11.3 combines this with
chunk 03's Theorem 3.3 to give the chapter's headline bound. §11.2.3 develops an independent,
purely combinatorial route: pseudo-dimension (Definition 11.5), a real-valued analogue of
VC-dimension defined via threshold-witnessed shattering (Definition 11.4, restated via its own
Eq. 11.3 as the VC-dimension of a thresholded indicator family); Theorem 11.8 gives a
pseudo-dimension generalization bound by reducing regression to a family of classification
problems (one per threshold t), using the tail-integral identity Eq. 11.5.
Theorem 11.1 (milestone). For L bounded by M and H finite: for any δ>0, with
probability at least 1-δ, for all h∈H: R(h) ≤ R̂_S(h) + M√((log|H|+log(1/δ))/(2m)).
Proposition 11.2 (milestone). For L non-negative, bounded by M, µ-Lipschitz in its
first argument: for any sample S, R̂_S(G) ≤ µR̂_S(H).
Theorem 11.3 — the mission's goal. Under Proposition 11.2's hypotheses on L: for any
δ>0, with probability at least 1-δ, for all h∈H: E[L(h(x),y)] ≤ (1/m)∑L(h(x_i),y_i) + 2µR_m(H) + M√(log(1/δ)/(2m)), and also with 2µR̂_S(H) + 3M√(log(2/δ)/(2m)).
Theorem 11.8 (milestone). For Pdim(G)=d, L non-negative bounded by M: for any
δ>0, with probability at least 1-δ over a sample of size m, for all h∈H: R(h) ≤ R̂_S(h) + M√(2d log(em/d)/m) + M√(log(1/δ)/(2m)).
Theorem 11.3 is the chapter's own choice of headline result (§11.2's stated goal is to show
"how the Rademacher complexity bounds of theorem 3.3 can be used to derive generalization
bounds for regression"), and its proof genuinely reuses two pieces of prior machinery from
this series — chunk 03's Theorem 3.3 and chunk 05's Talagrand's-lemma-style contraction —
combined via a new observation (Proposition 11.2) specific to loss-composed families, not a
restatement of either. Theorem 11.8 is the chapter's second, structurally independent
technique: its em/d bound parallels chunk 03's Corollary 3.19 (both ultimately reduce to a
VC-dimension-style growth-function argument), but the reduction itself — regression to a
continuum of threshold classification problems, via the Lebesgue-integral tail identity Eq.
(11.5) applied to |R(h)-R̂_S(h)| — is genuinely new content for this book, and pseudo-dimension
has no prior art on the platform or in Mathlib. No prior art exists for this chapter's overall
content either: GET /theorems?q=generalization%20bound%20regression and
GET /theorems?q=pseudo-dimension both return zero hits.
Proposition 11.2's proof needs Talagrand's contraction lemma applied with the Lipschitz
constant taken in the first argument of L only — the predicted value h(x_i), holding the
true label y_i fixed — exactly the pitfall BRIEF.md names: a loss Lipschitz in the wrong
argument, or in both arguments jointly, would not license this step. Theorem 11.8's proof is
the chapter's most involved: it defines, for every h∈H and threshold t≥0, a classifier
c(h,t):(x,y)↦1_{L(h(x),y)>t}, bounds |R(h)-R̂_S(h)| by M·sup_{t∈[0,M]}|R(c(h,t))- R̂_S(c(h,t))| via the tail-integral identity, and then applies a VC-dimension-style
classification bound (Corollary 3.19) to the family of thresholded classifiers — whose
VC-dimension is, by Eq. (11.3), exactly Pdim(G) by construction. A formalization that
conflated pseudo-dimension with ordinary VC-dimension, or reused chunk 03's HasVCDim
definition by relabeling, would misrepresent this chapter's genuinely different (real-valued,
threshold-witnessed) combinatorial notion — precisely the pitfall BRIEF.md flags.
Y := ℝ throughout (the book's own "Y a measurable subset of ℝ"), a harmless
simplification consistent with every hypothesis, loss and Lipschitz condition in this chapter
being stated for real-valued scores and labels. EmpiricalRademacherComplexity/
RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2 locally, since a
draft item cannot import another chunk's draft module. Shatters/PseudoDim are formalized
via the book's own equivalent reformulation (Eq. 11.3, the thresholded-indicator form), rather
than the sign-function form of Definition 11.4 directly, since the two coincide except at a
measure-zero boundary the book itself does not address; PseudoDim mirrors chunk 03's
HasVCDim Prop-valued pattern (does not cover Pdim(G)=+∞; every consuming theorem takes it
as an explicit hypothesis) but is a structurally distinct definition built on Shatters, never
a relabeling of HasVCDim, per BRIEF.md's pitfall note. Proposition 11.2's and Theorem
11.3's Lipschitz hypothesis (hLlip) is stated with the true label y' universally quantified
outside the two-point comparison y1, y2 (the predicted values), matching "for any fixed
y' ∈ Y, y ↦ L(y,y') is µ-Lipschitz" exactly — Lipschitzness in the first argument only,
per BRIEF.md's pitfall note. RademacherComplexity (Measure.map Prod.fst D) H m gives the
book's R_m(H) (H's Rademacher complexity under the marginal sampling distribution of the
inputs x, i.e. D's first marginal). No numerical constant is altered from the book in any
of the four theorems.
Not formalized: the L_p-loss worked example following Theorem 11.3's proof (an instantiation
of the general theorem for a specific loss family, not a separate numbered theorem); Theorem
11.6 and Theorem 11.7 (worked pseudo-dimension examples for hyperplanes and vector spaces,
background/illustration rather than the chapter's general machinery — drafting only these
examples instead of the general Theorem 11.8 would be this chapter's trivializing
formalization); the two-sided variant of Theorem 11.1 mentioned immediately after its proof
(an unnumbered remark, not a separately displayed/numbered theorem); and all of §11.3 (linear
regression, kernel ridge regression, SVR, Lasso and their online variants), which is
applications-heavy per BRIEF.md's chapter restriction to §11.1-11.2.
A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range , and let it degrade at a controlled rate outside, proportionally to the distance from . That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.
Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most " has no direct meaning. What replaces it is the observation that a scalar inequality is the inclusion , and that the violation is the distance from the left hand side to . In that form the notion lifts verbatim, and the whole chapter follows.
Definition 11.1.2. Consider an uncertain convex constraint
with nonempty, closed and convex. Let the perturbation space split as , each factor carrying a normal range , a closed convex cone and a norm , and let be a norm on . A candidate is robust feasible with global sensitivities if
where and .
The object that makes the analysis work is the recessive cone of (Definition 11.3.1): for any ,
which does not depend on and is a nonempty closed convex cone.
A candidate is feasible for the GRC (11.1.6) if and only if it satisfies the system
Line (a) is the ordinary robust counterpart over the normal range. Each line (b) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to itself.
The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.
The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function
of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that of a map with respect to a setup equals of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.
The recessive cone results are the vocabulary. The one that earns its place is : the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.
The goal is an equivalence and the two directions are asymmetric.
Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix and in the unit ball of , and run out along the cone. The GRC bounds the distance to by , so there are with ; the rescaled points stay bounded, and a limit point of them lies in by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not — is what appears in lines (b).
Backward is a decomposition-and-assemble: split each with , realizing the distance, get a point of from line (a) and a recession direction from each line (b), and add them — using that .
Proposition 11.4.1 is a chain of polarity identities: the polar of is for compact convex containing the origin, the polar of a norm ball of radius is the dual-norm ball of radius , and bipolarity. Each step is standard and the composition is not.
Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function .
Conventions committed to:
IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and
nonnegativity follows from them.Erdős asked, repeatedly and with a rising price tag, for an asymptotic formula for the largest subset of 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 .
Timeline.
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 .
Fix an integer . A non-trivial -term arithmetic progression is a list of natural numbers with common difference ; the requirement is what "non-trivial" means, and it forces the terms to be distinct. A finite set is -AP-free if it contains no such progression. Write
The mission takes its formal definition of verbatim from the formal-conjectures 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 when every subset of it that is an arithmetic progression of length forces . Progressions of length and count as trivial, so under that convention every set is free of them and ; the interesting range begins at . Every statement in this mission that depends on the convention carries an explicit hypothesis on .
On that range, is non-decreasing in both and , satisfies , and hence, by Fekete's subadditivity lemma, converges. Szemerédi's theorem is the statement that the limit is ; the whole difficulty of this mission lies in how fast it goes to .
This is erdos_142.variants.lower of the formal-conjectures file for Erdős 142, reproduced binder for binder, over that file's own definition of .
The headline theorem in that file, erdos_142, states 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 " — has no known right-hand side for any , 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 — it follows from Bloom–Sisask 2020, and a fortiori from Kelley–Meka 2023 — trivial for , where , and open for every . It fixes no constants, so no future improvement can invalidate it.
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 , and variants above, and the only two files in that repository that mention at all are the ones for #142 and #139.
Proving for all yields, by a standard summation argument, Erdős's conjecture that every with 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 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 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 ; those are the only two files there that mention . 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.
Every known upper bound for runs a density increment: if of density has no -term progression, find a long subprogression on which has density , and iterate. The bound this produces is governed entirely by two quantities — how large the increment is, and how much of the interval survives one step. For the increment is extracted from an inverse theorem for the Gowers -norm, and the best available correlation bounds there are quasipolynomial in ; iterating a quasipolynomial increment cannot do better than , which is nowhere near . Reaching requires an increment with polynomial dependence on together with a subprogression of polynomial length, and that combination is currently available only for , through the sifting and almost-periodicity machinery of Kelley–Meka. No soft or averaging argument can substitute: Behrend's construction shows the truth at is , so the answer is not a power of and cannot be produced by any argument whose output has that shape.
The mission's definition file Erdos142Basic carries two layers, and every statement in the mission is written against them.
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 with first term and difference when it has exactly elements and equals ; it is free of length- progressions when every progression of length inside it forces ; and is the supremum of over subsets free of length- progressions. The ground set is Finset.Icc 1 N, and the supremum is sSup over ; the file proves the two facts that make it a genuine maximum (le_r and r_le).
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 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- and length- progressions are trivial, so every set is free of them and ; monotonicity of in therefore holds only from onward, and the corresponding milestone carries that hypothesis. Asymptotic statements use Asymptotics.IsLittleO and Filter.atTop over with real-valued casts, and real division is Lean's, so (N : ℝ) / Real.log N is at ; this is invisible to atTop.
A trivializing formalization is ruled out by construction: one milestone asserts 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 , 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 case of a general- milestone, and reusable Fourier-analytic infrastructure are all valuable even when they do not close a milestone.
FormalConjectures/ErdosProblems/142.lean — the source of the goal statement and of the definition of . https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.leanAn elliptic curve over is a smooth cubic curve with a rational point. Its rational points form a finitely generated abelian group (Mordell, 1922), so for an integer , the rank. No algorithm is known that decides, for a given curve, whether , i.e. whether there are infinitely many rational points. The Birch and Swinnerton-Dyer conjecture predicts from an analytic object, the Hasse–Weil -function : it asserts that equals the order of vanishing of at . It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute; the official formulation is Andrew Wiles' problem description, The Birch and Swinnerton-Dyer Conjecture (2000). This mission formalizes that statement, its weak form, and the results Wiles lists as known.
Timeline.
A Weierstrass equation over is
with discriminant ; in Lean, WeierstrassCurve ℚ. It is an elliptic curve when (Mathlib's typeclass IsElliptic). Its rational points are the rational solutions together with the point at infinity , an abelian group under the chord-and-tangent law (W.toAffine.Point). The rank is the rank of this group as a -module,
the in .
The Hasse–Weil -series is built prime by prime. For each prime take a Weierstrass equation for that is minimal at (integral coefficients, with the -adic valuation of as small as possible) and reduce it modulo ; put when the reduction is smooth (good reduction). The local factor is
and , convergent for by Hasse's bound. In Lean this is Mathlib's WeierstrassCurve.LSeries W s, defined by exactly this recipe (WeierstrassCurve.LFunction is the arithmetic function , an Euler product of local factors computed on a model minimal at each prime); where the Dirichlet series does not converge, Mathlib's LSeries takes the junk value . This is the complete -series of Wiles' Remark 1; it differs from the incomplete product over in Wiles' display by finitely many factors holomorphic and non-zero at , so both have the same order of vanishing there.
An -function of is an entire function with for (BSD.IsLFunction W Λ). By the identity theorem there is at most one; by modularity there is exactly one. The order of vanishing of at is the with , ; in Lean, analyticOrderAt Λ 1, valued in , with value exactly when vanishes identically near .
BSD.birch_swinnerton_dyer)For every elliptic curve over there is an entire agreeing with on such that
This is Wiles' Conjecture (Birch and Swinnerton-Dyer): with and . Open.
BSD.weak_birch_swinnerton_dyer)There is an -function of with if and only if is infinite. Wiles: "In particular this conjecture asserts that is infinite." Open.
BSD.mordell): is a finitely generated abelian group.BSD.lSeriesSummable): converges for . Wiles: "this Euler product is then known to converge for ."BSD.exists_isLFunction): has an -function. Wiles: Hasse's conjecture, "now been proved" by Wiles, Taylor–Wiles and Breuil–Conrad–Diamond–Taylor.BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one): if an -function of vanishes to order at most at , its order equals the rank. Wiles: "If with and or , then the conjecture holds."A bridging lemma, BSD.isLFunction_unique, records that an -function of is unique when it exists.
The result itself. The conjecture makes the finiteness of decidable from and, in its refined form, gives an effective procedure for finding generators (Manin, 1971). Conditionally on it, Tunnell (1983) characterises the congruent numbers, the areas of right triangles with rational sides, a problem open since the tenth century. It is the prototype of the conjectures of Tate, Deligne, Beilinson and Bloch–Kato relating ranks of arithmetic groups to orders of vanishing of -functions.
Formalizing it. None of the statements in this mission has a machine-checked proof. Mathlib provides the objects: the group law on , minimal models and reduction types over discrete valuation rings, and the Hasse–Weil -series as a Dirichlet series (2025–2026). It does not contain Mordell's theorem (no theory of heights), Hasse's bound, modularity, or the continuation of . On this platform, earlier library entries named birch_swinnerton_dyer are retired placeholders whose formal statements reduce to trivialities such as ; they carry a notice saying so and are not formalizations of the conjecture. This mission gives the first faithful statement against Mathlib's own -series. Two published platform results bear directly on the milestones: the descent step WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex (finite index of implies finite generation) reduces milestone 1 to the weak Mordell–Weil theorem, and WeierstrassCurve.modularity_of_semistableModel from the platform's Fermat's Last Theorem development proves modularity of semistable curves for a notion of modularity defined through eigenform coefficients; relating that notion to WeierstrassCurve.LSeries would give milestone 3 for semistable curves.
Neither side of the equation is computable in general. On the algebraic side, descent bounds the rank from above by the rank of a Selmer group, but the gap is the Tate–Shafarevich group Ш, which is not known to be finite; the obvious plan, compute the Selmer group and show it has the rank of , founders on Ш. On the analytic side one can certify or numerically but cannot certify an exact zero, and the only known bridge from -values to rational points, the Heegner point construction, produces at most one independent point. This is why milestone 4 stops at order and the conjecture is not known for a single curve of rank . Iwasawa theory (Kato, Skinner–Urban) relates -adic -functions to Selmer groups but yields -adic, not Archimedean, orders of vanishing.
The formalization adds its own obstacles: milestone 1 needs heights and the weak Mordell–Weil theorem (Kummer theory over number fields, finiteness of class groups and units); milestone 2 needs Hasse's bound, i.e. the degree of the Frobenius endomorphism; milestones 3 and 4 rest on modularity, Galois representations, modular curves and Euler systems.
WeierstrassCurve ℚ with IsElliptic (); no minimality or integrality of the model is assumed. Mathlib's -series passes to a minimal model at each prime internally, and the point group depends only on the curve, so every statement is invariant under change of Weierstrass equation.Module.finrank ℤ W.toAffine.Point: for a finitely generated abelian group, the in ; for a group of infinite rank Mathlib's finrank is , a case milestone 1 excludes.WeierstrassCurve.LSeries, with all Euler factors including the bad primes, and junk value where the Dirichlet series diverges. BSD.IsLFunction constrains only on ; milestone 2 shows the series is genuine there, and the bridging lemma shows is then unique.analyticOrderAt Λ 1 : ℕ∞; equating it with a natural number asserts in particular that near .No trivializing formalization. The existential cannot be chosen freely: it must agree with the honest, non-zero Dirichlet series on a half-plane, so it is unique, and is excluded by the finite value of the rank. Without IsElliptic the statements would concern singular cubics, whose point group is or ; the hypothesis is required, not decorative.
Out of scope. The refined conjecture (the leading coefficient in terms of Ш, the regulator, the real period and the Tamagawa numbers), the finiteness of Ш, number fields and abelian varieties, and the functional equation of .
Infrastructure needed and welcome contributions. Heights on and the weak Mordell–Weil theorem; Hasse's bound and the multiplicativity of ; a bridge from Mathlib's WeierstrassCurve.LSeries to the -series of a weight-two newform, so that existing modularity results yield milestone 3; Heegner points and Kolyvagin's Euler system for milestone 4; and the bridging lemma, provable now from the identity theorem. Decompositions of every milestone and lemmas about WeierstrassCurve.LFunction (its values at primes, multiplicativity, independence of the model) are welcome.
Our goal
This project aims to formalize the Poincaré conjecture in Lean, following the approach in Kleiner and Lott's Notes on Perelman's Papers.
Important references
Poincare-Conjecture and DifferentialGeometry are important references for this project, providing existing work on proof planning and foundations in differential geometry. We thank the authors and contributors of both projects. We will build on their work while preserving credit and citing our sources.
OpenGA's role
OpenGA focuses on manual review, curation and reuse: checking existing code, adapting it to the required versions, and organizing reusable definitions and theorems in the library.
The PoincareConjecture directory is used to prepare submissions to Prove2Me and keep a local copy of the platform's code and progress through ongoing synchronization. Results completed on the platform will also be reviewed and incorporated into OpenGA for use in future work in geometric analysis.
We thank the Prove2Me team for running the platform and exploring collaboration between humans and AI in mathematical formalization. We are honored to take part.
If is algebraic and , is transcendental? Guy Diaz asked this in 2004 and it is still open. Note it is , not — the latter would follow at once from Hermite–Lindemann. The whole difficulty is that itself may be transcendental while only its modulus is constrained.
Write for the algebraic numbers in and
for the logarithms of algebraic numbers. In 2004 Guy Diaz asked, and conjectured, that no non-zero element of has algebraic modulus. He states it as
« Soit avec ; alors est transcendant. »
The statement fits on one line and needs no machinery beyond and . It has been open for twenty-two years.
It is not a curiosity. Diaz records that it follows from Schanuel's conjecture and also from the strong four exponentials conjecture, so it sits underneath two of the standard pillars of transcendence theory while being far more concrete than either. Anything that settles it settles a case of both.
The mission decomposes into work that can be done now, without any open input.
Two milestones are conditional theorems — "Schanuel implies Diaz", "strong four exponentials implies Diaz". Diaz asserts both implications in a single sentence and does not write out either derivation; as far as I can establish, neither has been written out anywhere. Each is a short, self-contained argument that any solver can attack today. Both are stated here without axioms: Schanuel, the strong four exponentials conjecture and Hermite--Lindemann are all Prop-valued definitions in the mission's definition bundle, so a conditional milestone takes its hypothesis explicitly and nothing is assumed silently.
A third milestone is the elementary geometry of the configuration — the coordinate axes, which turn out to be exactly the degenerate branch where and are -linearly dependent.
The remaining two milestones are classical theorems that the platform's Mathlib does not have: Hermite--Lindemann and the six exponentials theorem. The first is needed by the four-exponentials route and by the axis case. The second is the proved member of the family this conjecture lives in, and the distance between it and the strong four exponentials conjecture is a fair measure of how far the known machinery falls short.
Only the top node needs genuinely new transcendence.
One structural remark that shapes the whole ladder: Hermite--Lindemann is a special case of the goal, not just an input to it. If is algebraic then is algebraic, hence so is , and the goal applied to gives that is transcendental. Diaz's conjecture is therefore strictly stronger than Hermite--Lindemann, and no route to it can avoid that node.
| 1873, 1882 | Hermite, then Lindemann: is transcendental for algebraic . In particular every non-zero element of is itself transcendental, so a counterexample would be a transcendental number with algebraic modulus and algebraic exponential. |
| 1934--35 | Gelfond and Schneider settle Hilbert's seventh problem. |
| 1966 | Lang's Introduction to Transcendental Numbers records Schanuel's conjecture, and gives the six exponentials theorem (also Siegel, unpublished; Ramachandra 1968). The four exponentials conjecture stays open, and still is. |
| 1966 | Baker's theorem on linear forms in logarithms. |
| 1997 | Diaz studies the companion condition , assertion (4-1), p. 237. |
| 2000 | Waldschmidt's Diophantine Approximation on Linear Algebraic Groups states the conjecture at p. 399, credited to Diaz 1997, and records the relevant four-exponentials configuration with , at p. 15. |
| 2004 | Diaz states the modulus question, §5.1, p. 550. On p. 551 he asks the accompanying methodological question: how could the non-holomorphic maps and enter a transcendence proof at all? |
| 2026 | A machine-checked negative result on a class of strategies (see below). The conjecture itself is untouched. |
For a candidate one has with algebraic, hence
So is not independent data: complex conjugation on is a rational function of the generator, determined by the ring structure. Three consequences follow, all formalised at https://github.com/carlok/diaz-modulus-lean: a ring homomorphism fixing and carrying to any other transcendental point of the same circle automatically intertwines conjugation; such a homomorphism exists whenever both points are transcendental over the base; and no vanishing-coefficient statement over separates a candidate from an ordinary complex number placed on the same circle.
The practical consequence for solvers: accumulating algebraic relations between and until they collide cannot settle this. A successful attack has to introduce information that is not a rational function of over — which is precisely Diaz's own methodological question, still open.
Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean — verified in all three of the platform's pinned revisions (0df444a3, c5ea0035, 777aaa61), none of which contains transcendental_exp. Hence the choice to carry it as a Prop and give it its own milestone rather than assume it. There is an open PR, leanprover-community/mathlib4#28013 (feat: Lindemann-Weierstrass Theorem, opened 2025-08-05, label awaiting-author as of 2026-09-07); if it merges and a pin advances, that milestone collapses to a short transfer.Algebra.trdeg has almost no computational API. It is cardinal-valued, with transcendence bases and lift_cardinalMk_eq_trdeg, but nothing that evaluates the degree of an explicitly adjoined finite set. The Schanuel milestone will want a lemma of the shape "if with transcendental over then ". That is worth splitting off as a child in its own right; it is reusable well beyond this mission.A -packing in a graph is a collection of pairwise vertex-disjoint paths on three vertices. Determining the largest such packing is NP-hard even in restricted graph classes, so structural hypotheses that force an optimal packing are of independent interest in graph factor theory. The present question asks whether 3-vertex-connectivity and cubicity force the strongest possible packing whenever the vertex count permits a perfect partition.
A. Kelmans attributes the broader packing problem to 1984. In Problem 1.10 of Packing 3-vertex Paths in Cubic 3-connected Graphs, the question is whether every cubic 3-connected graph satisfies . Theorem 3.1 of that paper proves that the divisible-order factor statement is equivalent to several apparently stronger deletion and prescribed-edge statements; it does not prove the open claim itself. OPG-46613 records the divisible-order form targeted here.
A 2026 candidate analysis in the Vibe Mathing problem repository investigated a tempting sufficient route: find a perfect matching whose complementary 2-factor has every cycle length divisible by three. Candidate C01 explains why that condition would yield a -factor. Candidate C02 gives an explicit proposed family of order that has -factors but is claimed not to satisfy the stronger matching condition. These candidate claims have computational and partial Lean checks, but no complete Lean kernel proof; they are milestones here, not declarations that the original problem or the candidate family has already been formally established.
All graphs are finite and simple. A graph is cubic when every vertex has exactly three neighbors. It is 3-vertex-connected here when it has at least four vertices and deleting any set of at most two vertices leaves a connected induced graph.
A -factor is represented by a natural number , together with a bijection
such that, in every block, positions and are adjacent and positions and are adjacent. The path is not required to be induced: an ambient edge between positions and is allowed because the two selected path edges still form a copy of .
A 2-factor is a spanning 2-regular subgraph. It is called divisible when every one of its connected components has order divisible by three. A divisible matching complement is a perfect matching such that the relative complement is a divisible 2-factor.
The explicit graph is defined on . Its first nine vertices form the fixed Petersen-minus-one-vertex brick from C02; the remaining vertices form the stated cycle-and-opposite-chord brick with three joining edges. The full adjacency relation is part of the Lean definition rather than an external data file.
For every finite simple graph ,
This is the OPG-46613 target. Cubicity forces the order to be even, so within this domain divisibility by three is equivalent to divisibility by six.
The mission also formalizes the part of Kelmans's Theorem 3.1: the divisible-order factor claim is equivalent to the assertion that deleting any specified 3-vertex path leaves a -factor. Two route lemmas state that divisible 2-factors split into -factors and that, in cubic graphs, divisible 2-factors are equivalent to divisible perfect-matching complements.
The C02 milestones ask first for the complete 18-vertex statement and then for the full family:
This separates a sufficient method from the root conclusion. It is not a counterexample to OPG-46613 because every in the proposed family explicitly satisfies the desired conclusion.
A proof of the main goal would settle the divisible-order form of a long-standing path-packing problem. Through Kelmans's equivalences it would also control several deletion and prescribed-edge variants for cubic 3-connected graphs. A disproof would require a graph satisfying all domain hypotheses but lacking a -factor; the C02 family does not claim this.
Formalizing the candidate boundary is useful even before the root is resolved. It turns a route exclusion into a checkable theorem and prevents a search campaign from silently assuming that every relevant graph possesses a divisible complementary 2-factor. The definitions of noninduced -factors, vertex connectivity by deletion, perfect matchings, 2-factors, and component-order divisibility are intended to be reusable in later graph-factor work.
The perfect-matching route is attractive because the complement of a perfect matching in a cubic graph is 2-regular. The obstruction is that its cycles need not have lengths divisible by three. The C02 candidate family is designed to expose exactly that gap: a persistent 5-cycle is claimed to occur in every complementary 2-factor even though an unrelated -factor exists. Consequently, proving the main theorem cannot simply assume that a favorable perfect matching always exists.
The formal difficulty is also semantic. Connectivity must mean vertex connectivity, the complement must be relative to on the same vertex set, component sizes must refer to the 2-factor rather than the ambient graph, and must remain noninduced. Weakening any of these points can create a materially different or vacuous theorem.
The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Graphs use SimpleGraph on finite vertex types. Degree is the cardinality of the actual neighbor subtype. Three-vertex-connectivity explicitly quantifies over all finite deletion sets of cardinality at most two and includes a four-vertex order guard.
The main theorem is universe-polymorphic and does not hard-code a finite graph enumeration. The family includes . The factor structure uses a bijection, so disjointness and coverage cannot be discharged by duplicate or omitted vertices. Ambient chords do not invalidate a block, while both required consecutive adjacencies must be genuine graph edges. The candidate family statements remain open theorem goals ending in sorry; the shared definition module itself is sorry-free.
Welcome contributions include proofs of the model lemmas, the finite statement, the general C02 family, Kelmans's equivalence, or decompositions of the root theorem into faithful reusable lemmas. Numerical enumeration alone is supporting evidence and should not be presented as a kernel proof.
14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c01/proof.md14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c02/proof.mdThe smooth four-dimensional Poincaré conjecture asks whether a smooth manifold with the topology of the four-sphere must also have its standard smooth structure, up to diffeomorphism. The distinction is between the existence of continuous coordinates and the compatibility of differentiable coordinates. The mission concerns this precise sphere question, listed as open in Problem 4.1 of K3 — A New Problem List in Low-Dimensional Topology. It does not treat a collection of algebraic obstructions as an existing proof of the conjecture. Baykur–Kirby–Ruberman, Problem 4.1
Let be the unit sphere in , with its standard stereographic smooth structure. A homeomorphism is a continuous bijection with continuous inverse; a diffeomorphism is a smooth bijection with smooth inverse. A smooth atlas is a collection of local Euclidean coordinates whose transition maps are smooth.
The manifold is compact and Hausdorff, has no boundary, and is equipped with a specified smooth atlas modeled on . The given atlas is arbitrary: it is not defined by transporting the standard structure from .
For a homeomorphism , let denote the atlas transported from the standard sphere along . A structomorphism for the smooth structure groupoid is a homeomorphism whose coordinate expressions belong to that groupoid. The predicate requires, for every given smooth atlas on such an and every such , a structomorphism between and . It does not require that structomorphism to be the identity. These are the conventions of the source definitions, not additional uniqueness assumptions. [Shin, SPC4.lean, lines 53–81 and 211–221]
For every manifold with the preceding hypotheses, the goal is
This is the source predicate . Its conclusion asserts the existence of a diffeomorphism; it does not assert that a particular supplied homeomorphism is smooth.
The atlas formulation has the exact equivalence
The source supplies a proof of this equivalence without invoking Freedman's theorem or assuming the conjecture as an unconditional fact. It is a reformulation, not a solution. Its foundations include the correspondence
where is the smooth coordinate-change groupoid for the common model. [Shin, SPC4.lean, lines 334–365; Bridge.lean]
Write for the following compact Hausdorff, boundaryless instance of Freedman's topological theorem:
where denotes homotopy equivalence and only topological manifold charts are assumed. This is established mathematics, but a proof in the present formal development remains a target. If denotes the analogous smooth conclusion from a homotopy equivalence, the relation to the main goal is recorded with its hypothesis visible:
Explicit standard-disk foundations form another track. For every , they concern the manifold-with-boundary structure on , its boundary set , and the smooth collar
The collar is a closed embedding, has image
and satisfies , using the boundary inclusion. Its image is a neighborhood of every boundary point in the disk. A companion interface characterizes a map from a manifold with corners into the disk as precisely a continuous map whose inclusion into Euclidean space is . These targets concern the actual disk smooth structure. [Shin, Disk.lean, lines 1076–1141 and 1263–1318]
For each integer , let be the closed unit disk in and let be any homeomorphism of its boundary. The twisted double identifies the boundary point in a left copy of the disk with in a right copy. With the quotient topology, the target is
This statement is published as SP4Gluing.twistedSphere_homeomorphic. The theorem and its supporting continuity and injectivity lemmas have accepted Lean proofs contributed by carlok. All three accepted proofs have also been checked locally with their proved dependencies. It concerns these explicit topological quotients, not arbitrary homotopy spheres or a prescribed smooth structure.
For every regional chart base point, the open-bicollar and left-interior transitions are smooth in both directions. Right-interior-to-seam smoothness requires smooth ; the reverse requires smooth . The single compatibility target concerns exact overlap sources, combining four source results internally. It provides neither a global smooth-manifold instance nor smooth standardness. [Shin, Hemisphere.lean, lines 2439–3577]
A proof of the main goal would identify every smooth structure in its stated sphere class with the standard one, up to diffeomorphism. A proof of the transported-atlas equivalence instead locates the same unresolved comparison in a different formal language. The distinction matters: constructing a smooth structure by transport is not the same as identifying an arbitrary pre-existing one.
The bridge, explicit disk atlas, and stated collar properties have accepted kernel-checked Lean proofs. The clean atlas equivalence also has a proof with no admitted theorem among its axioms. The conjecture remains open, and Freedman's topological theorem remains unproved in this formal development despite its published mathematical proof.
The topological two-disk gluing result identifies the homeomorphism type of these quotients for every boundary homeomorphism and every disk dimension at least one. The accepted formalization supplies a global topological comparison for this explicit quotient. It does not resolve the comparison with a prescribed smooth structure or recognition of general smooth four-manifolds.
Four supporting algebraic tracks concern orbit coinvariants, homology dimension budgets, finite-support shift rigidity, and Laurent-polynomial positivity. Their source results arose in route-specific obstruction studies. As of 6 September 2026, all eleven theorem targets in these algebraic tracks have accepted Lean proofs. The five additional formal proofs were contributed by wamlart: orbit augmentation, region homology budgets, two-corner homology budgets, the Laurent mass threshold, and mass-two positivity. No theorem currently connects their completion to a proof or disproof of . They are exploratory tools, not established milestones in a proof of the main goal.
A homeomorphism can transport the standard atlas, but that observation does not compare the transported atlas with the one already specified on the manifold. Treating those two atlases as equal would remove the central mathematical question by changing its hypotheses.
Likewise, topological recognition does not supply a smooth recognition theorem. Standard disk and collar constructions establish local models; they do not establish a smooth gluing or recognition theorem for an arbitrary prescribed smooth structure, a recognition theorem for arbitrary smooth balls, or a smooth Schoenflies theorem. The missing global comparison cannot be replaced by successful finite algebraic tests or by constructing a standard local chart.
The sphere goal quantifies over Type in universe zero, exactly as in the source. It uses real four-dimensional Euclidean chart models, compactness, the Hausdorff condition, and smoothness of order . Boundaryless manifolds are built into that model. No orientation, fixed parametrization, or identity-map uniqueness is imposed.
The geometric foundations use charted spaces, structure groupoids, models with corners, homotopy equivalences and diffeomorphisms. Disk results include every , so their dimensions are . The boundary-set identification does not by itself construct a general induced smooth boundary structure. Nor is smoothness asserted for a radial clamp across its nonsmooth locus.
The separate source assertion SPC4Ball is not treated as equivalent to the sphere goal: the required formal boundary, capping and gluing bridge is absent. The transported-annulus product diffeomorphism is not a current target; its chart instances serve only as constructor support. No unconditional implication is taken through the source's admitted Freedman declaration. Gaussian coupling, transport defects, partition incidence and merge-score results remain outside this mission because no mathematical dependency on them has been established.
R. İnanç Baykur, Robion C. Kirby and Daniel Ruberman, eds., K3 — A New Problem List in Low-Dimensional Topology, Mathematical Surveys and Monographs 295, American Mathematical Society, 2026, Problem 4.1, pp. 191–192. Author PDF.
Michael Hartley Freedman, The topology of four-dimensional manifolds, Journal of Differential Geometry 17 (1982), 357–453, Theorem 1.6, p. 371. DOI; primary-article scan.
Stephen Smale, Generalized Poincaré's Conjecture in Dimensions Greater Than Four, Annals of Mathematics 74 (1961), 391–406, Theorem A. DOI; primary-article scan.
Ryan Shin, SPC4.lean, Bridge.lean and Disk.lean, unpublished source files, 2026; no public manuscript URL available. SHA-256, respectively: b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc, e8ea6b66f6bd675ca272e862e0825ab2db1f8bb792eaffe1b9e8f5d89024d302, 889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e.
Ryan Shin, Hemisphere.lean, unpublished Lean source file, 2026, declaration twistedSphereHomeoSphere; source SHA-256 c48843d2c4ec6987acfd7f7ab3a92bfed990376206142e74712795b4e9399828. Published topological two-disk gluing target; the recovered local construction is checked; the accepted proof and its two supporting lemmas were contributed by carlok.
Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.
This mission turns CUHK-Shenzhen AI Math Problem 16, Existence of complete sets of mutually unbiased bases, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
Construct seven 6 by 6 unitary-column matrices whose every distinct pair has all transition amplitudes of squared modulus 1/6. The baseline milestone constructs three pairwise mutually unbiased bases, a known lower bound that tests all matrix conventions.
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in quantum information theory, mutually unbiased bases, finite fields, Hilbert spaces. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
The equations are a large coupled system of polynomial equalities over complex phases, modulo substantial gauge symmetry. Numerical near-solutions do not certify exact existence, while nonexistence would require a global obstruction beyond currently known bounds. Dimension six lacks the finite-field structure that supplies complete prime-power constructions.
Formalize standard gauge reductions: fix the first basis to the identity and dephase transition Hadamard matrices. Verify a three-basis tensor-product construction. Then encode additional bases through complex Hadamard matrices and study algebraic constraints, Gröbner-style eliminations, semidefinite bounds, or exact certificates. Computational searches may guide conjectures, but uploaded proofs must convert numerical evidence to exact algebraic identities or certified inequalities.
The Lean target is exact: column orthonormality is U-adjoint times U equals identity, and mutual unbiasedness uses Mathlib complex norm squared. Seven bases are indexed by Fin 7. No quotient by phase, permutation, or global unitary is built into the statement, since these symmetries preserve the predicate and can be used within proofs.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
Publish an exact three-basis construction in dimension six, then formalize dephasing and obstruction lemmas for extending a partial family.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a -dimensional polytope with facets is at most . Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the polynomial Hirsch conjecture: is the diameter bounded by a polynomial in and ?
Work in . An H-polytope is a set cut out by finitely many linear inequalities: given vectors and reals , it is
where is the standard inner (dot) product — so each condition is one linear inequality, with normal vector and offset . Throughout, is assumed nonempty and bounded. The parameter counts the inequalities in the given description; since every polytope with facets admits a description by exactly inequalities, bounds stated in terms of over all descriptions are equivalent to bounds in terms of facet counts.
A vertex of is an extreme point. Two vertices are adjacent when the segment is an extreme subset of ; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that is a one-dimensional face — an edge. The combinatorial diameter of is the diameter of the graph of vertices and edges. Throughout, "diameter at most " is expressed as: every two vertices are joined by a walk of steps, each step staying put or crossing an edge — a form that is monotone in and asserts connectivity of the graph (Balinski's theorem) as part of the claim.
Every polynomial in and is dominated by some and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents.
Six classical results over the same definitions: the Hirsch bound in dimension (Klee; Klee–Walkup); Larman's bound ; Naddef's bound for -polytopes; the Kalai–Kleitman bound ; Todd's bound for full-dimensional with ; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds .
A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß (Math. OR 2010) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes.
None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge.
The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving any polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters large is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial.
The Lean model commits to: ambient space EuclideanSpace ℝ (Fin d); the polytope as Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i} for a : Fin n → EuclideanSpace ℝ (Fin d), b : Fin n → ℝ, with nonemptiness and Bornology.IsBounded as explicit hypotheses (boundedness is essential: Klee–Walkup's unbounded counterexample would otherwise trivialize the Santos milestone); vertices as Set.extremePoints ℝ; adjacency as u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v); and diameter bounds as the walk predicate DiamLE, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through Real.logb and the natural floor. In larman_bound and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all in scope. The dimension parameter is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with todd_bound requiring full-dimensionality ((interior P).Nonempty) as in its source.
Welcome contributions: any milestone in any order (dimension_three_bound for cases and structural lemmas about Adj and DiamLE are natural entry points, and kalai_kleitman_bound is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions.
No problem in mathematics carries more weight than the Riemann hypothesis. In his single eight-page paper of 1859, 'On the Number of Primes Less Than a Given Magnitude,' Bernhard Riemann linked the seemingly erratic distribution of the primes to the zeros of the analytic continuation of the zeta function ζ(s), and conjectured that every nontrivial zero lies exactly on the critical line where the real part equals 1/2. The truth of this statement would pin down the error term in the prime number theorem and tame the fluctuations of the primes around their expected count, and hundreds of theorems already stand proven only 'conditional on RH,' waiting for it to be settled. David Hilbert placed it in his eighth problem in 1900, alongside Goldbach and the twin primes; in 2000 the Clay Mathematics Institute named it one of the seven Millennium Prize Problems, with a million-dollar reward. G. H. Hardy proved in 1914 that infinitely many zeros lie on the critical line, and trillions more have since been verified by computation to do so — overwhelming evidence that is nonetheless not a proof. After more than 160 years it remains unresolved. This mission takes Mathlib's own definition of the hypothesis as its target.
Value iteration and its policy-evaluation special case, value computation, are the basic algorithms of dynamic programming for Markov decision processes (MDPs). Both are fixed-point iterations of a -contraction, so they converge at the geometric rate , the discount factor. When is close to , which is the regime of long effective horizons in reinforcement learning ( or ) and in healthcare and operations applications, the number of iterations grows like .
Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) observe that behaves like the gradient of a function with smoothness constant and strong-convexity constant . This suggests importing the accelerated schemes of convex optimization: Nesterov's acceleration and Polyak's momentum (heavy-ball) method (Polyak 1964; Ghadimi, Feyzmahdavian, Johansson 2015). For the affine operator of a fixed policy, they prove that both schemes converge at a rate governed by rather than , with , provided the Markov chain of the policy is irreducible and reversible. This mission poses the momentum result, Theorem 5.5.
A finite MDP has a state set with , a finite action set , transition probabilities (from state to state under action ; each is a probability vector), rewards , and a discount factor . A policy is a matrix with nonnegative rows summing to ; it induces
The value function of is , the expected discounted reward from each starting state; it is the unique fixed point of .
Reversibility (Definition 2.1): the chain with transition matrix is irreducible, and it has a stationary probability distribution with for all .
Momentum Value Computation (M-VC) starts from arbitrary and iterates
with the constant step sizes (4.2)
The analysis runs through the matrix
which propagates the error of the pair , and its spectral radius , the largest modulus of a complex eigenvalue.
For a valid MDP and a policy whose chain is irreducible and reversible, the M-VC iterates with step sizes (4.2) converge to , and for every
The goal states the paper's three clauses as printed: convergence, the little-o rate for every , and the comparison with .
The rate is the optimal rate of the heavy-ball method on strongly convex quadratics with condition number . Theorem 5.5 shows that policy evaluation for reversible chains enjoys the same improvement over , so that an -approximation of needs a number of iterations scaling like rather than . The paper also shows that the reversibility assumption cannot simply be dropped: on a cyclic chain both accelerated schemes may diverge. Lemma B.2 is an exact spectral computation for a structured block matrix that reappears in any heavy-ball analysis driven by a matrix with real spectrum in .
The paper is a sibling series of four missions. This one poses Theorem 5.5; the others pose Theorem 5.1 (Accelerated Value Computation), Theorem 6.3 (a lower bound for first-order methods on a chain MDP) and Theorem 7.1 (Safe Accelerated Value Iteration). The results are proved on paper; none of them has a machine-checked proof. The work here is to formalize the known argument: the linear-recursion representation, the spectrum of , and the passage from spectral radius to a little-o rate.
The obvious argument bounds in some norm and iterates. No such bound by the rate holds in general: is not normal, and for eigenvalues of the two roots of (B.1) coincide, producing Jordan blocks. The rate must come from the spectral radius, and the gap between and is exactly what the absorbs. Computing needs two separate facts: the eigenvalues of are tied to those of through the quadratic (B.1), which needs a determinant identity for block matrices with commuting blocks; and the eigenvalues of are real and lie in , which needs reversibility together with irreducibility, used to make the stationary distribution positive. For non-real the modulus computation fails, which is why the hypothesis cannot be dropped.
States and actions are finite types. The MDP data is a plain structure, with validity (stochastic , ) a separate hypothesis; the paper's initial distribution plays no role and is omitted. The value function is the Neumann series . The norm on is the sup norm, and is with respect to it as . Spectra and spectral radii are those of the complexified matrices, so that the non-real eigenvalues of are seen. Reversibility uses the published mm_basic notions: irreducibility, a stationary probability distribution, and detailed balance with respect to it; detailed balance alone would be trivially satisfied by and is not used.
Three printed slips are corrected, and each milestone keeps the printed text verbatim. Lemma B.1 is printed with , but is undefined; the statement uses . Lemma B.2 prints , a negative number; its proof computes , the rate of Theorem 5.5, which is stated. On p. 22 the constant is printed as . The second step size, printed in (4.2), is the of (M-VC) and App. B.
A statement that holds only vacuously, for example one in which reversibility is replaced by detailed balance with an arbitrary vector or in which is unconstrained, is ruled out by the hypotheses above. Lemma B.2 is an equality and must not be weakened to an upper bound.
A complete development needs the determinant of a block matrix with commuting blocks, the reality of the spectrum of a reversible chain (implied by the published MarkovMixing.spectral_representation once the stationary distribution is shown positive), Gelfand's formula for matrices, and the convergence of the Neumann series. The spectral facts about reversible chains and the block-matrix spectrum are reusable beyond this mission. Proofs of any milestone are welcome independently.
Value iteration is the standard method for solving a discounted Markov decision process (MDP), and its policy-evaluation variant, value computation (VC), computes the value of a fixed policy by iterating an affine contraction. Both converge geometrically at rate , the discount factor. When is close to one, as in long-horizon reinforcement-learning benchmarks ( or ), the number of iterations grows like , and each iteration costs a full sweep over states and actions.
In convex optimization, gradient descent on a -strongly convex, -smooth function has the same kind of rate, and Nesterov's acceleration improves the dependence on the condition number from to . Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read as a gradient with "strong convexity" and "smoothness" , transfer Nesterov's and Polyak's step sizes to value iteration, and ask when the transferred methods are actually faster. This mission covers the first answer they give: for policy evaluation on a reversible chain, the accelerated scheme converges at a rate of order instead of .
An MDP has a finite set of states with , a finite set of actions , transition probabilities (from state to state under action ; each is a probability distribution), real rewards , and a discount factor . A policy assigns to every state a probability distribution over actions. It induces the reward vector , the transition matrix , the policy operator , and the value function
the expected discounted reward when actions are drawn from . VC iterates .
Accelerated Value Computation (A-VC) starts from arbitrary and sets, for ,
with the constant step sizes and . Write .
A transition matrix is reversible if it is irreducible (every state reaches every other with positive probability in some number of steps) and has a stationary probability distribution satisfying detailed balance, for all .
The analysis runs through the matrix
whose powers propagate the stacked error , where and . Its spectral radius is the largest modulus of a complex eigenvalue.
If is irreducible and reversible, then , and for every
The goal is stated with the slack because the iteration matrix has a defective leading eigenvalue: the error is of exact order in general, so a clean bound is false.
The result. Since , A-VC reaches an -approximation of in iterations against for VC, at the same per-iteration cost. This matches the rate of Nesterov's method for strongly convex functions with the paper's identification of the constants. The same paper shows that this improvement does not extend to arbitrary MDPs: Theorem 6.3 gives a lower bound for every first-order method on a chain MDP, which is why reversibility (or a real spectrum, Remark 5.4) is needed here.
Formalizing it. The result is proved in the paper; no machine-checked proof exists. A formal proof needs the reality of the spectrum of reversible chains, the localization of the spectrum of a structured block matrix, and the passage from the spectral radius to a little-o rate for a matrix with a nontrivial Jordan block. The paper's printed statement puts under the square root, . That rate is faster than and is false (a one-state chain is a counterexample). The mission poses the rate that the paper's own proof concludes on p. 9. This is one of four missions from this paper; the other three pose Theorem 5.5 (momentum value computation), Theorem 6.3 (the first-order lower bound) and Theorem 7.1 (safe accelerated value iteration).
The obvious argument says ", so at rate ". That argument breaks twice. First, computing requires knowing where the eigenvalues of lie. For a general stochastic matrix they fill the unit disk, and then the roots of (5.3) can exceed in modulus. Reversibility is what confines them to , and the reality of the spectrum of a reversible chain is not in Mathlib. Second, the eigenvalue of (coming from ) is a double root of (5.3) with a single eigenvector, so is not ; only the -relaxed little-o holds. The eigenvalues of are non-real for , so the whole computation must be done over .
FoundationsML.ReinforcementLearning definitions; irreducibility, stationarity and detailed balance are the published mm_basic. is the discounted reward series, not an arbitrary fixed point of .Ruling out trivial readings: the hypotheses are satisfiable (a two-state chain with is valid, reversible and has a policy), the rate is stated with rather than for some , and is a fixed object rather than a variable constrained by hypotheses.
Needed infrastructure, reusable beyond this mission: the reality and location of the spectrum of reversible stochastic matrices (also used by the sibling mission on momentum value computation); spectra of block matrices with commuting blocks; and the bound from Gelfand's formula. Contributions of any of these as stand-alone lemmas are welcome.
Banks lend to one another, and the shape of the resulting network decides how a loss at one bank reaches the others. A long line of work, starting with Allen and Gale (2000) and continued by Acemoglu, Ozdaglar and Tahbaz-Salehi (2015), compares the ring network, where each bank is owed money by one neighbour, with the complete network, where every bank holds an equal share of every other bank's debt. That literature studies contagion after shocks hit and finds that the complete network spreads losses thinly and can absorb small shocks better.
Shu's paper (Management Science, doi:10.1287/mnsc.2022.01519) asks the ex-ante question: when banks choose how much risk to take, knowing the network they sit in, which network makes them take more? A successful bank subsidizes its failed counterparties through the clearing of interbank debt, and anticipating that subsidy pushes it toward riskier projects. Proposition 4 of the paper says that this effect is stronger in the complete network. This mission formalizes that proposition and the computation behind it.
There are banks. In a regular network with share matrix , bank owes bank the face value , every bank has total interbank liability , and every bank also owes a senior deposit . The two networks of Definition 3 are
Each bank chooses a project in a common interval . The project pays with probability and otherwise, independently across banks. Assumption 1 requires , decreasing, and concave. The standing assumption says a successful bank never defaults.
After the state is realized, interbank payments clear. A payment equilibrium is a vector with
where if bank succeeds and if it fails. Bank 's profit is . A risk-taking equilibrium is a profile in which each maximizes bank 's expected profit given . Equilibria need not be unique, and the paper selects the least one.
The key quantity is the network risk-taking distortion
which is bank 's expected net interbank payment to the other banks when its own project succeeds. In a regular network, expected profit equals , so acts like extra debt that the bank repays only when it succeeds. Superscripts and mark the complete and ring networks.
With the least equilibrium of the complete network and the least equilibrium of the ring,
The result. Proposition 4 reverses the conventional reading of the complete network as the safer structure. The co-insurance that makes it resilient after a shock is the same cross-subsidy that weakens incentives before the shock. Two networks with the same face-value liabilities therefore induce different equilibrium risk-taking. Liabilities alone are not a sufficient statistic for risk incentives, and the network topology matters in its own right. The same comparison is the template for the paper's later results on the number of banks and on central clearing.
Formalizing it. The proposition is proved in the paper, not open, and none of it is machine-checked yet. A formal proof must establish the two clearing vectors, the counting identity behind (I.15), and the two closed forms of the distortion. The printed argument also leaves a step to be supplied: its final appeal to "the monotone selection theorem" needs the distortion comparison at every profile of the other banks. It is proved only when they all choose the same project, and it is false in general. The goal is nevertheless stated for least equilibria exactly as in the paper, and its formal proof has to bridge that gap. The milestones are true as stated.
The distortion of the ring is not a function of the number of failures alone. What a successful bank receives depends on the length of the run of failed banks immediately upstream of it, so the closed form needs an exact count of the binary strings with a given number of failures and a given initial run length. The comparison of the two distortions is not termwise either: the positive part sits inside a sum on the ring side and outside it on the complete side.
The obvious final step is to say that the distortion is larger in the complete network, and that a larger distortion raises the optimal risk exposure. That step does not go through as stated. The equilibrium comparison needs control of the best-response maps at every profile, while the distortion comparison holds only on the diagonal, where all other banks choose the same project. Some further structure of the two games is needed to restrict attention to that diagonal.
Banks are Fin N with , and states are Fin N → Bool with true meaning success. The paper's general model is specialized to a regular network given by , which covers both networks of Definition 3. Every expectation is a finite sum over the states, so no measure theory is involved. The payment equilibrium is the greatest solution of the clearing system, because the paper asserts only generic uniqueness. Every bank's project lies in , and is a hypothesis of every statement.
The distortion milestones (2, 5 and 8) are stated at the constant profile in which every bank chooses the same , which is how the page's single reads. At , where every other bank fails, the printed ring binomial has lower index , and the weight is fixed explicitly to at . Proposition 4 is stated for least equilibria and weak inequality. It adds one hypothesis the page does not state, continuity of on , so that best responses and least equilibria exist. Without it the IsLeast hypotheses could be unsatisfiable and the goal vacuous.
Trivializing encodings are ruled out: is an actual solution of the clearing system, not a junk supremum, and the run length is only used in states where some bank succeeds.
A complete development needs Knaster–Tarski on the box , the clearing computations for the two networks, binomial identities, and a monotone comparative statics argument for the equilibria. Published Topkis results on supermodular games (existence of least equilibria, and monotonicity of least fixed points in a parameter) are included by reference as tools. The clearing and counting lemmas are reusable for the paper's other results on ring and complete networks. Proofs of any milestone, and of the goal, are welcome.
Not posed here: Proposition 1 (strategic complementarity in any network, a separate mission), Proposition 2 (existence), and the later comparative statics in the number of banks, central clearing and bailouts.
Demand, prices and click-through rates often follow seasonal cycles: weekly, monthly, yearly. A decision maker who repeatedly chooses among options whose expected payoffs repeat in time faces a non-stationary multi-armed bandit. Chen, Wang and Wang (arXiv:2005.08088v4, Operations Research, 2025) study the model in which each arm's mean reward is periodic with its own unknown period. They give a two-stage policy whose regret is , and a lower bound showing that no policy, even one told the periods, does better than . This mission formalizes that lower bound, Theorem 3 of the paper. A companion mission of the same series covers the upper bound.
Lower bounds of this kind fix what is achievable. For the stationary -armed bandit, the minimax regret is of order (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020, Ch. 15). In the periodic model a learner effectively faces "effective arms" (arm at each phase of its cycle), which suggests the rate . The paper proves the weaker but general bound , which matches the upper bound up to a factor and logarithms.
There are arms and epochs . An instance is a family of mean rewards . If arm is pulled at epoch , the reward is drawn from the Gaussian law , independently of the past given the arm.
A sequence has minimum period if for all and no smaller positive integer has this property.
A policy chooses the arm at epoch at random, from a distribution that depends on the previous arms and rewards. Its expected regret on is display (1) of the paper:
Three classes of instances appear, all with unit-variance Gaussian rewards and means in (Assumption 1):
The proof compares instances through the metric (B-48),
The periods satisfy Assumption 3 with the parameters (7): with and , , and for every .
For every policy there is with
Theorem 3 shows that knowing the periods does not remove the cost of learning them phase by phase: the regret must grow like , not like . Together with the paper's upper bound and the inequality , it shows the two-stage policy is near-optimal when is fixed. The intermediate results are reusable: Lemma 12 is a clean two-point Gaussian lower bound, Lemma 13 is a phase-decomposition argument that applies to any bandit model with known cyclic structure, and facts 1 and 2 give a continuity framework for the regret as a function of the instance.
The result has a published proof. As far as the platform's records show, none of it has been machine-checked. The stationary minimax lower bound of Lattimore and Szepesvári (a different family and constant) exists on the platform, together with the Bretagnolle–Huber inequality, the Gaussian KL divergence and the divergence decomposition, which this mission lists as tools.
The two-point argument of Lemma 12 is standard, but its constant needs , so small horizons must be handled separately. Lemma 13 decomposes the problem into phase problems; making this rigorous means showing that a policy on the periodic problem induces, on each phase, a policy on a stationary problem of horizon , with a history law that factorizes accordingly. The phase-wise instances produced by the decomposition need not have minimum period exactly (all phases may coincide), so a perturbation is needed to land in ; the constant has slack for it. Fact 2 asks for continuity of an integral against the law of a -round adaptive process, uniformly over all policies, which needs a domination argument that does not depend on the policy's kernels.
Fin K, 0-based: the paper's first arm is index . Epochs are 1-based natural numbers; history coordinate is epoch . Values of the means at are ignored.BanditAlgorithm.BanditPolicy K: one Markov kernel per round from the history to the next arm. The history law periodicMeasure reuses the platform's step kernel with the Gaussian bandit of the current epoch's means; with constant means it is BanditAlgorithm.banditMeasure of BanditAlgorithm.gaussianBandit. Lemma 12 is stated with the platform's banditRegret, , which equals (1) for Gaussian arms; the other statements use (1) directly.Welcome contributions: the bridge between periodicMeasure with constant means and banditMeasure, the phase decomposition of the history law, and the uniform continuity of the regret in the means.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
The value
is the headline conditional witness of S. Jain's integer-mult-kappa, round eight, at revision 5868dc7. It is bound by the complex side ().
The repository states that the claim is conditional: it assumes the full upstream multiplication theorem (the OpenAI manuscript and Colkitt's framework) and that stage two is the complement time-reversal of stage one, and it rests on three further interfaces that are stated but not machine-checked there — IceKylin's normal form for alternating residuals, the cost of binary address adapters for the exterior fix-up children, and the row stock of the stopped bit interchange. Its Lean files check only finite rational statements (moment certificates, the stopped mix and the parameter assembly), not the analytic inequalities or the multiplication theorem. It has not had independent review.
Earlier claims appear as milestones: Harvey–van der Hoeven (), OpenAI Theorem 1 (), Colkitt's checkpoint, Jain rounds six and seven, and community PR #62. Each is implied by this goal because decreases in .
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
The value
is the conditional witness of S. Jain's integer-mult-kappa, round seven, at revision c05adfe, with the sharper moment certificate merged there (research/round7-moment-refinement/). The README's headline for the same construction is the slightly smaller ; the refinement keeps the frozen round-seven bit network, histogram, complex saving and assembly unchanged, and replaces the reciprocal bound in the moment certificate by a degree-eight Taylor enclosure, which certifies the bit saving .
The construction builds on the OpenAI manuscript and on Colkitt's integer-mult-bounds (it uses the PR #62 producer with interval strips and core-aware pair assembly). Its new ingredients are lifted frames with late copies, deferred readouts, and per-use leaves on the bit side; the complex side is round six's. The repository states that the claim is conditional on the OpenAI manuscript and Colkitt's framework, that stage two (the complement time-reversal of stage one) is assumed rather than machine-checked, and that its Lean files check only finite rational statements (moment certificates and parameter assembly), not the analytic tail inequalities or the multiplication theorem. It has not had independent review.
Earlier claims appear as milestones: Harvey–van der Hoeven (), OpenAI Theorem 1 (), Colkitt's checkpoint, Jain round six () and community PR #62 (). Each is implied by this goal because decreases in .
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
Lower bounds on the regret of stochastic multi-armed bandit strategies say how often any reasonable strategy must sample an arm that is not the best one. They are the benchmark against which upper bounds for UCB, KL-UCB and Thompson sampling are judged optimal. The classical bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) were proved by changes of measure on carefully chosen events, combined with Markov–Chernoff estimates of their probabilities.
Garivier, Ménard and Stoltz (arXiv:1602.07182v3), published in Mathematics of Operations Research in 2019, replace those arguments with one inequality, which they call the fundamental inequality of their article, inequality (6), p. 6. Every lower bound in the paper follows from it: the asymptotic Lai–Robbins / Burnetas–Katehakis bound for an arbitrary model (Theorem 1), the non-asymptotic bounds for small horizons (Theorems 2–4), and the non-asymptotic logarithmic bound for large horizons (Theorem 5). The same inequality, in the form of Lemma 1 of Kaufmann, Cappé and Garivier (2016), underlies lower bounds for best-arm identification. This mission formalizes the inequality and the lemma that carries its proof.
A bandit problem with arms is a family of probability distributions on , each with a finite expectation. A strategy plays for rounds. In round it picks an arm as a measurable function of , where the are independent uniforms on . It then observes a reward drawn from and a fresh independent uniform . The strategy together with the problem determines the law of ; is its expectation. The number of draws of arm is
is the Kullback–Leibler divergence between two probability measures: when is absolutely continuous with respect to and the integral exists, and otherwise. The binary divergence , for , is the Kullback–Leibler divergence between the Bernoulli distributions of parameters and . For it is given by (5):
It equals for and .
The Lean development builds on the published StochasticBandit K, which holds the arm laws ν.P a. The local FullStrategy K implements the paper's measurable strategy on ; fullHistoryMeasure ν ψ T is the law of , fullPullCount ψ a is , and fullExpPulls ν ψ T a is its expectation. The published BanditPolicy K describes the observed-history kernel model used by the two referenced chain-rule results. The shared definitions supply the Bernoulli law and klBer p q for .
For every strategy , every pair of bandit problems , every horizon , and every -measurable statistic with values in :
in , with . The arm laws have the finite expectations required in §1.1; their divergences may be infinite.
The result. Inequality (6) turns a lower bound on the number of draws into a choice of an alternative problem and a statistic , usually . The binary divergence then contains expected numbers of draws directly, and no event or concentration estimate is needed. In the paper this gives a few-line proof of the Lai–Robbins / Burnetas–Katehakis bound for any model. It also gives the non-asymptotic bounds showing that the regret grows almost linearly while is below a divergence-determined threshold. Each of these is a separate mission of this series, and each applies (6) once.
The formalization. The paper calls the equality in (8) standard and re-proves it for completeness; the inequality half, Lemma 1, is its own contribution. Observed-history kernel versions of the equality in (8) and the one-round step (9) are already formalized on the platform, under the hypothesis that every arm divergence is finite. Lemma 1 and the full-information inequality (6) itself are proved in the paper but not formalized. A machine-checked (6), stated with no divergence-finiteness hypothesis, would make every downstream lower bound in the series a matter of calculus with the binary divergence.
Two points need care. First, Lemma 1 is stated for an arbitrary -valued . The data-processing inequality only gives it directly for indicators of events, and pushing forward by gives a law on , not a Bernoulli law. The paper's route enlarges the space by an independent uniform variable, which needs the product with Lebesgue measure, the invariance of the divergence under that product, and Tonelli's theorem. Second, the goal has no finiteness hypothesis on the arm divergences, while the published chain-rule results assume it. When for an arm that is drawn with positive probability, the left side is and there is nothing to prove. When such an arm is never drawn, its term is . The divergence between the history laws must then be shown to be finite and equal to the remaining sum, which the published decomposition does not cover.
Fin K, indexed from . The horizon is a natural number; at both sides are . For no policy exists, so needs no hypothesis.FullStrategy K, measurable functions of the paper's . The same strategy runs under and . The local history law includes every auxiliary uniform, so may depend on any of them.Integrable id for each arm, expressing §1.1's finite-expectation condition. The published StochasticBandit structure supplies only the probability-law condition.klBer, never a real formula. A real formula would return a finite junk value at , where (5) is , and would make the goal trivially true there. A version with a finiteness hypothesis on the arm divergences, or with a real-valued binary divergence restricted to , would be a weaker theorem and is not the target.unitInterval. is real-valued and measurable, with values in .StochasticBandit and BanditPolicy and on Mathlib's InformationTheory.klDiv. The goal uses a local explicit auxiliary-uniform strategy; the published chain-rule references use observed-history kernel policies and are related proof tools. Other tools are data processing (klDiv_map_le), the chain rule for klDiv and composition products, and Tonelli. The tensorization identity for products of probability measures is Proved on the platform as Tensorization.klDiv_prod_eq_add. Lemma 1 is reusable well beyond bandits, wherever a divergence must be compared with the means of a bounded statistic. Proofs of the milestones, and an extension of the chain rule to infinite arm divergences, are welcome.When many independent users share a network, each routes its own traffic to minimize its own delay, and nobody optimizes the system as a whole. Koutsoupias and Papadimitriou asked how much this lack of coordination can cost: how far the social cost of a Nash equilibrium can be from the social optimum, in the worst case. Their paper Worst-case equilibria (STACS 1999; journal version 2009, doi:10.1016/j.cosrev.2009.04.003) introduced this ratio, later named the price of anarchy, and studied it on the simplest network: parallel links between one source and one destination. The ratio has since become a standard measure of the inefficiency of equilibria in routing, scheduling and auctions (see Chapters 17–20 of Nisan, Roughgarden, Tardos and Vazirani, Algorithmic Game Theory, 2007).
Most of the paper concerns links of equal capacity. Its last result, Theorem 4, turns to two links of different speeds and shows that unequal speeds make equilibria worse: the worst-case ratio rises from for two identical links to the golden ratio .
Timeline. 1999: Koutsoupias and Papadimitriou define the coordination ratio; for two identical links they prove it is exactly , and for two links with speeds they give the golden-ratio lower bound of Theorem 4. 2002–2003: Mavronicolas and Spirakis, Koutsoupias, Mavronicolas and Spirakis, and Czumaj and Vöcking determine the asymptotic order of the price of anarchy for identical and for related links (Czumaj–Vöcking, ACM TALG 2007).
There are agents and parallel links. Agent has an amount of traffic , and link has a speed . A pure profile sends each agent's whole traffic over one link . The load of link is , and an agent on link experiences the delay .
A mixed strategy of agent is a probability distribution over the links; the agents randomize independently. The expected cost of agent is its expected delay. A profile is a Nash equilibrium if no agent can lower its expected cost by changing its own distribution. The expected traffic on link is , and the cost to agent of placing its traffic on link is
The social cost of is the expected makespan, the expected maximum delay over the links,
and is the optimal makespan over pure assignments. The price of anarchy is the largest ratio over instances and equilibria.
For two links with speeds , there is an instance with positive traffic and a Nash equilibrium with and
moreover on this range, and when .
The result. Theorem 4 shows that the price of anarchy of parallel links depends on the heterogeneity of the links, not only on their number: two identical links have price of anarchy (Theorems 1 and 3 of the paper), while two links of different speeds already reach . The setting is that of related (uniformly related) machines, the model in which Czumaj and Vöcking later proved the asymptotic order of the price of anarchy for links.
Formalizing it. The result is proved on paper; this mission produces a machine-checked proof. Beyond the theorem, it yields reusable statements about mixed equilibria of load-balancing games on the published agt_games vocabulary: the closed form (8) of a pure deviation's expected cost and the support characterization of equilibria, both stated for any number of agents and links. A search of the Prove2Me catalog (October 2026) found no formalization of any part of this result.
The arithmetic of the instance is elementary, so the work lies in connecting the paper's computations to the definitions. The paper's notion of equilibrium quantifies over all mixed deviations, and its expected costs are sums over all pure profiles; the proof reasons instead with the per-link costs of (8) and the indifference of each agent between the links it uses. Turning that into a proof requires showing that an agent's expected cost is the -weighted average of the (linearity over independent randomization) and that the average over outcomes reduces to the paper's four-term formula. A naive approach that checks only pure deviations does not give the equilibrium property directly; one must pass from pure to mixed deviations. The restriction is not cosmetic: beyond it the second agent's probability is negative.
The game is defined in WorstCaseEq.Speeds.Model on top of the published agt_games definitions (AGT.IsMixedNash, AGT.expectedPayoff, AGT.profileProb). These maximize payoffs, so an agent's payoff is minus its delay. Agents and links are Fin n and Fin m, indexed from , so the paper's links 1, 2 and agents 1, 2 are 0, 1. A mixed profile is a real matrix p i j; being a family of probability distributions is part of the Nash condition. Makespan, social cost and opt require at least one link (NeZero m).
The paper does not print the social cost for links with speeds; the computation in the proof of Theorem 4 uses the expected maximum of load divided by speed, and that is the definition. It is not the maximum of the expected loads, a smaller quantity. The page numbers cited are PDF page indices of the journal version (dated April 29, 2009), which prints no page numbers after page 1.
"The price of anarchy is at least " is formalized as the existence of an instance and an equilibrium whose social cost equals times a positive optimum. A quotient is avoided because it takes the junk value when , and the requirement rules out degenerate witnesses with no traffic. The ratio conditions and are written and (equivalent since ), and is Mathlib's Real.goldenRatio.
Contributions welcome: proofs of any milestone. Milestones 1 and 2 are general facts about mixed equilibria of weighted load-balancing games and are reusable beyond this mission.
Primal–dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal–dual pairs. Two families dominate the theory. Path-following methods keep the iterates in a neighbourhood of the path and measure progress by the duality gap. Potential-reduction methods measure progress by a merit function, the primal–dual potential of Todd and Ye (Todd–Ye 1990), and choose the step to decrease it.
The potential carries a parameter . The classical analyses (Ye 1991, Freund, Anstreicher–Bosch, Kojima–Mizuno–Yoshise) give iterations with . Practical codes, however, performed better with much larger (McShane–Monma–Shanno, Lustig–Marsten–Shanno). Mizuno, Todd and Ye (Cornell ORIE Technical Report No. 944, 1990, rev. 1991; journal version Math. Oper. Res. 18(4), 1993, doi:10.1287/moor.18.4.964) supply a worst-case justification for a large parameter. With and the step chosen to minimise the potential inside the wide neighbourhood , the method needs iterations. That matches the adaptive-step path-following method in the same neighbourhood (their Theorem 2).
Timeline:
Fix , , , , . The primal problem is subject to , . The dual is subject to , . The strictly feasible set is the set of pairs with , , and for some . The duality measure is .
For put and . For , the wide neighbourhood is
i.e. for all , where and is the all-ones vector.
The potential is
with the natural logarithm. At and for , a search direction solves
and the iterates move along , . The scaled vectors are and , , and .
Algorithm 3. Start from with and . While , compute at , choose with and for every with , and move to .
Let with and
For every and every run of Algorithm 3,
The paper states " iterations". The explicit count is the one its own proof yields, and it is stated so that the goal is not an existential over a constant.
The result shows that a potential-reduction method with of order keeps a polynomial worst-case bound. The earlier analyses cited by the report used of order . It thereby gives a worst-case justification for the large parameters that worked in practice. It also connects the two families: the direction is the path-following direction, and only the step rule changes. Corollary 3 of the paper adds that iterations with a small second-order term decrease the potential far more.
The result is proved in the report. As far as the platform's index shows, no part of it has been machine-checked. The platform already holds the potential function (Bertsimas–Tsitsiklis §9.3) and a proved bookkeeping theorem converting a constant per-iteration decrease into an iteration count (Bertsimas–Tsitsiklis Theorem 9.4). This mission adds the analysis of a concrete algorithm: the admissibility of the step in , the potential decrease (16), and the complexity bound.
The step is defined by minimisation, not by an explicit formula, so its decrease must be bounded by comparison with a step whose effect can be computed. That reference step must be shown to stay in the neighbourhood. This requires controlling the second-order term of the Newton direction in the one-sided norm , together with the centrality of the current iterate. A fixed decrease of order arises only because is of order . Below that scale, the duality-gap term of the potential no longer dominates the loss in centrality from a long step.
A second obstacle is specific to formal work. Algorithm 3's rule ranges over every real whose point lies in the neighbourhood, and a minimiser need not exist. The goal must hold for every run, including the degenerate ones.
Vectors are Fin n → ℝ, with index mapped to Fin n; is Mathlib's sup norm. The general standard-form LP pair is a separate definition, and the neighbourhood and algorithm build on its strict feasibility predicate. is the published definition LinearOptimization.interiorPointPotential with . It equals (1) at every strictly positive pair, and it is evaluated only at points of . All logarithms are natural, and are real powers with real . A run is a pair of sequences satisfying the start conditions and, whenever the current gap exceeds , the step relation of Algorithm 3. Iterates after termination are unconstrained.
Conventions and repairs:
A formalization in which no run can exist for any instance, or in which or the iteration count absorbs an instance-dependent constant, would trivialize the goal. The step relation above is satisfiable for whenever the potential attains its minimum along the line, and the count is the explicit expression above.
Needed infrastructure: the algebra of system (2), namely , the identity , and . Also needed are the bounds and on when , and the arithmetic–geometric mean inequality for . These facts are shared with the sibling missions on the predictor–corrector and wide-neighbourhood algorithms of the same paper, and lemmas proved here are welcome there. The proved Bertsimas–Tsitsiklis theorem LinearOptimization.interior_point_potential_reduction is included as a reference item for the final counting step. Its hypotheses quantify over all iterations and need explicit dual iterates, so it does not apply verbatim.
The multiarmed bandit problem asks how to allocate a single resource, one play per period, among several alternative projects whose states evolve only while they are worked on. It models the scheduling of jobs on one machine, the sequencing of research projects, and the design of sequential clinical trials. Gittins and Jones (1974) showed that the problem with discounted rewards is solved by an index policy: compute for every project a number depending only on that project's current state, and always work on a project of greatest index. Weber's paper (Ann. Appl. Probab. 2 (1992)) gives a short proof of this theorem through fair and prevailing charges, and uses the same accounting to derive bounds on how much any other policy loses.
In practice the optimal policy is often not the one used: indices may be expensive to compute, or a simpler heuristic may be preferred. A bound on the loss of an arbitrary policy, computable along that policy's own trajectory, tells a practitioner how far from optimal the chosen heuristic is. This mission formalizes the first such bound of the paper, Theorem 2, which Weber attributes to Glazebrook (1990).
Timeline. Gittins and Jones (1974) and Gittins (1979) proved optimality of the index policy by an interchange argument. Whittle (1980) gave a proof through a retirement option. Glazebrook (1982) bounded the suboptimality of a policy in terms of Gittins indices only; Glazebrook (1990) gave the sharper bound stated here as Theorem 2. Weber (1992) rederived it from the prevailing-charge accounting and added the index-gap bound (Theorem 3) and the submodularity of the optimal value (Theorem 4).
There are bandits. Bandit has a state at each epoch . At each epoch the gambler plays one bandit , receives the reward , and the state of bandit moves according to a Markov kernel ; the states of all other bandits stay unchanged. Rewards are nonnegative and uniformly bounded, and future rewards are discounted by a factor with . A policy chooses , possibly at random, as a function of everything observed so far. Its value from the initial states is
The fair charge of a state is the per-play charge at which a gambler holding a single bandit in state , free to stop at any time, would only just break even. Equivalently it is the largest ratio of expected discounted reward to expected discounted time over stopping times . Weber's Gittins index is . The prevailing charge of bandit at time is the least fair charge seen so far on that bandit, . A Gittins policy plays at each epoch a bandit of greatest index; Theorem 1 of the paper says it is optimal.
For a Gittins policy , every policy and every initial state vector ,
The result. Inequality (6) bounds the loss of an arbitrary policy by a quantity observed along that policy's own trajectory: at each epoch, how far the reward collected falls below the greatest prevailing charge. A policy that plays a bandit of greatest prevailing charge whenever possible and collects its charge as reward loses nothing, which recovers Theorem 1. The bound is the basis of Glazebrook's analysis of near-optimal heuristics for bandit and stochastic-scheduling problems, and of the index-gap bound (7) of Theorem 3, which is the second mission of this series.
Formalizing it. Theorem 1 of the paper (optimality of the Gittins policy) is already formalized and proved on Prove2Me as BanditAlgorithm.gittins_index_theorem (Shuze Chen, following Lattimore and Szepesvári, Theorem 35.9), together with the finite-horizon prevailing-charge accounting and the charge-stack interleaving lemmas (Harry_Xu). Theorem 2 itself has no machine-checked proof. This mission produces the infinite-horizon forms of the charge accounting, (5) and its equality case for the Gittins policy, and the realisation-wise comparison of greatest prevailing charges, and combines them into (6). Missions 2 (Theorem 3, the index-gap bound) and 3 (Theorem 4, submodularity of the optimal value) of this series state the paper's other results on the same model; none of the three relies on the others.
The paper's proof is one sentence: combine (5) with the realisation-wise observation. The two pieces live on different probability spaces. Inequality (5) and the equality for the Gittins policy are expectations under the law of each policy's own history, while the comparison of greatest prevailing charges is made on a fixed realisation of each bandit's state sequence. Transferring the deterministic comparison into an inequality between expectations under two different policies needs a coupling under which every policy sees the same per-bandit state sequences, so that the prevailing-charge stacks are the same random objects under and . The naive approach, comparing the two laws round by round, fails: the round- histories of and have different distributions, and no pointwise inequality holds between them. The infinite-horizon statements also require controlling the terminal retirement potential, which vanishes only in the discounted limit.
The development uses the published BanditAlgorithm model (GittinsIndex, GittinsTerminalPotential, GittinsPrevailingChargeValue, GittinsChargeInterleaving). Conventions committed to:
gittinsIndex (the ratio (4)); is a new definition weberIndex. The goal uses and the factor , as in (6); milestones 1 and 3 use , as the paper does.IsGittinsIndexPolicy (with probability one it plays an arm of greatest index, ties arbitrary). The goal does not assume such a policy exists; a one-armed instance shows the hypotheses can be met.Replacing by in (6) would weaken the bound by the factor , and dropping the boundedness of rewards would let the published value be a junk ; neither is the paper's statement, and both are ruled out by the conventions above.
Contributions welcome: the infinite-horizon limits of the published finite accounting, a coupling of all policies on independent per-bandit state sequences, and the deterministic comparison of greatest exposed charges, which is reusable for any interleaving argument on nonincreasing sequences.
The multi-armed bandit problem asks how to share effort sequentially among several independent projects, each of which evolves only while it is worked on. It models the scheduling of jobs on a single machine, the order in which to explore candidate sites, sequential clinical trials and the allocation of research effort among competing projects. Before 1972 the problem had no general solution: dynamic programming over the joint state of all projects is intractable as soon as there are more than a few of them.
J. C. Gittins and D. M. Jones (1974) announced, and Gittins (1979) set out in full, a solution of a striking form: each project can be assigned a number depending only on its own current state, its dynamic allocation index (DAI, now the Gittins index), and it is optimal to work on a project whose index is largest.
Timeline. Gittins and Jones presented the index result at the European Meeting of Statisticians in 1972 (proceedings 1974). Gittins (1979) gave the general discrete-time formulation, stated the Forwards Induction Theorem and the DAI Theorem without proof, and proved the attainment Lemma of its Section 4. Whittle (1980) gave a dynamic-programming proof through the retirement formulation, Weber (1992) the prevailing-charge interchange argument, and Tsitsiklis (1994) a short inductive proof. Gittins, Glazebrook and Weber (2011) is the standard monograph; Lattimore and Szepesvári (2020, Chapter 35) give a measure-theoretic treatment on general state spaces.
A bandit process is a Markov chain on a measurable state space with transition kernel . Applying the continuation control at process time earns the discounted reward , with , and moves the chain one step; the freezing control leaves the state unchanged and earns nothing. For a stopping time of the chain (possibly infinite) write
The dynamic allocation index of in state is the largest reward per unit of discounted time obtainable by continuing for at least one step:
A simple family of alternative bandit processes consists of bandit processes. At each stage a policy chooses exactly one of them to continue, possibly at random and as a function of the whole past; the others are frozen. A policy is optimal if it attains the supremum of the total expected discounted reward over all policies.
The Lean development uses the published objects markovChainMeasure P x (the chain law), IsPositiveStoppingTime, stoppedRatio P r α τ x (), gittinsIndex P r α x (), MarkovBanditPolicy k S, markovBanditMeasure P π x n (the law of the first stages) and markovBanditDiscountedValue P r α π x (the total expected discounted reward), with written α and written r.
For every policy and initial state vector ,
BanditAlgorithm.gittins_index_theorem, already Proved.The result. The DAI Theorem replaces a dynamic program on the product of state spaces by one-dimensional optimal stopping problems. The "only if" half says more than that the index rule is one optimal policy: it characterizes every optimal policy, so any rule that departs from the index on a set of positive probability loses reward. The Lemma identifies the stopping rule that attains the index, which is how indices are computed in practice, and Corollary 1 is the finite-horizon version on which the paper's numerical algorithm (Section 7) rests.
Formalizing it. The sufficiency half is formalized: BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári Theorem 35.9) is Proved on the platform, together with gittins_index_policy_dominates, gittins_stopping_ratio_le_index and gittins_epsilon_optimal_stopping. The attainment Lemma is Proved only for countable state spaces with bounded rewards (AllocationIndices.optimal_stopping_set, Gittins–Glazebrook–Weber Lemma 2.2), and the necessity half is on no platform item. This mission asks for the Lemma on general standard Borel state spaces with integrable rewards, the finite-horizon Corollary 1, and the full equivalence. The Forwards Induction Theorem of p. 153, which needs superprocesses and forwards induction policies, is outside its scope.
The "only if" direction is the new content, and it does not follow from the sufficiency theorem: knowing that one index policy is optimal says nothing about a policy that sometimes plays a lower-index process. The deviation must be shown to cost a strictly positive amount whenever it happens with positive probability, which requires a strict comparison that survives discounting, ties in the index and infinite stopping times. A second obstacle is measure-theoretic. On a general state space the index is a supremum over uncountably many stopping times, its measurability is not available, and the Lemma's stopping rule is a stopping time only if is measurable; the arguments of the countable case, which treat each state separately, do not transfer.
All objects are the published discounted -armed Markov bandit of Def_GittinsIndex and the stopping-time quantities of Def_AllocationIndices_Index; time is indexed from , stopping times are -valued and adapted to the coordinate filtration, and the index is the real supremum over stopping times . The explicit readings committed to are:
A trivializing formalization is ruled out: the goal is not stated for index policies on every history (which would only restate the referenced theorem), the index is the published supremum over stopping times rather than a one-step reward or a finite-horizon quantity, competitors are not restricted to Markov or deterministic policies, and the Lemma's stopping rule starts at time , so it never stops at once. A one-point state space satisfies all hypotheses together and admits a policy.
Useful infrastructure, reusable beyond this mission: measurability of the Gittins index on standard Borel spaces, a measurable selection of a maximal-index arm, and an interchange argument for -armed Markov bandits on general state spaces. Proofs of any milestone, and of either half of the goal, are welcome.