Get started

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

Discover

Find your next mission.

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

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Integer Multiplication Below n log n

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

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

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

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

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

NoneFormalized record≥ 0.00003666565558019Open frontier

3 provers on it0 of 4 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

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

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

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

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

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

9 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

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

References:

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

≤ 70Formalized record

3 provers on it8 of 8 missions formalized

Odd numbers as sums of primes

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

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

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

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

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

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

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

Discover

Find your next mission.

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

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

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

Discover

Find your next mission.

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

Campaigns (experimental)

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.

Integer Multiplication Below n log n

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

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

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

NoneFormalized record≥ 0.00003666565558019Open frontier

3 provers on it0 of 4 missions formalized

3SUM Exponent

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

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

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

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

9 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

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

References:

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

≤ 70Formalized record

3 provers on it8 of 8 missions formalized

Odd numbers as sums of primes

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

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Group Theory·Captain: dbenbenn

Cannon–Floyd–Parry: Thurston's piecewise integral projective models of F and TTextbook

This mission formalizes §7 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: W. Thurston's interpretations of Thompson's groups $F$ and $T$ as groups of piecewise integral projective homeomorphisms of the interval and the circle.

Motivation

The notes describe their last section as follows: "In §7 we give W. Thurston's interpretations of $F$ and $T$ in terms of piecewise integral projective homeomorphisms" (p. 216). Elements of $F$ and $T$ are piecewise linear, with dyadic breakpoints and slopes powers of $2$ . Thurston's models replace the linear pieces by linear fractional maps $t \mapsto (at + b)/(ct + d)$ with integer matrices of determinant $\pm 1$ , and the dyadic intervals by the intervals of the Farey tree. The two descriptions give isomorphic groups because both are read off the same tree diagrams.

Earlier missions on this platform formalize $F$ (§1 and §4), its tree diagrams (§2), its presentations (§3) and the group $T$ (§5); this one states their projective models.

Setting

The simplex. $\Delta_n$ (Simplex n) is the standard $n$ -simplex in $\mathbb{R}^{n+1}$ , and $\rho(x) = x / \sum_i |x_i|$ (rho). A map on $U \subseteq \Delta_n$ is integral projective (IsIntegralProjective) when it is $\rho \circ A$ for some $A \in GL(n+1, \mathbb{Z})$ with $A(U)$ in the nonnegative orthant (p. 249). Subdivisions of $\Delta_n$ are Mathlib's geometric simplicial complexes (Geometry.SimplicialComplex), finite and with underlying space $\Delta_n$ ; a subdivision is rational or integral when each $n$ -simplex has rational vertices, or is the image of $\Delta_n$ under an integral projective map. lift and ind are the primitive integer lift of a rational point and the index of a rational simplex (p. 250).

PIP maps. $PIP(\Delta_n)$ (PIPSet n) is the set of homeomorphisms of $\Delta_n$ that are integral projective on each simplex of some integral subdivision. $PIP^+(\Delta_n)$ (PIPPlusSet n) consists of the orientation-preserving ones; in Lean orientation is read off the pieces, which are required to be $\rho \circ A$ with $\det A = 1$ .

The interval and the circle. On p. 251 the notes move $\Delta_1$ to $\Delta_1' = \{(t, 1)\}$ and identify it with $[0,1]$ . There a map is integral projective (IsIntegralProjective01) when it is $t \mapsto x/y$ with $(x, y) = A(t, 1)$ , $A \in GL(2, \mathbb{Z})$ and $0 \le x \le y$ . An interval $[a/b, c/d]$ is recorded by four natural numbers (FracInterval), with left part $[a/b, (a+c)/(b+d)]$ and right part $[(a+c)/(b+d), c/d]$ , and fareyNode follows a path of left and right steps from $[0,1]$ down the tree $\mathcal{T}'$ of integral subsimplices. $PIP^+$ of $[0,1]$ (PIPPlus01Set) consists of the order isomorphisms of $[0,1]$ that are integral projective on each interval of an integral partition, and RepresentsPIP reads a §2 tree diagram on $\mathcal{T}'$ instead of on the dyadic tree. $PIP^+(S^1)$ (PIPPlusCircleSet) consists of the permutations of UnitAddCircle with an order-preserving lift to $\mathbb{R}$ commuting with $x \mapsto x + 1$ that is integral projective, up to an integer, on each interval of an integral partition of $[0,1]$ , the way the published $T$ is defined through lifts.

Target

The goal is Theorem 7.3 (p. 254),

T \cong PIP^+(S^1),

together with the sentence that follows it, which names the three maps of $PIP^+(S^1)$ corresponding to $T$ 's generators $A$ , $B$ , $C$ : the goal asks for an isomorphism sending them to exactly those maps (pipA, pipB, pipC).

The milestones follow the section. For $\Delta_n$ : integral projective maps are homeomorphisms onto their images, $PIP(\Delta_n)$ is closed under inversion, two integral subdivisions have a common rational refinement (the notes cite Rourke and Sanderson), the index of a rational simplex, Theorem 7.1 (every rational subdivision refines to an integral one), $PIP(\Delta_n)$ is a group, and $PIP^+(\Delta_n)$ has index $2$ in it. For the interval: $PIP^+(\Delta_1)$ is isomorphic to its model on $[0,1]$ ; $[a/b, c/d]$ is an integral subsimplex exactly when $ad - bc = -1$ ; left and right parts are integral; $\mathcal{T}'$ is an ordered rooted binary tree; integral projective maps between integral subsimplices are unique and given by an explicit formula; they restrict to, and are glued from, maps of the left and right parts; reduced tree diagrams correspond bijectively to $PIP^+$ of $[0,1]$ ; and Theorem 7.2, $F \cong PIP^+(\Delta_1)$ .

Significance

The result. Thurston's description identifies $F$ and $T$ with groups of piecewise $PSL(2, \mathbb{Z})$ maps of the interval and the circle, the dyadic tree becoming the Farey tree. The same substitution carries each element of $F$ or $T$ to its projective model; the conjugating map is Minkowski's question mark function.

Formalizing it. Nothing on this platform or in Mathlib concerns piecewise projective groups, the Farey tree of intervals or Minkowski's function. The mission reuses the published $F$ , $T$ and the tree diagrams of §2.

Difficulty

Theorem 7.1 is the one argument in the section that is not about the interval: a descent on the index, starring a rational subdivision at a well-chosen rational point. Mathlib has geometric simplicial complexes but no subdivisions, starring or common refinements, so both Theorem 7.1 and the cited results of Rourke and Sanderson need that apparatus built. The interval half is elementary number theory of $2 \times 2$ integer matrices (the notes' proof of connectedness of $\mathcal{T}'$ is a Euclidean-algorithm descent), followed by the tree-diagram argument of §2 repeated on $\mathcal{T}'$ .

What is left out

The Farey-tree remark on p. 252 (replacing each vertex $[a/b, c/d]$ of $\mathcal{T}'$ by the mediant $(a+c)/(b+d)$ gives the Farey tree): a relabelling that no statement uses.
The remark after Theorem 7.2 that the proof of Theorem 7.2 also proves Theorem 7.3; Theorem 7.3 is stated directly.

Formalization scope

$PIP(\Delta_n)$ and $PIP^+(\Delta_n)$ are sets of homeomorphisms Simplex n ≃ₜ Simplex n. The milestones that they are groups assert a subgroup with exactly that carrier, and Theorem 7.2 asserts such a subgroup for $PIP^+(\Delta_1)$ together with an isomorphism from $F$ .
The index-2 milestone assumes $n \ge 1$ : for $n = 0$ , $\Delta_0$ is a point and $PIP^+(\Delta_0) = PIP(\Delta_0)$ .
The converse of p. 253 (two integral projective maps of the left and right parts glue to one) is stated for maps carrying endpoints to the corresponding endpoints, the orientation the section works with; maps swapping the endpoints of both parts do not glue.
Reused platform theorems, which solutions may import: the §2 tree-diagram theorems (every tree diagram represents an element of $F$ , every element has a unique reduced tree diagram, tree diagrams compose).

Selected references

J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, §7 pp. 249–254. doi:10.5169/seals-87877
C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Ergebnisse der Mathematik und ihrer Grenzgebiete 69, Springer, 1972. doi:10.1007/978-3-642-81735-9

25 thms1 active userReviewed

Discrete Geometry·Captain: Minghui

Kepler Conjecture — Flyspeck finite-container theoremResearch Paper

Packing equal balls in three dimensions

The Kepler conjecture asks how much of three-dimensional Euclidean space can be filled by congruent solid balls whose interiors do not overlap. It is a question about all arrangements, including irregular arrangements with no repeating cell. A lattice calculation can exhibit an efficient packing but cannot bound every packing. The result is a central extremal theorem of discrete geometry and a substantial example of a proof combining geometry with finite computation. Hales published a proof in 2005; the later Flyspeck project verified a revised proof in HOL Light and Isabelle. This mission concerns a Lean 4 formalization of that verified result. Its authority is Hales et al., A Formal Proof of the Kepler Conjecture (2017), especially sections 3–4.

Centers, separation, and finite containers

A unit-sphere packing is a set $V\subseteq\mathbb R^3$ of centers such that $\|u-v\|\ge2$ whenever $u,v\in V$ are distinct. The occupied region is the union of the open balls $B(v,1)$ . Tangency is allowed. The ambient metric is the Euclidean metric, represented by EuclideanSpace ℝ (Fin 3).

For a real radius $r$ , write $N_V(r)=\#(V\cap B(0,r))$ , where the observation ball is open. Uniform separation makes this intersection finite. The definition of a packing does not assume that the whole set is finite, periodic, saturated, or contains the origin. A saturated packing is one to which no further center can be added while preserving separation. Saturation occurs in an intermediate theorem; an extension theorem must remove it before the final conclusion. These conventions follow the formal source statement and the packing definitions in the accompanying repository.

Formalization targets

The source-faithful goal is

\forall V\text{ a unit-sphere packing},\quad \exists c\in\mathbb R,\quad\forall r\ge1,\qquad N_V(r)\le\frac{\pi r^3}{\sqrt{18}}+cr^2.

The constant may depend on the packing and must work for every indicated radius. This is the finite-container statement displayed in Hales et al., section 3, published PDF page 6. Its quadratic boundary term is part of the target.

Two additional statements record the conventional density consequence. Define the upper packing density by

\overline\delta(V)=\limsup_{r\to\infty} \frac{\operatorname{vol}((\bigcup_{v\in V}B(v,1))\cap B(0,r))} {\operatorname{vol}(B(0,r))}.

The optional targets are $\overline\delta(V)\le\pi/\sqrt{18}$ for every packing and $\sup_V\overline\delta(V)=\pi/\sqrt{18}$ . They are separate from the core theorem. The analytic count-to-volume bridge and the explicit face-centered cubic witness $\sqrt2\{z\in\mathbb Z^3:\sum_i z_i\equiv0\pmod2\}$ are stated independently. The density need not have an actual limit. This distinction also makes comparison with the current Lean-Eval statement precise.

What the formalization contributes

The finite-container theorem bounds every arrangement at every radius at least one, up to its stated boundary error. The density corollary identifies the optimal asymptotic occupied fraction once a close-packing witness is supplied. It makes no uniqueness assertion: an upper bound and an attaining example do not classify all optimizers. The normalizing unit-ball volume is $4\pi/3$ ; it cancels against the same factor in the observation-ball volume when comparing $N_V(r)/r^3$ to occupied density. The Blueprint, section 1.2, describes the close packings.

Flyspeck already provides a machine-checked proof in its original systems. The work here is to express and prove the same mathematics with Lean's kernel and Mathlib, and to develop reusable geometric, combinatorial, and certificate interfaces. Existing partial Lean 4 work is acknowledged; no priority claim is made. The proposal supplies statements and conditional assembly, not a completed Lean proof.

Why the interfaces matter

The revised proof does not reduce to optimizing a lattice cell. Its local configurations have varying combinatorial types, and the necessary nonlinear estimates and linear relaxations must apply to all their geometric realizations. The primary account, sections 4–9, distinguishes the geometric argument, nonlinear inequalities, tame-graph classification, and linear-program verification. The public milestones preserve these distinctions and use the revised annulus estimate, rather than importing the original decomposition-star architecture unchanged.

Formalization scope and verification

Seven milestones cover packing foundations; the fixed nonlinear catalog; the global geometric reduction; extraction and tameness of a local counterexample; archive classification; exhaustive geometric LP certificates; and the local annulus bound. The last states that every finite packing in $2\le\|v\|\le2.52$ satisfies $\sum_v(2.52-\|v\|)/0.52\le12$ . This is section 4.2, equation (1). A compiled conditional theorem composes these interfaces into the exact final goal.

The nonlinear catalog contains actual real formulas from the six selectors in the pinned final Flyspeck statement: 580 family occurrences indexing 539 distinct source-ID records. These 539 source IDs have 498 distinct normalized syntactic bodies; repeated formulas are retained, and no claim of semantic inequivalence is made. All 539 domains have separately kernel-checked witnesses; this does not prove the inequalities. The graph archive is fixed independently of tameness. The reported 18,762 matches the AFP 2013-12-11 archive: 9 triangular, 1,105 quadrilateral, 15,991 pentagonal and 1,657 hexagonal cases. The AFP entry records a change of tameness constants and archive on 3 July 2014. The final archive has 19,715 rows: 9 + 1,253 + 16,080 + 2,373; the pinned make_archive.hl explicitly records this July-2014 count. Exact permutation comparison shows all 18,762 older classes retained and 953 added, with no duplicate or mirror-equivalent rows within either archive. The mission uses the final accompanying archive, whose source SHA-256 is 703ea865a124aa69f0ee12d94df7065bbbf5701a3085776e24632d14493474db. These are candidate graphs: the classification is coverage, not a claim that every stored row is tame or geometrically realizable (primary §7.2).

The final LP family is pinned to the completed Flyspeck revision 1ce0353008eba83d3c76ae9a25c3c242e4802d53: 19,715 graph-indexed trees and exactly 43,078 leaves from all 39 final binary containers. Every branch, face refinement, rounded row template and selected row index is concrete Lean data. The 42,889 objective-bound leaves include the source score-lower-bound row; 189 leaves are direct infeasibility cases. M6 requires complete decoding, local feasibility at the fixed geometric evaluator, and a checked rational certificate for every structural leaf, including unreachable leaves. Solvers cannot replace the source family by a freely chosen LP. See the completed source verifier and primary §9.

The fixed LP selector table is split into forty consecutive data definition files. The archive and graph case trees each occupy two data files, with separate reusable interfaces. Every definition file is below 900,000 UTF-8 bytes, within the platform's observed 1,048,576-byte scanner limit. Ordered concatenation preserves all 19,715 archive records, 19,715 graph trees and 43,078 LP leaves; this packaging adds no mathematical assumption or milestone.

External search may generate data. Coverage, real-expression bounds, exhaustive branching, and rational infeasibility must be justified by Lean theorems. Interval/Taylor certificates have separate encoding, acceptance, and soundness obligations; exact rational LP soundness and the conditional assembly are already checked infrastructure. Floating-point optimization, source hashes, and unchecked native computation are not proofs. All statements target Lean 4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f.

Selected references

Hales et al., A Formal Proof of the Kepler Conjecture, Forum of Mathematics, Pi 5 (2017), e2. DOI, arXiv.
Hales, Dense Sphere Packings: A Blueprint for Formal Proofs, Cambridge University Press (2012). Author's extended version.
Hales, A Proof of the Kepler Conjecture, Annals of Mathematics 162 (2005). Paper.
Bauer and Nipkow, Flyspeck I: Tame Graphs. Archive of Formal Proofs.
Solovyev and Hales, Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations (2013). Paper.
Solovyev and Hales, Efficient Formal Verification of Bounds of Linear Programs. Paper, sections 2–3.

73 thms1 active userReviewed

Combinatorics Graph Theory·Captain: Minghui

Formalize the Four Color Theorem in Lean 4Research Paper

Why formalize the Four Color Theorem in Lean 4?

The Four Color Theorem links a short mathematical statement to a large collection of finite checks. For contributors to graph theory and proof assistants, it is a concrete test of whether abstract mathematics, executable verification, and a public theorem statement can share one auditable foundation. The proposed result is a complete Lean 4 formalization, reusing Mathlib and adapting the established proof architecture to Lean.

The mathematical result is established. Robertson, Sanders, Seymour, and Thomas gave a modern computer-assisted proof in 1997. Gonthier subsequently developed a Coq formalization covering both mathematical reasoning and computation, described in his 2005 report and 2008 Notices article. This mission is classified as ResearchPaper because it formalizes these published results. (RSST, Gonthier 2005, Gonthier 2008)

Graphs, drawings, and colors

The root Lean interface uses Mathlib's SimpleGraph: a finite vertex set with a symmetric, irreflexive adjacency relation. Edges in this representation carry no additional identities or multiplicities. The conventional statement also permits parallel edges. Already-proved local infrastructure uses Mathlib's Graph V E to erase parallel edges while preserving a genuine plane drawing and proper vertex colorings; only the actual vertex set must be finite. A proper vertex coloring assigns a color to every vertex and assigns different colors to adjacent vertices. Four available colors means at most four colors are used; there is no requirement that each color occur.

A planar drawing places distinct vertices at distinct points of the real plane and represents each edge by an injective continuous arc joining its endpoints. An arc contains no other vertex, and arcs of different undirected edges meet only at shared endpoints. Reversing the orientation of an edge reverses its parameterization. A graph is planar when such a drawing exists. This is a geometric condition independent of coloring and of the eventual configuration checkers. Gonthier discusses the graph-embedding formulation in Section 2, PDF p. 4 of the 2005 report.

Write $V$ for the vertex set, $G$ for its adjacency relation, and $C=\{0,1,2,3\}$ for the available colors. Empty graphs, isolated vertices, and disconnected graphs are included. The drawing is a witness to a hypothesis; the theorem does not impose coordinates, a prescribed embedding, or a straight-line representation.

Formalization target

For every finite loopless planar graph, establish

\forall\,G=(V,E),\qquad \operatorname{Planar}(G)\Longrightarrow \exists c:V\to C,\quad \forall v,w\in V,\ \{v,w\}\in E\Longrightarrow c(v)\ne c(w).

The draft Lean target is FourColor.four_color: for every finite vertex type and every SimpleGraph on that type, FourColor.IsPlanar G implies G.Colorable 4. Its graph formulation follows RSST's Section 1, PDF p. 2 of the author-hosted manuscript. The manuscript's PDF page numbers differ from the journal's pagination.

The exact unchanged root signature is:

FourColor.four_color.{u} :
  ∀ (V : Type u) [Finite V] (G : SimpleGraph V),
    FourColor.IsPlanar G → G.Colorable 4

This is an open target signature, not a completed proof. The existing FourColor.FinalAudit.multigraph_four_color_of_necessary_targets conditionally connects the mission obligations to the conventional finite loopless planar multigraph statement. Its drawing has distinct vertex positions and injective continuous arcs for each edge identity; erasing parallel edges is proved to preserve planarity and every proper-coloring constraint. This bridge adds no simplicity, connectedness, triangulation, or nonemptiness assumption to the conventional conclusion. The root target itself remains unchanged.

An equivalent combinatorial formulation is welcome only with the formally verified translations needed to recover this target. If equivalence is claimed, both directions must be proved under precisely stated conventions. In particular, a hypermap coloring theorem alone does not complete this mission.

The original seven structural milestones remain unchanged:

Milestone	Deliverable
1. Graph realization	Construct a planar plain hypermap whose faces represent exactly the nonisolated graph vertices and whose edge steps encode precisely adjacency.
2. Cubic normalization	Construct a plain cubic hypermap with six times as many darts, preserving planarity and bridgelessness and transporting a coloring back.
3. Minimal counterexample	Choose a least-dart counterexample within the planar, bridgeless, plain, precubic comparison class.
4. Counterexample structure	Prove cubicity, connectedness and minimum face arity five as consequences of minimality.
5. Charge conservation	Prove total face charge $120c$ for $c$ components under arbitrary rational dart transfers, and a positive-charge face when connected.
6. Elimination	Complete the source's reducibility and unavoidability analysis to exclude every minimal counterexample.
7. Hypermap theorem	Assemble four-colorability for all planar bridgeless hypermaps.

These correspond to Gonthier's reductions in Section 3, PDF pp. 6–9, and development in Sections 5.1–5.6 of the 2005 report. Exact locations and executable-reference declarations accompany each milestone. Milestones 2, 3 and 6 imply milestone 7; milestones 1 and 7 imply the graph target. Those two conditional implications have been checked in Lean against the exact proposed statements. Milestone 6 now has thirteen concrete supporting targets:

Core target	Deliverable
Catalogue geometry	Prove geometric admissibility of every one of the fixed 633 configurations.
Catalogue reducibility	Kernel-check reducibility of every fixed map and contract using the proved complete checker or a verified refinement.
Reflection	Prove that the explicit mirror preserves minimal counterexamples.
Geometric exclusion	Prove that a C-reducible configuration cannot occur in a minimal counterexample; this includes the Birkhoff and patching arguments.
Presentation soundness	Prove the concrete finite presentation checker's generic soundness as one route to coverage.
Seven coverage cases	Independently handle positive hubs of degrees 5, 6, 7, 8, 9, 10 and 11, allowing reflected occurrences and unbounded neighboring arities.
Transfer bound	Bound each directed transfer by five under the explicit absence-of-configurations hypothesis; proved arithmetic then excludes positive hubs of degree at least 12.

The fixed catalogue and fixed rules are shared by both branches. The local Lean assembly checks that reducibility, geometric exclusion, reflection, the transfer bound, the seven degree cases, and milestones 4–5 imply milestone 6. It then connects to the unchanged hypermap and graph targets. The generic presentation checker offers a sufficient route to the semantic degree targets; its ability to certify every source presentation is not presumed. That route also requires actual presentation certificates and proofs of acceptance for the degree cases. Generic soundness and catalogue geometry alone do not supply those witnesses. Direct proofs of the seven semantic coverage obligations remain valid. Catalogue geometry remains a separate, meaningful finite theorem.

Exact mission obligations

There are 21 open theorem targets: 20 supporting milestones and one root. Every name below has prefix FourColor.. All remain future mission work; the checked conditional assembly is not a proof of any of these targets.

#	Exact target name	Obligation
1	`graph_realization`	Realize a finite drawn graph by a planar plain hypermap with exact face/adjacency incidence.
2	`cubic_normalization`	Construct the sixfold plain cubic map with the stated preservation and coloring transport.
3	`minimal_counterexample_exists`	Select a least-dart counterexample in the precubic comparison class.
4	`minimal_counterexample_structure`	Derive cubicity, connectedness and face arity at least five from minimality.
5	`charge_conservation`	Prove total charge and existence of a positive face for a connected host.
6	`catalogue_embeddable`	Prove the fixed 633 entries satisfy configuration geometry.
7	`catalogue_reducibility_certificates`	Establish accepted reducibility certificates for every fixed entry.
8	`mirror_minimal_counterexample`	Preserve minimal-counterexample status under the specified mirror.
9	`reducible_configuration_exclusion`	Exclude a C-reducible occurrence from a minimal counterexample.
10	`discharge_presentation_soundness`	Prove generic soundness of the concrete finite presentation checker.
11	`degree_5_coverage`	Derive a catalogue occurrence, in either orientation, from a positive degree-5 hub.
12	`degree_6_coverage`	Establish the same semantic occurrence obligation for degree 6.
13	`degree_7_coverage`	Establish the same semantic occurrence obligation for degree 7.
14	`degree_8_coverage`	Establish the same semantic occurrence obligation for degree 8.
15	`degree_9_coverage`	Establish the same semantic occurrence obligation for degree 9.
16	`degree_10_coverage`	Establish the same semantic occurrence obligation for degree 10.
17	`degree_11_coverage`	Establish the same semantic occurrence obligation for degree 11.
18	`discharge_transfer_bound`	Bound each transfer by five under minimality and absence of catalogue occurrences in either orientation.
19	`no_minimal_counterexample`	Assemble the core argument to exclude all minimal counterexamples.
20	`hypermap_four_color`	Assemble four-colorability of every planar bridgeless hypermap.
21	`four_color`	Prove the unchanged finite planar graph root above.

The degree cases quantify over minimal counterexamples with the exact positive score defined by the fixed rules; neighboring degrees have no artificial upper bound. The dependency path uses 16 necessary input targets to derive targets 19, 20 and 21. Targets 6 and 10 support the optional presentation-certificate route. None of targets 19, 20 or 21 is assumed as a shortcut in this assembly.

What completion would provide

The theorem provides a uniform existence guarantee for all finite planar graphs, without a bound on their size. Its Lean development should also make reusable graph embeddings, finite combinatorial maps, coloring transports, and verified finite checkers available to later work.

The existing Rocq development is an executable reference for definitions, dependency structure, and proof behavior. It is not a proof import into Lean. The proposed contribution is a Lean development whose proof objects and computation are justified within Lean's documented foundations. A mechanically translated collection of scripts is not required; contributors should choose abstractions that work well with Mathlib.

Where the difficulty lies

Checking finitely many small graphs does not establish the theorem for arbitrary finite graphs. The development must justify why its finite computational tasks suffice, and must connect their results to the graph statement. The mathematical and computational obligations must meet at explicit, proved interfaces.

There is also a representation gap. The standard target concerns vertex colorings of graphs drawn in the plane, whereas the reference implementation's combinatorial core colors faces of planar bridgeless hypermaps. The latter endpoint is four_color_hypermap in combinatorial4ct.v. Correct treatment of duality, connected components, and isolated vertices is part of the work. Renaming a combinatorial predicate “planar” cannot establish that connection.

Formalization scope and acceptance criteria

Use Lean 4 with a supported, pinned Mathlib revision. The initial draft is checked against Lean v4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Any later migration must preserve the statements and repeat the relevant checks. Reuse Mathlib's graph and coloring interfaces where appropriate, and develop missing infrastructure as reusable modules. The topological definition must not assume colorability, successful certificate verification, or the conclusion of an intermediate theorem.

The definition layer now provides plane drawings, finite permutation hypermaps, an exact graph/face incidence representation, minimal counterexamples, and rational face charges. Coloring equivalence across a face representation is proved for every positive number of colors, with isolated vertices handled explicitly. Exact Euler equality defines combinatorial planarity; geometric realization is a theorem obligation and cannot be assumed from the name.

The concrete core now defines configurations, ordered boundary traces, contracts, chromograms, Kempe closure, kernel preembeddings and reflected occurrences. The reference reducibility checker has proved soundness and completeness. All 633 maps, rings and contracts are literal data with kernel-validated table/index proofs. The 38 base entries and their 71 symmetrized entries are explicit, and the executable matcher has proved semantic correctness. These infrastructure results do not prove the catalogue's geometric validity, its reducibility, or unavoidability.

The production targets import FourColor.CompactCatalogue.configurations, a compact catalogue containing the same literal maps, rings and contracts. A generic verified decoder constructs validated entries without storing large evaluated proof terms in every import. A separate kernel-checked comparison proves exact ordered equality with the original catalogue, proves that every raw entry is accepted, and proves that none is dropped. The original certificate batches remain available for that audit but are excluded from production target imports. This representation change does not alter any of the 21 mathematical obligations.

Data provenance is pinned to Rocq commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Independent fresh-source comparisons check all 633 configurations and every base/expanded rule entry against that snapshot, including actual evaluated Lean payloads. These comparisons establish source correspondence; they are not proofs of reducibility or unavoidability.

The duplicate-data gate rejects unexplained or unintended duplicates and permits verified source-mandated repetition encoding multiplicity or weight. The only repeated rule payload is drule1, deliberately listed twice: the source explains its two-point transfer in discharge.v, lines 17–24 and retains both copies in base_drules (line 145). The Lean rule-match count also counts both copies, preserving weight two. Thus there are 38 base entries with 37 distinct payloads, and 71 expanded entries with 70 distinct payloads. Both copies must remain. No configuration duplicates or other repeated rule payloads are permitted without separately verified source justification.

The reference reducibility evaluator is exponentially expensive. Contributors should implement verified compressed representations or efficient checkers, with acceptance implying the same semantic C-reducibility. Completeness of the reference checker then recovers the stated certificate-existence target. The presentation language is a transparent finite baseline; its generic soundness is an open target, and no completeness claim is made. Source-style quizzes/hubcaps or direct Lean proofs can close the same seven semantic coverage targets. This keeps performance choices separate from the mathematical endpoint.

All computational claims needed by the theorem must be established in Lean. External generators may prepare candidate data or certificates, but their output must be validated by a checker with proved correctness, and the resulting proof must be accepted by the Lean kernel. A recorded successful run of an external program is insufficient. The final theorem and its dependency closure must contain no sorry, admit, unproved custom axiom, or unsupported computational assumption. An axiom audit must identify only Lean/Mathlib's documented foundations. The current 37-declaration conditional/infrastructure audit uses only propext, Classical.choice and Quot.sound; it does not claim an unconditional Four Color proof. Python generators and runtime JSON extraction are outside the mathematical trust boundary and cannot discharge the 21 targets.

Completion requires a reproducible repository in which lake build succeeds from a clean environment and builds the final theorem. Pin toolchain, dependencies, source revisions, and certificate data; document regeneration and verification commands. Maintain a dependency map connecting Lean declarations to exact paper locations and Rocq declarations, and record justified differences in representation. The local multigraph adapter already justifies forgetting parallel-edge multiplicities and transports proper colorings. Any auxiliary restrictions such as connectedness or nonemptiness must be discharged before the root theorem. The current statement and conditional builds verify proposal infrastructure. Success requires proofs of the mission obligations and the final theorem in the reproducible clean build, with no unproved assumptions beyond the documented Lean/Mathlib foundations. All 21 targets remain open at proposal finalization. The submission snapshot records the repository base commit, exact working-file hashes, toolchain, Mathlib revision, payload hashes and audit report; it must not misrepresent uncommitted files as contents of the base commit.

Selected references

Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem, technical report, 2005. Sections 2–5. Microsoft Research PDF.
Georges Gonthier, Formal Proof—The Four-Color Theorem, Notices of the AMS 55(11), 1382–1393, 2008. Theorem 1 and the formalization architecture. AMS PDF.
Gonthier and Rocq-community contributors, fourcolor, executable formalization, pinned to commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Repository.
Neil Robertson, Daniel Sanders, Paul Seymour, Robin Thomas, The Four-Colour Theorem, Journal of Combinatorial Theory, Series B 70(1), 2–44, 1997. DOI; author-hosted manuscript.

54 thms1 active userReviewed

Algorithmic Game Theory Operations Research Optimization+1·Captain: mikedeng1

A Supply Chain Theory of Factoring and Reverse Factoring 1: The Supplier's Equilibrium Choice Among Recourse, Non-Recourse and Reverse FactoringResearch Paper

Motivation

Small and medium-sized suppliers that sell to large retailers typically ship first and are paid weeks or months later. Until the invoice is paid, the supplier's cash is trapped in accounts receivable, while production has to be financed up front. Factoring (selling or pledging the receivable to a financial intermediary for immediate cash) and reverse factoring (a buyer-initiated program in which the retailer approves the invoice and the supplier is paid early by the retailer's bank) are the standard remedies, and reverse factoring programs of large buyers are often coupled with an extension of payment terms. Which of these instruments a supplier should use, and how the answer depends on the credit ratings of the two firms, is the question addressed by Kouvelis and Xu, "A Supply Chain Theory of Factoring and Reverse Factoring", Management Science 67(10):6071–6088, 2021 (doi:10.1287/mnsc.2020.3788). The paper embeds each financing scheme in the pull wholesale-price game of Cachon (2004) and compares the resulting equilibria.

