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.
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 .
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.
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.
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.
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.
Many questions about polynomial equations — which equations can be solved by radicals, which geometric constructions are possible with ruler and compass, how the roots of a polynomial are related — become questions about the symmetries of a field extension. The fundamental theorem of Galois theory, going back to Évariste Galois, is the dictionary that makes this possible: for a finite Galois extension it matches intermediate fields with subgroups of a finite group, so that questions about fields become questions in finite group theory. The same dictionary underlies Kummer theory and class field theory, and it is the step that turns the unsolvability of the general quintic (Abel–Ruffini) into a statement about solvable groups.
This mission follows the Wikipedia article Fundamental theorem of Galois theory (revision 1345286594): its main statement, its list of properties of the correspondence, three of its worked examples, and its section on the infinite case.
A field extension is a field with a field inside it; it is finite when is finite-dimensional as an -vector space, of dimension . An intermediate field is a field with . The automorphism group is the group of field automorphisms of with for every .
The two maps of the correspondence are:
The extension is Galois when it is normal and separable; for a finite extension this is equivalent to . When is Galois, is written .
For an infinite algebraic Galois extension, carries the Krull topology: the coarsest topology for which each restriction map , with a finite Galois subextension and discrete, is continuous.
For a finite extension ,
The result. The correspondence turns the lattice of intermediate fields of a finite Galois extension into the (reversed) lattice of subgroups of a finite group, with degrees matching indices and normal subextensions matching normal subgroups. This is the tool used to classify subfields, to compute Galois groups of explicit polynomials, and to prove that solvability by radicals corresponds to solvability of the Galois group.
Formalizing it. The theorems are classical, and Mathlib contains formal proofs of the general finite and infinite correspondences (for example IsGalois.intermediateFieldEquivSubgroup and the InfiniteGalois namespace). This mission's contribution is a statement set indexed by the source: the converse direction ("only if Galois") as the goal, the non-Galois behaviour, each listed property, and the concrete examples of the article. The explicit examples require genuine computation: degrees of towers, minimal polynomials, and counting subgroups and subfields.
The general statements reduce to Artin's theorem and a degree count, but the non-Galois milestone asks for four separate claims about injectivity and surjectivity, each needing the correct direction of Artin's theorem. The examples cannot be settled by a general principle: showing that has exactly five intermediate fields, or that the splitting field of has degree , requires irreducibility arguments and an explicit transfer through the correspondence. Showing that has no non-trivial automorphism requires knowing that the other two roots of are not real.
All statements use Mathlib's IntermediateField F E, IntermediateField.fixedField, IntermediateField.fixingSubgroup, the automorphism group E ≃ₐ[F] E, and IsGalois (normal and separable). Finite means FiniteDimensional F E. Subgroups in the finite statements range over all subgroups; in the infinite case the Krull topology is Mathlib's standard topology on E ≃ₐ[F] E. Degrees are Module.finrank, orders are Nat.card, and the index is Subgroup.index. The concrete fields of the examples are taken inside (for and , with the real cube root) or as the abstract splitting field (for ). The quotient milestone takes the normality of and of as instance hypotheses; they are equivalent by milestone 5, so neither is vacuous.
The article's Example 3 (the anharmonic group acting on ) and the "Applications" section are out of scope for this first mission. No new definitions are needed; contributions of proofs for any milestone are welcome.
Line search methods for unconstrained minimization of a smooth function choose a direction and a step and set . Classical rules (Armijo, Wolfe) insist that every step decrease . For quasi-Newton and conjugate gradient directions this monotonicity requirement often forces short steps, and nonmonotone line searches, which only ask for a decrease relative to some reference value built from past iterates, have been used since Grippo, Lampariello and Lucidi (1986) to let such methods take longer steps.
Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum of recent function values used by Grippo et al. with a weighted average of all past function values. The paper proves two results: global convergence to stationary points (the companion mission) and, the subject of this mission, R-linear convergence of the function values when is strongly convex.
Timeline:
Fix parameters , and . Write and . The Nonmonotone Line Search Algorithm (NLSA) keeps weights and reference values :
with chosen freely at each step. A step is accepted either by the nonmonotone Wolfe conditions
or by the nonmonotone Armijo rule , where is a trial step and is the largest integer such that the first inequality holds and . With one recovers the monotone rules.
The direction assumption asks for constants with and . The function is strongly convex with constant if
Let be the minimizer, , , and the set of points within distance of .
Let be strongly convex with minimizer , let be Lipschitz continuous on bounded sets, let , let the directions satisfy the direction assumption at every iteration, and let for all . Then there is with
The goal fixes no value of : it asserts only the existence of a linear rate.
In the paper's order of use:
Here is a Lipschitz constant of on . A further result on the same definitions is Theorem 3.2: if converges R-linearly with ratio inside a compact convex set on which is strongly convex, then the sufficient decrease condition with reference value holds for all large .
Theorem 3.1 shows that averaging past function values costs nothing in the rate: on strongly convex functions the nonmonotone method keeps the linear rate of monotone descent, for any direction sequence satisfying the direction assumption (steepest descent, L-BFGS with bounded condition numbers, and so on). Theorem 3.2 is the converse side: for weights close enough to 1, the averaged test eventually accepts the steps of any R-linearly convergent iteration of this kind. The paper contrasts this with the max-based test of Grippo et al.
These results are proved in the paper. As far as the platform catalogue shows, no line search with the Wolfe conditions or a nonmonotone reference value has been formalized. The only related item is a monotone backtracking gradient descent rate, which is a different theorem. Machine-checked proofs would give reusable Lean statements of the nonmonotone Wolfe and Armijo rules and of the averaged reference value. They would also give the explicit constants , and in checked form, and a checked record of the repair of the printed statement described below.
The obvious argument would show that contracts at each step. It fails: the method is nonmonotone, and may exceed . The quantity that contracts is , and only is controlled by the line search. The contraction must be derived by relating to in two regimes, and the second regime needs a bound on from the gradient at the previous iterate. That bound requires the Lipschitz constant on a region containing every point the line search examines, which is why the region and the step bound enter. In Lean, the sufficient decrease (3.6) also rests on the step-length lower bounds of Lemma 2.1 for both rules, including the integer-exponent Armijo rule with its maximality condition.
Conventions:
EuclideanSpace ℝ (Fin n), is ContDiff ℝ 1, and is ⟪gradient f x, d⟫_ℝ.IsGreatest.Repair of the printed statement: the paper's direction assumption holds only for all sufficiently large , but Theorem 3.1 concludes (3.5) for each , and its proof uses the assumption at every . As printed the theorem is false: with the Wolfe step gives , which violates (3.5) at whenever . The goal therefore requires the direction assumption for every .
The step bound "there exists with " is stated with the algorithm's parameter. For the Armijo rule this holds by construction. The Wolfe rule does not use , so nothing is lost.
Trivializing formalizations are ruled out:
A complete development needs:
The NLSA definitions are reusable by any later mission on nonmonotone line searches. Proofs of the milestones in any order are welcome, as are a proof of the counterexample to the printed statement and a proof that the platform theorem ConvexOptimization.strong_convexity_quadratic_lower_bound implies (3.4).
In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first rounds.
The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.
Fix a dimension and an unknown parameter . In round the learner is given a nonempty decision set , chooses , and observes the reward
There is a filtration such that is -measurable and is -measurable and conditionally -sub-Gaussian: for all , with fixed.
For a regularization parameter let and let be the regularized least-squares estimate. With and a known bound , the confidence ellipsoid is
The OFUL algorithm chooses, in round , a pair maximizing over . The pseudo-regret is , where .
If , for all , and , then for every , with probability at least ,
For any positive definite , and : with probability at least , for all ,
With probability at least , for all (first claim). If , then with probability at least , for all , (second claim, stated here for ).
Theorem 3 bounds the regret of OFUL by with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.
All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases , , of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.
The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix , which is itself built from the adaptively chosen actions; a bound for each fixed does not give it.
Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed for , so sums over are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy ) requires; this is an added hypothesis. Every "with probability at least , for all " is stated as an outer-measure bound on the failure event, with the time quantifier inside the event. is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.
OFUL is a predicate on the whole process: in every round the chosen pair maximizes over , with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward is the supremum over , finite because of the reward bound.
Two corrections to the printed Theorem 3 are made and disclosed. The printed is replaced by , which is what the determinant–trace bound gives; for the corrected bound implies the printed one. The hypothesis is added: for the printed logarithm can be negative, and the printed bound would then assert . In the second claim of Theorem 2, is added, because at the claim does not follow from the first claim and the paper's proof is not available.
The goal is a probability bound over the noise, not the pathwise statement "if for all then ". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same as the conclusion.
Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on , log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general and , and reusable determinant lemmas are all welcome.
A cooperative game with transferable utility assigns to every coalition of players the total payoff the coalition can secure on its own. Two solution concepts for such games go back to the foundations of game theory: the core, the set of payoff divisions no coalition can improve upon, and the stable set (von Neumann–Morgenstern solution), a set of divisions that is internally consistent and externally absorbing under the relation of domination. For general games the two concepts behave badly: the core may be empty, stable sets may fail to exist (Lucas 1968), and when they exist there are usually many of them.
Lloyd Shapley's paper Cores of Convex Games (Int. J. Game Theory 1, 1971) isolates a class of games, the convex games (supermodular characteristic functions), on which all of this becomes well behaved. Convex games arise in cost allocation, in bankruptcy and airport problems, in scheduling and sequencing games, and in any setting with increasing returns to cooperation; the supermodular functions behind them are the same objects studied as polymatroid rank functions in combinatorial optimization (Edmonds 1970). For such games the paper shows that the core is nonempty, that its faces fit together in a rigid combinatorial pattern, that its vertices are exactly the marginal-contribution vectors, and that the core is the unique stable set.
Let be a finite set of players. A game is a function from subsets of to the reals with . It is convex if
A payoff vector is , and . It is feasible if . The core is the set of feasible with for every ; in particular on .
For a nonempty coalition , the face is the set of core points with ; by convention , and . The family is the core configuration. It is complete if no is empty, and regular if and
For an ordering of the players, is the set of the first players, and the marginal vector pays each player its marginal contribution .
A payoff vector is dominated by if some nonempty coalition has and for all . A set of feasible vectors is stable if every feasible vector is either a member of or dominated by a member of , but not both.
The goal contains both halves of the page's statement: stability of the core, and uniqueness ("the unique von Neumann–Morgenstern solution").
The mission also states Theorem 3 (p. 19), the vertices of a regular core are exactly the marginal vectors , as a further item that is not on the path to the goal.
The result. Theorem 8 gives, for a natural and widely occurring class of games, a complete answer to the existence and uniqueness questions for von Neumann–Morgenstern solutions, which are open or negative in general. Theorems 3 and 5 describe the core of a convex game explicitly as the polytope spanned by the marginal vectors, the combinatorial description that underlies later work on the Shapley value, the Weber set, and the polymatroid greedy algorithm. Theorem 5 is the geometric characterization of supermodularity through the face structure of the core.
Formalizing it. All results in this mission are proved in the paper; none has a machine-checked proof on the platform. Theorem 4 is already stated on the platform (as part of a statement that also puts every marginal vector and the Shapley value in the core) and enters the mission as an existing item. The remaining work is a formal development of face configurations of the core, of stable sets and domination, and of the passage from supermodularity to the geometry of the core. The definitions of stable set and domination are general and reusable for any transferable-utility game.
The internal half of stability is immediate from the definitions: a core point cannot be dominated by any vector satisfying a coalition constraint . Uniqueness also follows from two short observations. The substance is external stability: every feasible vector outside the core must be dominated by a core point, and the dominating vector has to be produced explicitly. The obvious attempt, raising the payoffs of one violated coalition and leaving the other coordinates of unchanged, does not in general produce a core point, and nothing in the definition of the core alone controls how the core meets the hyperplane of a given coalition; that control is what the face theory of §3 is about. For non-convex games the external half genuinely fails, so no argument that ignores convexity can succeed.
Players are Fin n (a relabelling of the paper's finite set ), a game is f : Finset (Fin n) → ℝ, payoff vectors are Fin n → ℝ, and is ∑ i ∈ S, a i. The existing platform definitions Supermodularity.Cooperative.IsConvexGame ( plus supermodularity on all subsets), Core, InitialCoalition and GreedyPayoff (the marginal vectors, orderings being permutations of Fin n) are reused; the reused Theorem 4 statement is Supermodularity.Cooperative.convex_game_core_and_shapley.
Conventions committed to:
IsConvexGame.Fin (m + 1).Set.extremePoints ℝ.A formalization in which the dominating coalition may be empty, in which regularity omits , or in which the goal asserts stability without uniqueness does not state the paper's theorem and is ruled out.
Welcome contributions: proofs of the milestones in any order, general lemmas about faces of polytopes cut out by set-function inequalities, and reusable API for domination and stable sets.
Call cube-free if no triple has all seven of , , , , , , inside . The triple is unconstrained, so a degenerate one counts. Write for the largest size of a cube-free subset.
The conjecture. for every .
This is Conjecture 5.1 of Jason Long and Adam Zsolt Wagner, The largest projective cube-free subsets of , arXiv:1810.01225. It has been open since October 2018, and a 2026 journal paper still names it as conjectured: Yuchen Meng, On Cube-Free Problems, Electron. J. Combin. 33(1) (2026) #P1.16.
The bound is sharp, and the extremal set is explicit: , the odd residues together with those congruent to 4 mod 8. Its size is . In the layer language of Long and Wagner this is .
The conjecture holds for unions of layers. That is Long-Wagner Theorem 1.10 at , and it is the largest class on which the conjectured constant is proved.
For arbitrary sets the best published unconditional bound is . Meng calls this bound "quite trivial" and gives it in one paragraph for every cyclic group, so it should not be read as progress toward . The residual gap is exactly , that is elements.
Small values are , , , , , , , matching from on.
State those values honestly. They come from solver searches, Gurobi in Long and Wagner for and an independent SAT reproduction. The SAT half that matters, the unsatisfiability of "a cube-free set of size 81 exists at ", is a solver claim with no proof certificate checked and no kernel check behind it. The witness half is verified: a set of exactly 80 elements was produced and re-checked cube-free. So is solid and is not certified. Nothing in this mission rests on either.
The goal item is the conjecture itself, for , and it is open. Every other item is a milestone that is proved mathematics, and the two closed instances and are stated separately because they are the only cases of the goal that a proof assistant has actually settled here.
The chain runs: the base case mod 8 by exhaustion, monotonicity under subsets, the bridge between the membership form and the Finset form of the forbidden configuration, sharpness, the odd-residue tight case, the layer-union theorem, the two-thirds bound, and then and .
Six definitions live in one definition item, Def_Z2nCubeFreeLayers: HasCube, CubeFree, config, ConfigFree, layerIdx and IsLayerUnion. layerIdx is written through the 2-adic valuation rather than through a congruence, because the congruence form leaves in no layer at all and needs the last layer special-cased.
CubeFree and ConfigFree are two encodings of the same condition and they are not definitionally equal, because config collapses duplicates on a degenerate triple. Their equivalence is a milestone rather than an assumption.