Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation one runs a Markov chain with stationary distribution and reports the sample average . The ergodic theorem guarantees , but honest error bars require more: a central limit theorem
On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions (-, -, -mixing) against moment conditions on . This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.
Every time a streaming service guesses what you would rate a film you have never seen, it is solving a matrix completion problem: fill in the missing entries of a vast user-by-item table from the few that are observed. The question became famous during the Netflix Prize (2006-2009), and it looks hopeless - infinitely many matrices fit the observed entries - until one assumes the structure that makes recommendation possible: the table is essentially low rank, because tastes are governed by a few latent factors. In their landmark 2009 paper 'Exact Matrix Completion via Convex Optimization' (Foundations of Computational Mathematics), Emmanuel Candes and Benjamin Recht proved that an n-by-n matrix of rank r can be recovered exactly, with high probability, from only about n^1.2 * r * log n randomly observed entries - not by the NP-hard route of minimizing rank, but by minimizing the nuclear norm, a convex surrogate (the sum of the singular values) solvable efficiently. The proof, in the lineage of Candes-Romberg-Tao compressed sensing, turns on two ideas: an incoherence condition ensuring the singular vectors are spread out rather than spiky, and a dual certificate witnessing optimality, whose existence rests on delicate random-matrix concentration. It transformed a practical engineering puzzle into rigorous theory and seeded a decade of work across machine learning, signal processing, computer vision, and sensor localization. This mission formalizes the Candes-Recht exact-recovery theorem in Lean, decomposed into its dual-certificate construction and the probabilistic concentration reductions at its core.
This Textbook project develops a reusable Lean library around Martin Aigner and Günter M. Ziegler's Proofs from THE BOOK. It combines results imported from the existing proof_in_the_book repository with precise contribution targets from the sixth edition (2018). The aim is to preserve mathematical meaning, reuse existing proofs, and make the remaining work accessible to other contributors.
The original import contains 156 distinct platform-accepted results. Euclid, the original main theorem, is retained as a completed milestone when the project goal moves to the sixth-edition extension. Every one of the repository's 40 chapter topics has accepted results. Each result certifies its actual Lean statement, including its hypotheses; this does not certify every argument or every theorem in a chapter. Some proofs reuse Mathlib, while others were developed in the repository. Their source and proof notes retain that distinction.
The imported source snapshot is 873d52e0c88cd351f594221e70c3c5b3559777a9. Imported results use Lean 4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Immutable public source links are used only where the linked source matches the verified artifact. Compatibility changes, unsuccessful attempts, and verification evidence are retained in the integration project.
The live goal is the explicit conjunction of the 21 linked sixth-edition extension targets. Its reduction connects these targets to the goal, so proving the remaining children advances the project. This goal is deliberately narrower than “every theorem and every proof in the book”; the unlinked topology tasks below are additional formalization work.
New milestones explicitly marked 6th ed. cover Chapters 7 (spectral theorem and determinants), 15 (round circles and links), 35 (finite Kakeya), 37 (permanents and entropy), and 45 (probabilistic counting). They include the precise definitions and boundary conditions needed to state the results. Compiled Open targets are requests for proofs, not proved results. The spectral theorem has a direct Mathlib proof; community results are reused under their actual statements and with attribution.
Two Chapter 15 tasks intentionally remain unlinked mathematical milestones: the full non-equivalence assertion for the depicted Borromean, Tait, and trivial links, and the Fox-coloring invariance bridge for equivalent link diagrams. These invite formalization of the diagrams and the topology bridge as well as proof. The separate modular Fox calculations do not by themselves establish ambient non-equivalence.
The crossing-lemma target is the universal good-drawing form: actual injective edge arcs and exact finite intersection records appear in its interface. It does not assume the desired crossing bound. The Ramsey target preserves the real exponent for odd k. The related public Erdős–Ramsey result with a rounded exponent is identified as a supporting result, not as proof of that full target.
Older milestones use the repository's chapter labels. Repository Chapters 1–21 match the bundled fourth edition; Chapter 22 inserts Van der Waerden's permanent theorem, and Chapters 23–40 correspond to fourth-edition Chapters 22–39. The sixth edition has 45 chapters, so these organizational labels are not sixth-edition chapter numbers. New milestones give sixth-edition numbers and printed source pages explicitly.
Some existing formalizations preserve narrower statements or additional premises. Examples include repository Chapter 13's dihedral-angle conclusion, Chapter 28's Dilworth lower-bound result, and the geometric premises in Chapter 36. Read the actual linked theorem and its description before reusing it. A chapter title or the former Euclid main theorem is not a completion certificate for the collection.
Choose an Open linked theorem and inspect its definitions, exact binders, Mathlib revision, and prior attempts. Reuse a compatible existing result when it proves that statement; preserve the original contributor's attribution. Submit a matching proof for verification. For an unlinked milestone, first formalize and review the source statement and its definitions. These are known textbook results awaiting formalization or proof in this project, rather than claims of new unresolved mathematics.
Source repository: https://github.com/xiangyazi24/proof_in_the_book
Book: Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), https://doi.org/10.1007/978-3-662-57265-8
A braid on strands is the everyday object it sounds like: strings hanging between two horizontal plates, each string descending monotonically, no two strings meeting. Emil Artin turned this picture into algebra in 1925 by showing that braids form a group under concatenation and that this group has a finite presentation with generators. The braid groups sit at the crossroads of low-dimensional topology (they are the mapping class groups of punctured discs, and closures of braids produce every link), of algebra (they are the prototypical Artin–Tits groups, torsion-free and orderable), and of representation theory and mathematical physics through the Burau, Lawrence– Krammer and Temperley–Lieb representations.
This mission formalizes the braid-group development of a 2023 master's dissertation, Alexsander Andrey Gomes Tarcha's Um Estudo Introdutório da Teoria de Tranças (UNESP, Rio Claro), whose capstone is Teorema 3.15: the braid group on strands admits Artin's presentation. The dissertation builds the group structure on equivalence classes of geometric braids (Teorema 3.9), shows that the Artin generators generate (Teorema 3.11), derives the braid and commutation relations (Proposição 3.14), establishes the presentation (Teorema 3.15), and closes with two structural properties: the full twist is central (Proposição 3.16) and embeds in for (Proposição 3.17).
Work in the plane . The ordered configuration space
carries the subspace topology of , and the symmetric group acts on it by permuting coordinates. The unordered configuration space carries the quotient topology; its points are the -element subsets of the plane. The base configuration is , and denotes its class in . The geometric braid group is
a loop of -point configurations being exactly a geometric braid, and homotopy of loops being exactly the equivalence by elementary moves used in the dissertation.
The elementary half-twist , for , is the loop that rotates the two base points and by the angle about their midpoint , leaving the other points fixed:
It returns to the base configuration at with the two moving points interchanged, so it is a loop in and defines a class in .
The abstract braid group is the group presented by generators subject to
This is the statement the dissertation actually proves: the map of its proof is defined on generators by , and the work consists in showing that it is a well-defined homomorphism which is surjective and injective. Asking only for an abstract isomorphism would leave the generators unconstrained; naming their images is what makes the presentation usable downstream.
Artin's presentation is what makes the braid groups computable: the word problem, the Burau and Lawrence–Krammer representations, the Markov moves on braid closures, and the Garside normal form all start from generators and relations, while the topological side supplies the meaning of those generators. A formalization that only exhibits an abstract isomorphism cannot be used to compute with a given geometric braid; the version stated here transports each half-twist loop to a generator word, which is what downstream work needs.
On the formalization side, the geometric model (configuration spaces and their fundamental groups) and the algebraic model (a presented group) are already available on the platform in this environment, and the abstract form of Artin's theorem is already stated there as an open problem. What this mission adds is: the elementary half-twist as an explicit, machine-checked loop in — this definition is proved sorry-free here, including the injectivity of the moving configuration at every time and the continuity of the path; the sharpened goal that fixes the isomorphism on generators; and the dissertation's supporting results, none of which is currently on the platform. None of the milestones or the goal has a machine-checked proof yet.
Surjectivity of — every braid is a product of half-twists — is a compactness-and-general- position argument in the dissertation: cut the braid into finitely many slabs in which a single crossing occurs. Turning that into a formal proof requires the homotopy-theoretic substitute, since "general position" is not available for free: a loop of configurations must be subdivided and each piece pushed to a standard crossing.
Injectivity is harder and is the step where a naive approach fails. It is not enough to check that the relations hold; one has to know that they are all the relations, i.e. that a word whose braid is null-homotopic is a consequence of the braid relations. The dissertation follows the classical route through elementary moves on braid diagrams (its Figuras 3.22–3.26), which formalizes as a long case analysis. The standard modern alternative is the Fadell–Neuwirth fibration together with an induction on ; its inductive step needs the exact sequence of the fibration , which is itself substantial work.
The plane is ; configurations are injective tuples indexed by Fin n; the unordered
configuration space is the quotient by the coordinate-permutation action with the quotient
topology; the base configuration is (not ). Braid generators are
indexed by Fin (n-1), the index standing for the book generator ; truncated
natural subtraction means the degenerate values give the trivial group, and the
statements are asserted for all including those cases. The abstract braid group is the
presented group on Fin (n-1) modulo the normal closure of the commutation and braid relators.
The half-twist rotates counterclockwise. The mirror symmetry fixes the base configuration and exchanges the two orientations, so the goal statement does not depend on this choice; a solver may use either convention internally.
The goal cannot be satisfied trivially: it asks for a group isomorphism whose values on the generators are the prescribed classes of explicit loops, so neither the identity on a presented group nor an abstract counting argument suffices.
Contributions welcome beyond the milestones: the Fadell–Neuwirth exact sequence for the plane, the pure braid group as the kernel of the map to , the exponent-sum homomorphism, and torsion-freeness of . The half-twist definition published with this mission is reusable for any further work on braids in this environment.
The matrix-multiplication exponent measures how the arithmetic complexity of multiplying square matrices grows with the ir dimension. Known upper bounds come from constructing large independent matrix products inside tensor powers whose asymptotic rank is controlled. Improving the extraction, rather than finding a lower-rank starting tensor, has driven several recent advances.
Alman, Duan, Vassilevska Williams, Xu, Xu, and Zhou improve the combination-loss analysis by allowing all three variable directions to be treated differently. Their original fourth-power computation gives the bound . The mission targets the slightly weaker rational endpoint , keeping the historical result distinct from the later AlphaEvolve numerical improvement incorporated into the latest manuscript. More Asymmetry Yields Faster Matrix Multiplication, version 2, SODA 2025.
Fix an arbitrary field . The matrix-multiplication tensor represents multiplication of an matrix by a matrix. A tensor's rank is the least number of pure tensors summing to it. The existing Lean definition matMulExp K is the infimum of for integer dimensions , with value at the excluded dimensions and . This definition, and the existing equivalence with the Strassen-preorder exponent, remain unchanged.
The source tensor is the literal fourth power of the Coppersmith–Winograd tensor. The public parenthesization is . Its asymptotic rank is at most . Its canonical coarse components are indexed by triples with . This is the fourth-power, recursion-level-three specialization described in Section 7, not the eighth-power specialization used by the later optimization note. More Asymmetry, Section 7.
A complete split distribution records frequencies of entire fine-grade words, rather than only the marginal split at the next recursion step. At level , these words have length over the alphabet . Three such distributions describe the X-, Y-, and Z-variable blocks. A restricted constituent power keeps only blocks approximately consistent with those distributions, in maximum-coordinate distance at most a specified . An interface tensor is a tensor product of these restricted constituent powers. The approximation tolerance and all three distributions are part of the interface. More Asymmetry, Definitions 3.4–3.6 and 4.1.
The goal is the unconditional field-uniform statement
Its binders and exponent definition match the existing Schönhage and Stothers goals; only the declaration name and endpoint differ. No optimizer result, characteristic condition, distribution, or assumed value surplus is a hypothesis of the root.
The compact proposal has four milestones and the root, totaling five review items. The milestones concern literal fine-to-coarse source restrictions; the fourth-power rank budget; an actual strict six-symmetrized value surplus at the chosen parameter; and the conditional implication from that surplus to the exponent bound. Existing proved source and rank theorems are reused. The open surplus target contains the new complete-split extraction and exact numerical obligations, which are described separately in the proof outline rather than hidden in an opaque certificate definition.
The chosen internal parameter is , so
The substantive value target is the existence of a real such that the actual source has six-symmetrized -value at least in the existing finite-witness semantics. The strict slack leaves room to translate limiting extraction rates into strict lower bases. Neither the existence of that surplus nor a completed exact numerical certificate is claimed at proposal time.
This formalization would capture a new structural improvement, not a re-optimization of the same DWZ square data. Its distinguishing feature is sequentially obtaining the necessary ownership properties for X, then Y, then Z, while preserving more useful fine blocks. The resulting complete-split and interface-tensor theory is also the mathematical foundation for the later AlphaEvolve optimization. More Asymmetry, Sections 2, 4–6; Dupont et al., Section 2.
The known mathematical result is not an open conjecture. The open work is its machine-checked reconstruction. The earlier square and Stothers roots are marked Proved. The newer DWZ fourth-power root has an accepted reduction but remains Open. Its literal fourth source, rank budget, sixfold-symmetry bridge and entropy-certificate infrastructure can be reused independently of that unfinished endpoint. A proof of the numerical DWZ bound alone would not imply the smaller bound targeted here.
The old hashing interface guarantees both coarse X- and Y-block uniqueness. The new method initially requires only coarse X-block uniqueness. Fine Y-block compatibility and usefulness must then establish the ownership needed for the subsequent Z-stage. Applying a theorem whose hypotheses already demand coarse Y uniqueness would discard the new method's essential advantage. Six coordinate permutations create six regions whose parameters and output interfaces must remain consistent. More Asymmetry, Section 4.1 and Figure 1.
Removing incompatible fine blocks creates holes. The relevant repair theorem concerns holes in all three modes and a quantitative supply of broken interface copies. It cannot be replaced without proof by the older square-specific Z-only repair interface. The global and recursive stages also carry subexponential losses and approximation tolerances; their limiting order must be explicit. Numerical feasibility is a separate obligation: floating-point parameters and optimization success are not exact normalization, marginal, entropy, or logarithm proofs. More Asymmetry, Theorem 4.2, Theorems 5.3 and 6.4, and Section 7.
The environment is pinned to Mathlib 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and Lean v4.29.0-rc3. The development reuses TensorObj, MMObj, restrictions, degenerations, tensor powers, existing tau-value predicates, and matMulExp. The root is uniform over arbitrary fields. Source relations remain target-first: a restriction of A from B is written Restrict A B. A collection of overlapping constituent restrictions must not be relabeled as an external direct sum.
Complete split distributions, simultaneous three-mode projections, interface tensors, region permutations, and explicit finite extraction maps form reusable infrastructure. Exact rational profiles require compatible lengths; approximate profiles require their stated tolerance and limiting argument. No constant-valued replacement for tensor value, vacuous witness hypothesis, or certificate that merely assumes the desired extraction is admissible.
The authors' released code and parameter archive is the provenance source for the original computation. Versioned archive and witness hashes belong to the companion source audit. The optimization program need not be formalized: an exact certificate checker must establish its own normalization, support, marginal and interval conditions. Contributions to complete-split interfaces, sequential ownership, three-mode repair, recursive extraction, entropy certificates, and finite source-to-exponent bridges all advance this mission.
The matrix-multiplication exponent measures how the arithmetic cost of multiplying square matrices grows with their dimension. An improvement in this exponent is relevant both to algebraic complexity and to algorithms whose running times depend on matrix multiplication. This mission formalizes a known improvement using the fourth power of the Coppersmith–Winograd tensor; it does not claim a new mathematical record.
Duan, Wu, and Zhou identify a loss that arises when constituent tensors are analyzed independently although some of their finer components can coexist inside a shared variable block. Their asymmetric-hashing method recovers part of this combination loss. The paper's headline result concerns the eighth power. Its separate fourth-power computation reports in Table 3, printed page 78. The present target is the slightly weaker exact rational endpoint . Duan–Wu–Zhou, Faster Matrix Multiplication via Asymmetric Hashing.
Fix an arbitrary field . The matrix-multiplication tensor encodes multiplication of an matrix by a matrix. Its tensor rank is the smallest number of pure tensors whose sum is that tensor. The existing Lean definition matMulExp K takes the infimum of over integers , with the value at the two excluded small dimensions. This definition is reused without alteration.
A restriction applies a linear map separately to each of a tensor's three variable spaces. A degeneration allows polynomial families of such maps and takes an appropriate leading coefficient. The order of the Lean relation is target first: Restrict A B means that is obtained from . A direct sum uses disjoint variable spaces; a collection of overlapping restrictions does not constitute a direct sum.
The Coppersmith–Winograd tensor has border rank at most . This mission fixes and uses the literal tensor , whose asymptotic-rank budget is . Its standard coordinate partition has 45 coarse components indexed by nonnegative integers . Each coarse component consists of ordered products of square components, whose grades sum to . Duan–Wu–Zhou, Sections 3 and 6–8.
A restricted-splitting value pair consists of a lower value bound and a prescribed distribution on finer Z-variable blocks. In a tensor power, Z-blocks with the wrong empirical split distribution are removed before measuring value. Sixfold symmetrization, using all permutations of the three modes, is part of this definition. Keeping the scalar and discarding the prescribed distribution loses information required by the recursion. Duan–Wu–Zhou, Definition 3.9, Equation (3), and Definition 8.1.
The goal is precisely
It has the same field quantification and exponent definition as the completed Schönhage and Stothers goals. Only the name and rational endpoint change. No distribution, optimizer, characteristic restriction, or unproved value bound is a hypothesis of this goal.
The supporting targets concern the literal fourth-power source; prescribed-splitting component values; the recursive and global extraction inequalities of Equations (34) and (25); an exact certificate for the released fourth-power computation; and the value-to-exponent implication of Theorem 3.2. The proof outline distinguishes stable formal statements from source-level tasks whose complete Lean interfaces still require development. It does not turn an unspecified certificate into an assumption that the desired extraction exists.
The compact milestone list contains four precise statements: the literal fine-to-coarse product restriction; the fourth-power asymptotic-rank bound; existence of a strict six-symmetrized value surplus; and the conditional implication from that surplus to the goal. Together with the root, these are five review items. The first, second, and fourth milestones are marked Proved. The surplus remains Open. An accepted root reduction links the surplus to the proved capstone; it is a proof sketch, not a proof of the exponent bound. Recursive component extraction and exact numerical certification remain substantial work inside that open target.
The planned internal parameter is . Thus . The substantive value obligation is a strict surplus over for the actual fourth-power source, with asymptotic losses absorbed by choosing strict lower rates. The exact certificate must establish this surplus; neither its existence nor its numerical slack is presently claimed as proved.
The result would extend the formalized Stothers endpoint to an asymmetric fourth-power bound. More importantly, it would provide restricted-splitting interfaces that can support subsequent higher-power and more-asymmetric analyses. The mathematical improvement is already established in the cited paper. The task here is to reconstruct its argument with machine-checked statements, concrete tensor maps, and exact numerical bounds.
The earlier square and Stothers mission roots are marked Proved. Reusable infrastructure includes polynomial degenerations, tensor powers, direct-sum value witnesses, hashing and hole-repair lemmas, the literal fourth-power grading, and the final exponent bridge. Two additional literal fourth-power support/restriction bridges and an additive entropy certificate with directed-log inputs are also marked Proved. These statuses do not imply that the new restricted-value recursion or numerical witness is already formalized.
The central difficulty is retaining the correct dependence between each value bound and its prescribed split distribution. The released fourth-power data contains consumer-specific copies of square value pairs. Equal coarse grades do not justify identifying their chosen distributions. The 21 positive fourth-power components use the six-region recursion, whereas the 24 components with a zero coordinate require the boundary merging argument. Duan–Wu–Zhou, Equation (34), Section 7.3, and released implementation.
Global hashing must additionally control competitors with the same marginals, shared Z-blocks, missing fine blocks, and subexponential losses. An isolated restriction into each constituent is insufficient to establish a simultaneous extraction. Numerical optimization presents a separate issue: floating-point normalization and approximate maximum-entropy computations are not exact feasibility or entropy proofs. Exact marginal constraints, positivity domains, and directed error bounds must all be checked.
The environment is pinned to Mathlib 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and Lean v4.29.0-rc3. The development reuses TensorObj, MMObj, Degenerates, HasTauValueAtLeast, the six-symmetrized value infrastructure, and matMulExp. All endpoint theorems remain uniform over arbitrary fields. Finite profiles use exact integer counts; rational distributions must have compatible unbounded lengths before an asymptotic statement is invoked. Real limiting rates are represented with explicit strict slack where the existing finite-witness predicate does not guarantee endpoint attainment.
No constant-valued replacement for tensor value, opaque witness carrying its desired conclusion, or external direct sum substituted for overlapping source blocks is admissible. New definitions must specify the actual coordinate projections and restrictions they represent. The authors' optimizer is used to find candidate data, not trusted as a proof oracle. Contributions to restricted-power semantics, consumer-specific square pairs, boundary merging, recursive extraction, exact entropy bounds, and source-to-exponent bridges are all directly relevant to the goal.
power4_dup_2.371919.mat. Authors' release.The basic UCB regret bound of Mission II is logarithmic but not tight: its leading constant is eight times the information-theoretic limit, and its worst-case rate carries a spurious . Chapters 8–9 of Lattimore–Szepesvári close both gaps. A refined confidence schedule yields the asymptotically optimal — exactly matching the instance-dependent lower bound of Mission VII for Gaussian noise. The MOSS index achieves minimax regret , matching the lower bound up to a constant. These two theorems are the gold standard for finite-armed stochastic bandits.
The Cook-Levin theorem states that CNF SAT is NP-complete. This mission formalizes the theorem over a multi-tape Turing machine model in Lean 4.
Prove CookLevin.cook_levin_theorem:
under the decider and reduction hypotheses.
A learner repeatedly chooses one of slot machines, observes only the reward of the chosen arm, and wants to earn almost as much as the best arm in hindsight. This is the stochastic multi-armed bandit, the canonical model of the exploration–exploitation dilemma. This mission formalizes the model (environments, policies, regret, and the regret decomposition ) and the two classical algorithms of Chapters 6–7 of Lattimore–Szepesvári: Explore-Then-Commit and the Upper Confidence Bound algorithm built on the optimism principle. The goal theorem is the instance-dependent UCB regret bound — logarithmic regret with explicit constants, the single most cited result of bandit theory — together with its distribution-free companion .
Multiplying two -bit integers is the basic operation underneath division, square roots, base conversion, evaluation of elementary functions to high precision, and polynomial and matrix arithmetic over ; the cost of all of these is usually quoted in units of the multiplication cost . In 1971 Schönhage and Strassen proved on a multitape Turing machine and conjectured that is the true order of growth. The upper half of that conjecture was settled by Harvey and van der Hoeven in 2019 (published 2021), who gave an algorithm achieving in the same machine model.
Timeline (multitape Turing model).
A -tape Turing machine, in the conventions of Montanaro's Computational Complexity lecture notes (§3, §3.4), has the following parts:
In one step the machine reads the symbol under every head, writes a symbol under every head, moves each head by at most one cell (never left of ), and changes state. Once in it stays there unchanged.
For a bit string , written most significant bit first, let be the integer it represents, and for let be the length- binary representation of , padded with leading zeros. The machine is started in with on the input tape. It computes the product if, for every and all , it reaches with the output tape holding exactly followed by blanks. Its running time is the largest number of steps it takes on any pair of -bit inputs. Write
There is one machine that computes the product and has running time
with the natural logarithm. That is, for all , for some constants and .
The milestones are the self-contained mathematical statements behind the Gaussian resampling step of the paper (§4.1–§4.2) and its prime-selection step (§5.2):
The result. Theorem 1.1 makes an unconditional upper bound for integer multiplication on multitape Turing machines, matching the Schönhage–Strassen conjecture. Through standard Newton-iteration reductions it gives the same bound for division and -th roots, and for computing elementary constants and functions to precision . No superlinear lower bound for is known, so the matching lower bound remains open.
Formalizing it. The theorem has a published proof but no machine-checked proof. A formal proof would also check the full chain of reductions (splitting into digits, Chinese-remainder multidimensional convolution, Gaussian resampling, Nussbaumer polynomial transforms, fixed-point error control, and Turing-machine data movement), each with explicit error and cost accounting. The resampling identity and the norm bounds are statements of independent interest in discrete harmonic analysis, and are useful to formalize on their own.
The obvious approach is a Fourier transform over with bits of precision. This leads to recursive estimates of the form , and every such scheme loses a factor that tends to infinity at each level of recursion. Reaching requires every level of recursion to cost a constant factor less than the previous one. That in turn requires transforms of prime length to be replaced by power-of-two transforms at essentially no extra cost, while keeping bits of precision loss per level. In the Turing model, every reshuffling of data also costs time proportional to the data volume times a logarithm, so the reductions must avoid general sorting wherever its cost would dominate.
IntMul_MultitapeModel, which follows the -tape conventions of Montanaro's lecture notes. Tapes are indexed by and begin with . There is a designated state that freezes the configuration. Tape is a read-only input tape and tape is the output tape. The input is , and the output tape must hold exactly followed by the product bits and then blanks. Running time is the number of steps until .IntMul_HvdH_Resampling.The braid group is one of the places where group theory, low-dimensional topology and knot theory meet. Artin introduced it in 1925 (E. Artin, Theorie der Zöpfe, Abh. Math. Sem. Univ. Hamburg 4 (1925), 47–72) and returned to it in 1947; since then it has become standard equipment in the study of links (closed braids and Markov's theorem), of mapping class groups of punctured surfaces, and of configuration spaces. Birman's Braids, Links, and Mapping Class Groups (Annals of Mathematics Studies 82, Princeton University Press, 1974) is the classical reference that develops all three subjects from the braid group outwards, and its Chapter 1 is the foundation on which the rest of the book rests.
The chapter's structure is itself the reason to formalize it first: everything later in the book — the closed-braid picture of links, Markov's theorem, the Magnus representations, the mapping class group of the punctured sphere — is phrased in terms of the group and of the presentation established here. A mission that fixes faithful Lean definitions of the configuration spaces and of the abstract braid group therefore fixes the vocabulary for the whole series.
Timeline of the results collected here: Artin (1925) gave the presentation and the characterization of braid automorphisms of a free group; Chow (1948) determined the centre; Fadell–Neuwirth (1962) introduced the configuration-space fibrations, and Fadell–Van Buskirk (1962) used them to give the proof of the presentation reproduced by Birman.
Write for the Euclidean plane, identified throughout with the complex numbers . For let
be the ordered configuration space of points in the plane, topologized as a subspace of . The symmetric group acts on it by permuting coordinates; the quotient
with the quotient topology, is the unordered configuration space. A point of is an unordered set of distinct points of the plane. The base configuration is , and all fundamental groups below are taken at or at its image.
The braid group of the plane is : a loop is a motion of points of the plane returning to the same set of points, and homotopy classes of such motions compose as braids. The pure braid group is , the subgroup of motions returning each point to its own starting position.
Separately, let denote the abstract group given by generators subject to
These are equations (1-1) and (1-2) of the book (p. 11). Geometrically interchanges the -th and -st points along a semicircle.
The group of motions of points of the plane is the group with generators and the two families of relations above: the relations are not only valid but defining.
The milestone list follows the chapter: the covering-space description of the projection (Proposition 1.1, p. 11), the Fadell–Neuwirth exact sequence (Theorem 1.4, p. 14), the semidirect-product decomposition of the pure braid group (Corollary 1.8.1, p. 24), the faithful representation of by automorphisms of a free group (Corollary 1.8.3, p. 25), the centre of (Corollary 1.8.4, p. 28, due to Chow), and Artin's algebraic characterization of the braid automorphisms (Theorem 1.9, p. 30).
Theorem 1.8 is what makes the braid group computable: with defining relations in hand one can combine braids into the normal form of Corollary 1.8.2 and solve the word problem, represent braids by automorphisms of a free group, and pass to the link-theoretic material of Chapters 2 and 5 where braid words, not motions, are the objects manipulated. Corollary 1.8.3 turns braids into concrete data — a braid is determined by what it does to the generators of a free group — and Theorem 1.9 says exactly which endomorphisms arise this way; both are the algebraic engine behind the conjugacy-problem and Magnus-representation chapters.
For formalization the state of play is that Mathlib has free groups, presented groups, the fundamental groupoid and fundamental group, covering maps and fibre bundles, but no braid groups and no configuration spaces: nothing here can be assembled from existing declarations. The mission therefore produces reusable infrastructure — configuration spaces of the plane, the symmetric-group quotient, the Artin presentation, the Artin action on a free group — as well as machine-checked proofs of results that are classical but, as far as the mission's search of the library showed, not yet formalized in Mathlib.
The generators and relations are easy to write down and easy to verify in ; what is hard is completeness, i.e. that no further relations are needed. The naive route — draw the braid, push it into a normal form by hand — is exactly what a formal proof cannot do. The Fadell–Van Buskirk argument reproduced by Birman instead runs an induction on driven by the fibration : its homotopy exact sequence gives a split extension of by a free group, presentations are assembled along the extension, and finally the covering with deck group transfers the answer from the pure braid group to the full braid group. Each of those steps needs genuine algebraic topology — local triviality of the projection, exactness of the homotopy sequence, freeness of of a punctured plane — which is where the formalization work actually lies.
The plane is . is the subtype of injective functions
; is its quotient by the equivalence "differ by
precomposition with a permutation", with the quotient topology. Base point: the configuration
, i.e. , and its image. Fundamental groups are Mathlib's
FundamentalGroup at those base points. Braid generators are indexed by
with -based indices ( stands for ), and free-group generators by
; the abstract braid group is a PresentedGroup on that index set. Truncated
subtraction makes the generator set empty for , so and are trivial, as
intended. Two milestones are stated with the shift (i.e. for the projection
) to avoid truncated subtraction in the maps.
Two conventions are worth flagging because they weaken what the Lean text asserts relative to the prose. First, the goal asserts the existence of some isomorphism ; it does not pin the isomorphism down on the geometric generators of Figure 2, since those loops are not part of the formal development. Second, Artin's representation is formalized as the existence of a homomorphism from to the automorphism group of the free group whose value on each is the explicit endomorphism of equation (1-14), together with its injectivity; Theorem 1.9 is then stated for an arbitrary such , given as a hypothesis, and is non-vacuous precisely because Corollary 1.8.3 supplies one.
No trivializing formalization is available: the goal is an isomorphism statement between two groups that are both defined independently of it, and the degenerate cases (both sides trivial) are genuine special cases of it, not the content.
Infrastructure a complete development needs, all reusable: freeness of of a punctured plane, local triviality of the Fadell–Neuwirth projection, the homotopy exact sequence of a fibration in the range needed, presentations of split extensions, and the transfer of a presentation along a regular covering. Contributions of any of these as standalone lemmas are welcome, as is a formalization of the geometric generators (1-9) that would let the goal be strengthened to pin the isomorphism on .
The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound means that, over the field under consideration, two matrices can be multiplied using field operations for every . It is a central benchmark in algebraic complexity and controls the exponent of many algorithms that use matrix multiplication as a subroutine.
Coppersmith and Winograd's 1990 analysis of the square of their tensor established . That number remained the record for roughly two decades. Stothers' 2010 thesis first obtained a smaller exponent by analyzing the fourth tensor power, and Davie and Stothers later supplied a self-contained journal treatment. Their Theorem 5.3 and numerical parameters give ; see Davie--Stothers, printed pp. 367--368. The result is the first historical step below the classical tensor-square barrier and is the natural next capstone after a formal proof of the bound.
This mission formalizes the Davie--Stothers fourth-power argument at the exact rational endpoint . It concentrates on the new mathematical layer introduced by the fourth power: five non-matrix constituents, their recursive value estimates, and the two-dimensional same-marginal ambiguity in the final distribution count.
For a field , an order-three tensor represents a bilinear map. The matrix-multiplication tensor
encodes multiplication of an matrix by a matrix. Restrictions apply linear maps to the three tensor legs; degenerations permit polynomial families of maps. A direct sum of matrix-multiplication tensors has disjoint variable blocks and can be converted into an exponent inequality by Schönhage's asymptotic sum inequality.
The Coppersmith--Winograd tensor has border rank at most and a three-class coordinate partition. Its square decomposes into fifteen coarse constituents with . Davie--Stothers square this decomposition again. The fourth power has forty-five constituents with indices summing to eight, grouped into ten symmetry classes represented by
The first five classes are rectangular matrix-multiplication tensors. The last five require recursive value bounds. With , the paper writes
and states the five lower bounds in Lemma 5.1. The final fourth-power extraction assigns frequencies to the ten symmetry classes. Their coordinate marginals are encoded by the matrix in Equation (5.2); its kernel is the two-dimensional space displayed immediately after that equation.
The paper's bounds are limiting exponential rates and may carry subexponential losses in their finite Salem--Spencer extractions. Prove2Me's HasTauValueAtLeast predicate instead records a constant-relative finite witness. The source-faithful formal statements therefore assert attainment of every fixed nonnegative base strictly below each displayed limiting rate, rather than unjustified attainment of the limiting endpoint itself. This downward-closed form retains the complete asymptotic conclusion and is exactly what the final strict numerical surplus needs.
For every field ,
The source's computed endpoint is strictly smaller, giving slack for an exact rational certificate. The Lean goal has exactly the same field quantification and matMulExp definition as the existing Coppersmith--Winograd mission; only the theorem identifier and endpoint change.
The mission records the canonical nine-grading of and the ten symmetry classes of Table 1. It formalizes all five clauses of Lemma 5.1 for , , , , and in every-strict-lower-base form; Equation (5.2) and the stated basis of ; Lemma 5.2's entropy minimization along that kernel; Theorem 5.3's downward-closed fourth-power value inequality; and the Table 2 numerical specialization. The final milestones connect the resulting tau-value surplus to the border-rank budget and transfer the Strassen-preorder exponent bound to matMulExp.
Mathematically, this theorem is the first improvement obtained by passing from the square to the fourth power of the Coppersmith--Winograd tensor. It establishes the recursive constituent pattern used by the later eighth-, sixteenth-, and higher-power analyses. In particular, the five formulas in Lemma 5.1 are the first complete catalogue of genuinely recursive fourth-power constituents.
For formalization, the mission creates a reusable representation of higher-power CW gradings and their symmetry orbits. It also forces a distinction between a locally chosen joint type and all other types with the same marginals. Lemma 5.2 is the exact finite-dimensional entropy correction needed when the marginal map has nontrivial kernel. That infrastructure can be reused by later refined-laser and complete-split missions.
The result is known mathematically. The open task is a machine-checked reconstruction. Prove2Me already contains the CW tensor, its characteristic-free border-rank degeneration, its canonical square grading and constituent restrictions, the Salem--Spencer layer, direct-sum tau-value witnesses, the asymptotic sum inequality, and the exponent bridge. The exact optimizer identity for the profile is also proved. The remaining frontier is to connect the literal fourth-power constituents to finite direct-sum extractions, then assemble all five value estimates and the final kernel-corrected distribution count.
The fourth power contains 225 ordered products before symmetry grouping. A formal proof must show that each claimed constituent is the literal block of and that its recursive decomposition uses the correct variable spaces. Replacing a sum of overlapping blocks by an external direct sum would make the value bound artificially strong.
The five non-matrix classes have different feasible frequency polytopes. Their optimizer formulas are valid only after the corresponding nonnegativity and normalization conditions are checked. The class already has a nontrivial same-marginal family. At the global level the map has a two-dimensional kernel, so marginal counts alone do not determine a unique joint distribution. Ignoring that kernel removes the entropy penalty and invalidates Theorem 5.3.
Finally, Table 2 contains decimal witnesses obtained numerically. A formal proof must replace floating-point evaluation by exact rational parameters and certified bounds for logarithms and real powers, while retaining strict slack at .
The development uses environment 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and the existing TensorObj, MMObj, restriction, degeneration, HasTauValueAtLeast, tensorAsymptoticRank, matMulExp_strassen, and matMulExp declarations. Top-level theorems quantify over an arbitrary field. Finite block indices and symmetry classes use finite types; frequency vectors and entropy inequalities use real numbers; exact finite profiles use natural numbers before passing to cofinal asymptotics.
The capstone specializes to and the fourth tensor power. Generic grading, orbit, multinomial, entropy, and optimizer lemmas are welcome when they shorten later missions. Every value theorem must ultimately be backed by restrictions or degenerations to direct sums of concrete matrix-multiplication tensors. An opaque value functional, a constituent definition that is an external sum rather than the source block, or a numerical hypothesis that assumes the desired endpoint is outside scope.
Contributions are welcome for the literal nine-grading, symmetry-orbit classification, the five constituent extractions, exact address factorizations, optimizer feasibility, the kernel calculation and Lemma 5.2, exact Table 2 arithmetic, and the final exponent assembly.
This mission develops Chapter 5 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
The period-finding problem: we are given for which there is an unknown with if and only if .
Let be the power of two with and . Let be the unitary on qubits, with read as an -bit number and written in bits, and let be the quantum Fourier transform on the first register. One run of Shor's algorithm prepares
(one evaluation of and two Fourier transforms) and measures the first register in the computational basis, obtaining . Call good if
Then:
So a good outcome determines : continued-fraction expansion of finds the unique fraction with denominator at most near , and its denominator is the period. This is the quantum core of Shor's factoring algorithm.
Formalization Note The state is the shared shorRunState, with (which gives ) and second register qubits. The intermediate measurement of the second register is omitted: it does not change the distribution of the first register. The probability of a good outcome is the total weight of the basis states whose first register is good. The constants and are quantified before , and . The source's per-run constant is not stated (see notes).
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
The value of the Riemann zeta function at five is the convergent sum
The target is that this number cannot be expressed as a ratio of integers. This mission concerns the complete proof development in mo271/Zeta5, pinned to commit 7fe736760f4b96bfdb4334b68e3b3124ecbe10b0. The repository follows Aabir Fauzan's preprint ζ(5) is irrational, while explicitly changing parts of its arithmetic normalization. Its formal target is the individual value at five. Results asserting that at least one member of a list of odd zeta values is irrational do not establish this target.
The repository reports a complete Lean proof with only the standard axioms propext, Classical.choice, and Quot.sound. That is a statement about the source project. The existing Prove2.me goal remains Open, and importing and checking the source proof against the platform environment is the work tracked here. The exact existing goal is reused as a reference; there is no second copy of the irrationality assertion.
The construction uses Hankel matrices, whose entries depend on the sum of their row and column indices. For a natural index , put , , and . The rational polynomial controls a family of rational functions. A rational linear functional takes prescribed Bernoulli-number values on powers of and prescribed affine-polynomial values on the simple poles . Polynomial division and residues extend it to .
Applying this functional to gives an matrix over . Write and , where is the explicit positive factorial ratio in the construction module. These are specified polynomials; their existence and properties are not abstract supply assumptions. The real number zeta5 is the convergent series, and a short bridge identifies it with Mathlib's complex zeta value.
The goal is
It is the existing theorem FCP.Zeta.irrational_zeta_five. The supporting target from the source main estimate is
The formal statement also requires to be a positive rational multiple of the explicit .
The milestone list records the general polynomial irrationality criterion, the exact degree calculation, the moment representation with integrability, strict determinant positivity, the real-value upper bound, integral normalization with its growth estimate, and the final small-value statement. A further supporting theorem states that tends to zero for every fixed positive integer and every . These targets cover the analytic, arithmetic, and final assembly parts of the source project.
The goal distinguishes a single zeta value from the disjunctive irrationality results for finite lists. The intermediate results also provide reusable infrastructure: an irrationality criterion for polynomials of varying degree, integral moment representations of rational functionals, determinant positivity, and estimates controlling rational normalizers.
For formalization, the concrete task is to transplant the source development while preserving its definitions, hypotheses, and actual constants. The source's existing proofs provide the intended implementations; the mission does not replace the difficult analytic or arithmetic statements with assumed approximation families. Proof imports and accepted submissions must eventually connect those implementations to the existing goal. The source's Apache-2.0 license and commit-pinned attribution accompany the code.
Small real values alone do not suffice: the integer coefficients and the degree growth must be controlled at the same time. The normalization needed to obtain integer coefficients can enlarge the values enough to destroy the analytic estimate. The decisive quantitative requirement is that its growth constant stay below the magnitude of the negative analytic constant.
Here the analytic estimate uses , and the implemented normalization uses . Their exact rational sum is negative. The milestone assertions retain the source's lower-order terms and the eventual quantifiers in the normalization estimate. They do not strengthen an eventual estimate to a uniform one, or infer positivity from a vanishing upper bound.
The scope is the complete importable proof path to Apery.irrational_five in the pinned repository, including the arithmetic modules, logarithmic-energy estimates, finite certificates, and the external prime-number-theorem dependency where the proof uses it. The headline milestones organize that full development; they are not a claim that every internal lemma is already published on the platform. The repository's optional stronger numerical rate and the preprint's irrationality-measure claim are outside this goal.
The source uses cutoff , a full rank loss in its outer-prime estimate, and direct class-wise partial fractions, as documented in its implementation notes. Its final estimate asserts some positive decay constant, not the paper's . The draft retains those choices. Polynomial evaluations take place over the reals, coefficients begin in the rationals and are normalized into the integers, and the moment integrals are Lebesgue integrals over . Definitions are total at zero, while the positivity and real-bound milestones explicitly require .
The source pins Lean 4.34.0-rc1 and Mathlib f385f9fd18abed332ebcd3df239cb357e264aceb. This proposal targets the available Lean 4.33.1 / Mathlib 0df444a360eaa60ab8c11dca51a86af692955474 environment. The draft definitions and milestone statements are checked locally in that target environment; acceptance of the complete imported proof graph is a separate verification step. The external dependency is mo271/PrimeNumberTheoremAnd at 04d81b2a68ea3548b9990813fdc463c78511f412. Any imported proof must retain a standard-axiom-only dependency check.
7fe736760f4b96bfdb4334b68e3b3124ecbe10b0. Pinned repository.RiemannZetaValues.irrational_five. Pinned challenge source.Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification of scheduling problems (Graham, Lawler, Lenstra and Rinnooy Kan 1979) with a resource field . They then drew the complete borderline between easy and hard problems for unit-time jobs, identical or uniform machines and the makespan criterion. Their Fig. 2 marks each problem type as polynomially solvable or NP-hard.
This mission formalizes the two hardness results of that classification that come from graph partition problems (Theorems 2 and 3, p. 15). Two identical machines are easy under any resource constraints (Theorem 1, after Garey and Johnson 1975). Theorems 2 and 3 show that a third identical machine, or two machines of different speeds, already makes the problem strongly NP-hard, once the number of unit resources is part of the input.
There are jobs and machines . Each machine processes at most one job at a time, and each job runs on one machine without interruption. Machine has a speed , and every job has unit execution requirement , so it takes time on . Identical machines () are the case ; uniform machines () allow arbitrary speeds.
There are resources . Resource has a positive integer size , the amount available at any time. Job needs a nonnegative integer amount of throughout its execution. A schedule assigns each job a machine and a start time . Its completion time is , and it is being executed at every time with . A schedule is feasible when:
The makespan is .
The resource type means three things: the number of resources is part of the input, every size is , and every requirement satisfies . A unit resource is therefore a conflict: two jobs that both need it can never run at the same time. The problems here have no precedence constraints. and ask for a feasible schedule of minimum makespan. Their decision versions ask, for a threshold , whether a feasible schedule with exists.
The source problems are two graph problems on a graph with :
Both are NP-complete (Garey and Johnson 1979, problems GT11 and GT13).
The construction of p. 15 introduces one job per vertex and one unit resource per nonadjacent pair , required by and only.
Formally: if the language of PARTITION INTO PATHS OF LENGTH 2 is NP-hard, then the language of unary codes of yes-instances of the decision version of is NP-hard. The two speeds are arbitrary positive integers.
The results. Theorems 2 and 3 are two of the minimal NP-hard problems in the paper's classification. Together with Theorem 1 they place the borderline exactly: with unit resources whose number is part of the input, two identical machines are polynomial, while three identical machines, or two machines of different speeds, are strongly NP-hard. Strong NP-hardness rules out pseudo-polynomial algorithms unless P = NP, and it carries over to every more general resource type and machine environment in Fig. 1 and Fig. 2. Section 4.1 of the paper also derives hardness for and from these instances.
Formalizing it. The results are classical and proved on paper, but the paper's proofs are one sentence each ("Clearly", "It is easily seen"). No machine-checked proof exists, and the platform has no model of resource-constrained scheduling with real-valued time. This mission produces that model. It also produces a precise statement of strong NP-hardness on top of Cook's Turing-machine definitions, and the first formal NP-hardness reductions from graph partition problems to scheduling.
The scheduling half of each equivalence depends on the real-time model. On two uniform machines of speeds 2 and 1, jobs take time and , so jobs on the fast machine start at half-integers or anywhere else. The resource constraint must hold at every real time, not at a finite set of checkpoints. An argument that treats time as integer slots applies to the triangle case but does not transfer to the paths case.
The complexity half needs polynomial-time computability of the construction on Cook's one-tape Turing machines, on encoded strings that include malformed inputs. It also needs closure of polynomial-time reductions under composition, which the imported complexity layer states but does not prove.
Fin n, Fin m, Fin l), so are q 0, q 1.CookPvsNP_defs.CubicP3Partition.P3Factor, a spanning non-induced -factor.Welcome contributions: proofs of the two equivalences, polynomial-time computability of the construction on Cook's machines, and a general composition lemma for polynomial-time reductions. The composition lemma is reusable for every hardness mission built on CookPvsNP_defs.
Several classical min-max theorems of combinatorial optimization say that a discrete maximization problem and a continuous minimization problem have the same optimal value, and that both have integral optimal solutions when the data are integral. Edmonds' polymatroid intersection theorem (1970), Fujishige's Fenchel-type duality for submodular functions (1984), Frank's discrete separation theorem for a submodular/supermodular pair (1982), and the potential characterizations of weighted matroid intersection (Frank's weight splitting theorem, 1981; Iri and Tomizawa's criterion for the assignment problem, 1976) are instances. Murota's paper Convexity and Steinitz's exchange property, 1996 places all of them under one theorem: a Fenchel-type min-max formula for a pair of an M-concave and an M-convex function, with integrality on both sides.
Timeline:
Let be a finite nonempty set. For , is its characteristic vector; for , are the sets of coordinates where is positive or negative, , and .
A finite integral base set is a finite nonempty such that for and some has . These are exactly the integer points of integral base polytopes of submodular systems. is the convex hull of .
A function has the exchange property (EXC), and is called M-concave, if for and some has and
A function is M-convex when is M-concave.
For and the concave conjugate and convex conjugate are
and the concave closure and convex closure are and ; they are finite exactly on and .
The primal problem maximizes over ; the relaxed primal problem maximizes over ; the dual problem minimizes over . A maximum over an empty family is .
If and satisfy (EXC), then
with (P1) a finite dual infimum forces , and (P2) if all values are finite and equal and the infimum is attained. If are integer-valued, the infimum may be taken over and is attained there when finite.
The formula gives, in one statement, the integrality of an optimal solution of the relaxed primal problem (the essential content of the first half, as the paper observes on p. 296) and of the dual problem. The paper presents it as a unification of two groups of theorems: Edmonds' polymatroid intersection theorem, Fujishige's Fenchel-type duality and Frank's discrete separation theorem on one side, and Iri and Tomizawa's potential characterization for independent assignment with its extensions by Fujishige and Frank (weight splitting) on the other. In the paper it yields the primal and dual separation theorems (Theorems 6.8, 6.9) and the convolution results (Theorems 6.10, 6.11), and it is the prototype of the Fenchel-type duality of discrete convex analysis.
All results here are proved in the literature; none is known to be formalized. Mathlib has no submodular base polytopes, no matroid intersection theorem and no discrete convex analysis. A formal proof of Theorem 6.4 would also require formal proofs of the two cited results, Frank's discrete separation theorem and the M-concave intersection theorem, which the paper uses without proof.
Lemma 6.3 is polyhedral convex duality and holds for any functions. The content is equality with the integral problem: the relaxed maximum over the polytope must be attained at an integer point. For general finite sets it is not, and the intersection of two integral polytopes generally has fractional vertices. Both the integrality of (Edmonds) and the existence of an integral optimal potential depend on the exchange structure; a direct argument from the definitions of conjugates does not see it. The dual integrality claim, that can be taken integral, is again specific to (EXC) and fails for general concave extensions.
Lean conventions, all in namespace SteinitzExchange.Duality:
[Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ; finite sets of integer vectors are Finset (V → ℤ).(V → ℤ) → ℝ used only at points of . M-convexity of is (EXC) for fun x => -ζ x; lives on and on , which are distinct sets in general.⨅/⨆ over and are evaluated only on the convex hulls, where they equal the paper's values; off the hulls they carry a junk value instead of , which no statement uses.EReal, as suprema and infima of coerced reals, so no occurs. EReal's supremum of the empty family is , the paper's convention. The dual infimum is never a real ⨅ (which would return when unbounded and make (P1) meaningless).V → ℤ.Formalizations that would trivialize the goal are excluded: an unrestricted real infimum for the dual, a convex closure built from instead of , a single base set for both functions, and a relaxed maximum taken over all of instead of .
Needed infrastructure: finite convex hulls and polyhedral Fenchel duality, submodular base polytopes and their integrality, Frank's separation theorem, and the valuated intersection theorem. The submodular-system layer (Theorem 2.1, Theorem 6.5) is reusable beyond this mission. Contributions to any milestone, including proofs of the two cited theorems, are welcome.
Matroids and their integral generalizations, integral base polytopes, are the combinatorial structures on which the greedy algorithm is exact. Edmonds' theory relates them to submodular and supermodular set functions: a polytope is a base polytope exactly when its support function, restricted to vectors, is supermodular and the greedy formula evaluates it everywhere. Dress and Wenzel's valuated matroids (1990) and Murota's M-concave functions carry the exchange axiom from sets to functions on sets. This paper (Adv. Math. 124, 1996) sets up the resulting theory of discrete concave functions on base sets, later developed into discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003).
The question behind this mission is how the set-level correspondence between exchange and supermodularity extends to functions. Section 5 of the paper answers it with the Local Supermodularity Theorem: the exchange property of a function is a supermodularity property of its concave conjugate, holding locally at every point.
Let be a finite nonempty set, . For let be the unit vector, for let be its characteristic vector, , and . For a finite , is its convex hull.
A finite integral base set is a finite nonempty such that
A function satisfies the exchange property (EXC) (is M-concave) if for and there is with and . Write and for the maximizers of on .
The support function of is . A positively homogeneous is "matroidal" if
The concave conjugate is , the concave closure is , the subdifferential is , and the localization of at is .
For on a finite integral base set ,
The printed Theorem 5.3 has only the second condition on the right. Its "only if" direction holds as printed; its "if" direction is false without the first condition, and a separate item of the mission states the counterexample: , .
The result. Theorem 5.3 is the function-level version of Theorem 5.1. Condition (C1) is a supermodularity condition, so the theorem expresses (EXC) as "a collection of local supermodularity" properties of , in the same way that (B1) corresponds to supermodularity of a support function. In the paper this characterization of the conjugate side underlies the Fenchel-type duality of Section 6, and more generally the conjugacy between M-concave and L-convex functions in discrete convex analysis.
The formalization. No part of this theory is formalized in Lean or on this platform: base sets, (EXC), "matroidal" functions and concave conjugates of functions on base sets are all new. The mission also corrects the published statement: the reduction from localizations to base sets needs every integer point of to be a maximizer, and the concave-closure condition supplies this. A machine-checked proof would settle both the corrected theorem and the counterexample. Theorem 2.1 and Lemma 5.2 are classical but have no formal proof either.
depends only on the concave closure , so any characterization of (EXC) through alone cannot see values of below . That is why the goal needs the extra clause. The "only if" direction needs the full theory of Section 4: M-concave functions coincide with their concave closure, and all their maximizer sets are base sets. Theorem 5.1 needs the greedy algorithm on integral base polytopes, together with the fact that the base polytope of an integral supermodular function has integral vertices. Theorem 2.1 is the folklore statement that polyhedral and exchange descriptions agree, and the paper does not prove it. Eq. (5.12) needs the subdifferential of a finite minimum of affine functions to be the convex hull of the active gradients, stated globally rather than only near .
Integer vectors are V → ℤ, real vectors V → ℝ, with [Fintype V] [DecidableEq V] [Nonempty V]. A finite subset of is a Finset (V → ℤ). A function on is a total function (V → ℤ) → ℝ whose values off are never used. The mission commits to the following readings:
sInf over the subdifferential, defined by (5.8)–(5.9) exactly, not by the formula (5.12). Eq. (5.12) is stated with IsLeast, so it asserts attainment, not just the value.Fin n ≃ V along which is non-increasing. This is equivalent to "for some" such indexing. "Matroidal" includes positive homogeneity but not concavity.Trivializing formalizations are ruled out. Defining by (5.12) would reduce the goal to Theorems 4.4 and 5.1. A "matroidal" without (C2) would be satisfied by support functions of non-base sets. An taken as a supremum would reverse the sign conventions.
The development needs: the greedy algorithm and integrality for integral base polytopes, supergradients of polyhedral concave functions, and the Section 4 results of the paper (concave closure of M-concave functions, Lemma 4.3). The base-set and "matroidal" layers can be reused beyond this mission. Proofs of any milestone, of the counterexample, and a proof of the "only if" direction on its own are all welcome.
Linear optimization over the bases of a matroid, over the integer points of a polymatroid, or over the flows of a network is well understood: the greedy algorithm is exact, the feasible sets are the integer points of polytopes described by submodular functions, and min-max theorems of Edmonds and Frank hold with integrality. Nonlinear objectives on the same sets are much less uniform. Valuated matroids (Dress and Wenzel, 1990; see Murota 2003) showed that a quantitative form of the Steinitz exchange axiom is exactly what keeps the greedy algorithm exact for a nonlinear weight. Kazuo Murota's paper Convexity and Steinitz's Exchange Property (Adv. Math. 124 (1996) 272–311) extends this exchange axiom from matroid bases to the integer points of arbitrary integral base polytopes, names the resulting functions M-concave, and proves that they are the discrete counterpart of concave functions. The paper is the starting point of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003), which is now used in auction theory (gross-substitutes valuations are M♮-concave), inventory and resource allocation, and combinatorial optimization.
This mission covers the first of the paper's three characterizations of M-concavity: the Extension Theorem (Theorem 4.6).
Let be a finite nonempty set. For , is the characteristic vector of . For , , , , and .
A finite integral base set is a finite nonempty such that for and there is with (axiom (B1)). Examples are the incidence vectors of the bases of a matroid. Its convex hull is an integral base polytope; in general, an integral base polytope is the convex hull of some finite integral base set.
A function satisfies the exchange property (EXC), and is called M-concave, if for all and there is with , and
The local exchange property (EXC) asks only, for with , for some and some with the same conclusion.
For , , and . For any , the concave conjugate is and the concave closure is , a concave function that is finite exactly on . A function extends if on .
For a finite integral base set and ,
The Extension Theorem identifies a combinatorial axiom with a convex-analytic property: M-concave functions are exactly the restrictions to lattice points of concave functions on the base polytope whose linear perturbations are all maximized on integral base polytopes. It is the reason the M-concave class supports a convex-analysis-style theory at all: local optimality implies global optimality, maximizers of linear perturbations are well behaved, and conjugacy (the paper's Theorems 5.3 and 6.4, separate missions of this series) can be developed. Theorem 3.1 on its own is widely used to verify M-concavity in applications, since it reduces the exchange axiom to pairs at distance four.
All results here were proved in 1996. To our knowledge none of them has a machine-checked proof; Mathlib has matroids on sets but no integral base sets in , no M-concave functions and no concave closure of a function on a finite set. A formal proof of this chain would be a first formal development of discrete convex analysis.
The equivalence of (EXC) with its local version (Theorem 3.1) is not a routine induction on : the exchange inequality for a far pair does not follow from the inequalities along a path of distance-4 pairs, because the exchange partner must be chosen consistently with the prescribed . For the "if" direction of Theorem 4.4, knowing that every maximizer set is an integral base set says nothing directly about the values of at non-maximizing points; turning this global information on maximizers into the local inequality (EXC) requires a supporting hyperplane of the concave closure at a well-chosen point and the integrality of the intersection of an integral base polytope with a box (a cited result on submodular systems). Theorem 4.6 then needs the concave closure to agree with on (Lemma 4.5), which fails for general .
All declarations live in the namespace SteinitzExchange.Extension. The ground set is a type V with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ, and toReal embeds the former into the latter. is a Finset (V → ℤ). A function is a total (V → ℤ) → ℝ whose values are only ever read at points required to be in . is Mathlib's convexHull ℝ of the image of . Pinned readings:
Trivializing formalizations are ruled out: the extension must agree with on and be concave on , the argmax is over and not over , and an integral base polytope is never empty.
A complete development needs basic facts on integral base sets (the equivalence of (B1) with the simultaneous exchange (B2), , and the paper's cited Theorem 2.1 relating them to submodular functions), the representation (4.3) of the concave closure as a maximum of convex combinations, and supporting hyperplanes of polyhedral concave functions. The layer of integral base sets and M-concave functions is reusable for the two other missions of this series and for any later formalization of discrete convex analysis; contributions of general-purpose lemmas about it are welcome.
The Riemann zeta function at integers splits into two very different worlds. At even arguments Euler's formula shows every is a rational multiple of , hence irrational and even transcendental. At odd arguments almost nothing is known. The single exception is , proved irrational by R. Apéry in 1978 (Astérisque 61 (1979), 11–13). For every other odd argument the arithmetic nature is open to this day: no individual value is known to be irrational.
What is known are localisation results, which assert that an irrational number occurs somewhere in a finite or infinite list of odd zeta values without saying where.
All objects below are those of the source note, in its own notation.
Fix odd integers and with , and positive integers subject to and
For each integer put and for , and consider the rational function
together with the linear form
Condition (1) gives , so the series converges.
Two arithmetic quantities control the denominators of . Write for the least common multiple of , put for , and set
the product running over primes, where is the integer-valued, nonnegative, -periodic function
The growth of is governed by the saddle points, the zeros of
and by the auxiliary function
Writing for the zero with of largest real part, the two competing constants of the method are
with the logarithmic derivative of the gamma function.
The goal fixes no witness: the statement is satisfied as soon as one of the four values is irrational, and remains the honest form of what the source proves. It is deliberately weaker than the (open) statement that each is irrational, and weaker than any claim identifying which of the four is irrational.
The milestones follow the source's own numbering: Lemma 1 (the linear form and its denominators), the prime-number-theorem asymptotics of , Lemma 2 (the saddle-point asymptotics of for ), the small-values criterion for display (4), Lemma 3 (the criterion ), and the numerical verification of at , , , , for , where and .
The result itself. Together with Apéry's theorem it gives the smallest list of small odd zeta values known to contain an irrational number, and it fixes the current record of the Ball–Rivoal hypergeometric method: the same machinery yields quantitative lower bounds for the dimension of the -span of odd zeta values, and any improvement of the arithmetic factor or the saddle-point estimate propagates directly to those bounds.
Formalizing it. The result is proved mathematically; nothing here is open. What is missing is a machine-checked proof. Mathlib contains the Riemann zeta function, the gamma function, and the prime number theorem, but not Apéry's theorem, not the Ball–Rivoal construction, and not the Chudnovsky–Rukhadze–Hata arithmetic method. A complete development produces reusable infrastructure: integrality of very-well-poised hypergeometric sums, the / denominator-saving mechanism, saddle-point asymptotics for a Barnes-type complex integral, and the standard linear-form irrationality criterion.
The obvious route — exhibit explicit rational approximations to a single and estimate them — fails, and that failure is the content of the field: no construction is known that separates a single odd zeta value. Zudilin's construction instead produces one real sequence that is simultaneously a -linear form in ; irrationality of some coefficient's argument then follows from the two-sided estimate, but the argument is blind to which one.
The three hard steps are independent of one another. First, integrality: the coefficients of have denominators controlled by , and the extra factor — a product of prime powers extracted from the -function — must be divided out; this is a delicate -adic valuation count. Second, asymptotics: the exact exponential rate of comes from a complex integral over a vertical line, evaluated by the saddle-point method at a zero of a degree- polynomial with no closed form. Third, the final comparison is a numerical inequality between two transcendental-looking constants that must be certified rigorously, including a Stieltjes integral of a piecewise-constant function against the digamma function.
Statements are formalized over the reals, with for an integer represented by the convergent series (zetaR); a bridging statement identifies it with Mathlib's riemannZeta at natural arguments, so the goal theorem may be stated with riemannZeta as it already is in the platform library. Admissible parameter sets are a structure carrying , , the sequence , and the hypotheses of the source, so no theorem quantifies over parameters the source excludes. R is a real-valued function of a real variable built from Real.Gamma, and is the tsum of its -st iteratedDeriv at natural arguments; convergence is a separate milestone rather than a silent assumption, so that the value is not asserted to exist by fiat. is the infimum over of the integer-valued expression above, a finite product over primes with (the integer form of ), and the Finset.lcm of . The Stieltjes integral is written as , which agrees with the Riemann–Stieltjes integral because is continuously differentiable on ; uses the principal branch of the complex logarithm.
The saddle point is not defined by a choice function: every statement that mentions it takes it as a parameter together with the hypotheses "root of the polynomial", "positive imaginary part", "maximal real part among such roots", and the two side conditions and of Lemma 2. No milestone is vacuous: for the concrete parameter set of the source such a exists, with .
Contributions of any size are welcome, including partial infrastructure: -adic valuation lemmas for products of factorials, asymptotics of Finset.lcm, saddle-point estimates, and interval-arithmetic machinery for the final numerical comparison.
A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range , and let it degrade at a controlled rate outside, proportionally to the distance from . That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.
Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most " has no direct meaning. What replaces it is the observation that a scalar inequality is the inclusion , and that the violation is the distance from the left hand side to . In that form the notion lifts verbatim, and the whole chapter follows.
Definition 11.1.2. Consider an uncertain convex constraint
with nonempty, closed and convex. Let the perturbation space split as , each factor carrying a normal range , a closed convex cone and a norm , and let be a norm on . A candidate is robust feasible with global sensitivities if
where and .
The object that makes the analysis work is the recessive cone of (Definition 11.3.1): for any ,
which does not depend on and is a nonempty closed convex cone.
A candidate is feasible for the GRC (11.1.6) if and only if it satisfies the system
Line (a) is the ordinary robust counterpart over the normal range. Each line (b) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to itself.
The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.
The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function
of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that of a map with respect to a setup equals of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.
The recessive cone results are the vocabulary. The one that earns its place is : the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.
The goal is an equivalence and the two directions are asymmetric.
Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix and in the unit ball of , and run out along the cone. The GRC bounds the distance to by , so there are with ; the rescaled points stay bounded, and a limit point of them lies in by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not — is what appears in lines (b).
Backward is a decomposition-and-assemble: split each with , realizing the distance, get a point of from line (a) and a recession direction from each line (b), and add them — using that .
Proposition 11.4.1 is a chain of polarity identities: the polar of is for compact convex containing the origin, the polar of a norm ball of radius is the dual-norm ball of radius , and bipolarity. Each step is standard and the composition is not.
Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function .
Conventions committed to:
IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and
nonnegativity follows from them.Call a set of reals a Sidon set when all its pairwise sums are distinct: if with all four in the set, then .
The goal. There is an absolute constant such that every finite set of positive reals contains a Sidon subset with .
This is the lower bound half of Erdos problem 530, which Riddell posed and which asks for the order of the largest guaranteed Sidon subset. That problem is open: it asks whether the guarantee is asymptotically , and the constant is not known. What is settled is the order, by Komlos, Sulyok, and Szemeredi, Linear problems in combinatorial number theory, Acta Math. Acad. Sci. Hungar. 26 (1975) 113-121, as a case of a general theorem about linear equations. Erdos had previously observed the cube-root lower bound and the matching upper bound from . A second and much shorter proof is in Bailleul and Riblet, arXiv:2605.03181.
A one-paragraph argument gives : take a Sidon subset of maximum size, and note that every outside it satisfies or for elements of , so .
That cube root is not a weak first attempt, it is the ceiling for any argument that only counts. An arithmetic progression of length has additive energy of order , so a probabilistic argument cannot see the difference between it and a generic set. Getting from to requires using the structure of the set, and that is what both published proofs do.
Compress, then pigeonhole against a known Sidon set.
An arbitrary finite set of reals has no arithmetic to work with, so first move it into : a finite set spans a finite dimensional -vector space, and a generic rational functional separates its points while preserving every relation . Then squeeze the resulting integers into an interval of length comparable to their number, keeping a constant fraction of them and keeping the property that a Sidon subset of the image lifts to one of the original. Finally intersect with a translate of the Erdos-Turan Sidon set, which has about elements inside . A set of size inside meets some translate of a Sidon set of size in order points, and that intersection is Sidon.
The two proofs differ only in the compression step, and the mission carries both.
The 1975 route compresses in four lemmas driven by a remainder map: choose a modulus dividing no difference, dilate so that the remainders are small, and observe that a small remainder map preserves . Finding the modulus needs a prime counting bound.
The 2026 route replaces all four with one averaging lemma over a real rotation parameter , keeping the elements whose fractional part of is below , where no carry occurs. No prime counting appears anywhere.
Every item is stated in Mathlib primitives alone, so the mission needs no definition items. The Sidon condition, the Erdos-Turan construction, and the reduction relation of the 1975 route are all written out at each use.
The published 2026 proof finishes with Singer's 1938 covering of by Sidon sets. Mathlib has no perfect difference sets, so the mission uses averaging over translates instead. It does the same job at the same order and gives a worse constant, which costs nothing because the goal asserts only that some exists.
Two lemmas of the 1975 paper are deliberately absent. A local formalization of Lemma 2 and Lemma 6 turned out to be false as stated, machine-checked in both cases, so neither is offered here as a milestone. Those are errors in that rendering rather than in the paper, and the 2026 route reaches the goal without either. Lemma 1' is absent for the same practical reason: the 2026 route does not need it.
Chapter 9 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) develops the differential calculus of mappings . The definition of the derivative changes character: it is no longer a number but a linear transformation , the one that approximates the increment of to first order. Once that is in place, the chapter proves the two theorems that make nonlinear analysis possible: the inverse function theorem (Theorem 9.24), which says that a continuously differentiable map with invertible derivative at a point is locally invertible with a continuously differentiable inverse, and the implicit function theorem (9.28), which solves locally for in terms of .
The message of both is that a nonlinear map behaves locally like its linearization, provided that linearization is invertible and varies continuously.
This mission is the ninth in a series formalizing Rudin Chapters 1–11; it uses the completeness and compactness results of Missions II and IV and the mean value estimates of Mission V, and it prepares the change-of-variables machinery used in Mission X.
is the space of linear maps with the operator norm . A map defined on an open is differentiable at with derivative if
and — a -mapping — if it is differentiable on and is continuous. The partial derivative is the derivative of at . A map of a metric space into itself is a contraction if for some .
Let be a -mapping of an open into and suppose is invertible at some . Then there are open sets and such that
The inverse function theorem is the local classification statement of differential calculus: it says that the only local obstruction to invertibility is degeneracy of the derivative, and it is the mechanism behind coordinate changes, the rank theorem (9.32), and the change-of-variables formula for integrals in Chapter 10. The implicit function theorem is its standard reformulation and is what makes level sets of smooth maps into manifolds. Theorem 9.21 is the practical criterion for the hypothesis, since it reduces it to continuity of finitely many partial derivatives; Theorem 9.41 shows that the symmetry of second derivatives, though intuitive, requires a hypothesis; Theorem 9.19 is the several-variable substitute for the mean value theorem, whose equality form already failed in Chapter 5.
Mathlib has the Fréchet derivative, the inverse and implicit function theorems for Banach spaces, the Banach fixed-point theorem, and symmetry of second derivatives. This mission states the Rudin versions concretely in — with the explicit open sets and and the inverse mapping produced as data, rather than through a bundled local homeomorphism — and so provides a bridge between the book's formulations and the library's.
The inverse function theorem is the first theorem in the book whose proof combines several chapters at once: the contraction principle (9.23) gives local surjectivity by solving as a fixed point of ; openness of the set of invertible operators (9.8) keeps the derivative invertible near ; the mean value inequality (9.19) controls the error; and the continuity of inversion gives the regularity of . The delicate point is that all estimates must hold uniformly on a neighbourhood chosen in advance, so the order in which the neighbourhoods are shrunk matters.
For Theorem 9.41 the trap is the hypothesis: continuity of at the single point is assumed, not continuity of both mixed partials on a neighbourhood; the conclusion is existence of at that point, and it genuinely fails without some such hypothesis.
Conventions fixed by this mission:
EuclideanSpace ℝ (Fin n); linear maps are →L[ℝ] (continuous linear
maps), which in finite dimension is the same as Rudin's , with
the operator norm.HasFDerivAt, and the condition is ContDiffOn ℝ 1.HasDerivAt of the line restriction
t ↦ f (x + t • eⱼ) at t = 0, avoiding any coordinate-projection bookkeeping;
eⱼ = EuclideanSpace.single j 1.Function.Bijective, which for a continuous linear map
between finite-dimensional spaces is equivalent to the existence of a continuous linear
inverse.inv constrained on the invertible
operators, so that continuity of inversion can be stated without bundling.D1f, D2f, D21f, which
is how Rudin states the hypotheses, and the conclusion asserts existence of D₁₂f at the
point as a HasDerivAt statement.α increasing and φ(·,t) ∈ ℛ(α).The oldest bandit algorithm (Thompson, 1933) is also the most modern: sample a parameter from the posterior and act greedily. Chapters 34–36 of Lattimore–Szepesvári develop the Bayesian view in two crowning results. The Gittins index theorem: for infinite-horizon discounted Markov bandits, the seemingly intractable dynamic program is solved exactly by an index policy — each arm gets a retirement-value index computable arm-by-arm, and playing the largest index is Bayesian optimal. And the frequentist analysis of Thompson sampling — the goal theorem: with Gaussian posteriors, Thompson sampling on 1-subgaussian bandits achieves , exactly asymptotically optimal, alongside the minimax-grade . Together they explain why posterior sampling is both principled and practically dominant.
Is the regret of LinUCB (Mission X) an artifact of the algorithm or a law of nature? Chapters 24–25 of Lattimore–Szepesvári prove it is essentially unimprovable. On the unit ball there is a parameter with forcing — the goal theorem — and the hypercube gives the same rate. The asymptotic chapter is more striking still: for fixed finite action sets, the instance-optimal constant is characterized by an allocation program, and optimism itself is provably suboptimal — LinUCB and Thompson sampling cannot achieve it, because exploration must sometimes deliberately play actions optimism would never touch. These lower bounds define the targets for the entire linear-bandit literature.
What if the rewards are not random at all, but chosen by an adversary who knows your algorithm? Remarkably, a randomized learner can still compete with the best fixed arm in hindsight. Chapters 11–12 of Lattimore–Szepesvári develop the adversarial -armed bandit: rewards are an arbitrary fixed matrix, the learner samples , and regret is measured against . The exponential-weights algorithm Exp3, fed by importance-weighted loss estimates , achieves — the goal theorem. The companion Exp3-IX, which deliberately biases its estimator, upgrades this to a bound holding with high probability rather than only in expectation. These results are the foundation of all adversarial online learning with partial feedback.