Setting

A retailer (the Stackelberg leader) offers a wholesale price $w$ to a capital-constrained supplier (the follower), who then chooses a production quantity $q \ge 0$ and carries the inventory; the retail price $p$ is fixed, and $0 < c < p$ is the unit production cost. Demand $D \ge 0$ has density $f$ , complementary distribution function $\bar F$ , finite mean, $f > 0$ on $[0, \mathbb Z]$ ( $\mathbb Z \le +\infty$ ), and a strictly increasing failure rate $z = f/\bar F$ (strict IFR). Expected sales are $S(q) = \int_0^q \bar F(\xi)\,d\xi$ , and $k(q) = S(q)/\bar F(q)$ .

Each firm $j \in \{s, r\}$ has a credit rating $C_j \in (C_{\min}, C_{\max})$ . The default probability $\rho_j = \rho(C_j) \in [0,1]$ is strictly decreasing in the rating, and the interest-rate premium $\eta_j = \eta(C_j) > 0$ is decreasing. Production takes a lead time $t_1$ , payment follows after a term $t_2$ , and the supplier faces a Poisson liquidity shock of rate $\lambda_s$ during production (the retailer, rate $\lambda_r$ ). Under a scheme $i \in \{\mathcal F, \mathcal N, \mathcal R\}$ (recourse, non-recourse, reverse factoring, the last with a payment extension $\tau \ge 0$ ), the supplier's expected profit is

\pi_i(q; w) = (1-\rho_s)\big(\Lambda_i e^{-\lambda_s t_1} w S(q) - c q e^{\eta_s t_1}\big),

with coefficients $\Lambda_{\mathcal F} = (1-\rho_r) + (1-\rho_s) - e^{\eta_s t_2}$ , $\Lambda_{\mathcal N} = e^{-\eta_r t_2}(1-\rho_r)$ , $\Lambda_{\mathcal R} = e^{-\eta_r(t_2+\tau)}$ , and effective unit cost $c_i = c\,e^{(\eta_s+\lambda_s)t_1}/\Lambda_i$ . The retailer's profit is $e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and carries the extra factor $2 - e^{-\lambda_r \tau}$ under reverse factoring.

Formalization targets

Goal: Proposition 5

For a given $\tau \ge 0$ , let $\mathbb C_3$ be the unique supplier rating with $\Lambda_{\mathcal F} = \Lambda_{\mathcal R}$ , $\mathbb C_1$ the one with $\Lambda_{\mathcal F} = \Lambda_{\mathcal N}$ , and $\mathbb C_{\mathcal F}, \mathbb C_{\mathcal N}, \mathbb C_{\mathcal R}$ the feasibility thresholds ( $c_i = p$ ). With all three schemes available,

e^{-\eta_r\tau} < 1-\rho_r:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_1,\qquad \mathcal N \text{ adopted} \iff \mathbb C_{\mathcal N} < C_s \le \mathbb C_1;

1-\rho_r \le e^{-\eta_r\tau}:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_3,\qquad \mathcal R \text{ adopted} \iff \mathbb C_{\mathcal R} < C_s \le \mathbb C_3.

Milestones

Proposition 2 (p. 6078): recourse factoring is feasible iff $C_s > \mathbb C_{\mathcal F}$ , and then the unique equilibrium solves $p\bar F(q) = c_{\mathcal F}[1+z(q)k(q)]$ , $w = c_{\mathcal F}/\bar F(q)$ .
Proposition 3 (p. 6079): the same for non-recourse factoring with $c_{\mathcal N}$ .
§5.2 (p. 6082, Proposition EC.2): the same for reverse factoring with $c_{\mathcal R}(\tau)$ .
§4.4 (p. 6080, Lemma EC.2): between feasible schemes, the supplier's equilibrium profits are ordered as the $\Lambda_i$ .
Proposition 4 (p. 6080): the choice between $\mathcal F$ and $\mathcal N$ alone.

A follow-on item states Corollary 1(i) (p. 6081): when the retailer's rating is at least the supplier's, non-recourse factoring strictly dominates recourse factoring whenever the latter is feasible.

Significance

Proposition 5 is the paper's main prediction: non-recourse factoring is the choice of medium-rated suppliers, recourse factoring of highly rated ones, and reverse factoring with a fixed payment extension is chosen only by low-to-medium-rated suppliers and only if the retailer's rating is not too high relative to the extension. The paper uses it to explain the documented reluctance of suppliers to join reverse-factoring programs that come with extended payment terms (Wuttke, Rosenzweig and Heese 2019; Corsten 2010, a teaching case), and it is the starting point of the paper's Proposition 6 on the retailer's optimal payment extension, which is the subject of the second mission of this series.

The results are proved in the paper's Online Appendix B. To the best of available knowledge none of them, and no model of supply chain finance, has a machine-checked proof. A formal development would also supply a reusable treatment of the pull wholesale-price game under a strictly IFR demand with an arbitrary effective unit cost, of which Propositions 2, 3 and EC.2 are three instances.

Difficulty

The case analysis of Proposition 5 is short once the milestones are available; the substance lies in them. Proposition 2 requires solving a bilevel problem: the follower's best response has to be identified for every wholesale price, including prices at which the supplier produces nothing, and the leader's objective has to be shown to have a single maximizer. The natural route through the first-order condition needs the IFR property to exclude multiple stationary points, and it has to cope with a support end $\mathbb Z$ that may be finite (where $\bar F$ vanishes and $k$ , $z$ lose meaning) or infinite. Lemma EC.2 requires the equilibrium supplier profit as an explicit function of the effective cost and a monotonicity argument for it; comparing the $\Lambda_i$ directly, without the equilibrium, does not prove it. The proofs themselves are not in the main text.

Formalization scope

Demand is a probability measure μ on ℝ with a density f, the support end Z : EReal, and the complementary distribution function Fbar μ x = μ((x, ∞)). The model data, the coefficients coef, the effective costs cF, cN, cR, the two profit functions, best responses, equilibria, feasibility and adoption are definitions; all theorems are for arbitrary data satisfying Params.Valid and DemandModel. Readings fixed by the formalization:

"Feasible": some wholesale price $w \ge 0$ with a supplier best response gives the retailer strictly positive profit. It is not defined as $c_i < p$ , which is what Propositions 2 and 3 prove.
"Adopted" / "should be adopted": the scheme is feasible and its equilibrium supplier profit is best among the feasible available schemes, with ties resolved $\mathcal R \succ \mathcal N \succ \mathcal F$ , the order forced by the paper's boundaries ( $C_s = \mathbb C_1$ , $C_s = \mathbb C_3$ , $C_r = \mathbb C_2$ ). Profits are compared, not the $\Lambda_i$ .
"The unique value of $C_s$ that satisfies …": a point of $(C_{\min}, C_{\max})$ satisfying the equation and the only such point. The equation $c_{\mathcal F} = p$ is cross-multiplied, $c\,e^{(\eta_s+\lambda_s)t_1} = p\Lambda_{\mathcal F}$ , since $\Lambda_{\mathcal F}$ may be $\le 0$ .
" $C_r > \mathbb C_2$ " is read through the paper's equivalence $\tau > -\eta_r^{-1}\ln(1-\rho_r)$ , i.e. $e^{-\eta_r\tau} < 1-\rho_r$ : the stated assumptions give no single crossing in $C_r$ .
"The unique equilibrium can be derived from …": the equilibrium exists and is unique, and it is exactly the solution of the system with $q \in (0, \mathbb Z)$ ; this part is stated under feasibility.
"Increasing/decreasing" is weak unless stated (p. 6075); $\rho$ is strictly decreasing, $\eta$ weakly.
Continuity of $f$ is read on $[0,\mathbb Z]$ , and $\mathbb Z$ as the upper end of the support.
Additions: wholesale prices are nonnegative; the retailer's reverse-factoring profit is the last line of the p. 6082 display (the middle line has a stray factor $w$ ).
Corollary 1(i): "higher credit rating" is read as $C_r \ge C_s$ , "dominates" as a strictly larger equilibrium supplier profit whenever recourse is feasible.

A formalization in which feasibility or adoption is defined by the inequalities being proved ( $c_i < p$ , largest $\Lambda_i$ ) makes the propositions trivial and is ruled out by the definitions above. The profit functions (7), (10) and the p. 6082 display are taken as the model; the derivation from bank and factor pricing (Eqs. (1), (5), (6), Lemma 1) is not formalized, and the unstated assumptions of Table EC.2 are not included. Contributions of reusable lemmas on $S$ , $k$ and $z$ under strict IFR are welcome.

Selected references

P. Kouvelis and F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0189
D. A. Wuttke, E. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019.
P. Kouvelis and W. Zhao, Who Should Finance the Supply Chain? Impact of Credit Ratings on Supply Chain Decisions, Manufacturing & Service Operations Management 20(1):19–35, 2018.

8 thms1 active userReviewed

Completed

Linear algebra Machine Learning Probability·Captain: Minghui

Fine-Tuning Can Distort Pretrained Features: Perfect-Feature LP-FT SeparationResearch Paper

Why initialization matters for transfer learning

Transfer learning starts with a representation learned on an earlier task and adapts it to a new one. Two common choices are linear probing, which changes only the final linear predictor, and fine-tuning, which changes the representation as well. These procedures optimize related training objectives, but their behavior away from the training data can differ. Kumar and coauthors study this distinction through two-layer linear networks, alongside experiments with nonlinear networks. This mission formalizes their perfect-feature LP-FT result, rather than the empirical claims or the general imperfect-feature comparison. See Section 3.4, Proposition 3.7, PDF p. 10.

LP-FT first learns a head by linear probing and then uses that head to initialize full fine-tuning. The perfect-feature setting isolates the effect of head initialization: the representation already contains exactly the features needed to predict the labels, but the head initially need not use them correctly. The mathematical question is whether joint training preserves or loses the representation's ability to predict outside the observed training subspace.

Linear predictors, training data, and OOD loss

An input is a vector $x\in\mathbb R^d$ . A feature extractor is a matrix $B\in\mathbb R^{k\times d}$ , and a head is a vector $v\in\mathbb R^k$ . Together they predict $v^\top Bx$ , with effective weight vector $B^\top v$ . The fixed matrix $X\in\mathbb R^{n\times d}$ contains the $n$ training inputs as rows. Their span is $S=\operatorname{rowspace}(X)$ , with dimension $m$ .

The ground truth has orthonormal-row features $B_\star$ and a nonzero head $v_\star$ . Write $w_\star=B_\star^\top v_\star$ and $Y=Xw_\star$ . Perfect pretrained features mean $B_0=UB_\star$ for an orthogonal matrix $U$ . The corresponding aligned head is $u=Uv_\star$ . The dimensions satisfy $1\le k\le m$ and $m+k<d$ .

The two geometric assumptions require the orthogonal projections from $R_0=\operatorname{rowspace}(B_0)$ into $S$ and into $S^\perp$ to be injective. In this dimension regime these are exactly the positive largest-principal-angle cosine conditions used by the paper. They demand more than two subspaces having some nonorthogonal directions. The Lean definition spells out injectivity of $v\mapsto\Pi_T B_0^\top v$ for each $T\in\{S,S^\perp\}$ . See Definition 3.2 and Appendix A.1, PDF pp. 7 and 22-23.

An out-of-distribution law $\mu$ is any probability measure on $\mathbb R^d$ with a finite second moment and positive-definite uncentered second-moment matrix $\Sigma=\mathbb E_\mu[xx^\top]$ . Its mean need not be zero. Define

L_{\rm OOD}(v,B)=\mathbb E_{x\sim\mu} [(v^\top Bx-w_\star^\top x)^2].

Both training methods use the unnormalized loss $\widehat L(v,B)=\|XB^\top v-Y\|_2^2$ . Fine-tuning follows its gradient flow in both parameters; linear probing keeps $B=B_0$ . Time is real and nonnegative. These are the paper's equations (3.2)-(3.3), PDF p. 6.

Formalization targets

The goal is Proposition 3.7 in an explicit nonzero-signal regime. For $\sigma>0$ , initialize an FT head with independent Gaussian coordinates, $v_0\sim\mathcal N(0,\sigma^2I_k)$ . Establish

\Pr\!\left[\forall t\ge0,\quad L_{\rm OOD}(v_{\rm FT}(t),B_{\rm FT}(t))>0\right]=1.

Linear probing, from any initial head, must converge to $u$ . Fine-tuning initialized at its limit must satisfy

v_{\rm LP}(t)\longrightarrow u,\qquad \forall t\ge0,\quad L_{\rm OOD}(v_{\rm LP\text{-}FT}(t),B_{\rm LP\text{-}FT}(t))=0.

The probability-one event applies to all times simultaneously. The goal also asserts existence of the relevant global flows; a conditional claim about a possibly nonexistent trajectory would not suffice. The statement does not assert a numerical error lower bound or a positive time-infimum.

Seven milestones supply the supporting results: global flow existence and FT uniqueness; unchanged features orthogonal to the training span; the balancedness invariant; the second-moment identity for OOD risk; almost-sure Gaussian head misalignment; exact LP recovery; and stationarity after LP initialization. The principal source is Appendices A.2 and A.7, PDF pp. 23-31 and 45-47.

What the result establishes

The result distinguishes two initializations of the same joint-training procedure. In this idealized setting, a head obtained by linear probing gives zero OOD loss throughout subsequent fine-tuning, while a Gaussian head almost surely has positive OOD loss at every finite time. The conclusion concerns population squared prediction error, not classification accuracy or a finite test-set estimate.

The paper establishes the mathematical claim; this mission asks for a Lean proof of the stated model and result. The scope is deliberately limited to perfect pretrained features. It does not claim an LP-FT upper bound for imperfect features, which the authors identify as a further challenge in Section 3.4, PDF p. 10. A completed development would also provide reusable components for finite dimensional gradient flows, factorized linear models, and population risk.

Why the proof needs the training dynamics

The training loss alone does not select a unique effective predictor in an overparameterized problem. Knowing that a predictor fits the observed examples therefore does not determine its OOD loss. Formalization must track the head and feature extractor together, and it must distinguish parameter stationarity from a claim that a derivative happens to vanish at one time. The Gaussian conclusion also requires one event controlling an uncountable set of times; separate probability-one statements for individual times would be weaker.

Formalization scope and conventions

Vectors use Mathlib's finite dimensional real Euclidean spaces. Matrices are represented as continuous linear maps, with Euclidean adjoints and operator norms. The feature update is written explicitly as the Frobenius-gradient equation; it is not a gradient with respect to the operator norm. Differentiability is imposed within $[0,\infty)$ , including the right derivative at zero.

The dimensions, nonzero target, positive Gaussian scale, finite second moments, and projection injectivity are explicit. The nonzero target restricts the formalization to the regime of the Gaussian alignment argument in Lemma A.12; $k\le m$ makes the identifiability condition used in Proposition A.20 precise. The random-head law is the scaled standard Gaussian measure. No randomness of the fixed training matrix or independence from an additional data draw is assumed.

The model contains no assumed convergence, invariant, or desired risk bound. Each of those is a theorem obligation. The well-posedness milestone makes explicit an analytic prerequisite of the source's flow notation. The risk milestone uses the identity in (A.29)-(A.32), avoiding the reversed inequality printed in (A.28). The quantitative constant in Theorem 3.3 is outside this mission. Source-aligned proofs and the supporting analysis infrastructure are welcome; changing the learning rule or assuming a milestone inside the model would change the task.

Selected references

Ananya Kumar, Aditi Raghunathan, Robbie Jones, Tengyu Ma, and Percy Liang, Fine-Tuning can Distort Pretrained Features and Underperform Out-of-Distribution, ICLR 2022, arXiv:2202.10054v1. Main target: Section 3.4, Proposition 3.7, PDF p. 10, equations (3.10)-(3.11); proof: Appendix A.7, PDF pp. 45-47, Proposition A.20 and (A.208)-(A.218). Supporting invariants: Appendix A.2, PDF p. 24, Lemmas A.3-A.4, equations (A.15)-(A.20). Gaussian alignment: Appendix A.3, PDF pp. 34-35, Lemmas A.11-A.12.

9 thms1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 100001 PrimesResearch Paper

Motivation

Goldbach's problem asks whether every integer greater than $1$ can be written as a sum of a small number of primes. The first unconditional result of this kind was obtained by Schnirelmann around 1930: there is an absolute constant $k$ such that every integer $n > 1$ is a sum of at most $k$ primes. His argument is elementary. It uses an upper-bound sieve and Chebyshev-type prime estimates, together with a notion of additive density, and it does not need the prime number theorem or complex analysis.

The constant has since been reduced by much deeper methods. A short timeline for odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Vinogradov (1937): every sufficiently large odd integer is a sum of three primes, with an ineffective threshold in the original argument.
Ramaré (1995): every even integer is a sum of at most six primes, which gives at most seven primes for every odd $n > 1$ . (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): every odd $n > 1$ is a sum of at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes (the ternary Goldbach conjecture). (arXiv:1312.7748)

This mission targets a much weaker constant than any of these, $k = 100\,001$ . It does so because the constant comes from Schnirelmann's elementary method with every estimate made explicit, and that proof is short enough to be a realistic target for a complete formalization.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset $s$ of natural numbers such that every element of $s$ is prime, the elements of $s$ sum to $n$ , and $s$ has at most $k$ elements counted with multiplicity. Repetitions are allowed and order is irrelevant.

The number $1$ is not a sum of primes, so the question concerns odd $n \ge 3$ . Even numbers are excluded from the campaign statement.

The Schnirelmann density of a set $A \subseteq \mathbb{Z}_{\ge 0}$ is

\sigma(A) = \inf_{N \ge 1} \frac{|A \cap \{1, \dots, N\}|}{N}.

This notion is the additive tool behind the elementary approach. Mathlib provides it as schnirelmannDensity.

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 100\,001,\ \textstyle\sum s = n.

This is the campaign template of Odd numbers as sums of primes with the value $100\,001$ filled in. A stronger explicit form in the source is that every odd $n \ge 200\,003$ is a sum of exactly $100\,001$ primes; the at-most form for all odd $n > 1$ follows from it immediately.

Significance

The result itself. The bound $100\,001$ is far from the best known constants; five (Tao) and three (Helfgott) are both known on paper. Its value is that it rests on an elementary argument with every constant written out. There is no "sufficiently large" threshold and no appeal to the prime number theorem, zero-density estimates, or large-scale computation.

Formalizing it. No finite bound in this problem has a machine-checked proof on this platform yet. A proof of this goal would be the campaign's first proved value. The components are reusable beyond this mission:

Explicit Chebyshev-type bounds for $\pi(y)$ .
An explicit Selberg upper-bound sieve for the number of representations of an even number as a sum of two odd primes.
An averaged bound for the associated singular-series factor.
Schnirelmann's density inequality $\sigma(D + E) \ge \sigma(D) + \sigma(E) - \sigma(D)\sigma(E)$ .

Difficulty

The only substantial step is an upper bound for

r(s) = \#\{(p, q) : p, q \text{ odd primes},\ p + q = s\}

that is sharp up to a constant factor, namely of order $s/(\log s)^2$ times an arithmetic factor depending on the prime divisors of $s$ , with an explicit constant. The trivial bound $r(s) \le \pi(s)$ is weaker by a factor of $\log s$ . That loss makes the density of sums of two primes appear to be zero, so the additive argument cannot start. Everything after the sieve bound is short and explicit.

Formalization scope

The Lean statement is the campaign template verbatim with $100\,001$ in place of the value. It uses Multiset ℕ, Nat.Prime, and Odd n ∧ 1 < n. The statement is fixed by the campaign, and it has no vacuous hypotheses: every odd $n > 1$ is covered.

Mathlib already contains schnirelmannDensity and the fact that $\sigma(A) + \sigma(B) \ge 1$ with $0 \in A \cap B$ implies $A + B = \mathbb{N}$ . It also contains the Λ² setup of the Selberg sieve (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial-coefficient bounds. Missing, and welcome as contributions:

The explicit sieve bound for $r(s)$ .
The mean-square bound for the arithmetic factor.
Schnirelmann's inequality for $\sigma(D + E)$ .
The explicit lower bound for $\pi(y)$ in the form needed here.

Selected references

P. Pollack, Not Always Buried Deep: A Second Course in Elementary Number Theory, AMS, 2009. Chapter 6, §6, "An application to the Goldbach problem", pp. 196–201. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa Cl. Sci. (4) 22 (1995), 645–706. http://www.numdam.org/item/ASNSP_1995_4_22_4_645_0/
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014), 997–1038. https://arxiv.org/abs/1201.6656
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
An explicit elementary constant for sums of primes, unpublished note, September 2026, Theorem 1. Source of the constant $100\,001$ (with $c_1 = 1/9$ , $c_2 = 860$ , $x_0 = e^{2000}$ , $\sigma(A) \ge 1/35\,000$ , $m = 25\,000$ ).

1 thm1 active userReviewed

Dynamical Systems Number Theory Probability·Captain: mysticflounder

Tao 2022: Almost All Collatz Orbits Attain Almost Bounded ValuesResearch Paper

Motivation

The Collatz map sends an even positive integer $n$ to $n/2$ and an odd one to $3n+1$ . The Collatz conjecture asserts that every orbit of this map eventually reaches $1$ . It remains an open problem.

Because the conjecture is open, a large part of the literature proves weaker statements that hold for almost all starting values. These results bound how small an orbit gets, not whether it reaches $1$ . They are the strongest unconditional evidence for the conjecture. Terence Tao's 2022 theorem is the strongest result of this type: outside a set of logarithmic density zero, every orbit drops below any prescribed function that tends to infinity, however slowly (Tao 2022).

Timeline

Attributions follow the survey in Tao 2022, Section 1. Here $\mathrm{Col}_{\min}(N)$ is the least value in the orbit of $N$ .

1976 to 1979, Terras and Everett. $\mathrm{Col}_{\min}(N) < N$ for almost all $N$ , in natural density.
1979, Allouche. $\mathrm{Col}_{\min}(N) < N^{\theta}$ for almost all $N$ , for every $\theta > 0.869$ .
1994, Korec. The same bound for every $\theta > \log 3/\log 4 \approx 0.7924$ .
2019 preprint, 2022 publication, Tao. The power $N^{\theta}$ is replaced by any $f(N) \to \infty$ , in logarithmic density instead of natural density (Forum of Mathematics, Pi 10, e12).
2026, ProofAtlas. A complete machine-checked proof of Tao's theorem in Lean 4 is published (formalization record).

Setting

Let $\mathrm{collatzStep} : \mathbb{N} \to \mathbb{N}$ be

\mathrm{collatzStep}(n) = \begin{cases} n/2 & n \text{ even},\\ 3n+1 & n \text{ odd}. \end{cases}

Write $\mathrm{collatzStep}^{[k]}$ for the $k$ -fold iterate, with $\mathrm{collatzStep}^{[0]}(n) = n$ . The orbit of $n$ is the set of values $\mathrm{collatzStep}^{[k]}(n)$ for $k \ge 0$ . It includes $n$ itself.

The Syracuse map acts on odd integers. It sends an odd $n$ to the odd part of $3n+1$ , which is $\mathrm{syracuseStep}(n) = (3n+1)/2^{\nu_2(3n+1)}$ . The Syracuse orbit minimum $\mathrm{syracuseOrbitMin}(n)$ is the least value $\mathrm{syracuseStep}^{[k]}(n)$ over $k \ge 0$ .

For a set $A$ of positive integers and a real cutoff $x \ge 2$ , the logarithmic mass of $A$ up to $x$ is

\mathrm{weightedLogMassReal}(x) = \frac{1}{\log x} \sum_{\substack{1 \le n \le x \\ n \in A}} \frac{1}{n}.

A set of positive integers has logarithmic density $d$ when this quantity tends to $d$ as $x \to \infty$ . Since $\sum_{n \le x} 1/n = \log x + O(1)$ , all positive integers together have logarithmic density $1$ , and the odd positive integers have logarithmic density $1/2$ .

A function $f : \mathbb{N} \to \mathbb{R}$ tends to infinity on positive inputs when for every real $M$ there is an $N$ such that $f(n) > M$ for all $n \ge N$ with $n > 0$ .

Formalization targets

Goal: Tao's Theorem 1.3

For every $f$ that tends to infinity on positive inputs,

\lim_{x \to \infty} \frac{1}{\log x} \sum_{\substack{1 \le n \le x \\ \exists k,\ \mathrm{collatzStep}^{[k]}(n) < f(n)}} \frac{1}{n} = 1.

This is the Lean theorem collatz_almost_bounded_logarithmic. It fixes no rate and no constant, so later improvements do not invalidate it.

Syracuse form: Tao's Theorem 1.6

For every $f$ that tends to infinity on odd positive inputs, the odd $n$ whose Syracuse orbit contains a value below $f(n)$ have logarithmic density $1/2$ , which is all of the odd integers. This is syracuse_almost_bounded_logarithmic.

Quantitative form: Tao's Theorem 3.1

There are constants $C, c > 0$ such that for all real $M \ge 2$ and $x \ge 2$ ,

\frac{1}{\log x} \sum_{\substack{1 \le n \le x,\ n \text{ odd} \\ \mathrm{syracuseOrbitMin}(n) > M}} \frac{1}{n} \le \frac{C}{(\log M)^{c}}.

This is syracuse_uniform_logarithmic_tail_bound. The three targets are listed from weakest to strongest. In Tao's paper, the goal and Theorem 1.6 both follow from Theorem 3.1.

Significance

The result. Theorem 1.3 improves the earlier almost-all bounds on Collatz orbit minima from a power of $N$ to any function that tends to infinity. For example, $\mathrm{Col}_{\min}(N) < \log\log\log\log N$ for almost all $N$ . The theorem does not settle the conjecture. A single divergent orbit or nontrivial cycle is not excluded, because its predecessors form a set with bounded orbit minima.

The formalization. The theorem is proved, and a complete formalization already exists. The ProofAtlas record Tao's Almost-Bounded Collatz Orbits proves the statement taoAlmostBoundedColMin_checked with the same step map and an orbit that includes its starting value. That package has 397 first-party Lean files and about 124,000 source lines. ProofAtlas records a passing build with no sorry and the axiom profile propext, Classical.choice, Quot.sound. The source is released under the Apache-2.0 licence at commit d53c8de00056fb05999e44589f2399d7efa026e4, with copyright held by Advameg, Inc. It was built with Lean v4.30.0-rc2.

The remaining work for this mission is therefore a port, not new mathematics. The existing Lean development must be moved to Lean v4.33.1 and Mathlib 0df444a, and then connected to the goal statement above.

Difficulty

The mathematical difficulty is already resolved in the existing proof. The classical first-descent argument shows that a typical orbit drops below its starting value. Repeating that argument fails, because after one descent the new value is no longer distributed like a random integer of its size, and the error compounds at each repetition. That is why earlier results stop at a power bound $N^{\theta}$ .

The difficulty of this mission is engineering. The port moves a development of about 124,000 lines forward across three minor Lean releases and the corresponding Mathlib changes. Lemma renames, deprecations, and changes in tactic behaviour must be repaired file by file without changing any statement.

Formalization scope

Step map. collatzStep n = if Even n then n / 2 else 3 * n + 1, so $\mathrm{collatzStep}(0) = 0$ . This is the same definition as in the ProofAtlas source.
Orbit. The witness $k$ ranges over all natural numbers, including $k = 0$ .
Density. The goal uses weightedLogMassReal: a real cutoff $x$ , the natural indices $0 \le n \le \lfloor x \rfloor$ , weights $1/n$ , and normalization by $\log x$ . The ProofAtlas statement instead uses integer cutoffs and normalization by the harmonic sum $\sum_{n \le N} 1/n$ . A short bridge between the two normalizations is part of the required work.
Threshold. The hypothesis on $f$ constrains only positive inputs. The value $f(0)$ is irrelevant.
Non-triviality. The case $k = 0$ alone covers only inputs with $n < f(n)$ . For slowly growing $f$ this set is finite, so the goal is not satisfied by the starting value.

The goal is already reduced, through accepted proofs, to the single open statement syracuse_uniform_logarithmic_tail_bound. Two routes therefore close the mission. The first is to port the ProofAtlas development and prove the goal directly through the density bridge. The second is to prove Theorem 3.1 in its stated form. Contributions welcome include ported modules as reusable solutions, the density bridge, and a proof of Theorem 3.1. Every ported file must keep the Apache-2.0 notice and attribution to the ProofAtlas source.

Selected references

Terence Tao, Almost all orbits of the Collatz map attain almost bounded values, Forum of Mathematics, Pi 10 (2022), e12. https://doi.org/10.1017/fmp.2022.8 and https://arxiv.org/abs/1909.03562
ProofAtlas, Tao's Almost-Bounded Collatz Orbits, Lean 4 formalization, source commit d53c8de00056fb05999e44589f2399d7efa026e4, Apache-2.0, 2026. https://proofatlas.ai/formalizations/tao-almost-bounded-orbits/
Jeffrey C. Lagarias (editor), The Ultimate Challenge: The 3x+1 Problem, American Mathematical Society, 2010. https://bookstore.ams.org/MBK/78

3 thms1 active userReviewed

Completed

Linear algebra Mathematical Physics·Captain: ShapeZero

The spectrum of the octonionic two-generator flowTextbook

Motivation

This mission is pure mathematics about objects it defines itself: an octonion multiplication built from the Fano plane of the companion mission The role postulates force exactly seven points, and the matrix of the linear map

p \;\mapsto\; p\,a + b\,p

for two unit imaginary octonions $a, b$ . It is motivated by the two-generator D8 flow $\dot\psi = \psi a + b\psi$ in the Shape Zero derivation (00_START_HERE/MODEL_SPEC.md §1b; 02_synthesis/D8_SYNTHESIS.md). The statements below do not depend on that motivation.

Result. For $a = e_1$ and $b = c\,e_1 + s\,e_2$ with $c^2 + s^2 = 1$ , the characteristic polynomial of $M = R_a + L_b$ is

X^2\,(X^2 + 4)\,\bigl(X^2 + (2 - 2c)\bigr)^2 .

With $c = \cos\theta$ , $2 - 2c = 4\sin^2(\theta/2)$ , so the eigenvalues are $0, 0, \pm 2i$ and $\pm 2i\sin(\theta/2)$ (each twice), and the ratio of the two nonzero frequencies is $1/\sin(\theta/2)$ .

What this mission does NOT prove.

Only the canonical pair. It proves the result for $a = e_1$ , $b = \cos\theta\, e_1 + \sin\theta\, e_2$ . That every pair of unit imaginary octonions at angle $\theta$ gives the same spectrum follows from the classical fact that $G_2$ acts transitively on such pairs — not formalized here.
Nothing about any model. It says nothing about which angle, if any, a physical model selects, or whether the D8 flow plays a role in one.
One orientation. The octonion table uses one orientation of the Fano lines; all valid orientations give isomorphic algebras, and the spectrum is basis-independent, but only this table is formalized.

Setting

Write $e_0 = 1, e_1, \dots, e_7$ for the standard basis of $\mathbb{R}^8$ . The imaginary unit $e_u$ ( $u = 1, \dots, 7$ ) is labelled by the Fano point $u - 1$ . For each line $\{l, l+1, l+3\}$ (mod $7$ ) of the companion mission's Fano plane RolesForceSeven.fanoLine, the product is oriented cyclically along the ordered triple $(l, l+1, l+3)$ :

e_{l+1}\,e_{l+2} = e_{l+4}, \qquad e_{l+2}\,e_{l+4} = e_{l+1}, \qquad e_{l+4}\,e_{l+1} = e_{l+2}

(unit indices mod $7$ , shifted into $1, \dots, 7$ ), with the reversed products negative, $e_u^2 = -1$ , and $e_0$ the identity. This defines OctonionD8.octTable and the bilinear product OctonionD8.omul on $\mathbb{R}^8$ .

For $a, b \in \mathbb{R}^8$ , Rmat a is the matrix of $p \mapsto p\,a$ and Lmat b the matrix of $p \mapsto b\,p$ (column $j$ is the image of $e_j$ ). The flow matrix is

M = \texttt{flowMat}\;c\;s = R_{e_1} + L_{c e_1 + s e_2}.

The Fano plane is imported from the companion mission, not restated. The reordering blockEquiv and the two blocks blockA c s, blockB c s are defined explicitly for the milestones.

Formalization targets

Goal: the characteristic polynomial

c^2 + s^2 = 1 \;\Longrightarrow\; \chi_M(X) = X^2\,(X^2 + 4)\,\bigl(X^2 + (2 - 2c)\bigr)^2 .

This is OctonionD8.flow_charpoly. The hypothesis $c^2 + s^2 = 1$ is the only one, and it is needed: without it the characteristic polynomial differs.

Milestones — the proof outline

The proof goes through an invariant-subspace decomposition. Reorder the basis as $(e_0, e_1, e_2, e_4 \mid e_3, e_5, e_6, e_7)$ (OctonionD8.blockEquiv).

M1 (block-diagonal form). For all real $c, s$ , in the reordered basis $M$ is block diagonal: $M = \begin{pmatrix} A & 0 \\ 0 & B \end{pmatrix}$ , with explicit $4\times4$ blocks $A$ on $(e_0, e_1, e_2, e_4)$ and $B$ on $(e_3, e_5, e_6, e_7)$ (OctonionD8.blockA, OctonionD8.blockB).
M2 (block $A$ ). If $c^2 + s^2 = 1$ , then $\chi_A(X) = X^2\,(X^2 + 4)$ .
M3 (block $B$ ). If $c^2 + s^2 = 1$ , then $\chi_B(X) = \bigl(X^2 + (2 - 2c)\bigr)^2$ .

The goal follows: the characteristic polynomial is unchanged by reordering the basis, and that of a block-diagonal matrix is the product of the blocks' characteristic polynomials.

Further results (after the goal)

It is the octonions: the norm is multiplicative. For all $p, q \in \mathbb{R}^8$ , $\sum_k (pq)_k^2 = \bigl(\sum_i p_i^2\bigr)\bigl(\sum_j q_j^2\bigr)$ — the eight-square identity, which certifies that the table defines a normed (composition) algebra, the octonions, rather than some other algebra.
The flow conserves the norm. $M^{\mathsf T} = -M$ .
An annihilating polynomial. If $c^2 + s^2 = 1$ , then $M\,(M^2 + 4)\,\bigl(M^2 + (2 - 2c)\bigr) = 0$ .

Corollary: the frequencies

For $0 < \theta < \pi$ , with $c = \cos\theta$ and $s = \sin\theta$ , the roots over $\mathbb{C}$ of the characteristic polynomial, with multiplicity, are exactly

0,\ 0,\ \pm 2i,\ \pm 2i\sin(\theta/2),\ \pm 2i\sin(\theta/2),

and $0 < \sin(\theta/2) < 1$ . So the two nonzero frequencies $2$ and $2\sin(\theta/2)$ are distinct, and their ratio is $1/\sin(\theta/2)$ . Uses $2 - 2\cos\theta = 4\sin^2(\theta/2)$ .

Significance

The result itself. It gives the spectrum of the two-generator flow for the canonical pair in closed form, for every angle, from an octonion table built on the formalized Fano plane.

Formalizing it. The spectrum had been checked numerically and symbolically only.

Numerical and symbolic cross-check (independent code)

check	result
table from the companion mission's Fano lines is a normed algebra (200 random pairs)	true
eigenvalue magnitudes $\{0 \times 2,\ 2\sin(\theta/2) \times 4,\ 2 \times 2\}$ at 5°, 30°, 60°, 76.3°, 90°, 120°, 150°	max error $1.8\times10^{-15}$
symbolic characteristic polynomial (sympy, $s^2 = 1 - c^2$ )	$X^2(X^2 + 4)(X^2 + 2 - 2c)^2$

These agree with the repository's shape_zero_tests/d8_closed_form.py (frequencies $\{0, 2\sin(\theta/2), 2\}$ to $5\times10^{-11}$ ), which uses a different octonion table.

Difficulty

Moderate. The goal needs the characteristic polynomial of an $8\times8$ matrix with symbolic entries; a direct determinant expansion is expensive. The milestones take the invariant-subspace route: the block-diagonal form (M1) is an entrywise computation from the octonion table, and each $4\times4$ block's characteristic polynomial (M2, M3) is a small determinant, reduced with $c^2 + s^2 = 1$ . The further results are large but mechanical polynomial identities (the eight-square identity; the annihilating polynomial), where the risk is performance, not ideas.

Formalization scope

Vectors are Fin 8 → ℝ; matrices are Matrix (Fin 8) (Fin 8) ℝ, with column $j$ the image of the basis vector $e_j$ .
The characteristic polynomial is Mathlib's Matrix.charpoly over $\mathbb{R}$ ; the corollary maps it to $\mathbb{C}$ and uses Polynomial.roots, a multiset, so multiplicities are part of the statement.
The table is one fixed orientation of the Fano lines; $G_2$ -invariance and other orientations are out of scope.

Selected references

Wikipedia, Octonion. https://en.wikipedia.org/wiki/Octonion
Wikipedia, Fano plane. https://en.wikipedia.org/wiki/Fano_plane
Shape Zero repository (motivation only). https://github.com/ShapeZeroSZ/shape-zero

11 thms1 active userReviewed

Completed

Dynamical Systems Mathematical Physics·Captain: ShapeZero

Every quadratic-force oscillator is the same oscillator in different unitsTextbook

Motivation

This mission is a statement about ordinary differential equations and nothing else. It is motivated by the scaling analysis in the Shape Zero derivation (00_START_HERE/MODEL_SPEC.md §1b), which found that the golden ratio in an on-site quadratic well is a coordinate choice. The statements below do not depend on that motivation.

Result. For any $a \neq 0$ and any two distinct real roots $r_1 \neq r_2$ , the equation

x'' = -a\,(x - r_1)(x - r_2)

becomes exactly

z'' = -(z^2 - 1)

under one fixed shift and scaling of the value and one fixed rescaling of time. So every oscillator with a quadratic restoring force and two real roots is the same oscillator, described in different units. In particular, the golden-ratio well $x'' = -(x^2 - x - 1)$ , whose roots are $\varphi$ and $-1/\varphi$ , is the normal form in disguise: its $\varphi$ is a choice of coordinates.

What this mission does NOT prove.

Nothing about any lattice or model. It concerns a single oscillator. It does not treat coupling terms, and it says nothing about which dimensionless combinations survive in a coupled system.
Not that $\varphi$ has no meaning anywhere. It shows only that $\varphi$ in this equation is a coordinate choice.
Only solutions defined on all of $\mathbb{R}$ . Some solutions of this equation escape to infinity in finite time; the theorem concerns twice continuously differentiable functions on the whole real line. The same transformation works on intervals, but that is not formalized.
Not uniqueness of the transformation. It proves one exists.

Setting

Solutions are functions $x : \mathbb{R} \to \mathbb{R}$ that are twice continuously differentiable on all of $\mathbb{R}$ (ContDiff ℝ 2 x), with $x''$ written deriv (deriv x). The transformation is

z(\tau) = \frac{x(\tau/\omega) - m}{d},

a shift by $m$ , a scaling by $d \neq 0$ of the value, and a rescaling $t = \tau/\omega$ of time with $\omega > 0$ .

Formalization targets

Goal: one transformation for every solution

Let $a \neq 0$ and $r_1 \neq r_2$ . There are real numbers $m$ , $d$ , $\omega$ with $d \neq 0$ and $\omega > 0$ , chosen once, before any solution is considered, such that for every twice continuously differentiable $x : \mathbb{R} \to \mathbb{R}$ :

\bigl(\forall t,\; x''(t) = -a\,(x(t) - r_1)(x(t) - r_2)\bigr) \iff \bigl(\forall \tau,\; z''(\tau) = -(z(\tau)^2 - 1)\bigr).

This is QuadraticWell.quadratic_well_equiv. Explicitly $m = (r_1 + r_2)/2$ , $d = \pm(r_1 - r_2)/2$ with the sign chosen so that $a d > 0$ , and $\omega = \sqrt{a d}$ .

Milestones

M1 (the force in shifted, scaled form). If $r_1 \neq r_2$ and $d = \pm(r_1 - r_2)/2$ (either sign), then for every real $y$ : $-a(y - r_1)(y - r_2) = -a\,d^2\bigl(((y - m)/d)^2 - 1\bigr)$ with $m = (r_1 + r_2)/2$ .
M2 (the sign can be chosen). If $a \neq 0$ and $r_1 \neq r_2$ , then $a (r_1 - r_2)/2 > 0$ or $a (r_2 - r_1)/2 > 0$ — so $\omega = \sqrt{a d}$ is real and positive for one choice of $d$ .
M3 (chain rule for the rescaling). For $x$ twice continuously differentiable, $\omega \neq 0$ and $d \neq 0$ , the second derivative of $\tau \mapsto (x(\tau/\omega) - m)/d$ at $\tau$ is $x''(\tau/\omega)/(\omega^2 d)$ .

The goal combines them: by M1 the equation reads $x'' = -a d^2 (y^2 - 1)$ with $y = (x - m)/d$ ; by M3 this becomes $z'' = -(a d/\omega^2)(z^2 - 1)$ ; and $\omega^2 = a d$ , available by M2, gives $z'' = -(z^2 - 1)$ . The converse uses $\tau = \omega t$ .

Corollary: the golden-ratio well

For every twice continuously differentiable $x : \mathbb{R} \to \mathbb{R}$ , $x'' = -(x^2 - x - 1)$ everywhere if and only if

z(\tau) = \frac{x(\tau/\omega) - \tfrac12}{\sqrt5/2}, \qquad \omega = \sqrt{\sqrt5/2},

satisfies $z'' = -(z^2 - 1)$ everywhere. This is the explicit instance with roots $\varphi$ and $-1/\varphi$ : $m = \tfrac12$ , $d = \sqrt5/2$ .

Significance

The result itself. It shows that the only content of a quadratic restoring force with two real roots, for a single oscillator, is the normal form $z'' = -(z^2 - 1)$ ; the roots and the stiffness are units.

Formalizing it. The equivalence had been checked numerically only.

Cross-check (independent code)

check	result
M1 identity, both signs of $d$ (sympy)	exact
golden-ratio well: $m$ , $d$ , $\omega$	$\tfrac12$ , $\sqrt5/2$ , $(\sqrt5/2)^{1/2} = 1.057371$
$z(\tau) = (x(\tau/\omega) - m)/d$ against a direct solution of $z'' = -(z^2 - 1)$ , 400 points	max difference $6.9\times10^{-13}$
a case needing the sign flip ( $a = -2$ , roots $3$ and $-1$ )	$a h = -4 < 0$ , so $d = -h$ gives $a d = 4 > 0$

These agree with the repository's shape_zero_tests/scale_invariance.py (runs at four unit choices agreeing to $1.3\times10^{-14}$ ).

Difficulty

Low–moderate. M1 and M2 are short. M3 is the only fiddly part: Mathlib's chain rule for a composition with $\tau \mapsto \tau/\omega$ , applied twice, needs the differentiability of $x$ and of $x'$ that ContDiff ℝ 2 supplies. The goal and corollary then follow by rewriting.

Formalization scope

Solutions are functions on all of $\mathbb{R}$ , twice continuously differentiable; the derivative is Mathlib's deriv.
$m$ , $d$ and $\omega$ are existentially chosen before the solution $x$ , so one transformation serves every solution.
The hypotheses of the goal are exactly $a \neq 0$ and $r_1 \neq r_2$ .

Selected references

Wikipedia, Nondimensionalization. https://en.wikipedia.org/wiki/Nondimensionalization
Wikipedia, Golden ratio. https://en.wikipedia.org/wiki/Golden_ratio
Shape Zero repository (motivation only). https://github.com/ShapeZeroSZ/shape-zero

5 thms1 active userReviewed

Discrete Geometry·Captain: xuanji

Spencer–Szemerédi–Trotter Unit Distance 4/3 Upper BoundResearch Paper

Motivation

How many pairs of points in an $n$ -point planar set can be at distance one? Counting all pairs gives the trivial bound $\binom n2$ , but Euclidean geometry imposes a much stronger restriction: there are at most $Cn^{4/3}$ unit-distance pairs, for an absolute constant $C$ .

This mission concerns that upper bound alone.

Statement

For a finite set $P\subseteq\mathbb R^2$ , let $u(P)$ be the number of unordered pairs of distinct points at Euclidean distance one:

u(P)=\#\bigl\{\{p,q\}:p,q\in P,\ p\ne q,\ \|p-q\|=1\bigr\}.

Prove that there exists a constant $C>0$ such that

u(P)\le C|P|^{4/3}

for every finite $P\subseteq\mathbb R^2$ . The constant must be independent of $P$ , and there are no general-position assumptions.

Proof idea

The supplied proof uses the crossing lemma. From the unit circles centred at the points of $P$ , it constructs an auxiliary graph with $n=|P|$ vertices and $e$ edges satisfying

u(P)-n\le e, \qquad \operatorname{cr}(G)\le 2n^2.

If $e<4n$ , then $u(P)<5n$ . Otherwise, the crossing lemma gives

\frac{e^3}{100n^2}\le \operatorname{cr}(G)\le 2n^2,

so $e\le \sqrt[3]{200}\,n^{4/3}$ . Together, these cases give the required bound.

The main work is in constructing the graph, controlling its crossings, and proving the crossing lemma. The final numerical deduction is short. The project includes a written proof alongside the Lean development.

Lean formulation and scope

The plane is represented by EuclideanSpace ℝ (Fin 2) and point sets by Finset. The definition of unitDist P counts ordered pairs of distinct points at distance one, then divides by two.

The target proposition is:

∃ C : ℝ, 0 < C ∧
  ∀ P : Finset (EuclideanSpace ℝ (Fin 2)),
    (unitDist P : ℝ) ≤
      C * (P.card : ℝ) ^ ((4 : ℝ) / 3)

This includes empty and singleton sets and uses real exponentiation.

The crossing-consequences project already contains a sorry-free proof of this theorem. The purpose of the mission is to make it available for publication and community verification on Prove2me. The crossing lemma and other supporting results are not separate mission targets. Neither an optimal constant nor a matching lower bound is required.

References

J. Spencer, E. Szemerédi, and W. T. Trotter, Jr., “Unit distances in the Euclidean plane,” in B. Bollobás (ed.), Graph Theory and Combinatorics, Academic Press, 1984, pp. 293–303. Full text.
wpegden/crossing-consequences, commit 8769d142033fce042f502bf2857afb6b1375b5c3. Project overview and build instructions.

2 thms1 active userReviewed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Branch-and-Price-and-Cut for the Split-Delivery Vehicle Routing Problem with Time Windows: Some Optimal Solution Traverses Each Pair of Reverse Customer Arcs at Most OnceResearch Paper

Motivation

Vehicle routing problems ask for minimum-cost vehicle routes that deliver goods from a depot to a set of customers. In the split-delivery vehicle routing problem with time windows (SDVRPTW) a customer's demand may be served by several vehicles, and each customer must be visited inside a prescribed time window. Allowing split deliveries matters in practice: for the variant without time windows, Dror and Trudeau (1989) showed empirically that splitting can save substantially, and Archetti, Savelsbergh and Speranza (2006) proved the savings can reach 50%.

Exact methods for the SDVRPTW are branch-and-price algorithms, and they rely on structural properties of optimal solutions to prune the search. Desaulniers (Operations Research 58(1), 2010) collects these properties in §2 of his paper and uses the strongest one, Corollary 2, as a family of valid inequalities (constraint (7)) in his branch-and-price-and-cut method.

Timeline (as reported by Desaulniers 2010, §§1–2).

1989–1990. Dror and Trudeau prove, for the SDVRP without time windows and with the triangle inequality, that some optimal solution has no two routes sharing more than one split customer.
2006. Gendreau, Dejax, Feillet and Gueguen observe that the property holds with time windows, derive the arc-based Corollary 1, and remark that elementary routes suffice (Remark 1).
2010. Desaulniers strengthens Corollary 1 to pairs of reverse arcs (Corollary 2) and exploits it as cutting planes.

Setting

An instance has $n$ customers $\mathcal N$ , a start depot $0$ and an end depot $n+1$ (the same location at the beginning and end of the planning horizon), and the following data: a vehicle capacity $Q > 0$ ; a demand $d_i > 0$ for each customer, which may exceed $Q$ ; a time window $[e_v, l_v]$ for each node, shared by the two depot copies; nonnegative travel times $t_{vw}$ , which include the service time at $v$ ; and nonnegative costs $c_{vw}$ . The arc set $\mathcal A$ contains the idle arc $(0, n+1)$ and every arc $(v, w)$ , $v \ne w$ , with $e_v + t_{vw} \le l_w$ . The triangle inequality $t_{vx} \le t_{vw} + t_{wx}$ , $c_{vx} \le c_{vw} + c_{wx}$ is assumed throughout.

A route is a walk $0 \to v_1 \to \dots \to v_m \to n+1$ along arcs of $\mathcal A$ , customers possibly repeated, with service start times inside the time windows that respect travel times (waiting is allowed), and nonnegative quantities delivered at its visits whose total is at most $Q$ . Its cost is the sum of its arc costs. A solution is a finite family of routes, one per vehicle, with no bound on their number; it is feasible if every customer $i$ receives in total at least $d_i$ , and optimal if it is feasible and no feasible solution costs less. For customers $i, j$ , let $x_{ij}$ be the number of times arc $(i, j)$ is traversed, summed over all routes of a solution, and let $\mathcal A(\mathcal N) = \mathcal A \cap (\mathcal N \times \mathcal N)$ .

Formalization targets

All four statements assume the triangle inequality and that the instance has a feasible solution, and assert the existence of an optimal solution with a structural property.

Goal: Corollary 2 (p. 181)

\exists \text{ optimal solution with } x_{ij} + x_{ji} \le 1 \quad \text{for all } (i,j) \in \mathcal A(\mathcal N).

The two arcs of a pair of reverse customer arcs are used at most once in total. This is the form constraint (7) of the paper gives to the corollary.

Milestones

Remark 1. Some optimal solution has only elementary routes: no route visits a customer twice.
Theorem 1. Some optimal solution has no two distinct routes with two customers in common.
Corollary 1. Some optimal solution has $x_{ij} \le 1$ for all $(i, j) \in \mathcal A(\mathcal N)$ .

Significance

The result. Corollary 2 turns a property of optimal solutions into linear inequalities on arc-flow variables. Adding them to the arc-flow formulation cuts off fractional points of its linear relaxation while keeping an optimal integer solution, which is how Desaulniers uses them. Remark 1 justifies pricing only elementary routes in column generation. Theorem 1 is the combinatorial fact underneath both corollaries and is reused throughout the split-delivery literature.

Formalizing it. The four results are proved in the literature (Dror–Trudeau; Gendreau et al. 2006); Desaulniers states them without proof. No machine-checked version exists. This mission produces a reusable Lean model of the SDVRPTW (instances, arc sets, feasible routes with schedules and delivery patterns, solutions, optimality) and checked proofs of these properties, including the existence of an optimal solution, which the paper takes for granted.

Difficulty

The obvious argument is local: take an optimal solution that violates the property, shift quantities between two routes, remove a visit, and shortcut. Three points make this less routine than it sounds. First, the statements are existential: each exchange must keep the solution optimal and not reintroduce a violation already removed, so one needs a termination measure that decreases under every exchange (Corollary 2 needs elementarity and the Theorem 1 property simultaneously, not two separate optimal solutions). Second, removing a visit is feasible only because the arc set is defined by time windows: the shortcut arc $(v, w)$ must be shown to exist from the schedule and the triangle inequality on travel times, and the new schedule must be built explicitly. Third, the feasible set is infinite (real quantities, unbounded walks, unbounded number of vehicles), so the existence of an optimal solution is itself a statement to prove, not a hypothesis.

Formalization scope

Namespace SplitDeliveryVRPTW.Known. Nodes are the inductive type Node n (start, cust i for i : Fin n, finish). All quantities, times and costs are real. The arc set is exactly the set the paper defines (read as "if and only if"), with arcs into the start depot and out of the end depot excluded. The triangle inequality for $t$ is imposed on pairwise distinct nodes and for $c$ on triples of arcs, where the paper's data is defined. A route is a customer list (repetitions allowed) with a time function over path positions and a quantity function over visits. A solution is an indexed family Fin m → Route I, so identical routes may appear twice. Demand satisfaction uses $\ge$ , as constraint (2) does. The per-vehicle bound $\min\{d_i, Q\}$ of constraint (14) is omitted because it changes neither the feasible route patterns nor the costs.

Explicit readings of imprecise phrases:

"split customer", "in common" (Theorem 1) are undefined in the paper. A customer two distinct routes visit is split, and the routes have it in common. This visit-based reading is at least as strong as a delivery-based one.
Corollary 2's wording "at most one arc in set $\mathcal A^*_{ij}$ appears at most once" is read through constraint (7): the total number of traversals of the arcs of $\mathcal A^*_{ij}$ is at most one. It is stated in the equivalent form free of the choice of $\mathcal A^*(\mathcal N)$ .
"there exists an optimal solution" is conditional on feasibility, which is the hypothesis added.

Ruled-out trivializations: routes are not restricted to elementary walks (that would make Remark 1 definitional), solutions are not sets (that would forbid duplicate routes), optimality compares against solutions with any number of routes and any visit pattern, "split" is never counted over visits by the same route, capacity and time windows are part of route feasibility, and deliveries occur only at visits.

Useful infrastructure, reusable beyond this mission: shortcut lemmas for feasible routes (removing a visit), exchange lemmas between two routes, and existence of an optimum for split-delivery routing. Contributions of any of these as separate lemmas are welcome.

Selected references

G. Desaulniers, Branch-and-Price-and-Cut for the Split-Delivery Vehicle Routing Problem with Time Windows, Operations Research 58(1):179–192, 2010. https://doi.org/10.1287/opre.1090.0713
M. Dror, P. Trudeau, Savings by split delivery routing, Transportation Science 23(2):141–145, 1989. https://doi.org/10.1287/trsc.23.2.141
M. Dror, P. Trudeau, Split delivery routing, Naval Research Logistics 37(3):383–402, 1990. https://doi.org/10.1002/nav.3800370304
M. Gendreau, P. Dejax, D. Feillet, C. Gueguen, Vehicle routing with time windows and split deliveries, Technical Report 2006-851, Laboratoire Informatique d'Avignon, 2006.
C. Archetti, M. W. P. Savelsbergh, M. G. Speranza, Worst-case analysis for split delivery vehicle routing problems, Transportation Science 40(2):226–234, 2006. https://doi.org/10.1287/trsc.1050.0117

6 thms1 active userReviewed

Control Theory Operations Research Optimization·Captain: mikedeng1

Optimizing Static Linear Feedback: Gradient Method II: The Gradient Flow Stays in the Sublevel Set and Converges Exponentially under State FeedbackResearch Paper

Motivation

The linear-quadratic regulator (LQR) is the basic problem of optimal control: steer a linear system $\dot x = Ax + Bu$ so as to minimize an integrated quadratic cost of state and input. When the full state is measured, the optimal law is a static linear feedback $u = -Kx$ obtained from an algebraic Riccati equation. When only an output $y = Cx$ is measured, the optimal static output feedback $u = -Ky$ has no closed form, and the problem is nonconvex. In both cases the cost can be written as a function $f(K)$ of the gain alone, which makes it natural to minimize $f$ by gradient methods directly in the space of gains. This view goes back to Levine and Athans (1970) for output feedback and was revived in reinforcement learning by Fazel, Ge, Kakade and Mesbahi (2018), who proved global convergence of policy gradient for discrete-time state-feedback LQR.

Fatkhullin and Polyak (arXiv:2004.09875v2, SIAM J. Control Optim. 2021) carry out this program for the continuous-time problem. They show that $f$ is coercive, that it is $L$ -smooth on every sublevel set, and that under state feedback it satisfies a gradient-domination (Łojasiewicz–Polyak) inequality. From these properties they derive convergence of the continuous gradient flow and of the discrete gradient method. This mission formalizes the continuous part, Theorem 4.1.

Setting

Fix real matrices $A\in\mathbb R^{n\times n}$ , $B\in\mathbb R^{n\times m}$ , $C\in\mathbb R^{r\times n}$ and symmetric positive definite weights $Q\in\mathbb R^{n\times n}$ , $R\in\mathbb R^{m\times m}$ and covariance $\Sigma\in\mathbb R^{n\times n}$ . A gain is $K\in\mathbb R^{m\times r}$ , and the closed-loop matrix is $A_K = A - BKC$ . A square matrix is Hurwitz if all its eigenvalues have negative real part. The stabilizing set is

\mathcal S = \{K : A_K \text{ is Hurwitz}\}.

For $K\in\mathcal S$ , let $X(K)$ and $Y(K)$ be the unique solutions of the Lyapunov equations

A_K^\top X + XA_K + C^\top K^\top RKC + Q = 0,\qquad A_KY + YA_K^\top + \Sigma = 0 .

The LQR cost is $f(K) = \mathrm{Tr}(X(K)\Sigma)$ . It equals the expected infinite-horizon quadratic cost when the initial state has covariance $\Sigma$ . Its gradient with respect to the Frobenius inner product $\langle M,N\rangle = \mathrm{Tr}(M^\top N)$ is

\nabla f(K) = 2\,(RKC - B^\top X(K))\,Y(K)\,C^\top .

Given a known stabilizing gain $K_0\in\mathcal S$ , the sublevel set is $\mathcal S_0 = \{K\in\mathcal S : f(K)\le f(K_0)\}$ . The gradient flow is the ODE

\dot K(t) = -\nabla f(K(t)),\qquad K(0) = K_0 .

State feedback (SLQR) is the case $C = I$ ; there $f$ is written $f_S$ , and $K_*$ denotes a minimizer of $f_S$ on $\mathcal S$ . Norms: $\|\cdot\|_F$ is the Frobenius norm and $\|\cdot\|$ the spectral norm. $\lambda_1(M)$ is the smallest eigenvalue of a symmetric $M$ .

Formalization targets

Goal: Theorem 4.1 for state feedback

For $C=I$ , let $L>0$ be a Lipschitz constant of $\nabla f$ on $\mathcal S_0$ and let $\mu$ be the constant (3.11),

\mu = \frac{\lambda_1(R)\lambda_1^2(\Sigma)\lambda_1(Q)}{8f_S(K_*)\big(\|A\| + \|B\|^2 f_S(K_0)/(\lambda_1(\Sigma)\lambda_1(R))\big)^2}.

Then the flow has a solution on $[0,\infty)$ , and every solution stays in $\mathcal S_0$ , has $f(K_t)$ nonincreasing, has $\nabla f(K_t)\to0$ and $\min_{0\le t\le T}\|\nabla f(K_t)\|_F^2\le f(K_0)/T$ , and

\|K_t - K_*\|_F \le \frac{\sqrt{2L(f(K_0)-f(K_*))}}{\mu}\,e^{-\mu t}\qquad(t\ge0).

Milestones

In attack order:

Existence of a minimizer (Corollary 3.10).
The gradient formula (Lemma 3.11).
Existence of a Lipschitz constant of $\nabla f$ on $\mathcal S_0$ (Theorem 3.15, qualitative).
The gradient-domination inequality $\tfrac12\|\nabla f_S(K)\|_F^2\ge\mu(f_S(K)-f_S(K_*))$ on $\mathcal S_0$ (Theorem 3.17).
The energy identity $\tfrac{d}{dt}f(K_t) = -\|\nabla f(K_t)\|_F^2$ .
The integral bound of Appendix D.1.
The output-feedback part of Theorem 4.1 (general $C$ with $\operatorname{rank} C = r$ ): existence, invariance of $\mathcal S_0$ , monotonicity and (4.2).

Significance

The theorem certifies a simple, model-based procedure: start from any stabilizing gain and follow the negative gradient of the cost. The iterate never loses stability, and it converges exponentially to the optimal gain. The same happens for state feedback even though neither $f$ nor $\mathcal S$ is convex. For output feedback it guarantees convergence to stationarity with an explicit $O(1/T)$ rate. The continuous-time result is the template for the discrete gradient method of the same paper (Theorem 4.2) and for policy-gradient analyses of LQR in learning-based control.

The result is proved in the paper. The paper writes out the proof of (4.2) in Appendix D.1. It describes the whole proof as a replica of Theorems 8 and 9 of Polyak 1963, which treat functions satisfying the Łojasiewicz–Polyak inequality on the whole space. No machine-checked version of any of these statements is known. A formal proof would give the first verified treatment of LQR as an optimization problem over gains. It needs Lyapunov equations, the stabilizing set and the cost, together with the analytic facts on which the policy-gradient literature rests: coercivity, smoothness on sublevel sets, and gradient domination.

Difficulty

The obvious argument is the textbook convergence proof for gradient flows of smooth functions satisfying the Łojasiewicz–Polyak inequality. That proof assumes the function is defined and smooth on the whole space. Here $f$ lives only on the open set $\mathcal S$ , blows up at its boundary, is unbounded on $\mathcal S$ and is not globally $L$ -smooth. The Łojasiewicz–Polyak inequality holds only on $\mathcal S_0$ , with a constant that depends on $K_0$ . The work therefore lies in keeping the trajectory inside $\mathcal S_0$ and showing it exists for all time. This requires compactness of $\mathcal S_0$ (coercivity of $f$ ) and a positive distance from $\mathcal S_0$ to the boundary of $\mathcal S$ . Local ODE existence alone gives neither. The explicit constant $\mu$ additionally requires lower bounds on solutions of Lyapunov equations and an upper bound on $\|K\|_F$ over $\mathcal S_0$ .

Formalization scope

Matrices are Matrix (Fin p) (Fin q) ℝ. Hurwitz means every complex eigenvalue of the complexified matrix has negative real part. $X(K)$ and $Y(K)$ are the unique solutions of their Lyapunov equations. Where the solution is not unique (possible only off $\mathcal S$ ) they take the value $0$ , and no statement uses these off- $\mathcal S$ values. $\nabla f$ is defined by formula (3.3), and Lemma 3.11 states that it is the Fréchet derivative with respect to the Frobenius inner product. A solution of the flow is a curve with $K(0)=K_0$ that stays in $\mathcal S$ for $t\ge0$ . Its entries have the prescribed derivative within $[0,\infty)$ . Global existence and invariance of $\mathcal S_0$ are conclusions, never hypotheses. Assuming a global solution, or a solution confined to $\mathcal S_0$ , would trivialize the theorem, and that encoding is excluded. The case $C=I$ is a matrix argument $C$ with $C=1$ . $\lambda_1$ is the minimum of the (unsorted) eigenvalues, and the spectral norm is $\sqrt{\lambda_{\max}(M^\top M)}$ . "Monotone decreasing" is rendered as nonincreasing. $\min_{0\le t\le T}$ is rendered as the existence of a point of $[0,T]$ where the bound holds.

The standing assumptions of p. 3 are hypotheses wherever they apply: $K_0\in\mathcal S$ , $Q,R,\Sigma\succ0$ , $\operatorname{rank}C=r$ , and $B\ne0$ . Deviations from the printed paper:

The paper's explicit Lipschitz constant (3.8) is false as printed; the planning notes record counterexamples for both output and state feedback. The goal therefore takes $L$ as any Lipschitz constant of $\nabla f$ on $\mathcal S_0$ , which is the paper's own definition of $L$ -smoothness (§3.6). Theorem 3.15 enters only in its qualitative form, as the existence of such an $L$ .
The set-builder for $\mathcal S$ on p. 3 writes $\mathbb R^{m\times n}$ ; gains are $m\times r$ .
The optimal gain $K_*$ is a hypothesis (its existence is Corollary 3.10), and $f(K_*)>0$ is not assumed.

A complete development needs the following: Lyapunov equations and their solution theory (uniqueness, positivity, integral representation), continuity and differentiability of $K\mapsto X(K)$ on $\mathcal S$ , coercivity of $f$ , global existence for ODEs confined to a compact invariant set, and the Łojasiewicz–Polyak argument for flows on a subset. The Lyapunov and stabilizing-set layer is reusable across control missions. Proofs of any milestone, and of auxiliary lemmas such as Lemmas 3.8, A.5, C.1–C.3, are welcome.

Selected references

I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, SIAM J. Control Optim. 59 (2021); preprint arXiv:2004.09875v2. https://arxiv.org/abs/2004.09875
M. Fazel, R. Ge, S. Kakade, M. Mesbahi, Global Convergence of Policy Gradient Methods for the Linear Quadratic Regulator, ICML 2018. https://arxiv.org/abs/1801.05039
W. S. Levine, M. Athans, On the determination of the optimal constant output feedback gains for linear multivariable systems, IEEE Trans. Automat. Control 15 (1970). https://doi.org/10.1109/TAC.1970.1099363
H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
B. T. Polyak, Gradient methods for the minimisation of functionals, USSR Comput. Math. Math. Phys. 3 (1963), 864–878. https://doi.org/10.1016/0041-5553(63)90382-3

11 thms1 active userReviewed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Scheduling Subject to Resource Constraints: Classification and Complexity III: The Two-Machine Algorithm for Q2 with One Resource and Unit-Time Jobs Is OptimalResearch Paper

Motivation

Many production and computing systems run jobs on parallel machines that also draw on a shared, limited resource: tools, workers, memory, power. Adding such a resource to a scheduling problem can change its complexity entirely. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the three-field classification $\alpha\mid\beta\mid\gamma$ of Graham, Lawler, Lenstra and Rinnooy Kan by a resource field $res\lambda\sigma\rho$ , and determined the complexity of every problem with unit-time jobs on identical or uniform machines under the makespan criterion. Their Fig. 2 separates the maximal polynomially solvable cases from the minimal NP-hard ones.

This mission formalizes the polynomial side. Two identical machines are easy under arbitrary resources (Theorem 1, due to Garey and Johnson, via maximum matching). Three identical machines with one resource are NP-hard in the strong sense (Theorem 4), and so are two uniform machines with unit resources (Theorem 3). What remains for uniform machines is settled by two algorithms: a sorting-and-shifting procedure for two uniform machines with one resource of arbitrary size (Theorem 5), and a bottleneck transportation problem for any number of uniform machines with one resource and 0–1 requirements (Theorem 6). The hardness results are the subject of the companion missions I and II.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$ . Machine $M_i$ has speed $q_i>0$ ; every job has unit execution requirement, so it takes time $1/q_i$ on $M_i$ . Identical machines ( $P$ ) have $q_i=1$ ; uniform machines ( $Q$ ) have arbitrary speeds. There are $l$ resources $R_h$ with positive integer sizes $s_h$ , and job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. The field $res\lambda\sigma\rho$ records restrictions: $\lambda$ bounds the number of resources, $\sigma$ their sizes, $\rho$ the requirements, a dot meaning "part of the input". So $res1{\cdot}{\cdot}$ is one resource with arbitrary size and requirements, and $res1{\cdot}1$ is one resource with requirements in $\{0,1\}$ .

A schedule gives every job a machine $\mu(j)$ and a start time $S_j\ge0$ ; the job is executed during $[S_j,C_j)$ with $C_j=S_j+1/q_{\mu(j)}$ . It is feasible if jobs on the same machine do not overlap and, at every time $t$ , the jobs executed at $t$ use at most $s_h$ of each resource $R_h$ . The makespan is $C_{\max}=\max_j C_j$ . No precedence constraints occur in this mission.

Formalization targets

Goal: Theorem 5, correctness of the algorithm

For $Q2\mid res1{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ with $q_1\ge q_2$ : put all jobs on $M_1$ in order of nonincreasing $r_{1j}$ , then repeatedly move the last job of $M_1$ to the earliest feasible time on $M_2$ after the jobs already there, as long as this strictly reduces $C_{\max}$ . For every order with nonincreasing requirements, the resulting schedule $A$ is feasible and

C_{\max}(A)\le C_{\max}(\sigma)\quad\text{for every feasible schedule }\sigma.

Milestones for the goal

The paper's proof has two steps, both milestones. Call a schedule an (a)–(c) schedule when (a) $M_1$ runs its jobs back to back from time $0$ in nonincreasing $r_{1j}$ , (b) $M_2$ runs its jobs in nondecreasing $r_{1k}$ , and (c) every requirement on $M_1$ is at least every requirement on $M_2$ .

The algorithm's schedule is feasible, is an (a)–(c) schedule, and is best among feasible (a)–(c) schedules.
Every feasible schedule can be transformed into a feasible (a)–(c) schedule with no larger $C_{\max}$ .

Further results

Theorem 1. For $P2\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ , with $G$ the graph joining two jobs when they can run together and $S$ a maximum matching of $G$ , the optimal makespan is $n-|S|$ .
Theorem 6. For $Q\mid res1{\cdot}1,\,p_j=1\mid C_{\max}$ with the $s_1$ fastest machines listed first, the optimal makespan equals the optimal value of a bottleneck transportation problem that assigns jobs to slots (machine, position) with cost $k/q_i$ , resource jobs only to the $s_1$ fastest machines.

Significance

Theorems 5 and 6 complete the classification of Fig. 2 for uniform machines: every special case of $Q\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ not covered by the hardness theorems has a polynomial algorithm. Theorem 1 is the classical reduction of two-machine resource scheduling to maximum matching, the model case for later work on scheduling with conflict graphs.

The paper proves these results briefly: "clearly" for the first half of Theorem 5, "obviously" for Theorem 1, and a one-paragraph model for Theorem 6. The exchange argument of Theorem 5 is presented "in an informal way" through five steps that pass through fractional, preempted jobs. A machine-checked proof makes these arguments exact on a model with real start times. No formalization of these results is known, and the platform had no statement about resource-constrained scheduling on uniform machines before this mission.

Difficulty

With $q_1\ne q_2$ the job boundaries on the two machines are misaligned: a job on $M_2$ overlaps parts of several jobs on $M_1$ , so the resource check cannot be done slot by slot, and discrete reasoning on integer time grids does not apply. The exchange argument of Theorem 5 must control the resource usage at every real time while jobs are moved between machines and reordered, and it has to end with a nonpreemptive schedule even though the paper's intermediate steps split jobs. For Theorem 1, the hard direction is the lower bound: a feasible schedule with arbitrary real start times must be converted into a matching, which is a statement about how unit jobs on two machines can overlap. For Theorem 6, one must show that restricting resource jobs to the fastest machines and to back-to-back positions loses nothing.

Formalization scope

Model. Jobs, machines and resources are Fin n, Fin m, Fin l (0-based). Speeds are positive reals, sizes positive naturals, requirements naturals. Start times are nonnegative reals, execution intervals are half-open, and the resource constraint is checked at every real time. $C_{\max}=0$ for $n=0$ . The model carries a precedence digraph for consistency with the companion missions; every statement here assumes it has no arcs.
Implicit hypothesis. Theorems 1 and 5 assume every job fits alone ( $r_{hj}\le s_h$ ), which the paper leaves unstated; without it no feasible schedule exists.
The algorithm is a Lean definition following the page: the order is an argument (any nonincreasing order), "as early as possible" is the earliest start after $M_2$ 's last job at which the resource constraint holds throughout, and the loop stops at the first move that does not strictly reduce $C_{\max}$ .
Optimality is always stated in full: feasibility plus a lower bound against every feasible schedule. No minimum is written as an infimum of a possibly empty set.
Theorem 6 is stated with 0–1 slot assignments, the interpretation the paper gives to $x_{ijk}$ ; the page's constraint $\sum_{k=1}^{m}$ is read as $\sum_{k=1}^{n}$ .
Not formalized: the running times $O(ln^2+n^{5/2})$ (Theorem 1), $O(n\log n)$ (Theorem 5, including the phrase "This O(n log n) algorithm") and $O(n^3)$ (Theorem 6), which depend on a machine model the paper does not fix and, for Theorems 1 and 6, on cited matching and transportation algorithms.
Ruled out: a formalization of the goal that proves optimality only against (a)–(c) schedules, against schedules with integer start times, or for one fixed tie-breaking order proves less than Theorem 5.

Contributions welcome: lemmas about step functions of resource usage on half-open intervals, a left-shifting lemma for unit-time schedules on two machines, and the exchange steps of Theorem 5 as separate lemmas.

Selected references

J. Błażewicz, J.K. Lenstra, A.H.G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
M.R. Garey, D.S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
S. Even, O. Kariv, An O(n^{2.5}) algorithm for maximum matching in general graphs, Proc. 16th IEEE FOCS (1975) 100–112. https://doi.org/10.1109/SFCS.1975.23

10 thms1 active userReviewed

Completed

Combinatorics·Captain: mysticflounder

Eliahou–Revuelta Schur degree: L(4) = 16 and 49 ≤ L(5) ≤ 65Research Paper

Motivation

A set of integers is sumfree when no two of its elements, equal or distinct, add up to an element of the set. The Schur number $S(n)$ is the largest $N$ such that $\{1, \dots, N\}$ can be partitioned into $n$ sumfree sets; only $S(1), \dots, S(5) = 1, 4, 13, 44, 160$ are known. For $n \ge 4$ the best theoretical upper bound that Eliahou and Revuelta could cite in 2021 was $S(n) \le R_n(3) - 2$ , where the Ramsey number $R_n(3)$ is the least $N$ such that every $n$ -colouring of the edges of the complete graph $K_N$ has a monochromatic triangle. The Ramsey numbers satisfy $R_n(3) \le n\,(R_{n-1}(3) - 1) + 2$ for $n \ge 2$ (Greenwood–Gleason 1955); for $S(n)$ the paper knows no recursive upper bound.

Eliahou and Revuelta proposed a conjectural one. They defined a number $L(n)$ through the Schur degree of block-sum sets, proved $S(n) \le n\,L(n)$ (Theorem 5.4) and $S(n-1) + 1 \le L(n) \le R_{n-1}(3) - 1$ (Proposition 5.3), and conjectured $L(n) = S(n-1) + 1$ (Conjecture 5.6). This would give $S(n) \le n\,(S(n-1) + 1)$ (Conjecture 5.7) and $S(6) \le 966$ (Conjecture 5.8), against the range $536 \le S(6) \le 1836$ that they give. For $n = 4$ they proved $14 \le L(4) \le 16$ , conjectured $L(4) = 14$ , and left the value open.

Timeline.

1955: Greenwood and Gleason prove $R_3(3) = 17$ and the recursive bound above.
1961: Baumert computes $S(4) = 44$ (cited by Eliahou–Revuelta as reference [2]).
2000: Fredricksen and Sweet prove $S(6) \ge 536$ (doi).
2004: Fettes, Kramer and Radziszowski prove $R_4(3) \le 62$ (listed in DS1, rev. 18).
2018: Heule proves $S(5) = 160$ with a certified SAT computation (arXiv:1711.08076).
2020–2021: Eliahou and Revuelta, preprint arXiv:2006.01502 and refereed version, with the same numbering of the items used here.
2026: McKenna, The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49 (Zenodo, doi:10.5281/zenodo.22987189), proves $L(4) = 16$ and $L(5) \ge 49$ ; its Lean library ClassicalSchur formalizes both, with $L(5) \le 65$ .

Setting

All numbers are natural numbers, except in the group $G$ below.

Sumfree sets. A set $S$ is sumfree when the sum of two of its elements, equal or distinct, is never in $S$ . A set $X$ is covered by $n$ sumfree sets when it lies in the union of $n$ sumfree sets.

Schur degree. The Schur degree $\operatorname{sdeg}(X)$ is the least $n \ge 1$ such that $n$ sumfree sets cover $X$ . If there is no such $n$ , it is $\infty$ .

For example, $\operatorname{sdeg}(\{1, \dots, N\}) \le n$ holds for $N \le S(n)$ and fails for $N > S(n)$ .

Block sums. Let $A = (a_1, \dots, a_L)$ be a finite sequence of length $|A| = L$ . Its block sums are the sums of runs of consecutive entries:

a_i + a_{i+1} + \dots + a_j \qquad (1 \le i \le j \le L).

The set of these sums is $\hat A$ . The average of $A$ is the rational number $\mu(A) = (a_1 + \dots + a_L)/L$ .

The number $L(n)$ . A length $L$ has the ER property for $n$ when every sequence $A$ of $L$ positive integers with $\mu(A) \le n$ has $\operatorname{sdeg}(\hat A) \ge n$ .

For $n \ge 2$ , the inequality $\operatorname{sdeg}(\hat A) \ge n$ holds when no $n - 1$ sumfree sets cover $\hat A$ . It fails when some $n - 1$ sumfree sets cover $\hat A$ .

The number $L(n)$ is the least $L \ge 1$ with the ER property for $n$ .

The pigeonhole bound. Let $\rho(0) = 2$ and $\rho(k+1) = (k+1)(\rho(k) - 1) + 2$ . The first values are $\rho(1) = 3$ , $\rho(2) = 6$ , $\rho(3) = 17$ and $\rho(4) = 66$ .

For $k \ge 1$ , $\rho(k)$ is an upper bound for the Ramsey number: $R_k(3) \le \rho(k)$ , with equality for $k \le 3$ .

The group $G$ . Let $G = \mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2}$ . A set $C \subseteq G$ is sumfree in $G$ when the sum in $G$ of two of its elements, equal or distinct, is never in $C$ .

The lifted sequence. Take $m_1 \ge 1$ and $M \ge m_1$ . Write the $m_1 m_2$ numbers $u + Mj$ , with $0 \le u < m_1$ and $0 \le j < m_2$ , in increasing order:

x_0 < x_1 < \dots < x_{m_1 m_2 - 1}.

The lifted sequence is the sequence of the $m_1 m_2 - 1$ gaps between consecutive terms, $x_1 - x_0, \dots, x_{m_1 m_2 - 1} - x_{m_1 m_2 - 2}$ . Lemma 4.1 below uses it to turn a cover of $G \setminus \{0\}$ into a sequence in ℕ.

Lean names.

SumFree S: $S$ is sumfree.
CoveredBySumFree X n: $X$ is covered by $n$ sumfree sets.
sdeg X : ℕ∞: the Schur degree, with ⊤ for $\infty$ .
blockSums A and average A, for A : List ℕ: $\hat A$ and $\mu(A)$ .
ERProperty n L: the length $L$ has the ER property for $n$ .
erL n: $L(n)$ .
ramseyBound k: $\rho(k)$ .
GroupSumFree C: $C$ is sumfree in $G$ . The Lean definition takes any type with an addition; the targets use it for ZMod m₁ × ZMod m₂.
liftPrefix m₁ M L: $x_L$ , defined for all $m_1$ and $M$ by $x_L = (L \bmod m_1) + M \lfloor L/m_1 \rfloor$ .
liftSeq m₁ m₂ M: the lifted sequence, defined for all $m_1$ , $m_2$ and $M$ as the list of the $m_1 m_2 - 1$ differences $x_{k+1} - x_k$ .

Formalization targets

Goal

\mathrm{erL}\ 4 = 16

An exact value, so no later result changes the statement; it is the case Eliahou and Revuelta left open.

Theorem 4.1 of Eliahou–Revuelta, in ℕ, with $\rho(k)$ for $R_k(3)$

\rho(k) \le |A| + 1 \implies k + 1 \le \operatorname{sdeg}(\hat A) \qquad (k \in \mathbb{N},\ A \text{ a finite sequence in } \mathbb{N}).

Upper bound of Proposition 5.3, with $\rho(k)$ for $R_k(3)$

\mathrm{erL}(k+1) \le \rho(k) - 1 \qquad (k \in \mathbb{N}).

No length below 16 has the property at $n = 4$

\neg\,\mathrm{ERProperty}\ 4\ L \qquad (1 \le L \le 15).

Lemma 4.1 (McKenna 2026): lift from a group

For $m_1, m_2, q \ge 1$ , $M \ge 3m_1 - 2$ and sets $C_1, \dots, C_q$ , sumfree in $G$ , that cover $G \setminus \{0\}$ , the sequence $A =$ liftSeq m₁ m₂ M satisfies

|A| = m_1 m_2 - 1, \quad a_i > 0, \quad \operatorname{sdeg}(\hat A) \le q, \quad a_1 + \dots + a_L = x_L \ \ (L \le m_1 m_2 - 1).

Corollary 4.2 (McKenna 2026): group coverings bound $L(n)$ from below

For $n \ge 3$ , $m_1, m_2 \ge 1$ and $n - 1$ sets, sumfree in $G$ , that cover $G \setminus \{0\}$ :

m_1 m_2 \le \mathrm{erL}\ n.

Theorem 1.2 (McKenna 2026), with the Lean upper bound: bounds for $L(5)$

49 \le \mathrm{erL}\ 5 \le 65.

Significance

$L(4) = 16$ . At $n = 4$ , Conjecture 5.6 predicts $L(4) = S(3) + 1 = 14$ . So $L(4) = 16$ refutes the conjecture at $n = 4$ . Here $L(n)$ equals the upper bound $R_{n-1}(3) - 1$ of Proposition 5.3.

The two bounds of Proposition 5.3 coincide at $n = 2, 3$ , where the paper gives $L(2) = 2$ and $L(3) = 5$ . So $n = 4$ is the first case in which the conjecture says more than Proposition 5.3.

$L(5) \ge 49$ . At $n = 5$ , Conjecture 5.6 predicts $L(5) = S(4) + 1 = 45$ . So $L(5) \ge 49$ refutes the conjecture at $n = 5$ .

What remains open. Conjectures 5.7 and 5.8 remain open.

The paper derives Conjecture 5.7 at each $n$ from Conjecture 5.6 at the same $n$ , with Theorem 5.4. At $n = 4, 5$ that derivation is not available. But Conjecture 5.7 holds there by the known values: $44 \le 4 \cdot 14$ and $160 \le 5 \cdot 45$ .

Conjecture 5.8 follows from Conjecture 5.6 at $n = 6$ (that is, $L(6) = 161$ ) with Theorem 5.4. Nothing here decides that case.

With $L(4) = 16$ , Theorem 5.4 gives only $S(4) \le 64$ . This is weaker than $S(4) \le R_4(3) - 2 \le 60$ .

Status. Every target is proved and formalized.

Theorem 4.1 and Proposition 5.3 are proved in the refereed paper.
$L(4) = 16$ (Theorem 1.1), Lemma 4.1, Corollary 4.2 and $L(5) \ge 49$ (Theorem 1.2) are proved in McKenna 2026 (doi:10.5281/zenodo.22987189). Before publication, separate agents, with their own code, checked the proofs in two rounds of adversarial audit.

At launch, all 12 theorems of the tree, the goal included, are Proved in Lean over 4 definition bundles. Their only axioms are propext, Classical.choice and Quot.sound.

An independent verifier checked the definitions and the six headline statements against Eliahou–Revuelta and McKenna 2026. The six statements are the goal, Theorem 4.1, Proposition 5.3, Lemma 4.1, Corollary 4.2 and Theorem 1.2.

Literature. The literature search for McKenna 2026 found no result on $L(4)$ , $L(5)$ or Conjectures 5.6–5.8. One citing text, in Jungić 2023, was not read. This records the search; it is not a claim of priority.

Open work, not targets.

The exact $L(5)$ : $49 \le L(5) \le 61$ on paper (with $R_4(3) \le 62$ ), and $49 \le L(5) \le 65$ in Lean.
The case $n = 6$ : $161 \le L(6) \le R_5(3) - 1 \le 306$ (DS1: $R_5(3) \le 307$ ). Here Conjecture 5.6 is the open step toward $S(6) \le 966$ .

Difficulty

Two kinds of bound. The two sides of an exact value of $L(n)$ are statements of different kinds.

An upper bound $L(n) \le m$ needs one length. It follows from $\operatorname{sdeg}(\hat A) \ge n$ for every sequence $A$ of positive integers of one length $L$ , with $1 \le L \le m$ and average at most $n$ .

A lower bound $L(n) \ge m$ needs every shorter length. For every $L$ with $1 \le L < m$ , it needs a sequence of $L$ positive integers, with average at most $n$ , whose block sums are covered by $n - 1$ sumfree sets.

One counterexample at length $m - 1$ is not enough. A sequence of length $L + 1$ and average at most $n$ need not contain $L$ consecutive entries of average at most $n$ . So monotonicity in $L$ does not follow directly from the definition.

The average bound. The lower bound $S(n-1) + 1$ of Proposition 5.3 comes from the constant sequence $(1, \dots, 1)$ , with $\hat A = \{1, \dots, L\}$ . Conjecture 5.6 states that at length $S(n-1) + 1$ , no sequence of average at most $n$ has $\operatorname{sdeg}(\hat A) \le n - 1$ .

Without the bound on the average, this fails. The paper gives a sequence of length 14 with $\operatorname{sdeg}(\hat A) = 3$ , found by semi-random search. Its average is 114, and the authors remark that such examples "are hard to come by".

The gap for $L(5)$ . The gap from 49 to 61 is open. By McKenna 2026 (§5), the construction of Corollary 4.2 gives nothing above 49 at $n = 5$ :

$S(4) = 44$ excludes the cyclic groups of order at least 46.
Solver runs exclude the non-cyclic groups of order 50 to 60. Their unsatisfiability proofs (in the DRAT format) were checked.
$L(5) \le 61$ excludes the orders of 62 or more.

McKenna 2026 knows no sequence of length 49 with average at most 5 and $\operatorname{sdeg}(\hat A) \le 4$ ; such a sequence would give $L(5) \ge 50$ .

Formalization scope

Ambient ℕ. The paper works in an abelian group; here sets are Set ℕ and sequences List ℕ. For $X \subseteq \mathbb{N}$ the Schur degree is the same in ℕ and in ℤ. Theorem 4.1 is formalized for sequences in ℕ only.
sdeg is sInf in ℕ∞, so it is ⊤ when no cover exists, and $\operatorname{sdeg}(\emptyset) = 1$ . Covers are Fin n → Set ℕ; the sets need not be disjoint or inside $X$ . Each lower bound on sdeg must exclude every cover.
blockSums A uses B <:+: A with B ≠ []; average [] = 0 is never used, since erL requires $L > 0$ .
erL n is sInf {L | 0 < L ∧ ERProperty n L} in ℕ, defined for every $n$ (the paper: $n \ge 2$ ). As sInf ∅ = 0, an upper bound on erL alone would hold if no length had the property; the Theorem 4.1 target excludes this, giving ERProperty (k+1) at length $\rho(k) - 1 \ge 1$ , and 0 satisfies neither the goal nor the lower bounds.
Ramsey bound. $\rho(k)$ replaces $R_k(3)$ . TriangleRamsey k N says every colouring of the pairs $x < y$ of at least $N$ naturals with at most $k$ colours has a monochromatic triangle; the tree proves it for $N = \rho(k)$ . As $\rho(4) = 66 > 62 \ge R_4(3)$ , the Lean upper bound for $L(5)$ is 65, not 61.
Lemma 4.1, Corollary 4.2. As in McKenna 2026, the sets need only cover $G \setminus \{0\}$ , and Lemma 4.1 requires $q \ge 1$ : for $q = 0$ , $m_1 = m_2 = 1$ the sequence is empty and $\operatorname{sdeg}(\emptyset) = 1$ . The prefix sums are exact: $x_L$ .
Subtraction is truncated; with $m_1, m_2 \ge 1$ and $\rho(k) \ge 2$ , none of 3 * m₁ - 2, m₁ * m₂ - 1, ramseyBound k - 1 and n - 1 in Fin (n - 1) ( $n \ge 3$ ) truncates, and the differences in liftSeq do not truncate when $M \ge m_1 \ge 1$ .
Finite checks use kernel decide; no native_decide, no external certificate.

Bundles: ClassicalSchurBasic (the objects of the Setting), ClassicalSchurRamsey (TriangleRamsey, ramseyBound), ClassicalSchurLift (GroupSumFree, liftPrefix, liftSeq), ClassicalSchurValues (the finite data of the two value theorems). As a check, the definitions give the paper's values erL 2 = 2 and erL 3 = 5 (checked in Lean by an independent verifier in a scratch file; not in the tree). Reusable: the definitions of ClassicalSchurBasic (the interface lemmas are inlined in the proofs, not separate nodes), TriangleRamsey k (ramseyBound k), and the lift from group coverings. Welcome beyond the targets: a formal TriangleRamsey 4 62, which with not_coveredBySumFree_blockSums gives $L(5) \le 61$ in Lean; the exact $L(5)$ ; the case $n = 6$ .

Selected references

S. Eliahou, M. P. Revuelta, The Schur degree of additive sets, Discrete Math. 344 (2021) 112332. https://doi.org/10.1016/j.disc.2021.112332
S. Eliahou, M. P. Revuelta, The Schur degree of additive sets, preprint, arXiv:2006.01502v1, 2020. https://arxiv.org/abs/2006.01502v1
R. E. Greenwood, A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955) 1–7. https://doi.org/10.4153/CJM-1955-001-4
H. Fredricksen, M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000) #R32. https://doi.org/10.37236/1510
M. J. H. Heule, Schur number five, Proc. AAAI-18, 2018; preprint arXiv:1711.08076, 2017. https://arxiv.org/abs/1711.08076
S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18, 2026. https://doi.org/10.37236/21
A. McKenna, The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49, Zenodo, 2026. https://doi.org/10.5281/zenodo.22987189 (version 1.0.1: https://doi.org/10.5281/zenodo.22987688). The Lean library ClassicalSchur and the comparator check: https://github.com/mysticflounder/schur-degree-block-sums (tag v1.0.1).

16 thms1 active userReviewed

Control Theory Dynamical Systems Operations Research+2·Captain: mikedeng1

Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations I: Almost Sure Asymptotic StabilityResearch Paper

Motivation

Many engineered systems switch between a finite number of operating modes at random times: a power grid after a line failure, a networked controller whose links drop, a manufacturing plant whose machines break down and are repaired. A standard model for such systems is a hybrid stochastic differential equation, also called an SDE with Markovian switching: the state follows an Itô equation whose coefficients depend on a mode that evolves as a continuous-time Markov chain. The monograph of Mao and Yuan (Stochastic Differential Equations with Markovian Switching, 2006) develops the stability theory of these equations.

A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times $0,\tau,2\tau,\dots$ and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations stabilizes a hybrid SDE in the sense of mean-square exponential stability when $\tau$ is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval $\tau$ , and proved $H_\infty$ -stability, mean-square asymptotic stability, almost sure asymptotic stability and exponential stability of the controlled system. This mission formalizes the almost sure asymptotic stability result, Theorem 3.4, and the results it is built on.

Setting

Let $(\Omega,\mathcal F,\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a probability space with a filtration satisfying the usual conditions (increasing, right-continuous, $\mathcal F_0$ contains the null sets). On it live an $m$ -dimensional $\{\mathcal F_t\}$ -Brownian motion $w$ and a right-continuous $\{\mathcal F_t\}$ -Markov chain $r$ on $S=\{1,\dots,N\}$ with generator $\Gamma=(\gamma_{ij})$ ( $\gamma_{ij}\ge0$ for $i\ne j$ , zero row sums), independent of $w$ . Fix $\tau>0$ and the sampling time $\delta_t=[t/\tau]\tau$ , the last observation time up to $t$ . The controlled system is

dx(t)=\big(f(x(t),r(t),t)+u(x(\delta_t),r(t),t)\big)dt+g(x(t),r(t),t)\,dw(t),\qquad x(0)=x_0,\ r(0)=r_0,\tag{2.1}

with $f,u:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^n$ and $g:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^{n\times m}$ . The feedback $u$ sees the state only at the observation times.

The hypotheses are:

Assumption 2.1: $f,g$ locally Lipschitz in $x$ , and $|f(x,i,t)|\le K_1|x|$ , $|g(x,i,t)|\le K_2|x|$ ( $|g|$ the trace norm).
Assumption 2.2: $|u(x,i,t)-u(y,i,t)|\le K_3|x-y|$ and $u(0,i,t)=0$ .
Assumption 3.1: there are $U\in C^{2,1}(\mathbb R^n\times S\times\mathbb R_+;\mathbb R_+)$ and $\lambda_1,\lambda_2>0$ with $\mathcal LU(x,i,t)+\lambda_1|U_x(x,i,t)|^2\le-\lambda_2|x|^2$ , where

\mathcal LU=U_t+U_x[f+u]+\tfrac12\operatorname{trace}[g^TU_{xx}g]+\sum_j\gamma_{ij}U(x,j,t).

Condition (3.5): $\lambda_2>\frac{\tau K_3^2}{\lambda_1}\big[2\tau(K_1^2+2K_3^2)+K_2^2\big]$ and $\tau\le\frac1{4K_3}$ .

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Condition35, in the namespace You2015.Asymp; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, and solutions SolvesSampledHybridSDE, in the namespace You2015.Shared shared with the companion mission.

Formalization targets

Goal: Theorem 3.4 (almost sure asymptotic stability)

Under the hypotheses above, every solution of (2.1) satisfies

\lim_{t\to\infty}x(t)=0\quad\text{a.s.}

for all $x_0\in\mathbb R^n$ and $r_0\in S$ . No rate is claimed; the statement is the qualitative convergence of almost every path.

Milestones, in the order the proof uses them

(3.15) $\mathbb E|x(t)-x(\delta_t)|^2\le2\mathbb E\int_{\delta_t}^t[\tau|f+u(x(\delta_s),\cdot)|^2+|g|^2]ds$ .
Theorem 3.2 ( $H_\infty$ -stability): $\int_0^\infty\mathbb E|x(s)|^2ds<\infty$ .
(3.21) $\mathbb E|x(s)-x(\delta_s)|^2\le\frac{3(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}\int_{\delta_s}^s\mathbb E|x(z)|^2dz+\frac{6\tau^2K_3^2}{1-6\tau^2K_3^2}\mathbb E|x(s)|^2$ .
(3.23) $\sup_{t\ge0}\mathbb E|x(t)|^2<\infty$ .
$|\mathbb E|x(t_2)|^2-\mathbb E|x(t_1)|^2|\le C(t_2-t_1)$ .
Theorem 3.3: $\lim_{t\to\infty}\mathbb E|x(t)|^2=0$ .
(3.24)–(3.25): $\mathbb E\int_0^\infty|x(t)|^2dt<\infty$ and $\liminf_{t\to\infty}|x(t)|=0$ a.s.
(3.28): $\mathbb P(\exists t:|x(t)|\ge h)\le C/h^2$ for $h>|x_0|$ .

Significance

The result. Theorem 3.4 says that a controller sampling the state at rate $1/\tau$ makes almost every trajectory of the switching system converge to the equilibrium, with an explicit, checkable bound (3.5) on $\tau$ . Mean-square convergence (Theorem 3.3) does not imply almost sure convergence in general, and a single trajectory is what an operator observes, so the pathwise statement is the one relevant to a deployed system. Condition (3.5) is stated in terms of the constants of Assumptions 2.1, 2.2 and 3.1, so for a concrete system (Section 6 of the paper) it gives a numerical bound on the observation interval.

Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a reusable definition layer: a filtration under the usual conditions, a multidimensional $\{\mathcal F_t\}$ -Brownian motion, an $\{\mathcal F_t\}$ -Markov chain with a given generator, the $L^2$ Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1).

Difficulty

Equation (2.1) is a stochastic differential delay equation with the delay $t-\delta_t$ , which is bounded but jumps at every observation time and has derivative $1$ in between. The stability theorems for hybrid delay equations in the literature require a differentiable delay with derivative less than one (Mao–Yuan, p. 285), so they do not apply. Applying $\mathcal LU$ directly to $U(x(t),r(t),t)$ leaves the term $U_x[u(x(t))-u(x(\delta_t))]$ , which has no sign and depends on the path over a whole observation interval, so a Lyapunov function of the current state alone does not close the argument.

For the goal, the natural first idea, deducing almost sure convergence from $\mathbb E|x(t)|^2\to0$ or from $\int_0^\infty|x(t)|^2dt<\infty$ a.s., fails: both are compatible with paths that make ever shorter excursions away from $0$ . The obstacle is to exclude infinitely many excursions of a fixed size, which neither moment statement controls.

Formalization scope

Conventions committed to in Lean:

The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm; the explicit constants in (3.5) and (3.21) depend on it. The diffusion $g$ is given by its $m$ columns and $|g|^2=\sum_k|g_k|^2$ (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of $\mathbb R$ at s.toNNReal.
Every expectation $\mathbb E|\cdot|^2$ and every time integral of a nonnegative quantity is a lower Lebesgue integral in $[0,\infty]$ , so a non-integrable process cannot produce a junk value $0$ .
"The solution of (2.1)" is read as every process satisfying the solution definition: progressively measurable, almost surely continuous paths, $\mathbb E|x(t)|^2<\infty$ for each $t$ , and for each $t$ , almost surely, the integral equation with Itô integrals in the $L^2$ sense. Existence and uniqueness (cited from Mao–Yuan on p. 908) are not asserted.
"An $m$ -dimensional Brownian motion" and "a Markov chain with generator $\Gamma$ " are read in the Mao–Yuan framework the paper cites: an $\{\mathcal F_t\}$ -Brownian motion with independent coordinates and increments independent of the past, and an $\{\mathcal F_t\}$ -Markov chain with transition matrix $e^{t\Gamma}$ . The usual conditions are kept as hypotheses.
"Locally Lipschitz" is uniform in the mode and time on each ball. $C^{2,1}$ carries its derivatives $U_t,U_x,U_{xx}$ as witnesses tied to $U$ by derivative relations and joint continuity.
" $\tau>0$ sufficiently small for (3.5)" means every $\tau>0$ satisfying both inequalities of (3.5). $U,\lambda_1,\lambda_2,\tau$ are data of each statement. The paper's " $C$ denotes a positive constant" is an existential chosen after $x_0$ , $r_0$ and the solution, and before the time variables and $h$ .
(3.15) and (3.21) are stated under fewer hypotheses than the surrounding proof has (Assumptions 2.1, 2.2, $\tau>0$ , and for (3.21) $\tau\le1/(4K_3)$ ), because their derivations use no more. Misprints on the page (for example $g(x,i,s)=f(x,i,0)$ on p. 909 and the swapped definitions of $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals (which vanish for non-integrable integrands), the solution notion admits the true solution and requires path continuity, the derivative witnesses of $U$ are tied to $U$ , and a sorry-free check shows that the data hypotheses (Assumptions 2.1, 2.2, 3.1, $C^{2,1}$ , (3.5)) are satisfiable, for example by $n=m=N=1$ , $f=g=0$ , $u(x)=-x$ , $U=|x|^2$ , $\lambda_1=1/4$ , $\lambda_2=1$ , $\tau=1/10$ .

Welcome contributions: the Itô isometry and Itô's formula for the $L^2$ integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, and Doob's maximal inequality in continuous time. These are reusable far beyond this mission. Section 4 of the paper (exponential stability) is a separate mission of the same series.

Selected references

S. You, W. Liu, J. Lu, X. Mao, Q. Qiu, Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations, SIAM J. Control Optim. 53(2), 905–925, 2015. https://doi.org/10.1137/140985779
X. Mao, C. Yuan, Stochastic Differential Equations with Markovian Switching, Imperial College Press, 2006. https://doi.org/10.1142/p473
X. Mao, Stabilization of continuous-time hybrid stochastic differential equations by discrete-time feedback control, Automatica 49(12), 3677–3681, 2013. https://doi.org/10.1016/j.automatica.2013.09.005

13 thms1 active userReviewed

Control Theory Operations Research Optimization+2·Captain: mikedeng1

A General Stochastic Maximum Principle for Optimal Control Problems: The Maximum Principle with First- and Second-Order Adjoint ProcessesResearch Paper

Motivation

Pontryagin's maximum principle gives necessary conditions for optimality in deterministic optimal control: along an optimal trajectory, the optimal control maximizes (or minimizes) a Hamiltonian built from an adjoint process. For a system driven by Brownian noise the analogous statement was open in full generality for two decades. The difficulty appears exactly when the diffusion coefficient depends on the control and the control domain is not convex, the situation of controlled volatility in finance, of controlled noise intensity in engineering, and of any problem whose admissible actions form a discrete or otherwise nonconvex set.

Shige Peng's 1990 paper (SIAM J. Control Optim. 28(4)) closed that case. It introduced the second-order adjoint process and a second-order variational inequality, and it is the starting point of the modern theory of stochastic Hamiltonian systems and of backward stochastic differential equations as a tool in control.

Timeline.

1972: Kushner obtains necessary conditions for diffusions whose diffusion coefficient does not depend on the control (SIAM J. Control 10).
1973–1978: Bismut introduces the adjoint equation as a linear backward stochastic differential equation and develops duality methods (SIAM Review 20).
Early 1980s: Bensoussan and Haussmann prove maximum principles for convex control domains or control-independent diffusion, using the first-order adjoint equation only.
1990: Peng proves the general principle, with control-dependent diffusion and an arbitrary nonempty control domain (this mission). In the same year Pardoux and Peng prove existence and uniqueness for nonlinear backward SDEs (Systems Control Lett. 14).
1999: Yong and Zhou give a textbook account of the theory (Springer).

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space carrying a standard $d$ -dimensional Wiener process $B=(B^1,\dots,B^d)$ , and let $\mathcal F^t=\sigma\{B(s);0\le s\le t\}$ be its natural filtration. Fix a horizon $T>0$ , an initial state $x_0\in\mathbb R^n$ and a nonempty control domain $U\subseteq\mathbb R^k$ . The data are

g:\mathbb R^n\times\mathbb R^k\to\mathbb R^n,\quad \sigma=(\sigma^1,\dots,\sigma^d),\ \sigma^j:\mathbb R^n\times\mathbb R^k\to\mathbb R^n,\quad l:\mathbb R^n\times\mathbb R^k\to\mathbb R,\quad h:\mathbb R^n\to\mathbb R .

An admissible control $v$ is a progressively measurable $U$ -valued process with $\sup_{t\le T}E|v(t)|^m<\infty$ for every $m\ge1$ . Its trajectory solves the state equation

dx(t)=g(x(t),v(t))\,dt+\sum_{j=1}^d\sigma^j(x(t),v(t))\,dB^j(t),\qquad x(0)=x_0,

and its cost is $J(v)=E\int_0^Tl(x(t),v(t))\,dt+E\,h(x(T))$ . A pair $(y,u)$ is optimal when $J(u)\le J(v)$ for every admissible $v$ .

Assumption (3): $g,\sigma,l,h$ are $C^2$ in $x$ , jointly continuous in $(x,v)$ together with their first and second $x$ -derivatives; $g_x,g_{xx},\sigma_x,\sigma_{xx},l_{xx},h_{xx}$ are bounded; and $g,\sigma,l_x,h_x$ grow at most like $C(1+|x|+|v|)$ .

The Hamiltonian is $H(x,v,p,K)=l(x,v)+(p,g(x,v))+\sum_j(K_j,\sigma^j(x,v))$ . The first-order adjoint process $(p,K)$ solves the backward equation

-dp=\Big[g_x^*p+\sum_j\sigma_x^{j*}K_j+l_x\Big]dt-\sum_jK_j\,dB^j,\qquad p(T)=h_x(y(T)),

and the second-order adjoint process $(P,Q)$ , symmetric-matrix valued, solves

-dP=\Big[g_x^*P+Pg_x+\sum_j\sigma_x^{j*}P\sigma_x^j+\sum_j\sigma_x^{j*}Q_j+\sum_jQ_j\sigma_x^j+H_{xx}\Big]dt-\sum_jQ_j\,dB^j,\qquad P(T)=h_{xx}(y(T)),

with all coefficients evaluated along $(y(t),u(t))$ and both solutions adapted to $\mathcal F^t$ .

Formalization targets

Goal: Theorem 3 (p. 975)

If $(y,u)$ is optimal, then adjoint processes $(p,K)$ and $(P,Q)$ exist in $L^2_{\mathcal F}$ , solving the two equations above, such that for every $v\in U$ , for almost every $\tau\in[0,T]$ , almost surely,

H\big(y,v,p,K-P\sigma(y,u)\big)+\tfrac12\operatorname{tr}\big(\sigma\sigma^*(y,v)P\big)\ \ge\ H\big(y,u,p,K-P\sigma(y,u)\big)+\tfrac12\operatorname{tr}\big(\sigma\sigma^*(y,u)P\big),

all evaluated at time $\tau$ .

Milestones

Lemma 1: the spike-perturbed state equals $y+y_1+y_2$ up to $o(\varepsilon^2)$ in mean square, where $y_1,y_2$ solve the first- and second-order variational equations (5), (6).
Lemma 2: the cost expansion (11) is $\ge o(\varepsilon)$ at an optimal control.
Eq. (13): existence and uniqueness of $(p,K)$ as a Riesz representer.
Eq. (14): the cost expansion in Hamiltonian form is $\ge o(\varepsilon)$ .
Eq. (17): existence and uniqueness of $(P,Q)$ as a Riesz representer.
Eq. (18): the variational inequality for these representers.
Eq. (19): $(p,K)$ is the unique solution of the first-order adjoint equation.
Eq. (20): $(P,Q)$ solves the second-order adjoint equation.

Significance

The result. Theorem 3 is the necessary condition for optimal control of diffusions in its general form. When $\sigma$ does not depend on the control the trace terms cancel and it reduces to the classical first-order principle. When the control enters the diffusion, the first-order condition is false in general, and the second-order adjoint $P$ is the correction. The theorem underlies stochastic linear-quadratic theory, the verification of optimal portfolio and volatility-control policies, and the relation between the maximum principle and the Hamilton–Jacobi–Bellman equation.

Formalizing it. The theorem is classical and proved; none of it is machine-checked. Mathlib has real Brownian motion but no stochastic integral, no SDE and no backward SDE. This mission produces the first formal statements on the platform of a controlled SDE, of a backward SDE and of the maximum principle, together with a precise definition layer (Itô integral, Itô process, BSDE solution) that later missions can reuse, e.g. for Peng's endpoint-constrained principle (§6 of the paper) or for the existence theory of BSDEs. A formal proof would also pin down the approximation arguments the paper leaves to the reader.

Difficulty

The obvious route perturbs the optimal control convexly, $u+\varepsilon(v-u)$ , and differentiates the cost. That needs $U$ convex. For nonconvex $U$ one uses a spike variation on a time interval of length $\varepsilon$ . For deterministic systems the state then moves by $O(\varepsilon)$ and a first-order expansion suffices. With control-dependent diffusion the stochastic integral over the spike interval moves the state by order $\sqrt\varepsilon$ in $L^2$ , so the first-order variational equation leaves an error of the same order as the effect being measured. Second-order terms in the state enter the cost at order $\varepsilon$ , and they are quadratic, so they cannot be handled by a single linear adjoint. The second-order expansion, the matrix-valued adjoint that represents the quadratic term, and the identification of both adjoints with backward SDEs are where the work lies. On the formal side, none of the stochastic calculus exists in Mathlib: the Itô isometry, Itô's formula for matrix-valued processes, moment estimates for linear SDEs and the martingale representation behind the backward equations all have to be built.

Formalization scope

Conventions committed to in Lean:

States, controls and noise are Fin n → ℝ, Fin k → ℝ, Fin d → ℝ with the sup norm; matrices are Matrix (Fin n) (Fin n) ℝ. Time is ℝ≥0, and time integrals are over [0, t] ⊂ ℝ.
The Wiener process is $\mathbb R^d$ -valued: the paper's " $R^n$ -valued standard Wiener process" (p. 967) is a misprint, since $\sigma(x,v)\in\mathcal L(R^d,R^n)$ . Coordinates are independent real Brownian motions (Mathlib's IsBrownianReal).
The filtration is the natural filtration of $B$ , not completed, as on p. 967.
"Adapted", for processes integrated in $dt$ , is read as progressively measurable.
The Itô integral is a relation (an $L^2$ limit of elementary integrals, as in Ikeda–Watanabe), not an operator. SDE and BSDE solutions hold "for every $t$ , almost surely", with $\sup_tE|x(t)|^2<\infty$ for forward solutions and $L^2_{\mathcal F}$ membership for backward ones.
Optimality is among admissible controls of finite cost, and the optimal cost is finite; the paper never states finiteness, and a cost can be $+\infty$ under (3).
Lemma 1 is stated with $o(\varepsilon^2)$ where the page prints " $\le C\varepsilon^2$ " in (4). The proof (via (10)) establishes $o(\varepsilon^2)$ , and Lemma 2 needs it. Lemma 1, (13), (17), (19) and (20) are stated for any admissible pair, since their proofs do not use optimality.
" $\ge o(\varepsilon)$ " means: some $r(\varepsilon)=o(\varepsilon)$ as $\varepsilon\to0^+$ bounds the left side from below for small $\varepsilon$ . " $\forall v\in U$ , a.e., a.s." quantifies $v$ first, then $\tau$ , then $\omega$ .
$P$ and $Q_j$ are symmetric-valued ( $R^{n,n}$ is the space of symmetric matrices, p. 973). Stochastic integrals against the matrix $\sigma$ or $Q$ are sums over the columns, $\sum_j(\cdot)_j\,dB^j$ .

Trivializing formalizations ruled out. Without adaptedness the backward equations have pathwise solutions with $K=0$ and the goal would be free; every adjoint and every solution is required to be progressive for the natural filtration of $B$ . The hypotheses are satisfiable: a sorry-free check shows that the zero problem has an optimal pair and that the Itô relation holds for the zero integrand.

Infrastructure needed, and reusable. The Itô integral and isometry, Itô's formula (vector and matrix forms), existence, uniqueness and moment estimates for linear SDEs with bounded coefficients, Riesz representation in $L^2_{\mathcal F}$ , and existence and uniqueness for linear BSDEs (via martingale representation for the Brownian filtration). All of these are reusable well beyond this mission; contributions of any of them, as separate theorems, are welcome. Related platform definitions: the Ethier–Kurtz series (EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE) formalizes an Itô integral by dyadic step approximation and uncontrolled SDEs over a completed filtration. The deterministic Pontryagin principle appears in Vector Space Methods XII and Dynamic Programming and Optimal Control III.

Selected references

S. Peng, A General Stochastic Maximum Principle for Optimal Control Problems, SIAM J. Control Optim. 28(4), 966–979, 1990. https://doi.org/10.1137/0328054
H. J. Kushner, Necessary Conditions for Continuous Parameter Stochastic Optimization Problems, SIAM J. Control 10(3), 550–565, 1972. https://doi.org/10.1137/0310041
J.-M. Bismut, An Introductory Approach to Duality in Optimal Stochastic Control, SIAM Review 20(1), 62–78, 1978. https://doi.org/10.1137/1020004
E. Pardoux and S. Peng, Adapted Solution of a Backward Stochastic Differential Equation, Systems & Control Letters 14(1), 55–61, 1990. https://doi.org/10.1016/0167-6911(90)90082-6
J. Yong and X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3

12 thms1 active userReviewed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

Online Network Revenue Management Using Thompson Sampling: Bayesian Regret of TS-fixedResearch Paper

Motivation

A retailer who sells several products from shared, non-replenishable inventory over a finite season must set prices without knowing how demand responds to them. Every price posted is both a sale and an experiment. This is the network revenue management problem with demand learning, and it sits between two literatures: dynamic pricing with inventory, where demand is known and the fluid linear program of Gallego and van Ryzin (1997) is the standard benchmark, and multi-armed bandits, where learning is the whole problem but there are no resource constraints.

Ferreira, Simchi-Levi and Wang (Oper. Res. 2018) combine Thompson sampling with a linear-programming step: sample a demand model from the posterior, solve the fluid LP for that model, and randomize prices according to its solution. The same paper extends the scheme to continuous price sets, contextual pricing and bandits with knapsacks.

Timeline of the relevant results:

1997: Gallego and van Ryzin introduce the fluid LP upper bound for network revenue management with known demand.
2012: Besbes and Zeevi give a non-Bayesian network pricing algorithm with worst-case regret $O(K^{5/3}T^{2/3}\sqrt{\log T})$ .
2013: Badanidiyuru, Kleinberg and Slivkins (bandits with knapsacks) give worst-case regret $O(\sqrt{KT\log T})$ .
2013–2014: Bubeck and Liu and Russo and Van Roy give prior-free Bayesian regret bounds for Thompson sampling in unconstrained bandits.
2018: Ferreira, Simchi-Levi and Wang prove the $O(\sqrt{TK\log K})$ Bayesian regret bound for TS-fixed (Theorem 1), the target of this mission.

Setting

There are $N$ products and $M$ resources. One unit of product $i$ consumes $a_{ij}\ge0$ units of resource $j$ , and resource $j$ starts with inventory $I_j\ge0$ that is never replenished. The season has $T$ periods. In each period the retailer posts one of $K$ price vectors $p_k=(p_{1k},\dots,p_{Nk})$ or a shut-off price $p_\infty$ under which demand is zero.

Given the posted price $p_k$ , the demand vector $D(t)\in\mathbb R^N_+$ has law $F(\cdot\,;p_k,\theta)$ , where $\theta\in\Theta$ is unknown and drawn from a known, arbitrary prior $\mu_0$ . Demand is independent of the past given the posted price and $\theta$ , and is bounded: $D_i(t)\in[0,\bar d_i]$ . Write $d_{ik}(\rho)$ for the mean demand of product $i$ under $p_k$ and parameter $\rho$ , and $d=d(\theta)$ .

When inventory covers all demand, all demand is sold. Otherwise the satisfied demand $\tilde D(t)$ satisfies $0\le\tilde D_i(t)\le D_i(t)$ , leaves every inventory nonnegative, and leaves at least one resource at zero; no other rule is imposed. Revenue is $\mathrm{Rev}(T)=\sum_t\sum_i\tilde D_i(t)P_i(t)$ .

For a mean-demand matrix $d$ and capacities $c_j=I_j/T$ , the linear program $\mathrm{LP}(d)$ is

\max_{x\ge0}\ \sum_{k=1}^K\Bigl(\sum_{i=1}^N p_{ik}d_{ik}\Bigr)x_k\quad\text{s.t.}\quad\sum_{k=1}^K\Bigl(\sum_{i=1}^N a_{ij}d_{ik}\Bigr)x_k\le c_j\ \ \forall j,\qquad\sum_{k=1}^K x_k\le1,

with optimal value $\mathrm{OPT}(d)$ .

TS-fixed (Algorithm 1): in each period, sample $\theta(t)$ from the posterior of $\theta$ given the history of posted prices and observed demands; let $x(t)$ be an optimal solution of $\mathrm{LP}(d(\theta(t)))$ ; post $p_k$ with probability $x_k(t)$ and $p_\infty$ with the remaining probability; observe demand and update the posterior.

Finally $p_{\max}=\max_k\sum_ip_{ik}\bar d_i$ and $p^j_{\max}=\max_{i:a_{ij}\neq0,\,k}p_{ik}/a_{ij}$ .

Formalization targets

Goal: Theorem 1 against the LP benchmark

For $K\ge2$ , $T\ge1$ , every prior, every bounded demand family, every admissible fulfilment rule and every run of TS-fixed,

\mathbb E\bigl[\mathrm{OPT}(d)\bigr]\cdot T-\mathbb E\bigl[\mathrm{Rev}(T)\bigr]\ \le\ \Bigl(18\,p_{\max}+37\sum_{i=1}^N\sum_{j=1}^M p^j_{\max}a_{ij}\bar d_i\Bigr)\sqrt{TK\log K}.

The paper prints this bound for $\mathrm{BayesRegret}(T)=\mathbb E[\mathrm{Rev}^*(T)]-\mathbb E[\mathrm{Rev}(T)]$ , where $\mathrm{Rev}^*$ is the revenue of the optimal policy that knows $\theta$ ; see Formalization scope for why the LP benchmark is stated instead.

Milestones

The article states Theorem 1 and says that its proof is in the online appendix (Supplemental Material at the DOI). The article itself contains no numbered lemma. The milestone list is therefore empty; the appendix's lemmas will be added as milestones once the appendix is held.

Significance

The bound is prior-free and has explicit constants that depend only on prices, consumption rates and demand bounds. Its dependence on $T$ matches the $\Omega(\sqrt{KT})$ lower bound for Bayesian regret in unconstrained bandits with rewards in $[0,1]$ , a special case of the model with no inventory constraints (Bubeck and Cesa-Bianchi 2012, Theorem 3.5). It shows that the posterior-sampling principle survives the addition of resource constraints, lost sales and randomized LP-based pricing, and it is the template for the paper's later results (TS-update, contextual pricing, bandits with knapsacks).

The theorem is proved on paper but, as far as a platform search shows, not formalized anywhere. The platform has a formal proof of the unconstrained Bayesian Thompson sampling bound $\sqrt{kn\log k/2}$ (BanditAlgorithm.thompson_sampling_bayesian_regret, Lattimore–Szepesvári Theorem 36.5) and an open single-product deterministic upper bound in revenue management (RevenueManagement.deterministic_upper_bound). Neither has inventory, an LP subroutine, or lost sales. A formal proof here would supply the first machine-checked analysis of Thompson sampling under resource constraints and would check the paper's constants.

Difficulty

In an unconstrained bandit, Thompson sampling's regret reduces to a sum of per-period gaps between an upper confidence bound and the sampled reward, because the sampled optimal arm and the true optimal arm are identically distributed given the history. Here the action is a randomized mixture $x(t)$ from an LP, the reward is not additive in the prices chosen, and revenue is lost when inventory runs out. Two quantities must be controlled: the revenue the algorithm would collect if all demand could be served, and the revenue lost to stock-outs. The second depends on the random time at which each resource is exhausted under a pricing rule that was optimized for a sampled, not the true, demand, and on an arbitrary fulfilment rule once some resource is empty. Standard bandit arguments do not bound such lost sales, which are a nonlinear function of the whole trajectory.

Formalization scope

Lean representation. Products, resources and price vectors are indexed by Fin N, Fin M, Fin K; the posted price is an Option (Fin K) with none the shut-off price. Periods are 0-based ( $t=0,\dots,T-1$ stands for the paper's $1,\dots,T$ ). $\Theta$ is a standard Borel space with a probability measure $\mu_0$ ; demand is a Markov kernel $F$ from $\Theta\times$ Fin K to $\mathbb R^N$ , bounded in $[0,\bar d_i]$ for every parameter. A run of TS-fixed is a family of random variables on a probability space satisfying, almost surely and via conditional expectations: $\theta\sim\mu_0$ ; the posterior-sampling property of $\theta(t)$ given everything before period $t$ ; the price draw with probabilities $x(\theta(t))$ for a measurable optimal LP selection $x$ ; the demand law given the past, $\theta(t)$ and the posted price; and fulfilment rules (a)/(b). The logarithm is natural. Prices, consumption and inventory are nonnegative (implicit in the paper). $\mathrm{OPT}(d)$ is a supremum over a nonempty bounded feasible set, so it has no junk value.

Corrections to the printed statement.

$K\ge2$ is added. At $K=1$ the printed right-hand side is $0$ , yet on a one-price instance with Bernoulli $(0.8)$ demand, $I=T/2$ and a point-mass prior, TS-fixed loses about $0.2p\sqrt T$ in expectation.
The LP benchmark replaces $\mathbb E[\mathrm{Rev}^*(T)]$ . Section 3.1.1 bounds $\mathbb E[\mathrm{Rev}^*(T)\mid d]$ by $\mathrm{OPT}(d)\cdot T$ , citing Gallego–van Ryzin. Under the paper's fulfilment rule this fails when products use disjoint resources: with two products, $I=(T,1)$ , $p_1=(1,0)$ , $p_2=(1/2,0)$ and deterministic demand $(1,1)$ , the known- $\theta$ policy earns at least $T$ while $\mathrm{OPT}(d)\cdot T=1$ . The paper states that its proof bounds the gap to "the LP benchmark defined in Section 3.1.1" (p. 1594), and the last display of Section 3.1.1 bounds $\mathrm{BayesRegret}(T)$ by exactly $\mathbb E[\mathrm{OPT}(d)]\cdot T-\mathbb E[\mathrm{Rev}(T)]$ . Wherever the Gallego–van Ryzin bound holds, the corrected goal implies the printed one.

Ruled out. A bound for the "ideal" revenue $\sum_iD_i(t)P_i(t)$ instead of the satisfied revenue, or for an arbitrary policy whose prices are merely close to the LP solution, is not Theorem 1; the goal carries the full TS-fixed run and the lost-sales accounting.

Infrastructure needed. Posterior-sampling identities for general (standard Borel) priors, a Hoeffding/Azuma-type concentration for bounded demand along the price-selection process, LP sensitivity with respect to the mean-demand matrix, and a pathwise bound on lost sales under an arbitrary fulfilment rule. The LP and fluid-benchmark definitions are reusable for later missions on TS-update (Theorem 2), contextual pricing (Theorem 4) and bandits with knapsacks (Theorem 5). Contributions welcome: proofs of the goal, and formal statements of the online appendix's lemmas.

Selected references

K. J. Ferreira, D. Simchi-Levi, H. Wang, Online Network Revenue Management Using Thompson Sampling, Operations Research 66(6):1586–1602, 2018. https://doi.org/10.1287/opre.2018.1755
G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1):24–41, 1997. https://doi.org/10.1287/opre.45.1.24
O. Besbes, A. Zeevi, Blind Network Revenue Management, Operations Research 60(6):1537–1550, 2012. https://doi.org/10.1287/opre.1120.1057
A. Badanidiyuru, R. Kleinberg, A. Slivkins, Bandits with Knapsacks, FOCS 2013. https://arxiv.org/abs/1305.2545
S. Bubeck, C.-Y. Liu, Prior-free and Prior-dependent Regret Bounds for Thompson Sampling, NeurIPS 2013. https://arxiv.org/abs/1311.0466
D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4):1221–1243, 2014. https://doi.org/10.1287/moor.2014.0650
S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://arxiv.org/abs/1204.5721
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 36. https://doi.org/10.1017/9781108571401

3 thms1 active userReviewed

Operations Research Optimization Probability+1·Captain: mikedeng1

An Optimal On-Line Algorithm for Metrical Task System 2: The Randomized Competitive Ratio of the Uniform Task System Lies Between H(n) and 2H(n)Research Paper

Motivation

Metrical task systems, introduced by Borodin, Linial and Saks (J. ACM 39(4), 1992), are a common abstraction of on-line problems in which a server occupies one of finitely many states, pays a cost for each task depending on its current state, and may pay a transition cost to change state first. Paging, list update and the $k$ -server problem all fit into this framework. The paper's first main result is that every deterministic on-line algorithm on an $n$ -state metrical task system has competitive ratio at least $2n-1$ , and that $2n-1$ is attained. The lower bound comes from an adversary that always charges the state the algorithm currently occupies. That adversary needs to know the algorithm's state, which suggests that randomization can help.

Section 7 of the paper makes this precise for the simplest system, the uniform task system, in which all transitions cost $1$ . There the randomized competitive ratio against an oblivious adversary is between $H(n)$ and $2H(n)$ , where $H(n)=1+\tfrac12+\cdots+\tfrac1n$ is between $\ln n$ and $1+\ln n$ . This was the first logarithmic bound for a task system.

Timeline:

1985: Sleator and Tarjan introduce competitive analysis for list update and paging (CACM 28(2)).
1987/1992: Borodin, Linial and Saks define metrical task systems, prove the deterministic ratio $2n-1$ , and prove $H(n)\le\bar w\le 2H(n)$ for the uniform system (conference version STOC 1987; journal version cited above).
1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the analogous $2H_k$ upper bound for randomized paging (J. Algorithms 12(4)).

Setting

A task system $(S,d)$ is a finite set $S$ of $n$ states with a transition-cost matrix $d$ : $d(i,i)=0$ , $d(i,j)>0$ for $i\ne j$ , and $d(i,k)\le d(i,j)+d(j,k)$ . In the uniform task system, $d(i,j)=1$ for all $i\neq j$ . A task is a vector $T\in\mathbb R_{\ge0}^S$ of processing costs. Given an initial state $s_0$ and tasks $\mathbf T=T^1\cdots T^m$ , a schedule is $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$ , of cost

c(\mathbf T;\sigma)=\sum_{i=1}^m d(\sigma(i-1),\sigma(i))+\sum_{i=1}^m T^i(\sigma(i)).

The off-line optimum $c_0(\mathbf T)$ is the least cost over all schedules.

A deterministic on-line algorithm chooses $\sigma(i)$ from $s_0$ and $T^1,\dots,T^i$ . A randomized on-line algorithm $R$ chooses $\sigma(i)$ at random, with a distribution that depends on $s_0$ , on $T^1,\dots,T^i$ and on the states $\sigma(0),\dots,\sigma(i-1)$ already visited. The task sequence is fixed before any random choice is made (an oblivious adversary). With $\mathrm{pr}(\sigma\mid\mathbf T)$ the probability that $R$ follows $\sigma$ , the expected cost is $\bar c_R(\mathbf T)=\sum_\sigma c(\mathbf T;\sigma)\,\mathrm{pr}(\sigma\mid\mathbf T)$ . For $w>0$ , $R$ is expected $w$ -competitive if there is a constant $K$ with

\bar c_R(\mathbf T)\le w\,c_0(\mathbf T)+K

for every finite task sequence and every initial state. The randomized competitive ratio $\bar w(S,d)$ is the infimum of all such $w$ over all $R$ .

Formalization targets

Goal: Theorem 7.1

For the uniform task system on $n\ge1$ states,

H(n)\;\le\;\bar w(S,d)\;\le\;2H(n).

Milestones

Upper bound (p. 759). Some randomized on-line algorithm is expected $2H(n)$ -competitive on the uniform task system.
Lemma 7.2 (p. 759). Let $D$ be a distribution on infinite task sequences over a finite task alphabet, with $E(c_0(\mathbf T^j))\to\infty$ , and let $m_j=\inf_A E(c_A(\mathbf T^j))$ over deterministic on-line algorithms. Then every achievable $w$ satisfies

\limsup_{j\to\infty}\frac{m_j}{E(c_0(\mathbf T^j))}\le w .

$m_j\ge j/n$ (p. 760) when the tasks are independent uniformly random unit elementary tasks $U_s$ (cost $1$ in $s$ , $0$ elsewhere).
Coupon collector (p. 760). For i.i.d. uniform states on $S$ , the expected number of draws until every state has appeared is $nH(n)$ .
Off-line cost (p. 760). Under the same distribution, $E(c_0(\mathbf T^j))\le j/(nH(n))+C$ for a constant $C$ independent of $j$ .

Significance

The theorem shows that randomization reduces the competitive ratio of the uniform task system from $2n-1$ to $\Theta(\log n)$ . That is an exponential improvement, and it identifies the adversary's knowledge of the algorithm's state as the source of the deterministic lower bound. Lemma 7.2 is a form of Yao's principle adapted to the additive-constant definition of competitiveness. It is the standard tool for randomized lower bounds in on-line computation, and the same argument shape reappears for paging and $k$ -server lower bounds.

On the formalization side, the result is proved but, as far as is known, has not been machine-checked. A complete development yields a reusable model of randomized on-line algorithms with oblivious adversaries, a Yao-type lemma usable for other on-line problems, and a coupon-collector expectation in the product-measure setting. The upper half additionally needs the continuous-time reduction of the paper's Lemma 3.1 in randomized form, or a direct discrete-time algorithm.

Difficulty

For the upper bound, the natural algorithm is continuous-time. It proceeds in phases, and inside a phase it stays in a state until that state has accumulated cost $1$ . A discrete task can saturate several states at once and straddle a phase boundary. So a discrete algorithm must either simulate the continuous one or be analyzed directly, and the expected transition count per phase must be controlled with the first phase starting in a deterministic state.

For the lower bound, the first obstacle is that the natural statement " $\bar w\ge\limsup m_j/E(c_0)$ " silently assumes that a randomized algorithm's expected cost, averaged over random inputs, is at least that of the best deterministic algorithm. With the behavioural (kernel) definition used here, this requires converting a kernel into a mixture of deterministic algorithms, which is Kuhn's theorem on each finite horizon. The second obstacle is that the paper's claim $E(c_0(\mathbf T^j))\le j/(nH(n))+O(1)$ is supported only by the elementary renewal theorem, which gives a limit of ratios; the additive bound needs a sharper renewal estimate. Mathlib has no renewal theory. The hypothesis $E(c_0(\mathbf T^j))\to\infty$ of Lemma 7.2 must also be established for the uniform distribution; the paper does not prove it separately.

Formalization scope

States form a finite nonempty type S, and $n$ = Fintype.card S; no $n\ge2$ assumption is made (at $n=1$ the goal reads $1\le\bar w\le2$ , and $\bar w=1$ ). $H(n)$ is Mathlib's harmonic n, cast to $\mathbb R$ . The uniform system has unit transition cost.
Tasks are finite and nonnegative. The paper also allows $+\infty$ entries; these are excluded. Task sequences are Fin m → S → ℝ and schedules are Fin (m+1) → S with σ 0 = s₀. $c_0$ is a finite minimum.
A randomized algorithm is a kernel S → List (S → ℝ) → List S → PMF S. This is the paper's scheduler–taskmaster description (p. 758), equivalent to a distribution over deterministic algorithms on every finite task sequence. $\mathrm{pr}(\sigma\mid\mathbf T)$ is the product of kernel probabilities, and $\bar c_R$ is a finite sum. That $\mathrm{pr}(\cdot\mid\mathbf T)$ sums to $1$ has been checked locally.
$\bar w(S,d)$ is the real sInf of $\{w : \exists R,\ R \text{ expected } w\text{-competitive}\}$ . On the empty set this would be $0$ , so the upper bound is stated as the existence of an expected $2H(n)$ -competitive algorithm, and Lemma 7.2 is stated for every achievable $w$ . The goal's lower half forces the set to be nonempty. Statements of the form " $\bar w\le c$ " alone are therefore not acceptable substitutes for milestones 1 and 2.
Lemma 7.2 is restricted to task sequences over a finite alphabet, with the product $\sigma$ -algebra and measurable singletons. This makes every $E(c_A(\mathbf T^j))$ a genuine integral for every deterministic $A$ , and it covers the paper's application. The $\limsup$ of Lemma 7.2 is taken in EReal.
The coupon-collector time takes values in $[0,\infty]$ and its expectation is a lower Lebesgue integral. Milestone 5 renders the paper's $O(1)$ as an explicit constant $C$ chosen before $j$ .

Contributions welcome: proofs of any milestone; a discrete-time randomized phase algorithm; a general Kuhn-type conversion from kernels to mixtures of deterministic algorithms; renewal-theoretic lemmas.

Selected references

A. Borodin, N. Linial, M. Saks, An Optimal On-Line Algorithm for Metrical Task System, J. ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Commun. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
A. C.-C. Yao, Probabilistic Computations: Toward a Unified Measure of Complexity, FOCS 1977, 222–227. https://doi.org/10.1109/SFCS.1977.24
S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970 (the elementary renewal theorem cited as [20] in the paper).

9 thms1 active userReviewed

Completed

Number Theory·Captain: Yuxuan Xu

Equal Sums of Two Squares: Parametrization and Infinite Primitive FamiliesResearch Paper

Motivation

The representation function $r_{2}(n)=\#\{(a,b)\in\mathbb Z^{2}:a^{2}+b^{2}=n\}$ is one of the oldest objects in number theory. Fermat characterised the integers with $r_{2}(n)>0$ — those in which every prime congruent to $3$ modulo $4$ occurs to an even power — and Euler's proof supplied the closed form $r_{2}(n)=4\,(d_{1}(n)-d_{3}(n))$ , where $d_{j}(n)$ counts divisors congruent to $j$ modulo $4$ (sum of two squares theorem).

That description counts representations but does not relate them to one another. The integers carrying several essentially different representations,

50=1^{2}+7^{2}=5^{2}+5^{2},\qquad 65=1^{2}+8^{2}=4^{2}+7^{2},

are exactly the integers that produce quadruples $(a,b,c,d)$ with

a^{2}+b^{2}=c^{2}+d^{2}

whose two sides are not identified by swapping the two entries or changing their signs. Three reasons make this relation worth a formal development rather than a passing remark.

Energy counts. Counting solutions of the equation inside a box is the additive energy of the set of sums of two squares, the quantity controlling mean-square errors for $r_{2}$ ; it is a genuinely different problem from determining $r_{2}(n)$ for a single $n$ , and every estimate for it starts from a description of the solution set.
Composition of representations. The Brahmagupta–Fibonacci identity

(p^{2}+q^{2})(r^{2}+s^{2})=(pr+qs)^{2}+(ps-qr)^{2}=(pr-qs)^{2}+(ps+qr)^{2}

takes two representations and produces a third. Known to Brahmagupta and stated by Fibonacci in Liber Quadratorum (1225), it is the multiplicativity of the norm in the Gaussian integers, and it is the engine behind every statement below.

Geometry. Over a field, the locus $a^{2}+b^{2}=c^{2}+d^{2}$ in projective three-space is the split quadric, isomorphic to $\mathbb P^{1}\times\mathbb P^{1}$ under the Segre embedding; the four parameters introduced below are Segre coordinates in this sense. The arithmetic content of the equation is precisely the integrality that this geometry ignores.

The parametrisation targeted here is classical. Nothing in this mission claims new mathematics; the aim is a machine-checked development in which every hypothesis is explicit.

Setting

Fix integers. A solution is a quadruple $(a,b,c,d)\in\mathbb Z^{4}$ with $a^{2}+b^{2}=c^{2}+d^{2}$ . It is trivial if the multisets $\{a^{2},b^{2}\}$ and $\{c^{2},d^{2}\}$ coincide, i.e. if $(c,d)$ equals $\pm(a,b)$ or $\pm(b,a)$ ; if entries are allowed to vanish, the least value carried by a non-trivial solution is $25=0^{2}+5^{2}=3^{2}+4^{2}$ , and requiring all four entries to be positive raises that value to $50$ . A solution is primitive when the four entries have greatest common divisor $1$ , and positive when all four entries are positive and pairwise distinct — the case in which nothing about the relation is explained by signs, zeros or coincidences.

Two constructions produce solutions. The four-parameter family associates to integers $p,q,r,s$ the quadruple

a=pr+qs,\qquad b=ps-qr,\qquad c=pr-qs,\qquad d=ps+qr,

which solves the equation because both sides equal $(p^{2}+q^{2})(r^{2}+s^{2})$ by the identity above. Substituting particular parameters is unrevealing, so a genuine supply comes instead from the elementary one-parameter family

1^{2}+(n^{2}-n+1)^{2}=(2n-1)^{2}+(n^{2}-n-1)^{2},

whose four entries $1$ , $n^{2}-n+1$ , $2n-1$ , $n^{2}-n-1$ are strictly increasing — hence positive and pairwise distinct — as soon as $n\ge 4$ . The bound is sharp: at $n=3$ the two entries $2n-1$ and $n^{2}-n-1$ are equal.

In the reverse direction, rewrite the equation as $(a+c)(a-c)=(d+b)(d-b)$ and set

X=(a+c)/2,\quad Y=(a-c)/2,\qquad U=(b+d)/2,\quad V=(d-b)/2 .

The halves are integers exactly when $a$ and $c$ share a parity and so do $b$ and $d$ , and in that case the equation becomes

XY=UV .

The development is organised in the namespace TwoSquares, with node names matching the roles above (four_param_identity, explicit_family_chain, sum_sq_eq_halves, four_factor_param, complete_parametrization).

Formalization targets

Goal — completeness of the four-parameter family

For all integers $a,b,c,d$ with $a^{2}+b^{2}=c^{2}+d^{2}$ , there are integers $p,q,r,s$ with

a=pr+qs,\quad b=ps-qr,\quad c=pr-qs,\quad d=ps+qr,

possibly after interchanging $c$ and $d$ . The goal asserts only the existence of integral parameters and the necessity of at most one swap; it does not assert uniqueness of $(p,q,r,s)$ , which is false, and it says nothing about how many solutions lie in a given box.

The four-parameter identity

The identity itself, over an arbitrary commutative ring, together with the two forms of the Brahmagupta–Fibonacci identity that imply it — so that the reason it holds, rather than the expansion, is what is recorded.

An explicit infinite family

For every integer $n\ge 4$ the displayed family is a positive pairwise distinct solution; the parametrisation $n\mapsto(1,\,n^{2}-n+1,\,2n-1,\,n^{2}-n-1)$ is injective; the set of quadruples it produces is infinite; and no member is a nontrivial integer multiple of another, each member being primitive.

From the sum-of-squares equation to $XY=UV$

The equivalence of $a^{2}+b^{2}=c^{2}+d^{2}$ with $(a+c)(a-c)=(d+b)(d-b)$ ; the parity statement that matching entries share a parity after at most one swap; and the resulting existence of the half-sum variables satisfying $XY=UV$ .

Parametrizing $XY=UV$

For all integers $X,Y,U,V$ with $XY=UV$ there are integers $p,q,r,s$ with $X=pr$ , $Y=qs$ , $U=ps$ , $V=qr$ — the coordinate form of the statement that a rank-one $2\times2$ matrix factors through the integers.

Significance

The result. Taken together, the reverse chain converts the Diophantine equation $a^{2}+b^{2}=c^{2}+d^{2}$ into four free integer parameters, at the cost of one possible swap. In that form every question about the solution set becomes a question about four independent variables, which is what makes energy estimates, density statements and searches for primitive solutions tractable. The chain also isolates where integrality enters: over a field the parametrisation of $XY=UV$ is formal, so the content is carried entirely by the parity step and by divisibility over $\mathbb Z$ .

Formalizing it. None of the mathematics is new, and that is the point: the value here is a development in which each link is a reusable statement with explicit hypotheses. Three conventions make the nodes reusable rather than bespoke. The algebraic identity is proved over a general commutative ring, not over $\mathbb Z$ . The positivity and distinctness of a family are packaged as one strict chain rather than as a list of inequalities, since later arguments use the ordering, not merely the disequalities. The parity issue is isolated into a single node stating a disjunction, instead of being discharged by case splits buried inside a later proof. Conversely, the shape of the final theorem records honestly what is not claimed: parameters are not unique, and no normal form is asserted.

As difficulty, the early nodes have short proofs, while completeness requires the full chain and is the substantial part of the mission.

Difficulty

The obvious first idea is to use the Gaussian integers: $a+bi$ and $c+di$ have the same norm, so factor both and compare. It fails. Equal norm does not make two Gaussian integers associates or divisors of one another — $1+8i$ and $4+7i$ both have norm $65$ and are related by no divisibility — because uniqueness of factorisation regroups prime factors in ways that the norm alone cannot distinguish. The correct route recovers the four parameters from the product equation instead, and there the friction is entirely arithmetic:

Clearing halves. The substitution $X=(a+c)/2$ is not available for arbitrary solutions: $a^{2}+b^{2}=c^{2}+d^{2}$ forces only that the multiset of parities of $(a,b)$ matches that of $(c,d)$ , so $(a,c)$ may have different parities and no integer $X$ may exist. The example $a=1,b=0,c=0,d=1$ shows this is not vacuous, and it is why the goal carries a swap.

Factoring $XY=UV$ . Taking $p=\gcd(X,U)$ yields $X=pr$ , $U=ps$ with $\gcd(r,s)=1$ , and Euclid's lemma then forces $s\mid Y$ and $r\mid V$ . The degenerate case $X=U=0$ — where the gcd vanishes and no cancellation is possible — must be handled separately, and because the variables range over $\mathbb Z$ rather than $\mathbb N$ , every divisibility step must be tracked with signs. Working over a ring where division is available would delete both issues and with them the entire content of the statement.

Formalization scope

All nodes are stated over $\mathbb Z$ , except the Brahmagupta–Fibonacci identity and the four-parameter identity, which are proved over an arbitrary commutative ring. No node is stated over $\mathbb N$ ; transporting the prime-level statements is out of scope.
Gaussian integers are deliberately unused. Mathlib carries them, but nothing here needs them, and a development depending on them would obscure the arithmetic that actually carries the proof.
No quotient types, no permutation machinery: the possible swap of $c$ and $d$ is expressed as a disjunction, and the parity statement as a disjunction over Even.
Trivializing formalizations are excluded. Over a field the parametrisation of $XY=UV$ holds trivially (take $p=X$ , $r=1$ , $s=U/X$ ), so the quarter-ring version carries no information; likewise, a completeness statement whose hypotheses already postulate the existence of the parameters would be vacuous. Both are explicitly not what is asked for.
Expected to be reusable beyond this mission: the two forms of the Brahmagupta–Fibonacci identity; the strict-chain packaging of positivity and distinctness for a family given by polynomials; and the integer parametrisation of $XY=UV$ , which is the Segre parametrization.
Contributions are welcome for any node, and especially for the integer factoring lemma, for which several proofs are available. Explicitly out of scope: uniqueness or normal forms for $(p,q,r,s)$ , counting asymptotics for solutions in a box, the Gaussian-integer reformulation, and all $\mathbb N$ -level variants.

Selected references

Sum of two squares theorem — Fermat's characterisation and Euler's divisor formula for $r_{2}$ .
Brahmagupta–Fibonacci identity — the two-square composition identity, its history, and its interpretation through norms.
Leonardo Pisano (Fibonacci), Liber Quadratorum, 1225. English translation: L. E. Sigler, The Book of Squares, Academic Press, 1987.
G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008 — Chapter XX on representations by two squares.
Segre embedding — the identification of the rank-one quadric in $\mathbb P^{3}$ with $\mathbb P^{1}\times\mathbb P^{1}$ .

13 thms1 active userReviewed

Completed

Analysis Machine Learning·Captain: Minghui

Sharp Minima Can Generalize: ReLU Rescaling and Hessian SharpnessResearch Paper

Why the geometry of a minimum needs a parameter convention

A trained neural network is used through its predictions, while its parameters are the coordinates in which training takes place. Distinct parameter vectors can describe exactly the same prediction function. A proposed explanation of generalization based on the shape of the parameter-space loss therefore needs to account for these equivalences. This mission concerns Hessian sharpness: the spectral norm of the matrix of second derivatives of the loss at a minimum. The question is whether that number is intrinsic to the predictor or can change without changing any prediction.

Dinh, Pascanu, Bengio, and Bengio establish that, for a one-hidden-layer rectified network, every sufficiently differentiable critical minimum with nonzero Hessian has equivalent parameterizations of arbitrarily large Hessian sharpness. The formalization target is their Section 4.2, Theorem 4, PDF pp. 5–6. The goal theorem and both supporting milestones now have accepted Lean proofs on Prove2Me. This public research-paper mission is complete.

The immediate historical sequence is:

2016–2017: Keskar and collaborators reported numerical evidence relating large-batch training, sharp minima, and a generalization gap. This is empirical context, not an assumption or a theorem to be proved in this mission. ICLR 2017 paper.
March 2017: Dinh and collaborators released a mathematical analysis of parameter symmetries and several flatness measures. The fixed source for this mission is their May 2017 revision, arXiv version 2, which determines the theorem numbering and PDF page citations. Version history.

Networks, losses, and reciprocal layer scaling

Fix positive integers $d$ and $h$ , the input dimension and hidden width. Let $W\in\mathbb R^{d\times h}$ and $v\in\mathbb R^h$ be the network's weights. For an input $x\in\mathbb R^d$ , define

f_{W,v}(x)=\sum_{j=1}^h \max\!\left(\sum_{i=1}^d x_iW_{ij},0\right)v_j.

This is a bias-free network with one hidden layer, rectified activation, and a scalar linear output. Its parameter vector $\theta=(W,v)$ has $n=dh+h$ coordinates and the Euclidean norm. A function-based loss is a real-valued functional $\ell$ of the entire prediction function, giving $L(\theta)=\ell(f_\theta)$ . The Hessian targets assume $L$ is continuous. These conventions come from Sections 2–3, PDF pp. 2–4, Definition 3.

Two parameters are observationally equivalent if their predictions agree on every input. For a positive real number $\alpha$ , the layer scaling is

T_\alpha(W,v)=(\alpha W,\alpha^{-1}v).

The definition rescales the incoming and outgoing weights in opposite ways. It is the transformation in Section 3, Definition 5, PDF p. 4.

Write $DL(\theta)$ for the first Fréchet derivative and $H_L(\theta)=D(DL)(\theta)$ for the second derivative. The local differentiability condition requires $L$ to be differentiable throughout a neighborhood of $\theta$ , with $DL$ differentiable at $\theta$ . This states the regularity needed for the paper's Hessian notation explicitly, without requiring global smoothness or continuous second derivatives. A critical local minimum satisfies $DL(\theta)=0$ and has no smaller loss in some neighborhood; it may belong to a continuum of minima.

Symmetry, derivative transformation, and the goal theorem

The first milestone formalizes the scaling consequence of positive ReLU homogeneity in Theorem 1 and Definition 5, PDF p. 4:

f_{T_\alpha\theta}=f_\theta,\qquad L(T_\alpha\theta)=L(\theta),

and $T_\alpha\theta$ is a local minimum precisely when $\theta$ is. These statements hold for every parameter and every $\alpha>0$ ; the milestone itself requires no loss regularity.

The second milestone is Theorem 3, Section 4.2, PDF p. 5. At every point satisfying the stated local differentiability condition,

DL(T_\alpha\theta)[u]=DL(\theta)[T_{\alpha^{-1}}u],

H_L(T_\alpha\theta)[u,w] =H_L(\theta)[T_{\alpha^{-1}}u,T_{\alpha^{-1}}w]

for all parameter directions $u,w$ . The same regularity holds at the rescaled point. This is the coordinate-free form of the paper's gradient formula and Hessian congruence with $D_\alpha=\operatorname{diag}(\alpha^{-1}I_{dh},\alpha I_h)$ .

The goal is Theorem 4. If $\theta$ is a critical local minimum with the stated differentiability and $H_L(\theta)\ne0$ , then

\forall M>0\ \exists\alpha>0:\qquad \|H_L(T_\alpha\theta)\|_2\ge M.

For that same rescaling, predictions and loss agree with the original ones, and the transformed parameter remains a critical local minimum with the required differentiability. The subscript $2$ denotes the Euclidean spectral norm. The source statement and its interpretation are in Section 4.2, PDF pp. 5–6. The relevant displays in all three targets are unnumbered.

What the formalization establishes

The result separates prediction behavior from this particular numerical measure of parameter-space curvature. Pointwise identical predictors have identical function-based evaluation losses wherever those are defined, even though their Hessian sharpness can be made arbitrarily large under the stated conditions. This is the scope of the obstruction: it concerns the unnormalized Euclidean Hessian norm and this rescaling symmetry. It does not assert that training reaches every point on a scaling orbit or supply a numerical bound on test error. Theorem 4 and following discussion, PDF p. 6.

The completed Lean development connects an explicitly computed ReLU prediction function to its actual first and second derivatives. It provides reusable results about invariant losses, transport of local minima, and curvature under linear changes of parameters. All three published theorem statements were proved unchanged and accepted on 26 September 2026. Both milestones are complete, and the goal has no remaining open leaves.

The analytic obligations

ReLU is not differentiable at every activation boundary. The loss-level local regularity must therefore be retained rather than inferred from the network's syntax. A nonzero symmetric matrix alone is also insufficient for the sharpness claim: local minimality supplies an additional sign constraint. Finally, the second derivative is an operator on the entire parameter space; bounds for a single arbitrarily chosen scalar model do not establish the quantified network result. These are obligations of the formal proof, not hypotheses assuming the desired transformation identities.

Formalization note: scope and conventions

Parameters are represented by EuclideanSpace over the disjoint union of first-layer matrix coordinates and output-weight coordinates. This retains the sum-of-squares geometry rather than a product maximum norm. The Hessian is the derivative of the actual Fréchet derivative, represented as a continuous bilinear form. Its operator norm is the spectral norm under the Euclidean/Riesz identification. The regularity condition excludes reliance on default derivative values at nondifferentiable points.

The statement covers every positive input dimension and hidden width, arbitrary function-based losses with the specified regularity, and arbitrary qualifying minima. It imposes no separate nonzero-weight or active-neuron assumption. An input or output weight block may vanish when the loss hypotheses still hold. The nonzero-Hessian requirement is essential. Scaling by zero or a negative number is outside the claim. No probability model, random initialization, sampling measure, or training algorithm is assumed.

The mission focuses on the single-hidden-layer Hessian result. Volume flatness, the multiple-eigenvalue deep-network theorem, and other reparameterizations remain separate results in the paper. The local environment is Lean 4.30.0 with supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f.

Selected references

Laurent Dinh, Razvan Pascanu, Samy Bengio, Yoshua Bengio. Sharp Minima Can Generalize For Deep Nets. ICML 2017, PMLR 70:1019–1028. arXiv:1703.04933v2. Primary anchors: Section 2, PDF p. 2; Section 3, PDF pp. 3–4, Definitions 3–5 and Theorem 1; Section 4.2, PDF pp. 5–6, Theorems 3–4.
Nitish Shirish Keskar, Dheevatsa Mudigere, Jorge Nocedal, Mikhail Smelyanskiy, Ping Tak Peter Tang. On Large-Batch Training for Deep Learning: Generalization Gap and Sharp Minima. ICLR 2017. arXiv:1609.04836v2. Historical context.

4 thms1 active userReviewed

Completed

Machine Learning Probability·Captain: Minghui

Neural Tangent Kernel: The Infinite-Width Initialization LimitResearch Paper

Why an initialization kernel matters

A neural network is nonlinear in its parameters, but a small change in those parameters changes its predictions through a Jacobian. The neural tangent kernel is the Gram kernel of that Jacobian: it records which changes in predictions can be produced by common parameter updates. An initialization limit identifies a deterministic object behind this random kernel. It supplies a mathematical starting point for studying wide networks through kernel methods, before addressing the additional question of how the kernel changes during training. Jacot, Gabriel, and Hongler establish this initialization limit in Section 4.1, Theorem 1, PDF p. 5.

The requested result is already a theorem of the paper. The open work here is its formal proof in Lean, including the probability model and the order of limits. The mission is classified as OpenProblem at the request of its proposer; that label does not assert that the underlying mathematical result remains an unsolved research question.

The source appeared in 2018 and was published at NeurIPS 2018; this formalization fixes arXiv version 4, dated February 10, 2020, so that page references and conventions remain stable. Its Appendix A explicitly distinguishes the sequential limit proved there from a possible stronger simultaneous-width limit.

Networks, randomness, and the two kernels

Fix positive integers $d$ and $q$ , the input and output dimensions, a hidden-layer count $h\ge0$ , a bias scale $\beta>0$ , and a Lipschitz function $\sigma:\mathbb R\to\mathbb R$ . Write $L=h+1$ for the number of affine layers, with $n_0=d$ , $n_L=q$ , and positive hidden widths $n_1,\ldots,n_h$ . The parameters are all entries of the weight matrices and bias vectors. Every parameter is sampled independently from $\mathcal N(0,1)$ .

For an input $x$ , let $a^{(0)}(x)=x$ and define

z^{(\ell+1)}_j(x)=\frac1{\sqrt{n_\ell}} \sum_i W^{(\ell)}_{ji}a^{(\ell)}_i(x)+\beta b^{(\ell)}_j.

At each hidden layer, $a^{(\ell)}=\sigma(z^{(\ell)})$ coordinatewise. The output is $f_\theta(x)=z^{(L)}(x)$ , with no final activation. These are the conventions of Section 2, PDF pp. 2–3. Matrix storage order in Lean uses destination then source; the displayed operation is unchanged.

For output coordinates $k,k'$ , set

\Theta^{(L)}_{kk'}(\theta;x,y)=\sum_p \partial_{\theta_p}f_{\theta,k}(x)\, \partial_{\theta_p}f_{\theta,k'}(y).

The sum includes every weight and every bias, as in Section 4, PDF p. 5.

The covariance kernel starts with

\Sigma^{(1)}(x,y)=\frac{\langle x,y\rangle}{d}+\beta^2.

Given a centered Gaussian pair $(U,V)$ with covariance matrix obtained by evaluating $\Sigma^{(\ell)}$ on $(x,y)$ , define

\Sigma^{(\ell+1)}(x,y)=\mathbb E[\sigma(U)\sigma(V)]+\beta^2, \qquad \dot\Sigma^{(\ell+1)}(x,y)=\mathbb E[\sigma'(U)\sigma'(V)].

The deterministic limiting NTK is

\Theta_\infty^{(1)}=\Sigma^{(1)},\qquad \Theta_\infty^{(\ell+1)}(x,y)=\Theta_\infty^{(\ell)}(x,y) \dot\Sigma^{(\ell+1)}(x,y)+\Sigma^{(\ell+1)}(x,y).

These recurrences appear in Section 4.1, Proposition 1 and Theorem 1, PDF p. 5; their displays are unnumbered.

Formalization targets

The goal is Theorem 1, on every fixed finite family $X=(x_1,\ldots,x_N)$ of inputs and for every $\varepsilon>0$ :

\Pr\!\left(\exists i,j,k,k': \left|\Theta^{(L)}_{kk'}(\theta;x_i,x_j) -\Theta_\infty^{(L)}(x_i,x_j)\delta_{kk'}\right|>\varepsilon\right) \longrightarrow0.

Here $\delta_{kk'}$ is one when the output coordinates coincide and zero otherwise. The limit takes $n_1\to\infty$ first, then $n_2\to\infty$ , through $n_h\to\infty$ , precisely as specified in Appendix A, PDF p. 11, and Appendix A.1, PDF pp. 12–13.

Two supporting milestones expose the required mathematical content. First, the recursively defined $\Sigma^{(L)}$ has positive semidefinite Gram matrices on every finite input family and satisfies $\Sigma^{(L)}(x,x)\ge\beta^2$ . This is a paper-derived well-definedness obligation for the covariance in Proposition 1. Second, Proposition 1 asserts joint convergence in distribution of $(f_{\theta,k}(x_i))_{i,k}$ to the centered Gaussian vector with covariance $\Sigma^{(L)}(x_i,x_j)\delta_{kk'}$ . This expresses the paper's independent output Gaussian processes through all their finite-dimensional distributions.

What completing the mission would establish

The result connects an explicitly parameterized random finite network to a deterministic kernel computed from its activation and depth. All output correlations, bias contributions, and layer normalizations remain visible in that connection. It would provide a checked foundation on which a separate training-stability development could build.

The formal contribution is the passage from finite random Jacobians to the limiting kernel. It does not assume that the empirical NTK already equals its limit. Nor does the goal claim convergence of a training trajectory, positive definiteness on a sphere, an early-stopping guarantee, or a generalization bound; those are separate results and questions in the source.

Where the mathematical work lies

The parameter space changes with the widths. Outputs, hidden activations, and their parameter derivatives are dependent random quantities, so the limit of their products requires more than a scalar law of large numbers. The weak Gaussian limit alone also does not justify substituting an arbitrary discontinuous derivative into expectations. The Lipschitz-only hypothesis is part of the target and must be retained, including for nonsmooth activations. Remark 3, PDF p. 5 identifies almost-everywhere differentiation as the relevant convention.

Formalization scope and conventions

Lean represents parameter coordinates by a finite dependent index carrying a layer, destination neuron, and optional source neuron; the missing source denotes a bias. Initialization is the finite product of Mathlib's standard Gaussian measures. Network outputs are obtained by the displayed recursion, and NTK entries use actual Fréchet derivatives in coordinate directions. Mathlib's derivative is zero where differentiation fails; the proof must establish that the exceptional parameters are null under the stated initialization law.

Centered Gaussian laws use Mathlib's multivariateGaussian, including singular covariance. The covariance-validity milestone must justify its covariance interpretation. No invertibility, distinct-input, smooth-activation, or positive-definite-kernel assumption is added. Positive actual hidden widths are indexed as $w_i+1$ for $w_i\in\mathbb N$ , a cofinal reindexing. Depth one, constant activations, repeated or zero inputs, and empty finite families are included. The empty family is harmless because the same theorem quantifies over every nonempty family as well.

The sequential filter puts the last hidden width outermost. For two hidden widths, a probability tolerance is met by first choosing a threshold for $n_2$ , then a threshold for $n_1$ that may depend on $n_2$ . There is no uniform limit over the entire input space and no simultaneous-width assertion. The development uses Lean 4.30.0 and supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The model and statements are locally checked; the three theorem proofs remain open. Contributions to Gaussian covariance consistency, finite-dimensional distribution limits, almost-everywhere network differentiation, and the NTK limit are in scope.

Selected references

Arthur Jacot, Franck Gabriel, and Clément Hongler, Neural Tangent Kernel: Convergence and Generalization in Neural Networks, Advances in Neural Information Processing Systems 31, 2018. arXiv:1806.07572v4. Primary anchors: Section 2, PDF pp. 2–3; Section 4.1, PDF p. 5, Proposition 1, Theorem 1, Remarks 2–3; Appendix A and A.1, PDF pp. 11–13. Relevant displays have no equation numbers.

4 thms1 active userReviewed

Completed

Machine Learning Optimization Probability·Captain: Minghui

Optimization Methods for Large-Scale Machine Learning: Stochastic Gradient ConvergenceResearch Paper

Why stochastic-gradient convergence matters

Training a machine-learning model often means choosing a vector of parameters to minimize an average loss. Evaluating the full gradient can require processing an entire dataset. A stochastic-gradient method instead updates the parameters using a random direction obtained from a smaller amount of information. Its computational appeal raises a mathematical question: which assumptions on those directions and the stepsizes guarantee progress, and what kind of convergence follows?

This mission formalizes the core convergence theory in Section 4 of Bottou, Curtis, and Nocedal, Optimization Methods for Large-Scale Machine Learning. The results distinguish strongly convex objectives, where expected objective error can be controlled, from general smooth objectives, where the guarantee concerns gradients. They also distinguish constant stepsizes, which leave a noise-dependent error bound, from diminishing stepsizes.

Historical timeline

1951: Robbins and Monro introduced stochastic approximation for finding a root using noisy observations. Their work is the historical foundation for the stepsize conditions used here; the original root-finding theorem is not a separate target of this mission. Original paper.
2016: Bottou, Curtis, and Nocedal released the first version of their survey, organizing stochastic-gradient theory around smoothness and moment assumptions. arXiv record.
2018: The revised survey appeared in SIAM Review. This mission fixes arXiv version 3 for stable theorem numbering and PDF page citations. Published article.

The mathematics targeted here is already proved in the literature; the task is its Lean formalization, not a claim that these convergence results are unresolved research conjectures.

Objective, algorithm, and probability model

Let $F:\mathbb R^d\to\mathbb R$ be differentiable with an $L$ -Lipschitz gradient, where $L>0$ . On a probability space $(\Omega,\mathcal A,\mathbb P)$ , let $\mathcal H_k$ contain the history before step $k$ . Starting from a deterministic vector $w_0$ , the algorithm uses positive deterministic stepsizes $\alpha_k$ and random directions $g_k$ to update

w_{k+1}=w_k-\alpha_k g_k.

The state $w_k$ is measurable with respect to $\mathcal H_k$ ; the direction $g_k$ is measurable with respect to $\mathcal H_{k+1}$ and has a finite second moment. Conditional assertions hold almost surely. This uses the adapted-process formulation expressly permitted in footnote 4, PDF p. 22, rather than requiring independent sample seeds. The local index $k=0$ corresponds to the paper's $k=1$ . Algorithm 4.1 and footnote 4.

Write $\mathbb E_k$ for conditioning on $\mathcal H_k$ . The moment conditions use constants $\mu_G\ge\mu>0$ and $M,M_V\ge0$ :

\langle\nabla F(w_k),\mathbb E_k g_k\rangle\ge\mu\|\nabla F(w_k)\|^2, \qquad \|\mathbb E_k g_k\|\le\mu_G\|\nabla F(w_k)\|,

\mathbb E_k\|g_k\|^2-\|\mathbb E_k g_k\|^2 \le M+M_V\|\nabla F(w_k)\|^2.

Define $M_G=M_V+\mu_G^2$ . The iterates lie almost surely in an open region on which $F\ge F_{\inf}$ for a real lower bound $F_{\inf}$ . These are Assumptions 4.1 and 4.3, PDF pp. 23–24, equations (4.6)–(4.9). Source.

Formalization targets

The goal is Theorem 4.10, Section 4.3, PDF p. 33, equations (4.30a)–(4.30b). Suppose

\sum_{k=0}^\infty\alpha_k=\infty,\qquad \sum_{k=0}^\infty\alpha_k^2<\infty.

For $A_K=\sum_{k=0}^{K-1}\alpha_k$ , establish both

\exists S\in\mathbb R:\quad \mathbb E\!\left[\sum_{k=0}^{K-1}\alpha_k\|\nabla F(w_k)\|^2\right]\longrightarrow S,

\frac{1}{A_K}\mathbb E\!\left[\sum_{k=0}^{K-1}\alpha_k\|\nabla F(w_k)\|^2\right] \longrightarrow0.

There is no convexity assumption and no restriction that the initial stepsizes already satisfy a small-step bound. Theorem 4.10.

Four milestones capture the surrounding theory. Lemma 4.4 gives the two successive conditional expected-descent inequalities (4.10a)–(4.10b), PDF pp. 24–25. It is a common input to the convergence results. Theorem 4.6 gives a geometric upper bound for strongly convex objectives with a constant stepsize. Theorem 4.7 gives the corresponding $O(1/k)$ bound for $\alpha_k=\beta/(\gamma+k+1)$ . These are parallel strongly convex targets, not prerequisites for the nonconvex goal. Theorem 4.8 gives finite-horizon sum and average squared-gradient bounds for general objectives with a constant stepsize. Section 4.

For example, if $c>0$ is the strong-convexity constant, $d\ge1$ , and $0<a\le\mu/(LM_G)$ , Theorem 4.6 states, with $B=aLM/(2c\mu)$ and $F_*=\inf_xF(x)$ ,

\mathbb E[F(w_k)-F_*]\le B+(1-ac\mu)^k(F(w_0)-F_*-B).

The upper bound tends to $B$ ; this does not assert that the actual expected error tends to $B$ . Every milestone retains the paper's constants and all displayed conclusions. Equations (4.13)–(4.14), PDF p. 26.

What a completed formalization provides

The result explains precisely how noise and stepsize interact. The general-objective goal guarantees that the stepsize-weighted expected squared gradients average to zero even when $M>0$ . The strongly convex milestones quantify objective error and the effect of initialization. These results concern the stated quantities; they do not assert convergence of iterates, global optimality for a nonconvex objective, or almost-sure convergence. Sections 4.2–4.3.

A completed development would provide reusable Lean results for smooth objective functions, conditional moment bounds, stochastic updates, and expected convergence. The proposed statements are open proof obligations. Compilation establishes that the definitions and statements are well formed, not that their convergence claims have already been proved.

Mathematical and formal difficulties

Finite conditional expectations must be connected to unconditional integrals without relying on total-function defaults. The infinite-horizon result also requires careful handling of a finite initial segment: square summability gives eventually small steps, not a bound at every step. Strong convexity must justify the objective-gap estimates and the properties of the optimum. Treating a descent recurrence as a hypothesis would omit the analytic content that this mission is intended to formalize.

Formalization scope

The model uses real finite-dimensional Euclidean space, Mathlib gradients, filtrations, Bochner conditional expectations, and ordinary real integrals. The probability space is arbitrary; no finite-support or standard-Borel restriction is imposed. Directions have explicit finite second moments, making the finite-expectation convention in the paper visible. Square integrability of iterates and integrability of losses are consequences to establish, not extra model fields.

Strong convexity uses Mathlib's StrongConvexOn, equivalent here to Assumption 4.5's first-order inequality. The optimum is defined as the infimum of the range of $F$ , with its finiteness to be derived in the strongly convex branch. That branch requires $d\ge1$ : the paper's deduction $c\le L$ implicitly uses a nontrivial space. The nonconvex statements allow $d=0$ . Zero noise is allowed. Finite-horizon averages require $K>0$ ; the value assigned at $K=0$ does not affect an asymptotic limit.

Contributions to the conditional-descent infrastructure and any of the four milestones are welcome. Variance reduction, Newton-type methods, and the remainder of the survey are outside this initial mission.

Selected references

Léon Bottou, Frank E. Curtis, and Jorge Nocedal. Optimization Methods for Large-Scale Machine Learning. SIAM Review 60(2), 223–311, 2018. arXiv:1606.04838v3; DOI. All page numbers above refer to the 95-page arXiv v3 PDF.
Herbert Robbins and Sutton Monro. A Stochastic Approximation Method. Annals of Mathematical Statistics 22(3), 400–407, 1951. DOI. Historical background only.

6 thms1 active userReviewed

Completed

Number Theory·Captain: willcook

Weighted support criteria for reciprocal Mersenne subseries (Erdős #257)Research Paper

Motivation

For every integer base $b\ge2$ , a finite-prime weighted summability witness on a positive-integer host $H$ makes the reciprocal Mersenne series irrational on every infinite subset of $H$ . A base-two witness gives that conclusion at every integer base. This is the source paper's proved Theorem 1; Erdős's unrestricted question for every infinite support remains outside its conclusion.

Setting

For an integer $b\ge2$ , write $X_A(b)=\sum_{a\in A}(b^a-1)^{-1}$ . Given a finite nonempty set $P$ of primes, let $h_P(a)=\prod_{p\in P}p^{v_p(a)}$ be the $P$ -part of $a$ , and set

W_{b,P}(A)=\sum_{a\in A}\frac{h_P(a)}{a(b^{h_P(a)}-1)}.

All support elements are positive. The prime set specifies the weight, not which exponents may belong to the support; the weighted series must also converge.

Formalization targets

Theorem 1 has two clauses for an infinite positive-integer host $H$ :

W_{b,P}(H)<\infty\quad\Longrightarrow\quad X_A(b)\notin\mathbb Q\qquad\text{for every infinite }A\subseteq H,

W_{2,P}(H)<\infty\quad\Longrightarrow\quad X_A(b)\notin\mathbb Q\qquad\text{for every infinite }A\subseteq H\text{ and every integer }b\ge2.

In each clause $P$ is finite and nonempty. In the second, one prime witness for $H$ is fixed before choosing $A$ and $b$ . Taking $A=H$ recovers the two direct assertions. The public formal main item states both hereditary clauses and has an accepted proof in the pinned Lean 4.30 environment.

Significance

Since $h/(2^h-1)\le1$ , this criterion includes reciprocal-summable supports. The paper also gives an explicit $A_\star$ with divergent reciprocal mass but finite weighted mass. The inherited conclusions let another formal result use one certified host for many infinite thinnings. The already proved Lean result makes the host criterion and its dependencies available for direct import; new applications can check the exact premise they need against the public statement.

Difficulty

Reciprocal summability cannot bound the tail for every weighted support. A faithful statement also has to preserve the different order of prime, subset and base quantifiers; dropping fixed-base inheritance changes Theorem 1.

Formalization scope

The formal support is a Set ℕ, and 0 ∉ H enforces positive exponents. FinitePrimeWeighted contains one finite nonempty set of primes and summability of its weighted terms. The public main item joins two accepted Lean results: the fixed-base hereditary theorem and the binary-host all-base theorem. These statements and their public definitions can be reused in the same pinned environment. The later no-cover host is a separate result; it is not a clause of Theorem 1 or the paper's $A_\star$ example. Will Cook is the named paper author; the paper discloses substantial AI-assisted research and drafting and does not claim independent human verification of every proof. Erdős’s earlier criterion and later platform contributions carry separate credit.

Selected references

Will Cook, Weighted Support Criteria for Reciprocal Mersenne Subseries, Erdős Problem Note #257, 2026, Theorem 1.
P. Erdős, On the irrationality of certain series, The Mathematics Student 36 (1968), 222–226 (issued 1969).

4 thms1 active userReviewed

Completed

Numerical Analysis Probability·Captain: shivm

Randomized Kaczmarz: Exponential Convergence in ExpectationResearch Paper

Problem

Solve a consistent system $Ax=b$ , with $A\in\mathbb{C}^{m\times n}$ of full rank and $m\ge n\ge 1$ . Kaczmarz's method (1937) projects the current iterate onto the solution hyperplane of one equation at a time. The cyclic version converges, but its rate depends on the order of the rows and has no clean bound in terms of a condition number.

Strohmer and Vershynin (2009) pick row $i$ at random with probability $\|a_i\|_2^2/\|A\|_F^2$ and prove

\mathbb{E}\,\|x_k-x\|_2^2 \le \bigl(1-\kappa(A)^{-2}\bigr)^k\,\|x_0-x\|_2^2,\qquad \kappa(A)=\frac{\|A\|_F}{\sigma_{\min}(A)}.

The rate does not depend on the number of equations $m$ .

Setting

Rows. $a_i\in\mathbb{C}^n$ is the conjugate of row $i$ , so equation $i$ reads $\langle a_i,x\rangle=b_i$ .
Condition number. $\sigma_{\min}(A)=\inf_{\|z\|_2=1}\|Az\|_2$ and $\kappa(A)=\|A\|_F/\sigma_{\min}(A)$ (Demmel). It satisfies $\sqrt n\le\kappa(A)\le\sqrt n\,\|A\|_2/\sigma_{\min}(A)$ .
Algorithm 1. From any $x_0$ , draw row $r$ independently with probability $p_r=\|a_r\|_2^2/\|A\|_F^2$ and set

x_{k+1}=x_k+\frac{b_r-\langle a_r,x_k\rangle}{\|a_r\|_2^2}\,a_r .

Expectation. $\mathbb{E}\|x_k-x\|_2^2$ is a finite sum over the $m^k$ possible row sequences.

Targets

Theorem 2 (goal): the bound above, for every $x_0$ and $k$ .
Theorem 3: some $x_0\ne x$ has $\mathbb{E}\|x_k-x\|_2^2\ge(1-2k/\kappa(A)^2)\|x_0-x\|_2^2$ for all $k\ge1$ , so $\kappa(A)^{-2}$ is sharp up to a constant. Caveat: the source's proof only reaches the unsquared bound $\mathbb{E}\|x_k-x\|_2\ge\dots$ and then cites Jensen, which goes the wrong way. Its estimates give the squared bound with $4$ in place of $2$ . Both forms are milestones.
Sharpness (§3.2): Theorem 2 is an equality when $\kappa(A)=\sqrt n$ .
Iteration count (§2.1): $k\ge 2\log\varepsilon/\log(1-\kappa(A)^{-2})$ steps give $\mathbb{E}\|x_k-x\|_2^2\le\varepsilon^2\|x_0-x\|_2^2$ .

Proof idea

A single projection can barely reduce the error, when the error is almost orthogonal to the chosen row. On average it always does. If $Z=a_j/\|a_j\|_2$ is drawn with probability $p_j$ , then

\mathbb{E}\,|\langle z,Z\rangle|^2=\frac{\|Az\|_2^2}{\|A\|_F^2}\ge\kappa(A)^{-2}\|z\|_2^2 .

Pythagoras for one projection then gives $\mathbb{E}\|x_{k+1}-x\|_2^2\le(1-\kappa(A)^{-2})\,\|x_k-x\|_2^2$ ; induct on $k$ .

Formalization

Vectors live in EuclideanSpace ℂ (Fin n) and matrices in Matrix (Fin m) (Fin n) ℂ. Mathlib's inner product is conjugate-linear in its first argument, which is why $a_i$ is a conjugated row.
Full rank is stated as injectivity of $z\mapsto Az$ .
The expectation expErrSq is an explicit finite sum, so no measure theory is needed. The tower identity is a milestone.
A zero row makes the step the identity (Lean's division by zero) and has probability $0$ , so it is harmless.
Mathlib has no Kaczmarz iteration, scaled condition number or $\sigma_{\min}$ lower bound; the mission builds them.

History

1937: Kaczmarz introduces the cyclic method and proves convergence, with no rate.
1970: Gordon, Bender and Herman rediscover it as ART for tomography.
2009: Strohmer and Vershynin give the first rate in terms of a condition number.
2010 onward: extensions to noisy systems, block methods, SGD and sketch-and-project (Needell; Needell–Tropp; Needell–Srebro–Ward; Gower–Richtárik).

References

S. Kaczmarz, Angenäherte Auflösung von Systemen linearer Gleichungen, Bull. Int. Acad. Polon. Sci. Lett. A 35 (1937), 355–357.
T. Strohmer and R. Vershynin, A randomized Kaczmarz algorithm with exponential convergence, J. Fourier Anal. Appl. 15 (2009), 262–278. arXiv:math/0702226
J. Demmel, The probability that a numerical analysis problem is difficult, Math. Comp. 50 (1988), 449–480. DOI
D. Needell, Randomized Kaczmarz solver for noisy linear systems, BIT Numer. Math. 50 (2010), 395–403. arXiv:0902.0958
D. Needell, N. Srebro and R. Ward, Stochastic gradient descent, weighted sampling, and the randomized Kaczmarz algorithm, Math. Program. 155 (2016), 549–573. arXiv:1310.5715
R. M. Gower and P. Richtárik, Randomized iterative methods for linear systems, SIAM J. Matrix Anal. Appl. 36 (2015), 1660–1690. arXiv:1506.03296

12 thms1 active userReviewed

Completed

Number Theory Numerical Analysis·Captain: Yuxuan Xu

Research Notes on ζ(9): Constructions, Computations, and Open Problems(v0.1)Research Paper

Motivation

A standard way to prove that a real number $\alpha$ is irrational is to produce integer linear forms $b+a\alpha$ that are nonzero but arbitrarily small: if $\alpha=p/q$ were rational, then $bq+ap$ would be a nonzero integer of absolute value below $1$ once the form is smaller than $1/q$ . This is the shape of every hypergeometric construction of linear forms in odd zeta values — Rivoal's proof that infinitely many $\zeta(2n+1)$ are irrational and Zudilin's proof that at least one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational both produce such forms and read off irrationality (of at least one member of a finite set) from a determinant condition.

The same reduction is useful in the other direction: it isolates exactly what a construction has to supply — small forms — from the arithmetic that consumes them. This mission formalizes that abstract layer: the criteria that turn small integer forms into irrationality, together with the positivity and quadrature lemmas used to certify that a form is nonzero.

The material is distilled from a research note on $\zeta(9)$ (Xu, 2026). That note does not prove the irrationality of $\zeta(9)$ , and nothing in this mission depends on whether it can be: every statement below is a statement about real numbers, integer linear forms, real polynomials, and finite sums, with $\zeta(9)$ and every other specific constant removed.

Setting

All objects live over $\mathbb{R}$ .

An integer linear form in $x$ is a number $b+a\,x$ with $a,b\in\mathbb{Z}$ ; the pair $(b,a)$ is its coefficient vector. Two forms are independent when their coefficient vectors have nonzero cross determinant, $b_1a_2\neq b_2a_1$ .
Irrational x is Mathlib's predicate: $x\notin\mathbb{Q}$ as a real number.
The moment-matching hypothesis for a linear functional $L$ on real polynomials, a five-point node vector $y$ and a weight vector $w$ , is $L(X^m)=\sum_{j}w_j\,y_j^{\,m}$ for every $m\le 4$ . A functional satisfying it is exact on a polynomial $p$ when $L\,p=\sum_j w_j\,p(y_j)$ .
A positive weight vector has $w_j>0$ for all $j$ ; a node vector is injective when $y$ is injective on Fin 5.
Polynomial.taylor u₀ p is the Taylor expansion of $p$ about $u_0$ ; its coefficients are nonnegative when $($ taylor u₀ p $).\mathrm{coeff}\ i\ge 0$ for every $i$ .
Matrix.mulVec M v is the usual matrix–vector product over Fin 5; $\sum'$ denotes tsum over a Summable family.

Formalization targets

Goal — the one-form criterion

$$ \bigl(\forall \varepsilon>0,\ \exists, b,a\in\mathbb{Z}:\ b+ax\neq 0\ \wedge\ |b+ax|<\varepsilon\bigr)\ \Longrightarrow\ \text{ $x$ irrational.}

The goal is the weakest non-vacuous statement in the family: it assumes one form at a time and no rate. ### Stronger — the two-form criterion

\bigl(\forall \varepsilon>0,\ \exists, b_1a_1b_2a_2\in\mathbb{Z}:\ b_1a_2\neq b_2a_1\ \wedge\ |b_1+a_1x|<\varepsilon\ \wedge\ |b_2+a_2x|<\varepsilon\bigr)\ \Longrightarrow\ \text{ $x$ irrational.} $$

Supporting targets

Moment-matching quadrature — matching the five moments $m\le 4$ implies exactness on every polynomial of degree at most $4$ .
Weighted average is interior — with positive weights summing to $1$ , a non-constant five-tuple has its weighted average strictly between its minimum and maximum.
Mediant is interior — the ratio $\sum w_ia_i\,/\,\sum w_ib_i$ with $w,b>0$ lies strictly between the extreme values of $a_j/b_j$ .
Positive matrices — an entrywise positive $5\times5$ matrix sends every nonzero nonnegative vector to a strictly positive vector.
Taylor-sign kernel sum — nonnegative Taylor coefficients at a lower bound of a sequence, positive summable weights, and one positive sample force a strictly positive weighted sum.
Five-sample nonvanishing — under moment matching with positive weights and injective nodes, a nonzero polynomial of degree $\le 4$ whose five sampled values share a sign has $L\,p\neq 0$ .

Targets 1–6 correspond to the mission's milestones; the goal and the two-form criterion close the mission.

Significance

The results. The two criteria are the exact statements that a linear-form construction has to feed, and they are what turns "small forms exist" into irrationality without any analytic input. The supporting lemmas are the standard certificates used to show a form is nonzero — which is the other half of the argument, and the half that finite checks can actually settle.

Formalizing them. All eight statements are elementary and already have informal proofs; each also has a locally compiled Lean proof (lake env lean, exit 0, no sorry) against Lean 4.33.1 and Mathlib revision 0df444a3, held by the mission captain and published in the companion repository. What this mission adds is platform verification plus reusable infrastructure: the moment-matching quadrature lemma, the weighted-average and mediant inequalities, and the positivity lemmas are stated in a form that transfers to any setting where five-point data is certified by moments. Alternative proofs, generalizations to $n$ -point quadrature, and sharper variants are welcome contributions.

Difficulty

The integrality step, not the estimate. In the one-form criterion the obvious move — take $\varepsilon=1/|q|$ — leaves the real inequality $|b+ax|<1/|q|$ , which says nothing until the form is rewritten as $(bq+ap)/q$ with $bq+ap\in\mathbb{Z}$ ; only then does $|\,\cdot\,|<1$ force vanishing and contradict nonzeroness. Writing that rewrite in Lean means carrying the cast from $\mathbb{Z}$ through field_simp and back through exact_mod_cast, which is where naive attempts break.

Moment matching needs a degree bound, not interpolation. The quadrature lemma is not "five values determine a degree- $4$ polynomial": the hypothesis is about the functional $L$ on the five monomials, and the proof must expand an arbitrary $p$ in the monomial basis (as_sum_range_C_mul_X_pow' with natDegree < 5) and commute two finite sums.

Sign conditions are load-bearing. In target 6, the shared-sign hypothesis is what turns a vanishing weighted sum into vanishing samples; the root-counting step then needs injective nodes and positive weights. Dropping either silently makes the statement false, and both are easy to forget.

Formalization scope

Everything is over $\mathbb{R}$ ; no complex numbers appear. The quadrature statements are fixed at five nodes (Fin 5) and degree $\le 4$ , as in the source note; the functional $L$ is a Polynomial ℝ →ₗ[ℝ] ℝ, not a measure. natDegree (not degree) is the degree notion. The infinite sum in target 5 is tsum with an explicit Summable hypothesis. Matrices are Matrix (Fin 5) (Fin 5) ℝ with mulVec; irrationality is Mathlib's Irrational.

Ruled out: a quadrature statement in which the weights are unconstrained by positivity but the conclusion is strengthened to a lower bound — target 1 assumes only moment matching, and any strengthening must add hypotheses rather than reinterpret the existing ones. A "criterion" whose hypothesis is vacuous for every real $x$ is likewise out of scope: both criteria are satisfiable hypotheses, not vacuous ones.

Infrastructure needed: the polynomial expansion and evaluation lemmas (as_sum_range, eval_eq_sum_range'), Finset sum rearrangement, Matrix.mulVec, Summable.tsum_lt_tsum_of_nonneg, and irrational_iff_ne_rational. The quadrature lemma, the mediant inequality, and the positivity lemmas are reusable beyond this mission.

Selected references

Y. Xu, Research Notes on ζ(9): Constructions, Computations, and Open Problems, v0.1, Zenodo, 2026. https://doi.org/10.5281/zenodo.22951155
W. Zudilin, Arithmetic of linear forms involving odd zeta values, J. Théor. Nombres Bordeaux 16:1 (2004), 251–291. https://arxiv.org/abs/math/0206176
T. Rivoal, La fonction zêta de Riemann prend une infinité de valeurs irrationnelles aux entiers impairs, C. R. Acad. Sci. Paris Sér. I Math. 331 (2000), 267–270. https://arxiv.org/abs/math/0008051

8 thms1 active userReviewed