Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
The value
is the headline conditional witness of S. Jain's integer-mult-kappa, round eight, at revision 5868dc7. It is bound by the complex side ().
The repository states that the claim is conditional: it assumes the full upstream multiplication theorem (the OpenAI manuscript and Colkitt's framework) and that stage two is the complement time-reversal of stage one, and it rests on three further interfaces that are stated but not machine-checked there — IceKylin's normal form for alternating residuals, the cost of binary address adapters for the exterior fix-up children, and the row stock of the stopped bit interchange. Its Lean files check only finite rational statements (moment certificates, the stopped mix and the parameter assembly), not the analytic inequalities or the multiplication theorem. It has not had independent review.
Earlier claims appear as milestones: Harvey–van der Hoeven (), OpenAI Theorem 1 (), Colkitt's checkpoint, Jain rounds six and seven, and community PR #62. Each is implied by this goal because decreases in .
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
The value
is the conditional witness of S. Jain's integer-mult-kappa, round seven, at revision c05adfe, with the sharper moment certificate merged there (research/round7-moment-refinement/). The README's headline for the same construction is the slightly smaller ; the refinement keeps the frozen round-seven bit network, histogram, complex saving and assembly unchanged, and replaces the reciprocal bound in the moment certificate by a degree-eight Taylor enclosure, which certifies the bit saving .
The construction builds on the OpenAI manuscript and on Colkitt's integer-mult-bounds (it uses the PR #62 producer with interval strips and core-aware pair assembly). Its new ingredients are lifted frames with late copies, deferred readouts, and per-use leaves on the bit side; the complex side is round six's. The repository states that the claim is conditional on the OpenAI manuscript and Colkitt's framework, that stage two (the complement time-reversal of stage one) is assumed rather than machine-checked, and that its Lean files check only finite rational statements (moment certificates and parameter assembly), not the analytic tail inequalities or the multiplication theorem. It has not had independent review.
Earlier claims appear as milestones: Harvey–van der Hoeven (), OpenAI Theorem 1 (), Colkitt's checkpoint, Jain round six () and community PR #62 (). Each is implied by this goal because decreases in .
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
The value of the Riemann zeta function at five is the convergent sum
The target is that this number cannot be expressed as a ratio of integers. This mission concerns the complete proof development in mo271/Zeta5, pinned to commit 7fe736760f4b96bfdb4334b68e3b3124ecbe10b0. The repository follows Aabir Fauzan's preprint ζ(5) is irrational, while explicitly changing parts of its arithmetic normalization. Its formal target is the individual value at five. Results asserting that at least one member of a list of odd zeta values is irrational do not establish this target.
The repository reports a complete Lean proof with only the standard axioms propext, Classical.choice, and Quot.sound. That is a statement about the source project. The existing Prove2.me goal remains Open, and importing and checking the source proof against the platform environment is the work tracked here. The exact existing goal is reused as a reference; there is no second copy of the irrationality assertion.
The construction uses Hankel matrices, whose entries depend on the sum of their row and column indices. For a natural index , put , , and . The rational polynomial controls a family of rational functions. A rational linear functional takes prescribed Bernoulli-number values on powers of and prescribed affine-polynomial values on the simple poles . Polynomial division and residues extend it to .
Applying this functional to gives an matrix over . Write and , where is the explicit positive factorial ratio in the construction module. These are specified polynomials; their existence and properties are not abstract supply assumptions. The real number zeta5 is the convergent series, and a short bridge identifies it with Mathlib's complex zeta value.
The goal is
It is the existing theorem FCP.Zeta.irrational_zeta_five. The supporting target from the source main estimate is
The formal statement also requires to be a positive rational multiple of the explicit .
The milestone list records the general polynomial irrationality criterion, the exact degree calculation, the moment representation with integrability, strict determinant positivity, the real-value upper bound, integral normalization with its growth estimate, and the final small-value statement. A further supporting theorem states that tends to zero for every fixed positive integer and every . These targets cover the analytic, arithmetic, and final assembly parts of the source project.
The goal distinguishes a single zeta value from the disjunctive irrationality results for finite lists. The intermediate results also provide reusable infrastructure: an irrationality criterion for polynomials of varying degree, integral moment representations of rational functionals, determinant positivity, and estimates controlling rational normalizers.
For formalization, the concrete task is to transplant the source development while preserving its definitions, hypotheses, and actual constants. The source's existing proofs provide the intended implementations; the mission does not replace the difficult analytic or arithmetic statements with assumed approximation families. Proof imports and accepted submissions must eventually connect those implementations to the existing goal. The source's Apache-2.0 license and commit-pinned attribution accompany the code.
Small real values alone do not suffice: the integer coefficients and the degree growth must be controlled at the same time. The normalization needed to obtain integer coefficients can enlarge the values enough to destroy the analytic estimate. The decisive quantitative requirement is that its growth constant stay below the magnitude of the negative analytic constant.
Here the analytic estimate uses , and the implemented normalization uses . Their exact rational sum is negative. The milestone assertions retain the source's lower-order terms and the eventual quantifiers in the normalization estimate. They do not strengthen an eventual estimate to a uniform one, or infer positivity from a vanishing upper bound.
The scope is the complete importable proof path to Apery.irrational_five in the pinned repository, including the arithmetic modules, logarithmic-energy estimates, finite certificates, and the external prime-number-theorem dependency where the proof uses it. The headline milestones organize that full development; they are not a claim that every internal lemma is already published on the platform. The repository's optional stronger numerical rate and the preprint's irrationality-measure claim are outside this goal.
The source uses cutoff , a full rank loss in its outer-prime estimate, and direct class-wise partial fractions, as documented in its implementation notes. Its final estimate asserts some positive decay constant, not the paper's . The draft retains those choices. Polynomial evaluations take place over the reals, coefficients begin in the rationals and are normalized into the integers, and the moment integrals are Lebesgue integrals over . Definitions are total at zero, while the positivity and real-bound milestones explicitly require .
The source pins Lean 4.34.0-rc1 and Mathlib f385f9fd18abed332ebcd3df239cb357e264aceb. This proposal targets the available Lean 4.33.1 / Mathlib 0df444a360eaa60ab8c11dca51a86af692955474 environment. The draft definitions and milestone statements are checked locally in that target environment; acceptance of the complete imported proof graph is a separate verification step. The external dependency is mo271/PrimeNumberTheoremAnd at 04d81b2a68ea3548b9990813fdc463c78511f412. Any imported proof must retain a standard-axiom-only dependency check.
7fe736760f4b96bfdb4334b68e3b3124ecbe10b0. Pinned repository.RiemannZetaValues.irrational_five. Pinned challenge source.Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification of scheduling problems (Graham, Lawler, Lenstra and Rinnooy Kan 1979) with a resource field . They then drew the complete borderline between easy and hard problems for unit-time jobs, identical or uniform machines and the makespan criterion. Their Fig. 2 marks each problem type as polynomially solvable or NP-hard.
This mission formalizes the two hardness results of that classification that come from graph partition problems (Theorems 2 and 3, p. 15). Two identical machines are easy under any resource constraints (Theorem 1, after Garey and Johnson 1975). Theorems 2 and 3 show that a third identical machine, or two machines of different speeds, already makes the problem strongly NP-hard, once the number of unit resources is part of the input.
There are jobs and machines . Each machine processes at most one job at a time, and each job runs on one machine without interruption. Machine has a speed , and every job has unit execution requirement , so it takes time on . Identical machines () are the case ; uniform machines () allow arbitrary speeds.
There are resources . Resource has a positive integer size , the amount available at any time. Job needs a nonnegative integer amount of throughout its execution. A schedule assigns each job a machine and a start time . Its completion time is , and it is being executed at every time with . A schedule is feasible when:
The makespan is .
The resource type means three things: the number of resources is part of the input, every size is , and every requirement satisfies . A unit resource is therefore a conflict: two jobs that both need it can never run at the same time. The problems here have no precedence constraints. and ask for a feasible schedule of minimum makespan. Their decision versions ask, for a threshold , whether a feasible schedule with exists.
The source problems are two graph problems on a graph with :
Both are NP-complete (Garey and Johnson 1979, problems GT11 and GT13).
The construction of p. 15 introduces one job per vertex and one unit resource per nonadjacent pair , required by and only.
Formally: if the language of PARTITION INTO PATHS OF LENGTH 2 is NP-hard, then the language of unary codes of yes-instances of the decision version of is NP-hard. The two speeds are arbitrary positive integers.
The results. Theorems 2 and 3 are two of the minimal NP-hard problems in the paper's classification. Together with Theorem 1 they place the borderline exactly: with unit resources whose number is part of the input, two identical machines are polynomial, while three identical machines, or two machines of different speeds, are strongly NP-hard. Strong NP-hardness rules out pseudo-polynomial algorithms unless P = NP, and it carries over to every more general resource type and machine environment in Fig. 1 and Fig. 2. Section 4.1 of the paper also derives hardness for and from these instances.
Formalizing it. The results are classical and proved on paper, but the paper's proofs are one sentence each ("Clearly", "It is easily seen"). No machine-checked proof exists, and the platform has no model of resource-constrained scheduling with real-valued time. This mission produces that model. It also produces a precise statement of strong NP-hardness on top of Cook's Turing-machine definitions, and the first formal NP-hardness reductions from graph partition problems to scheduling.
The scheduling half of each equivalence depends on the real-time model. On two uniform machines of speeds 2 and 1, jobs take time and , so jobs on the fast machine start at half-integers or anywhere else. The resource constraint must hold at every real time, not at a finite set of checkpoints. An argument that treats time as integer slots applies to the triangle case but does not transfer to the paths case.
The complexity half needs polynomial-time computability of the construction on Cook's one-tape Turing machines, on encoded strings that include malformed inputs. It also needs closure of polynomial-time reductions under composition, which the imported complexity layer states but does not prove.
Fin n, Fin m, Fin l), so are q 0, q 1.CookPvsNP_defs.CubicP3Partition.P3Factor, a spanning non-induced -factor.Welcome contributions: proofs of the two equivalences, polynomial-time computability of the construction on Cook's machines, and a general composition lemma for polynomial-time reductions. The composition lemma is reusable for every hardness mission built on CookPvsNP_defs.
Several classical min-max theorems of combinatorial optimization say that a discrete maximization problem and a continuous minimization problem have the same optimal value, and that both have integral optimal solutions when the data are integral. Edmonds' polymatroid intersection theorem (1970), Fujishige's Fenchel-type duality for submodular functions (1984), Frank's discrete separation theorem for a submodular/supermodular pair (1982), and the potential characterizations of weighted matroid intersection (Frank's weight splitting theorem, 1981; Iri and Tomizawa's criterion for the assignment problem, 1976) are instances. Murota's paper Convexity and Steinitz's exchange property, 1996 places all of them under one theorem: a Fenchel-type min-max formula for a pair of an M-concave and an M-convex function, with integrality on both sides.
Timeline:
Let be a finite nonempty set. For , is its characteristic vector; for , are the sets of coordinates where is positive or negative, , and .
A finite integral base set is a finite nonempty such that for and some has . These are exactly the integer points of integral base polytopes of submodular systems. is the convex hull of .
A function has the exchange property (EXC), and is called M-concave, if for and some has and
A function is M-convex when is M-concave.
For and the concave conjugate and convex conjugate are
and the concave closure and convex closure are and ; they are finite exactly on and .
The primal problem maximizes over ; the relaxed primal problem maximizes over ; the dual problem minimizes over . A maximum over an empty family is .
If and satisfy (EXC), then
with (P1) a finite dual infimum forces , and (P2) if all values are finite and equal and the infimum is attained. If are integer-valued, the infimum may be taken over and is attained there when finite.
The formula gives, in one statement, the integrality of an optimal solution of the relaxed primal problem (the essential content of the first half, as the paper observes on p. 296) and of the dual problem. The paper presents it as a unification of two groups of theorems: Edmonds' polymatroid intersection theorem, Fujishige's Fenchel-type duality and Frank's discrete separation theorem on one side, and Iri and Tomizawa's potential characterization for independent assignment with its extensions by Fujishige and Frank (weight splitting) on the other. In the paper it yields the primal and dual separation theorems (Theorems 6.8, 6.9) and the convolution results (Theorems 6.10, 6.11), and it is the prototype of the Fenchel-type duality of discrete convex analysis.
All results here are proved in the literature; none is known to be formalized. Mathlib has no submodular base polytopes, no matroid intersection theorem and no discrete convex analysis. A formal proof of Theorem 6.4 would also require formal proofs of the two cited results, Frank's discrete separation theorem and the M-concave intersection theorem, which the paper uses without proof.
Lemma 6.3 is polyhedral convex duality and holds for any functions. The content is equality with the integral problem: the relaxed maximum over the polytope must be attained at an integer point. For general finite sets it is not, and the intersection of two integral polytopes generally has fractional vertices. Both the integrality of (Edmonds) and the existence of an integral optimal potential depend on the exchange structure; a direct argument from the definitions of conjugates does not see it. The dual integrality claim, that can be taken integral, is again specific to (EXC) and fails for general concave extensions.
Lean conventions, all in namespace SteinitzExchange.Duality:
[Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ; finite sets of integer vectors are Finset (V → ℤ).(V → ℤ) → ℝ used only at points of . M-convexity of is (EXC) for fun x => -ζ x; lives on and on , which are distinct sets in general.⨅/⨆ over and are evaluated only on the convex hulls, where they equal the paper's values; off the hulls they carry a junk value instead of , which no statement uses.EReal, as suprema and infima of coerced reals, so no occurs. EReal's supremum of the empty family is , the paper's convention. The dual infimum is never a real ⨅ (which would return when unbounded and make (P1) meaningless).V → ℤ.Formalizations that would trivialize the goal are excluded: an unrestricted real infimum for the dual, a convex closure built from instead of , a single base set for both functions, and a relaxed maximum taken over all of instead of .
Needed infrastructure: finite convex hulls and polyhedral Fenchel duality, submodular base polytopes and their integrality, Frank's separation theorem, and the valuated intersection theorem. The submodular-system layer (Theorem 2.1, Theorem 6.5) is reusable beyond this mission. Contributions to any milestone, including proofs of the two cited theorems, are welcome.
Matroids and their integral generalizations, integral base polytopes, are the combinatorial structures on which the greedy algorithm is exact. Edmonds' theory relates them to submodular and supermodular set functions: a polytope is a base polytope exactly when its support function, restricted to vectors, is supermodular and the greedy formula evaluates it everywhere. Dress and Wenzel's valuated matroids (1990) and Murota's M-concave functions carry the exchange axiom from sets to functions on sets. This paper (Adv. Math. 124, 1996) sets up the resulting theory of discrete concave functions on base sets, later developed into discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003).
The question behind this mission is how the set-level correspondence between exchange and supermodularity extends to functions. Section 5 of the paper answers it with the Local Supermodularity Theorem: the exchange property of a function is a supermodularity property of its concave conjugate, holding locally at every point.
Let be a finite nonempty set, . For let be the unit vector, for let be its characteristic vector, , and . For a finite , is its convex hull.
A finite integral base set is a finite nonempty such that
A function satisfies the exchange property (EXC) (is M-concave) if for and there is with and . Write and for the maximizers of on .
The support function of is . A positively homogeneous is "matroidal" if
The concave conjugate is , the concave closure is , the subdifferential is , and the localization of at is .
For on a finite integral base set ,
The printed Theorem 5.3 has only the second condition on the right. Its "only if" direction holds as printed; its "if" direction is false without the first condition, and a separate item of the mission states the counterexample: , .
The result. Theorem 5.3 is the function-level version of Theorem 5.1. Condition (C1) is a supermodularity condition, so the theorem expresses (EXC) as "a collection of local supermodularity" properties of , in the same way that (B1) corresponds to supermodularity of a support function. In the paper this characterization of the conjugate side underlies the Fenchel-type duality of Section 6, and more generally the conjugacy between M-concave and L-convex functions in discrete convex analysis.
The formalization. No part of this theory is formalized in Lean or on this platform: base sets, (EXC), "matroidal" functions and concave conjugates of functions on base sets are all new. The mission also corrects the published statement: the reduction from localizations to base sets needs every integer point of to be a maximizer, and the concave-closure condition supplies this. A machine-checked proof would settle both the corrected theorem and the counterexample. Theorem 2.1 and Lemma 5.2 are classical but have no formal proof either.
depends only on the concave closure , so any characterization of (EXC) through alone cannot see values of below . That is why the goal needs the extra clause. The "only if" direction needs the full theory of Section 4: M-concave functions coincide with their concave closure, and all their maximizer sets are base sets. Theorem 5.1 needs the greedy algorithm on integral base polytopes, together with the fact that the base polytope of an integral supermodular function has integral vertices. Theorem 2.1 is the folklore statement that polyhedral and exchange descriptions agree, and the paper does not prove it. Eq. (5.12) needs the subdifferential of a finite minimum of affine functions to be the convex hull of the active gradients, stated globally rather than only near .
Integer vectors are V → ℤ, real vectors V → ℝ, with [Fintype V] [DecidableEq V] [Nonempty V]. A finite subset of is a Finset (V → ℤ). A function on is a total function (V → ℤ) → ℝ whose values off are never used. The mission commits to the following readings:
sInf over the subdifferential, defined by (5.8)–(5.9) exactly, not by the formula (5.12). Eq. (5.12) is stated with IsLeast, so it asserts attainment, not just the value.Fin n ≃ V along which is non-increasing. This is equivalent to "for some" such indexing. "Matroidal" includes positive homogeneity but not concavity.Trivializing formalizations are ruled out. Defining by (5.12) would reduce the goal to Theorems 4.4 and 5.1. A "matroidal" without (C2) would be satisfied by support functions of non-base sets. An taken as a supremum would reverse the sign conventions.
The development needs: the greedy algorithm and integrality for integral base polytopes, supergradients of polyhedral concave functions, and the Section 4 results of the paper (concave closure of M-concave functions, Lemma 4.3). The base-set and "matroidal" layers can be reused beyond this mission. Proofs of any milestone, of the counterexample, and a proof of the "only if" direction on its own are all welcome.
Linear optimization over the bases of a matroid, over the integer points of a polymatroid, or over the flows of a network is well understood: the greedy algorithm is exact, the feasible sets are the integer points of polytopes described by submodular functions, and min-max theorems of Edmonds and Frank hold with integrality. Nonlinear objectives on the same sets are much less uniform. Valuated matroids (Dress and Wenzel, 1990; see Murota 2003) showed that a quantitative form of the Steinitz exchange axiom is exactly what keeps the greedy algorithm exact for a nonlinear weight. Kazuo Murota's paper Convexity and Steinitz's Exchange Property (Adv. Math. 124 (1996) 272–311) extends this exchange axiom from matroid bases to the integer points of arbitrary integral base polytopes, names the resulting functions M-concave, and proves that they are the discrete counterpart of concave functions. The paper is the starting point of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003), which is now used in auction theory (gross-substitutes valuations are M♮-concave), inventory and resource allocation, and combinatorial optimization.
This mission covers the first of the paper's three characterizations of M-concavity: the Extension Theorem (Theorem 4.6).
Let be a finite nonempty set. For , is the characteristic vector of . For , , , , and .
A finite integral base set is a finite nonempty such that for and there is with (axiom (B1)). Examples are the incidence vectors of the bases of a matroid. Its convex hull is an integral base polytope; in general, an integral base polytope is the convex hull of some finite integral base set.
A function satisfies the exchange property (EXC), and is called M-concave, if for all and there is with , and
The local exchange property (EXC) asks only, for with , for some and some with the same conclusion.
For , , and . For any , the concave conjugate is and the concave closure is , a concave function that is finite exactly on . A function extends if on .
For a finite integral base set and ,
The Extension Theorem identifies a combinatorial axiom with a convex-analytic property: M-concave functions are exactly the restrictions to lattice points of concave functions on the base polytope whose linear perturbations are all maximized on integral base polytopes. It is the reason the M-concave class supports a convex-analysis-style theory at all: local optimality implies global optimality, maximizers of linear perturbations are well behaved, and conjugacy (the paper's Theorems 5.3 and 6.4, separate missions of this series) can be developed. Theorem 3.1 on its own is widely used to verify M-concavity in applications, since it reduces the exchange axiom to pairs at distance four.
All results here were proved in 1996. To our knowledge none of them has a machine-checked proof; Mathlib has matroids on sets but no integral base sets in , no M-concave functions and no concave closure of a function on a finite set. A formal proof of this chain would be a first formal development of discrete convex analysis.
The equivalence of (EXC) with its local version (Theorem 3.1) is not a routine induction on : the exchange inequality for a far pair does not follow from the inequalities along a path of distance-4 pairs, because the exchange partner must be chosen consistently with the prescribed . For the "if" direction of Theorem 4.4, knowing that every maximizer set is an integral base set says nothing directly about the values of at non-maximizing points; turning this global information on maximizers into the local inequality (EXC) requires a supporting hyperplane of the concave closure at a well-chosen point and the integrality of the intersection of an integral base polytope with a box (a cited result on submodular systems). Theorem 4.6 then needs the concave closure to agree with on (Lemma 4.5), which fails for general .
All declarations live in the namespace SteinitzExchange.Extension. The ground set is a type V with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ, and toReal embeds the former into the latter. is a Finset (V → ℤ). A function is a total (V → ℤ) → ℝ whose values are only ever read at points required to be in . is Mathlib's convexHull ℝ of the image of . Pinned readings:
Trivializing formalizations are ruled out: the extension must agree with on and be concave on , the argmax is over and not over , and an integral base polytope is never empty.
A complete development needs basic facts on integral base sets (the equivalence of (B1) with the simultaneous exchange (B2), , and the paper's cited Theorem 2.1 relating them to submodular functions), the representation (4.3) of the concave closure as a maximum of convex combinations, and supporting hyperplanes of polyhedral concave functions. The layer of integral base sets and M-concave functions is reusable for the two other missions of this series and for any later formalization of discrete convex analysis; contributions of general-purpose lemmas about it are welcome.
The Riemann zeta function at integers splits into two very different worlds. At even arguments Euler's formula shows every is a rational multiple of , hence irrational and even transcendental. At odd arguments almost nothing is known. The single exception is , proved irrational by R. Apéry in 1978 (Astérisque 61 (1979), 11–13). For every other odd argument the arithmetic nature is open to this day: no individual value is known to be irrational.
What is known are localisation results, which assert that an irrational number occurs somewhere in a finite or infinite list of odd zeta values without saying where.
All objects below are those of the source note, in its own notation.
Fix odd integers and with , and positive integers subject to and
For each integer put and for , and consider the rational function
together with the linear form
Condition (1) gives , so the series converges.
Two arithmetic quantities control the denominators of . Write for the least common multiple of , put for , and set
the product running over primes, where is the integer-valued, nonnegative, -periodic function
The growth of is governed by the saddle points, the zeros of
and by the auxiliary function
Writing for the zero with of largest real part, the two competing constants of the method are
with the logarithmic derivative of the gamma function.
The goal fixes no witness: the statement is satisfied as soon as one of the four values is irrational, and remains the honest form of what the source proves. It is deliberately weaker than the (open) statement that each is irrational, and weaker than any claim identifying which of the four is irrational.
The milestones follow the source's own numbering: Lemma 1 (the linear form and its denominators), the prime-number-theorem asymptotics of , Lemma 2 (the saddle-point asymptotics of for ), the small-values criterion for display (4), Lemma 3 (the criterion ), and the numerical verification of at , , , , for , where and .
The result itself. Together with Apéry's theorem it gives the smallest list of small odd zeta values known to contain an irrational number, and it fixes the current record of the Ball–Rivoal hypergeometric method: the same machinery yields quantitative lower bounds for the dimension of the -span of odd zeta values, and any improvement of the arithmetic factor or the saddle-point estimate propagates directly to those bounds.
Formalizing it. The result is proved mathematically; nothing here is open. What is missing is a machine-checked proof. Mathlib contains the Riemann zeta function, the gamma function, and the prime number theorem, but not Apéry's theorem, not the Ball–Rivoal construction, and not the Chudnovsky–Rukhadze–Hata arithmetic method. A complete development produces reusable infrastructure: integrality of very-well-poised hypergeometric sums, the / denominator-saving mechanism, saddle-point asymptotics for a Barnes-type complex integral, and the standard linear-form irrationality criterion.
The obvious route — exhibit explicit rational approximations to a single and estimate them — fails, and that failure is the content of the field: no construction is known that separates a single odd zeta value. Zudilin's construction instead produces one real sequence that is simultaneously a -linear form in ; irrationality of some coefficient's argument then follows from the two-sided estimate, but the argument is blind to which one.
The three hard steps are independent of one another. First, integrality: the coefficients of have denominators controlled by , and the extra factor — a product of prime powers extracted from the -function — must be divided out; this is a delicate -adic valuation count. Second, asymptotics: the exact exponential rate of comes from a complex integral over a vertical line, evaluated by the saddle-point method at a zero of a degree- polynomial with no closed form. Third, the final comparison is a numerical inequality between two transcendental-looking constants that must be certified rigorously, including a Stieltjes integral of a piecewise-constant function against the digamma function.
Statements are formalized over the reals, with for an integer represented by the convergent series (zetaR); a bridging statement identifies it with Mathlib's riemannZeta at natural arguments, so the goal theorem may be stated with riemannZeta as it already is in the platform library. Admissible parameter sets are a structure carrying , , the sequence , and the hypotheses of the source, so no theorem quantifies over parameters the source excludes. R is a real-valued function of a real variable built from Real.Gamma, and is the tsum of its -st iteratedDeriv at natural arguments; convergence is a separate milestone rather than a silent assumption, so that the value is not asserted to exist by fiat. is the infimum over of the integer-valued expression above, a finite product over primes with (the integer form of ), and the Finset.lcm of . The Stieltjes integral is written as , which agrees with the Riemann–Stieltjes integral because is continuously differentiable on ; uses the principal branch of the complex logarithm.
The saddle point is not defined by a choice function: every statement that mentions it takes it as a parameter together with the hypotheses "root of the polynomial", "positive imaginary part", "maximal real part among such roots", and the two side conditions and of Lemma 2. No milestone is vacuous: for the concrete parameter set of the source such a exists, with .
Contributions of any size are welcome, including partial infrastructure: -adic valuation lemmas for products of factorials, asymptotics of Finset.lcm, saddle-point estimates, and interval-arithmetic machinery for the final numerical comparison.
A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range , and let it degrade at a controlled rate outside, proportionally to the distance from . That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.
Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most " has no direct meaning. What replaces it is the observation that a scalar inequality is the inclusion , and that the violation is the distance from the left hand side to . In that form the notion lifts verbatim, and the whole chapter follows.
Definition 11.1.2. Consider an uncertain convex constraint
with nonempty, closed and convex. Let the perturbation space split as , each factor carrying a normal range , a closed convex cone and a norm , and let be a norm on . A candidate is robust feasible with global sensitivities if
where and .
The object that makes the analysis work is the recessive cone of (Definition 11.3.1): for any ,
which does not depend on and is a nonempty closed convex cone.
A candidate is feasible for the GRC (11.1.6) if and only if it satisfies the system
Line (a) is the ordinary robust counterpart over the normal range. Each line (b) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to itself.
The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.
The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function
of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that of a map with respect to a setup equals of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.
The recessive cone results are the vocabulary. The one that earns its place is : the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.
The goal is an equivalence and the two directions are asymmetric.
Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix and in the unit ball of , and run out along the cone. The GRC bounds the distance to by , so there are with ; the rescaled points stay bounded, and a limit point of them lies in by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not — is what appears in lines (b).
Backward is a decomposition-and-assemble: split each with , realizing the distance, get a point of from line (a) and a recession direction from each line (b), and add them — using that .
Proposition 11.4.1 is a chain of polarity identities: the polar of is for compact convex containing the origin, the polar of a norm ball of radius is the dual-norm ball of radius , and bipolarity. Each step is standard and the composition is not.
Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function .
Conventions committed to:
IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and
nonnegativity follows from them.Call a set of reals a Sidon set when all its pairwise sums are distinct: if with all four in the set, then .
The goal. There is an absolute constant such that every finite set of positive reals contains a Sidon subset with .
This is the lower bound half of Erdos problem 530, which Riddell posed and which asks for the order of the largest guaranteed Sidon subset. That problem is open: it asks whether the guarantee is asymptotically , and the constant is not known. What is settled is the order, by Komlos, Sulyok, and Szemeredi, Linear problems in combinatorial number theory, Acta Math. Acad. Sci. Hungar. 26 (1975) 113-121, as a case of a general theorem about linear equations. Erdos had previously observed the cube-root lower bound and the matching upper bound from . A second and much shorter proof is in Bailleul and Riblet, arXiv:2605.03181.
A one-paragraph argument gives : take a Sidon subset of maximum size, and note that every outside it satisfies or for elements of , so .
That cube root is not a weak first attempt, it is the ceiling for any argument that only counts. An arithmetic progression of length has additive energy of order , so a probabilistic argument cannot see the difference between it and a generic set. Getting from to requires using the structure of the set, and that is what both published proofs do.
Compress, then pigeonhole against a known Sidon set.
An arbitrary finite set of reals has no arithmetic to work with, so first move it into : a finite set spans a finite dimensional -vector space, and a generic rational functional separates its points while preserving every relation . Then squeeze the resulting integers into an interval of length comparable to their number, keeping a constant fraction of them and keeping the property that a Sidon subset of the image lifts to one of the original. Finally intersect with a translate of the Erdos-Turan Sidon set, which has about elements inside . A set of size inside meets some translate of a Sidon set of size in order points, and that intersection is Sidon.
The two proofs differ only in the compression step, and the mission carries both.
The 1975 route compresses in four lemmas driven by a remainder map: choose a modulus dividing no difference, dilate so that the remainders are small, and observe that a small remainder map preserves . Finding the modulus needs a prime counting bound.
The 2026 route replaces all four with one averaging lemma over a real rotation parameter , keeping the elements whose fractional part of is below , where no carry occurs. No prime counting appears anywhere.
Every item is stated in Mathlib primitives alone, so the mission needs no definition items. The Sidon condition, the Erdos-Turan construction, and the reduction relation of the 1975 route are all written out at each use.
The published 2026 proof finishes with Singer's 1938 covering of by Sidon sets. Mathlib has no perfect difference sets, so the mission uses averaging over translates instead. It does the same job at the same order and gives a worse constant, which costs nothing because the goal asserts only that some exists.
Two lemmas of the 1975 paper are deliberately absent. A local formalization of Lemma 2 and Lemma 6 turned out to be false as stated, machine-checked in both cases, so neither is offered here as a milestone. Those are errors in that rendering rather than in the paper, and the 2026 route reaches the goal without either. Lemma 1' is absent for the same practical reason: the 2026 route does not need it.
Chapter 9 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) develops the differential calculus of mappings . The definition of the derivative changes character: it is no longer a number but a linear transformation , the one that approximates the increment of to first order. Once that is in place, the chapter proves the two theorems that make nonlinear analysis possible: the inverse function theorem (Theorem 9.24), which says that a continuously differentiable map with invertible derivative at a point is locally invertible with a continuously differentiable inverse, and the implicit function theorem (9.28), which solves locally for in terms of .
The message of both is that a nonlinear map behaves locally like its linearization, provided that linearization is invertible and varies continuously.
This mission is the ninth in a series formalizing Rudin Chapters 1–11; it uses the completeness and compactness results of Missions II and IV and the mean value estimates of Mission V, and it prepares the change-of-variables machinery used in Mission X.
is the space of linear maps with the operator norm . A map defined on an open is differentiable at with derivative if
and — a -mapping — if it is differentiable on and is continuous. The partial derivative is the derivative of at . A map of a metric space into itself is a contraction if for some .
Let be a -mapping of an open into and suppose is invertible at some . Then there are open sets and such that
The inverse function theorem is the local classification statement of differential calculus: it says that the only local obstruction to invertibility is degeneracy of the derivative, and it is the mechanism behind coordinate changes, the rank theorem (9.32), and the change-of-variables formula for integrals in Chapter 10. The implicit function theorem is its standard reformulation and is what makes level sets of smooth maps into manifolds. Theorem 9.21 is the practical criterion for the hypothesis, since it reduces it to continuity of finitely many partial derivatives; Theorem 9.41 shows that the symmetry of second derivatives, though intuitive, requires a hypothesis; Theorem 9.19 is the several-variable substitute for the mean value theorem, whose equality form already failed in Chapter 5.
Mathlib has the Fréchet derivative, the inverse and implicit function theorems for Banach spaces, the Banach fixed-point theorem, and symmetry of second derivatives. This mission states the Rudin versions concretely in — with the explicit open sets and and the inverse mapping produced as data, rather than through a bundled local homeomorphism — and so provides a bridge between the book's formulations and the library's.
The inverse function theorem is the first theorem in the book whose proof combines several chapters at once: the contraction principle (9.23) gives local surjectivity by solving as a fixed point of ; openness of the set of invertible operators (9.8) keeps the derivative invertible near ; the mean value inequality (9.19) controls the error; and the continuity of inversion gives the regularity of . The delicate point is that all estimates must hold uniformly on a neighbourhood chosen in advance, so the order in which the neighbourhoods are shrunk matters.
For Theorem 9.41 the trap is the hypothesis: continuity of at the single point is assumed, not continuity of both mixed partials on a neighbourhood; the conclusion is existence of at that point, and it genuinely fails without some such hypothesis.
Conventions fixed by this mission:
EuclideanSpace ℝ (Fin n); linear maps are →L[ℝ] (continuous linear
maps), which in finite dimension is the same as Rudin's , with
the operator norm.HasFDerivAt, and the condition is ContDiffOn ℝ 1.HasDerivAt of the line restriction
t ↦ f (x + t • eⱼ) at t = 0, avoiding any coordinate-projection bookkeeping;
eⱼ = EuclideanSpace.single j 1.Function.Bijective, which for a continuous linear map
between finite-dimensional spaces is equivalent to the existence of a continuous linear
inverse.inv constrained on the invertible
operators, so that continuity of inversion can be stated without bundling.D1f, D2f, D21f, which
is how Rudin states the hypotheses, and the conclusion asserts existence of D₁₂f at the
point as a HasDerivAt statement.α increasing and φ(·,t) ∈ ℛ(α).A strongly regular graph with parameters is a finite simple graph on vertices in which every vertex has exactly neighbours, every pair of adjacent vertices has exactly common neighbours, and every pair of non-adjacent vertices has exactly common neighbours. For most parameter tuples the elementary counting and integrality conditions already decide existence; the interesting cases are those that survive every known feasibility test and still resist construction. The tuple is the smallest such case in the family , , and its existence has been open for more than fifty years. John Horton Conway offered $1000 for a resolution, as one of five problems posed at the 2014 DIMACS conference on Challenges of Identifying Integer Sequences (Conway, Five $1,000 Problems (Update 2017)).
Timeline of the problem and of what is known about it:
No graph with these parameters has been found, and no non-existence proof is known.
Fix a finite vertex set and a simple graph on (irreflexive, symmetric adjacency ). For vertices write for the neighbourhood of and for the set of common neighbours. The graph is strongly regular with parameters , written , when
The case says that every edge lies in exactly one triangle — equivalently, the neighbourhood of each vertex induces a perfect matching, so such graphs are locally linear. The case says that every non-adjacent pair is the pair of opposite corners of exactly one -cycle. Conway's problem asks for with these two local conditions.
Counting paths of length two from a fixed vertex gives , which for , reduces to ; with this yields . Writing for the adjacency matrix, for the identity and for the all-ones matrix, strong regularity is equivalent to the matrix identity , which for reads ; the eigenvalues of other than are then and , and integrality of their multiplicities ( and ) is one of the feasibility conditions that passes.
The goal is Mathlib's own proof_wanted conway_99 in Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean, stated verbatim: existence of a finite type carrying a strongly regular graph with parameters . A resolution in either direction is welcome — a proof settles the existence half, and a proof of the negation settles the non-existence half; the platform records the two as proof and disproof of the same statement.
for every strongly regular graph with , : the counting identity, local linearity, and the integrality restriction that cuts the family down to five non-degenerate parameter tuples.
the two members of the family that are known to exist: the rook's graph (the Paley graph on vertices) and the Berlekamp–van Lint–Seidel graph.
structural consequences for a hypothetical -graph, the last one being Wilbrink's theorem.
A graph, if it exists, is a locally linear graph of maximal density in its parameter range and a partial linear space of girth with points and lines of size ; its existence would also produce new association schemes and new examples for the general classification of strongly regular graphs. A non-existence proof would be the first case in this family ruled out by anything other than the classical feasibility conditions, and would say something new about how far local conditions (, ) constrain global structure.
Nothing in this mission is presently formalized. Mathlib defines SimpleGraph.IsSRGWith, proves the counting identity IsSRGWith.param_eq, the complement rule IsSRGWith.compl, and the matrix identity IsSRGWith.matrix_eq, and records the -graph problem as a proof_wanted. The supporting targets are of three kinds: results that are proved in the literature and only need formalizing (existence at and ; Wilbrink's non-vertex-transitivity; the integrality restriction on ); routine consequences that supply reusable infrastructure (edge and triangle counts, the spectral identity, evenness of ); and the goal itself, which is open mathematics.
The obvious approaches fail for concrete reasons. Exhaustive search is out of range: the graph has edges among pairs, and no isomorph-free generation of locally linear graphs on vertices is feasible. Algebraic constructions are blocked by Wilbrink's theorem — the graph cannot be vertex-transitive, so it is not a Cayley graph and cannot be produced by the group-theoretic constructions that yield most known strongly regular graphs, including the two that work at and . On the non-existence side, every classical feasibility test (the counting identity, integrality of the eigenvalue multiplicities, the Krein conditions, the absolute bound) is passed by , so a proof of non-existence needs an argument that does not factor through the parameters alone.
All statements are phrased with Mathlib's SimpleGraph.IsSRGWith on a Fintype vertex type with DecidableRel adjacency, and use Fintype.card, SimpleGraph.edgeFinset, SimpleGraph.cliqueFinset 3 (triangles as -cliques), SimpleGraph.adjMatrix over , and graph isomorphisms g ≃g g for automorphisms. The goal quantifies over α : Type together with a Fintype α instance, so the vertex set is finite by construction and the empty type does not satisfy the cardinality clause; the statement is therefore not vacuously satisfiable. Note that Mathlib's definition constrains only through pairs that are actually adjacent and only through pairs that are actually distinct and non-adjacent, so degenerate small graphs (the one-vertex graph, ) do satisfy IsSRGWith with , ; the supporting statements carry the cardinality hypotheses (, ) that exclude them where needed, and the degenerate degree is listed explicitly in the classification of feasible degrees.
Infrastructure a complete development needs, and which is reusable beyond this mission: interface lemmas for counting common neighbours in a strongly regular graph; the spectral theory of the adjacency matrix (multiplicities of the two non-principal eigenvalues, and their integrality), which is the missing ingredient for the classification of feasible degrees; a Lean construction of the perfect ternary Golay code and its coset graph, for the case; and decision procedures for strong regularity of an explicitly given small graph, for the case. Contributions to any of these are welcome, as are partial non-existence results (for instance, restrictions on automorphisms of prime order) submitted as separate statements.
Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.
Fix vectors with Euclidean norm . A sign vector is an : one sign per vector. Writing for the -th coordinate of the vector , the discrepancy of the family under is the largest coordinate, in absolute value, of the signed sum — that is, , the norm of the signed sum. The Komlós property at constant — KomlosBound K — says that every such family, in every and every , admits a sign vector with every coordinate of the signed sum at most in absolute value.
Set systems embed as the special case of -incidence matrices: if is an matrix of s and s in which every column has at most ones (every element lies in at most sets), the columns scaled by have norm at most one, so the Komlós property gives discrepancy — the Beck–Fiala conjecture.
The goal fixes no value of : any finite universal constant settles it, so the statement survives every improvement in the constant.
Eight results over the same definitions: Beck–Fiala's for degree- set systems; Spencer's for sets on points; Banaszczyk's for the Komlós setting; its corollary for set systems; the reduction "Komlós at implies Beck–Fiala at "; Kunisky's lower bound ; and the two 2025 Bansal–Jiang breakthroughs — for the Komlós setting, and the Beck–Fiala conjecture's bound in the regime .
The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.
None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.
Random signs lose: they give , not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least — so any proof must handle instances strictly harder than the set-system case.
The Lean model commits to: vectors as EuclideanSpace ℝ (Fin m), whose norm is the norm (the hypothesis reads ‖v i‖ ≤ 1); the conclusion written coordinatewise as ∀ j, |∑ i, ε i * v i j| ≤ K, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with ε i = 1 ∨ ε i = -1; and set systems as matrices A : Fin m → Fin n → ℝ with an entrywise hypothesis and column-degree counted by Set.ncard. Quantifier order matters everywhere: in KomlosBound K the constant is fixed before and — a depending on would make the statement the trivial bound. In beck_fiala the hypothesis is required (the degree- system has discrepancy otherwise); the Banaszczyk-form bounds use so that the bound is positive already at . In the Bansal–Jiang milestones the asymptotic and are rendered by existential constants quantified before all instances: the hidden factor becomes for some fixed (the inner shift keeps the iterated logarithm positive), and the threshold becomes for some fixed .
Welcome contributions: any milestone in any order — beck_fiala and komlos_implies_beck_fiala are self-contained finite arguments and the natural entry points; spencer_six_deviations and banaszczyk_bound each import a major technique; komlos_lower_bound needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.
Harmonic maps into singular nonpositively curved spaces arise in geometric analysis, rigidity theory, and the study of group actions on buildings. Near a point in the domain, their infinitesimal growth is measured by an order, obtained from an Almgren-type frequency quotient. For smooth targets that order is tied to familiar Taylor expansion data. Euclidean buildings are instead assembled from Euclidean apartments along reflection walls, so a map can branch through a singular link and a priori might exhibit a much less controlled spectrum of homogeneities. Breiner and Dees prove that, for maps from surfaces, this spectrum is discrete and is governed by the finite rotational Weyl group of the building. The mission formalizes their headline classification theorem, Theorem 1.1 of Breiner--Dees.
The discreteness matters because frequency information is a basic input to stratification and regularity arguments for singular harmonic maps. A finite list of possible denominators prevents homogeneities from accumulating arbitrarily and isolates rank-one behavior. The formal target makes explicit the nonconstant condition used by the source paper's tangent-map reduction. Without it, the usual numerator and denominator of the frequency quotient both vanish for a constant map, so its order is not defined.
A Euclidean Coxeter complex consists of Euclidean space together with an affine reflection group. Taking the linear parts of its affine isometries produces a finite rotational reflection group . A Euclidean building of type is a complete metric space covered by isometric Euclidean apartments whose overlaps are related by elements of the affine Weyl group; the atlas is required to contain the relevant geodesic segments, rays, and lines and to be maximal with these compatibility properties.
The domain is a connected open subset of a complex one-dimensional manifold, hence a Riemann surface domain. The formalization uses a concrete Korevaar--Schoen-style metric Sobolev energy built from normalized local difference quotients and Lebesgue area in charts. A map is harmonic when it has finite local energy and minimizes that energy against competitors with the same trace. For and small radii , the energy and boundary moment determine a frequency quotient. When its limit exists with positive denominator, that limit is the order .
For a nonconstant energy-minimizing harmonic map and any , prove that the order is defined and that there are positive integers such that
If the building has rank one, prove the sharper form
The same theorem also records the small-scale energy and positive-boundary-moment facts needed for the order to be meaningful; these are conclusions, not assumptions supplied by a solver.
The result identifies a purely algebraic constraint on an analytic singularity invariant: every denominator divides the order of the finite rotational Weyl group. In rank one, where the target is a tree or an -tree, it recovers the half-integer spectrum and its lower bound. This converts an apparently continuous local invariant into a discrete one determined by the building type.
Formalizing the theorem requires reusable infrastructure that is largely absent from current Mathlib: concrete Euclidean-building atlases, metric-valued Sobolev energy, trace and boundary-moment constructions, harmonic energy minimization, frequency quotients, and homogeneous tangent-map interfaces. The paper theorem is proved in ordinary mathematics; the open task is to replace the single sorry in the target with a machine-checked Lean proof. A completed development would provide components useful for other singular-target harmonic-map and CAT(0) formalizations.
The target is not a direct consequence of treating the building as a Euclidean vector space. A harmonic map can cross apartment walls, and a single chart need not contain the image of a punctured neighborhood. The local problem must respect both metric energy and Weyl-group compatibility. Moreover, the frequency quotient is defined through limiting analytic quantities, while the conclusion is an exact rational arithmetic classification. Bridging those levels requires controlling tangent maps and the geometry of directions in the building rather than merely proving monotonicity of the frequency.
The rank-one clause is not obtained by substituting into the general statement alone: it also asserts . The formal proof therefore must preserve the nonconstant hypothesis and the positivity information that rules out the degenerate zero-order case.
The Lean bundle fixes a complex one-dimensional manifold model for the source, a genuine complete metric target, a finite affine reflection group acting by Euclidean isometries, and an explicit building atlas. The rotational group is the image of the affine group under taking linear parts, so is not an arbitrary external number. The domain carries a point and is nonempty by construction. The map is required to be nonconstant on the domain; this is the necessary explicit repair of the printed headline, whose later reduction theorem uses the same condition.
Energy, trace, boundary moment, frequency, and order are transparent definitions tied to the supplied geometry. In particular, the caller cannot choose a zero measure or an unrelated predicate to make the target vacuous. The theorem must establish finite small-scale energy, positivity of the boundary moment, existence of the frequency limit, and its classification. Solvers may contribute supporting files for metric Sobolev estimates, tangent-map compactness, homogeneous harmonic-map classification, or finite-reflection-group lemmas, provided they preserve the exact conventions in the definition bundle.
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.
Differentiation replaces a polynomial's zeros by a smaller set of critical points. Repeating it produces a sequence of finite root sets, ending at one point. The derivative-zero-chain problem asks whether a single path can visit an actual zero in every set without accumulating a length that grows with the degree. The question concerns the geometry of polynomial differentiation, rather than numerical root finding: every point of the path must satisfy the appropriate polynomial equation.
Ingo Althöfer posed the uniform-length question and the specific bound four in his derivative-chain problem announcement. Earlier work on assignments between roots and critical points is described in Konrad Kaffka's 2012 thesis. The established geometry includes the Gauss–Lucas theorem and the stochastic and convex-order refinements proved by S. M. Malamud. These results provide reusable inputs; they do not by themselves establish a degree-independent chain-length bound.
A root list is a finite list of complex numbers, with repeated entries recording multiplicity and with . It determines the monic polynomial
For , define its degree- row by , where is ordinary polynomial differentiation. A complete derivative-root chain chooses one complex number from every row, satisfying . Its cost is the Euclidean length
The order runs from the degree-one row to the original polynomial. The first point is therefore the centroid of the original root slots. Reversing the path gives the same cost. All source roots are normalized to the closed unit disk. Degree one has a single point and zero cost; no derivative row is omitted.
The mission's main goal is the weakest stable uniform assertion:
The same real constant must work for all degrees and all root lists. It cannot depend on the polynomial or its degree. This target remains unproved in this development.
The stronger unrestricted milestone is the four-bound, . The original announcement asks for total path length at most and specifically suggests , so this is the corresponding stated target. Additional open milestones concern real-coefficient polynomials with at most two, three or four nonreal conjugate pairs, counting multiplicity. Their proposed bounds are respectively , strictly less than , and . These are explicit statements to prove or refute, not accepted consequences of a scalar estimate. Their real-coefficient hypotheses must not be transferred to the unrestricted goal.
A uniform bound would control one compatible path through every nonconstant derivative row, even as the number of rows grows. It would give information beyond the containment of critical points in the convex hull of their parents. The stronger bound four specifies a quantitative target within the same problem.
The initial accepted development contained 52 proved theorem records and three definition bundles: derivative-chain foundations, root probability, and the finite Hermite model. All three bundles are now listed directly in this proposal. The six additional proved library references retain their original contributors and are separate from those initial 52 accepted proofs. They include standard mathematics, supporting lemmas, conditional constructions, overlapping formulations and restricted class results. This count is not a claim of 52 original discoveries. In particular the square-root baseline is already stated in the organizer-hosted report, while the explicit barycentric root weights and multiplicity-aware Rolle counting are available in Mathlib.
The accepted class results include the length bound for real-coefficient unit-disk polynomials with at most one nonreal conjugate pair, and the bound for real-compressed polynomials , where , , is real, and is its multiplicity-counted nonreal-root deficit. The compressed ray and pair-count bounds are corollaries within that family. The accepted cubic-cube theorem gives a complete chain for , for any monic complex cubic whose roots lie in a radius- disk, with length at most , a common monotone orthonormal coordinate frame and a repeated source-root tail. These are restricted results, not solutions of the main goal.
The proposal also references six existing public results: the real and multivariate martingale-coupling characterizations of convex order, the absolute-deviation and integrated-tail criteria, equality of means under multivariate convex order, and finite optimal-transport attainment and its triangle inequality. These are references to the original records, not duplicate submissions or claims of new proofs by this project. The five stochastic-order proofs are credited to Nickrobbins95 and the finite-transport proof to MKPynnic; theorem submitter and proof author can differ.
These results are supporting inputs, not proofs of the derivative-chain goal. Applying the coupling results still requires a proved convex-order statement for the actual polynomial root laws, with the correct multiplicity weights and uniform marginals. Repeated root slots yield a pseudometric, so the finite metric theorem needs distinct locations with multiplicity weights. The default norm on a real coordinate function space is not automatically the complex Euclidean norm. Neither coupling existence nor separate short edges supplies a complete uniform-length chain without a further compatible selection argument.
The fourth-power theorem and fifth-power theorem now have complete Lean proofs accepted by Prove2me. For every monic complex cubic whose roots lie in a disk of radius , they construct compatible chains through all twelve or fifteen ordinary derivative rows, respectively, with length at most .
Both theorems retain the cubic centroid, one common monotone orthonormal coordinate frame and a final source-root suffix of four or five entries. Repeated roots, zero radius and degenerate centered coefficients are included. Neither statement assumes a supplied prefix or continuation theorem. The accepted cubic-cube result remains a separate restricted-class theorem; these three class results do not settle either unrestricted goal or arbitrary larger powers.
The fourth-power research source, fifth-power research source and their checkpoint archive preserve the original analytic work. The linked theorem records carry the accepted formal proofs and their proved dependency chains.
The public Lean proof archive contains 193 Lean files (182 proof modules and 11 dependencies), reproduction instructions and SHA-256 manifests. This is the complete local-proof snapshot prepared before the final server submission packaging; the accepted submissions and their dependency chains on Prove2me are the authoritative server-verified artifacts. The archive README and formal-proof metadata record the accepted status of both theorems. The original research files are preserved unchanged; their earlier Open notices describe the historical research snapshot.
Convex containment does not control the sum of successive movements. Choosing a short edge separately at each row also need not produce a compatible path: the endpoint of one choice must be the start of the next. The known general square-root bound grows with degree, so it does not answer the uniform question. A variance bound controls squared increments and cannot simply be read as a constant bound on their unsquared sum.
Repeated roots and collisions are genuine cases, not numerical exceptions. The accepted Hermite obstruction rules out a particular local variance-increment estimate; it does not refute the unrestricted chain-length questions. Likewise, accepted scalar and conditional lemmas establish only their displayed conclusions under their stated hypotheses. A proposed polynomial application must prove those hypotheses for the same actual chain.
The Lean model uses Fin n → ℂ root slots, fromRoots for the product polynomial, row a m for the ordinary derivative row, IsChain for actual root membership and chainCost for the finite sum of complex norms. Positive degree, all nonconstant rows, source normalization and multiplicity counting are explicit. No root simplicity assumption or supplied short chain is permitted in the unrestricted goal. Real-coefficient and compressed-form restrictions belong only to their named class theorems.
The accepted proofs use Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Existing declarations retain their identifiers and attribution. Generic convex-order and martingale-coupling results are reusable, but a citation to them does not prove the polynomial-specific uniform-root marginal property. Contributions are welcome on exact root-law adapters, compatible selection estimates and the listed open targets. Novelty and faithfulness to the stated problem should be assessed separately from successful Lean verification.
Ingo Althöfer, Math with AI — Diary, derivative-chain problem announcement, 15 August 2026. Announcement.
A Bound for Chains of Zeros of Successive Derivatives, organizer-hosted report. Report.
Konrad Kaffka, Zuordnungen zwischen Nullstellen und kritischen Punkten von Polynomen, Diplomarbeit, Friedrich-Schiller-Universität Jena, 2012. Thesis.
S. M. Malamud, Inverse spectral problem for normal matrices and a generalization of the Gauss–Lucas theorem, Transactions of the American Mathematical Society 357 (2005), 4043–4064. Preprint.
Rajesh Pereira, Differentiators and the geometry of polynomials, Journal of Mathematical Analysis and Applications 285 (2003), 336–348. Article.
Thorsten Theobald and Timo de Wolff, Norms of Roots of Trinomials, 2015 preprint version. Trinomial geometry.
Public formalization reference package: 60 numbered records, including the three definitions, five open targets and 52 accepted proof sources. Statements, proofs and source conventions.
Distributionally robust optimization evaluates a decision against a set of plausible probability laws rather than against a single estimated law. A common way to specify that set is to choose a nominal law and allow every law whose discrepancy from is below a radius . Different discrepancies produce different ambiguity sets, so comparing them tells a modeler what one constraint guarantees about another. Rahimian and Mehrotra collect such constructions in their survey and state a chain of comparisons among variation, Hellinger, Kullback–Leibler, and J-divergences in Lemma 5.4 (arXiv:1908.05659v1, pp. 31, 34–35). The chain connects four common ways of controlling model error without requiring a finite outcome space or a common density chosen in advance.
The source is the 2019 arXiv v1 preprint of a survey. Its proof of Lemma 5.4 cites earlier work rather than giving a full derivation. The preprint also prints an additional J-to- comparison that is false; this mission isolates the part that holds for every pair of probability measures. The distinction matters when an ambiguity set is used to certify a bound under a different divergence: an inclusion based on the false link can certify laws that are outside the intended set.
Let be a measurable space, and let be its probability measures. Given , a -divergence compares their densities using a function with . The paper assumes is convex. To account for measures that are not mutually absolutely continuous, take the common dominating measure and write and . The integrand is when and when , where ; a point with contributes zero (§5.1.2, p. 31).
Table 1 gives four generators used here:
The first two divergences are the full variation discrepancy and the unhalved squared Hellinger discrepancy. In particular, , where is the total variation distance defined later in the paper. The J generator has , understood as its limit at zero; under . The recession slopes of the four generators, in the displayed order, are (Table 1, p. 31; §5.1.3, p. 35).
For a nominal probability measure and a nonnegative radius , equation (5.9) defines the ambiguity ball
The three milestone comparisons are the valid initial part of (5.10), for every :
The middle comparison is also stated in footnote 18. The mission goal is the corrected Lemma 5.4: it joins these three comparisons to the resulting valid part of (5.11), for every nominal and radius :
Each inclusion has the direction induced by the preceding divergence inequality: a stronger divergence constraint gives a smaller ball. The first comparison retains the paper's factor , and the final ball retains its radius (Lemma 5.4, p. 34).
The result allows a J-divergence or KL-divergence ambiguity model to carry a simultaneous bound in Hellinger and full variation divergence. A Hellinger radius yields the explicit variation radius ; this makes the scale change visible when comparing two models built with different discrepancies. Without a general-measure statement, a finite-outcome approximation does not itself cover continuous laws or pairs with a singular component.
The paper presents the inequalities as known and cites sources for them. A finite-alphabet TV–Hellinger–KL chain and a general-measure KL–affinity bound already have machine-checked results in the platform catalog. The work here is to formalize the four generators with one shared general-measure divergence, close the remaining inequalities in that representation, and connect them to the ambiguity-ball inclusions. This also provides reusable definitions for other distributionally robust models that use the same divergence convention.
Writing the density ratio only with respect to loses the part of singular to . That would change both variation and Hellinger divergence and make the stated chain an unreliable comparison of the paper's objects. At the opposite boundary, can vanish on a set that charges. There the J generator must be infinite, although a direct use of a total real logarithm at zero can assign it an incorrect finite value. These two edge cases make an apparently routine pointwise comparison insufficient for the full measurable-space theorem.
Lean represents and as ProbabilityMeasure Ξ on an arbitrary MeasurableSpace Ξ. It computes Radon–Nikodym densities relative to , evaluates the divergence with an extended nonnegative Lebesgue integral, and represents both divergence values and radii in ENNReal. The generic definition computes the recession slope as a limsup; for the four Table 1 generators this is the limit in the paper. The formal ambiguity ball contains probability measures only. A top radius is allowed by the type; the finite nonnegative radii are the paper's intended model parameters. The generic operation does not take a convexity certificate, but the four named generators are the only ones used in the theorem.
The formalization must not turn a nondominated pair into divergence zero or assign : either choice changes the claimed chain. It must also retain the full variation divergence, without the half factor used for total variation distance. The definitions of the common-measure divergence, its four generators, and the ambiguity ball are intended for reuse. Contributions establishing properties of the recession slopes, comparison lemmas on arbitrary measurable spaces, and their ambiguity-set consequences are within scope.
The paper's final inequality in (5.10), , and the associated first inclusion in (5.11) are removed. They are false even on a two-point space: with and , J-divergence is while the order-two -divergence is . Thus lies in the latter ball of radius but outside the J ball of that radius. The source's footnote 18 separately notes an error in a cited Hellinger–KL comparison; the corrected Hellinger–KL inequality is retained (pp. 34–35).
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
This entry targets the reviewed PR #62 checkpoint, . The pinned repository attributes the selected construction to Avi Eisenberg’s interval strips and core-aware pair assembly, eumemic’s joint frame compiler, and Alejandro Zarzuelo Urdiales’s exact parameter refinement and scoped Lean certificates. Douglas Colkitt maintains the project and its integration. The checkpoint combines a bit network with 575-way branching and 137,151,806 physical roles with the retained complex construction. Its finite arithmetic checks do not prove the complete multiplication algorithm. The full theorem remains an open obligation.
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
Schönhage and Strassen conjectured in 1971 that is the optimal order of growth for multiplying two -bit integers on a multitape Turing machine. Harvey and van der Hoeven proved the matching upper bound (Annals of Mathematics, 2021). In September 2026, a preprint by OpenAI, Integer multiplication below , claimed that this bound can itself be beaten by a power of the logarithm, in the same model. If correct, the upper half of the conjecture's "" is false. Two independent follow-up projects then increased the exponent saving by many orders of magnitude. This mission targets the strongest claimed saving and takes the earlier claims as milestones.
Timeline (multitape Turing model; all bounds are of the form ).
A -tape Turing machine, in the conventions of Montanaro's Computational Complexity lecture notes (§3, §3.4), has the following parts:
In one step the machine reads the symbol under every head, writes a symbol under every head, moves each head by at most one cell (never left of ), and changes state. Once in it stays there unchanged.
For (most significant bit first), is the integer that represents, and is the length- binary representation of . A machine computes the product if, for every and all , when started on input it reaches with the output tape holding exactly followed by blanks. Its running time is the largest number of steps on any pair of -bit inputs. With , define
Each milestone is implied by the goal, because decreases in . Each one is also a published claim in its own right and a natural intermediate formalization target. The and constructions are the ones that the later claims rely on.
The result. Any shows that is not the optimal running time for multitape machines, which refutes the upper half of the Schönhage–Strassen conjecture as usually stated. The OpenAI preprint also derives the same bound for exact division and integer square roots (its Corollary 2). Larger values of quantify how far below multiplication can go. The bound is a statement about growth rates, and the constants involved are astronomically large.
Formalizing it. None of the three positive- results has been refereed, and the two follow-ups explicitly depend on the OpenAI manuscript. Their written arguments, their computer-checked combinatorial certificates (rank sums, moment bounds, rational margins), and the full multiplication theorem have not been formally verified. Machine-checking any of the milestones would be the first independent confirmation of the corresponding claim. A formal disproof, or a formal identification of a gap, would be equally informative.
Fourier-based multiplication scans stored bits at each of transform levels, so any algorithm that performs those levels one at a time pays for data movement and arithmetic alone. Beating this requires both moving data and carrying out butterfly layers at cost on a tape that is accessed sequentially, where is the stored volume. In the preprint this is done with recursive linear networks whose total number of smaller calls is strictly less than (number of roles) × (arity). The follow-ups improve by finding better networks and tighter parameter choices, all certified by large exact computations. Each claim therefore combines a long analytic argument, a Turing-machine implementation, and a finite certificate, and all three must be formalized.
IntMul_MultitapeModel, shared with the Harvey–van der Hoeven mission, and follow the -tape conventions of Montanaro's lecture notes. Tapes begin with . There is a state that freezes the configuration. Tape is a read-only input tape holding , and tape is the output tape, which must hold exactly , then the product bits, then blanks. Running time is the number of steps until .When many independent users share a network, each routes its own traffic to minimize its own delay, and nobody optimizes the system as a whole. Koutsoupias and Papadimitriou asked how much this lack of coordination can cost: how far the social cost of a Nash equilibrium can be from the social optimum, in the worst case. Their paper Worst-case equilibria (STACS 1999; journal version 2009, doi:10.1016/j.cosrev.2009.04.003) introduced this ratio, later named the price of anarchy, and studied it on the simplest network: parallel links between one source and one destination. The ratio has since become a standard measure of the inefficiency of equilibria in routing, scheduling and auctions (see Chapters 17–20 of Nisan, Roughgarden, Tardos and Vazirani, Algorithmic Game Theory, 2007).
Most of the paper concerns links of equal capacity. Its last result, Theorem 4, turns to two links of different speeds and shows that unequal speeds make equilibria worse: the worst-case ratio rises from for two identical links to the golden ratio .
Timeline. 1999: Koutsoupias and Papadimitriou define the coordination ratio; for two identical links they prove it is exactly , and for two links with speeds they give the golden-ratio lower bound of Theorem 4. 2002–2003: Mavronicolas and Spirakis, Koutsoupias, Mavronicolas and Spirakis, and Czumaj and Vöcking determine the asymptotic order of the price of anarchy for identical and for related links (Czumaj–Vöcking, ACM TALG 2007).
There are agents and parallel links. Agent has an amount of traffic , and link has a speed . A pure profile sends each agent's whole traffic over one link . The load of link is , and an agent on link experiences the delay .
A mixed strategy of agent is a probability distribution over the links; the agents randomize independently. The expected cost of agent is its expected delay. A profile is a Nash equilibrium if no agent can lower its expected cost by changing its own distribution. The expected traffic on link is , and the cost to agent of placing its traffic on link is
The social cost of is the expected makespan, the expected maximum delay over the links,
and is the optimal makespan over pure assignments. The price of anarchy is the largest ratio over instances and equilibria.
For two links with speeds , there is an instance with positive traffic and a Nash equilibrium with and
moreover on this range, and when .
The result. Theorem 4 shows that the price of anarchy of parallel links depends on the heterogeneity of the links, not only on their number: two identical links have price of anarchy (Theorems 1 and 3 of the paper), while two links of different speeds already reach . The setting is that of related (uniformly related) machines, the model in which Czumaj and Vöcking later proved the asymptotic order of the price of anarchy for links.
Formalizing it. The result is proved on paper; this mission produces a machine-checked proof. Beyond the theorem, it yields reusable statements about mixed equilibria of load-balancing games on the published agt_games vocabulary: the closed form (8) of a pure deviation's expected cost and the support characterization of equilibria, both stated for any number of agents and links. A search of the Prove2Me catalog (October 2026) found no formalization of any part of this result.
The arithmetic of the instance is elementary, so the work lies in connecting the paper's computations to the definitions. The paper's notion of equilibrium quantifies over all mixed deviations, and its expected costs are sums over all pure profiles; the proof reasons instead with the per-link costs of (8) and the indifference of each agent between the links it uses. Turning that into a proof requires showing that an agent's expected cost is the -weighted average of the (linearity over independent randomization) and that the average over outcomes reduces to the paper's four-term formula. A naive approach that checks only pure deviations does not give the equilibrium property directly; one must pass from pure to mixed deviations. The restriction is not cosmetic: beyond it the second agent's probability is negative.
The game is defined in WorstCaseEq.Speeds.Model on top of the published agt_games definitions (AGT.IsMixedNash, AGT.expectedPayoff, AGT.profileProb). These maximize payoffs, so an agent's payoff is minus its delay. Agents and links are Fin n and Fin m, indexed from , so the paper's links 1, 2 and agents 1, 2 are 0, 1. A mixed profile is a real matrix p i j; being a family of probability distributions is part of the Nash condition. Makespan, social cost and opt require at least one link (NeZero m).
The paper does not print the social cost for links with speeds; the computation in the proof of Theorem 4 uses the expected maximum of load divided by speed, and that is the definition. It is not the maximum of the expected loads, a smaller quantity. The page numbers cited are PDF page indices of the journal version (dated April 29, 2009), which prints no page numbers after page 1.
"The price of anarchy is at least " is formalized as the existence of an instance and an equilibrium whose social cost equals times a positive optimum. A quotient is avoided because it takes the junk value when , and the requirement rules out degenerate witnesses with no traffic. The ratio conditions and are written and (equivalent since ), and is Mathlib's Real.goldenRatio.
Contributions welcome: proofs of any milestone. Milestones 1 and 2 are general facts about mixed equilibria of weighted load-balancing games and are reusable beyond this mission.
A finite Markov chain moves among states according to transition probabilities. Its second largest eigenvalue measures how slowly some variation in the starting state can disappear. Directly computing that eigenvalue is often difficult when the state space is large. A geometric bound can be more useful: choose a route between each ordered pair of states and measure how much weighted traffic the routes impose on each transition. Diaconis and Stroock present this route-based bound as Proposition 7 of their 1991 paper, following the canonical-path method of Jerrum and Sinclair (Diaconis–Stroock, §3B). It makes a spectral estimate depend on the geometry of chosen routes and the stationary weight of each edge.
The paper's purpose is to compare methods for bounding eigenvalues of reversible chains. Its earlier Poincaré estimate uses weighted path lengths. Proposition 7 instead passes through a bottleneck constant and Cheeger's inequality. These are different summaries of the same chain: one examines a system of paths, and the other examines flow across every cut. The comparison is useful on graphs where paths are easy to choose but the cut minimizing the bottleneck constant is not apparent (Diaconis–Stroock, pp. 52–55).
Let be a finite state space with at least two states. A transition matrix has entries and each row sums to one. It is irreducible when every state can be reached from every other state in some number of steps. A stationary distribution is a nonnegative probability vector satisfying . The chain is reversible when it satisfies detailed balance: . Write for the stationary edge flow. These are the standing assumptions of the paper's §1A, restated in §3B (Diaconis–Stroock, pp. 36, 54).
For every distinct ordered pair , choose a finite walk from to . Every consecutive step of the walk must have . The walk may revisit a vertex or an edge; §3B places no no-repetition condition on these choices. An oriented edge is an ordered pair with positive flow. A walk contains it when one of its consecutive steps traverses it in that direction. The canonical-path congestion of the chosen walk system is the paper's quantity
The sum assigns weight to an ordered pair, once for each directed edge that its chosen walk uses. Irreducibility ensures that walks between different states exist. Under the mission's assumptions the positive-flow edge set is nonempty, so the maximum has its ordinary finite meaning (Diaconis–Stroock, (3.2), p. 54).
For a nonempty set with , let be the total stationary flow from to its complement. The bottleneck constant is
The denominator is positive under irreducibility. Write for the largest eigenvalue of other than the simple eigenvalue , and write for the spectral gap. These conventions match §1A and equation (3.4) (Diaconis–Stroock, pp. 36, 56).
The mission's goal is Proposition 7, for every valid choice of :
Its milestones record the source's cut argument: a selected walk from to crosses an oriented cut edge; the total pair weight obeys ; and consequently . The final milestone is the already formalized version of the paper's equation (3.4), (Diaconis–Stroock, pp. 54, 56).
The companion result is the graph specialization (3.3). For simple random walk on a connected graph , let be the maximum degree and let be the maximum number of ordered-pair walks traversing an oriented edge. It gives
This statement uses the exact displayed bound of Remark 3.1; the earlier sentence in that remark uses a different normalization of (Diaconis–Stroock, p. 55).
The proposition converts any usable path system into an explicit spectral estimate. Once a graph or chain supplies paths whose edge loads can be bounded, the formula bounds without diagonalizing or finding the set that minimizes . In the graph case, equation (3.3) expresses the estimate using only the edge count, maximum degree, and maximum directed path load. The paper compares that bound with its Poincaré bound on examples including cycles, cubes, and binary trees (Diaconis–Stroock, pp. 55–56).
Equation (3.4) already has a proved formalization in the published MarkovMixing library, under the same finite reversible-chain conventions. This mission adds the paper's path-congestion definition and cut estimates, then states the still-needed Proposition 7 and graph specialization against that library. The result is a reusable connection between a chosen family of walks and a chain's existing bottleneck and spectral objects.
The route load concerns individual directed edges, whereas takes a minimum over all admissible cuts. A single heavily loaded edge does not by itself identify the minimizing cut. The central difficulty is to control, for every cut at once, all weighted ordered pairs whose walks leave it. The direction of a crossing matters: counts edges directed out of , and must count traversals of those same orientations. Omitting an orientation or allowing negative unused edge flow would invalidate the intermediate cut estimate.
There is also a printed discrepancy. Proposition 6 on p. 52 displays a stronger upper bound on than the inequality established in §3C. The mission uses equation (3.4), whose lower gap bound yields the constant actually stated in Proposition 7 (Diaconis–Stroock, pp. 52, 54, 56).
Lean represents the state space as a finite type, the chain as a real matrix, and the stationary distribution as a real function. It imports the published MarkovMixing definitions of stochasticity, irreducibility, stationarity, detailed balance, , , , and simple random walk. A local definition represents each selected walk by its vertex list and derives directed edges from consecutive vertices. The hypothesis makes the paper's second eigenvalue and excludes the one-state junk value of the real supremum used in its definition. Positivity of follows from the chain and walk assumptions; it is not inserted as an extra assumption.
The walk system is universally quantified: the theorem concerns every valid selection, rather than one favorable selection. The local definition ignores equal-endpoint choices because they do not cross any -to- cut; §3B mentions all ordered pairs, so this convention gives a slightly stronger target and is stated explicitly. The cut lemma retains stochasticity and nonnegative stationary weights to keep the flow of unused cut edges nonnegative. The graph companion derives its Markov-chain properties from connectedness rather than assuming them.
The shared vertex-list representation and the cut crossing statement can serve later path-based bounds. Contributions toward positivity and finiteness of congestion, the uniform cut estimate, the bottleneck estimate, and the graph specialization all fit the mission. A definition that forces by fiat, or a goal that assumes the bottleneck estimate or Cheeger's inequality, would erase the mathematical content.
Airline and hotel revenue-management systems have traditionally been built around nesting by fare order: classes are ranked by price, and as capacity runs short the cheapest open class is closed first, so that the set of open fares is always a top segment of the fare ladder. This structure is what makes booking limits, protection levels and bid-price controls work, and it is optimal in the classical independent-demand model of Lee and Hersh (1993), where each customer wants one specific class.
When customers instead choose among the classes on offer (buying down to a cheaper fare, or not buying at all when their preferred fare is closed), the optimal policy need not be nested by fare order. Talluri and van Ryzin (2001 working paper; Management Science 2004) formulate single-resource capacity control under a general discrete choice model and ask which choice models still have optimal policies nested by fare order. Their Theorem 2 answers this with a characterization in terms of the choice probabilities alone. The paper's later sections use it to show that the independent-demand and multinomial-logit models have the property; the mission on the multinomial-logit model in this series builds on that.
There are fare products , indexed so that . A choice model assigns to every offer set and product a probability that an arriving customer buys when is offered, with for and purchase probability ; the remainder is the probability of no purchase.
A set is complete if it has the form , (with ), and incomplete otherwise. For values (in the dynamic program, for a marginal value of capacity ), consider the static problem
The choice model has the nesting-by-fare-order property (Definition 4) if (i) is increasing, for , and (ii) for every , problem (9) has an optimal solution that is complete. For convex weights write for the purchase probabilities of the corresponding randomized mixture of complete sets.
The choice model has the nesting-by-fare-order property if and only if is increasing and, for every incomplete set , there are convex weights such that
That is, some mixture of complete sets majorizes in fare order. Both directions are part of the goal, and the right-hand side contains no optimization over .
The paper remarks (p. 21) that the proof never uses completeness: the same characterization holds for any specified family of offer sets in place of the complete sets. Example 2 (pp. 18–19) gives a three-product model, arising from a mixture of two customer types, in which the incomplete set is the unique maximizer of (9) at , so the property fails.
Theorem 2 turns a statement quantified over all value vectors and all offer sets into a finite collection of linear feasibility problems, one per incomplete set, involving only the choice probabilities. Combined with the paper's Theorem 1 (the optimal policy offers nondominated sets, nested in capacity and time), it gives a checkable criterion for when a nested-by-fare-order booking-limit or bid-price policy is optimal under customer choice. The paper uses it to verify the property for the independent-demand model (Proposition 5) and the multinomial-logit model (Proposition 6), and the p. 21 remark makes it a tool to test conjectures that optimal offer sets come from another structured family.
The result is proved in the paper; the mission's contribution is a machine-checked version of the characterization and of each proof step, which are the reusable pieces for the follow-up mission on the multinomial-logit model. Farkas' lemma in inequality form is already formalized on the platform (LinearOptimization.farkas_inequality_form, referenced here); the theorem of this mission is not.
The argument is short on paper but the bookkeeping is where the content sits. The reduction of Definition 4(ii) to infeasibility of (10)–(11) needs care with ties: (9) only needs some complete optimum, so the system asks that beat every complete set strictly, not that be the unique optimum. The dual system must then be matched exactly to the primal: the multiplier of the ordering constraint enters two adjacent equations, the boundary multipliers and are fixed at zero, and the inhomogeneous constraint on is what forces . A naive application of Farkas' lemma to the strict system, without homogenizing in , gives the wrong normalization. The boundary case is what produces the equality of totals rather than a further inequality, and the fare order of is the only link between the prefix-sum conditions and revenue.
Products are Fin n (product is the element ), offer sets are Finset (Fin n), probabilities are real. The choice-model axioms are the platform definition RevenueManagement.IsChoiceModel ( and ), reused by reference, together with the model's own standing convention for (SupportedOn), which is needed because and the totals sum over all products. The order is Antitone x. The maximum in (9) is over all subsets of .
Complete sets are for , so is complete and the weights live on sets. The page indexes the weights by ; with included the property is the one the paper's applications need (for the multinomial-logit model and all the unique optimum of (9) is ), and the family companion contains the page's literal version as an instance. The prefix conditions are stated for , where is trivial.
A formalization that put an optimization over on the right-hand side of the goal, or dropped condition (i) from either side, would be a restatement rather than the characterization; the goal's right-hand side mentions only the choice probabilities.
The development needs finite sums over Fin n, and a Farkas lemma (available on the platform). Proofs of the milestones and of the companions are welcome individually; the family version of the characterization is reusable for any conjectured family of optimal offer sets.
Markov chain Monte Carlo methods, card-shuffling schemes and randomized counting algorithms all run a Markov chain until its distribution is close to the stationary distribution. The quantity a user needs is a number of steps after which is within a prescribed variation distance of . For reversible chains the standard way to get such a number is to bound the eigenvalues of the transition matrix and convert the eigenvalue bound into a variation distance bound.
P. Diaconis and D. Stroock, in Geometric bounds for eigenvalues of Markov chains (Ann. Appl. Probab. 1, 1991), prove geometric (path-counting) bounds on the second largest and the smallest eigenvalue of a reversible chain. Their §1D supplies the conversion step: Proposition 3 bounds the variation distance to stationarity, in discrete and in continuous time, by the eigenvalues. This mission formalizes that proposition. The eigenvalue bounds themselves are the subject of the other missions of this series.
Let be a finite set with elements and the transition matrix of a Markov chain on : and . The chain is irreducible if every state can be reached from every other state: for all there is with . A probability distribution on is stationary if , and the chain is reversible with respect to if
For an irreducible chain for every . Reversibility makes a self-adjoint operator on , so its eigenvalues are real; they are written
the strict inequality coming from irreducibility. Put , the largest modulus of an eigenvalue other than .
The variation distance between probability distributions and on is
is the distribution of the chain after steps from . The continuous-time chain jumps according to at the times of a rate-one Poisson process, and has kernel
For every and every ,
The steps of the paper's proof (p. 42), in order:
For every and every ,
The paper gives no separate proof of (1.10); it says only that "the continuous time version can be proved by a virtually identical argument".
Inequality (1.9) is the step that turns an eigenvalue estimate into a mixing-time estimate: if , then as soon as , up to the usual comparison . The examples of the paper's Section 2 use Propositions 1 and 2 to bound and , and this proposition to translate the bounds into a number of steps. Inequality (1.10) does the same for the continuous-time chain, where only is needed because the continuous-time chain has no periodicity.
The result is classical and its proof is short; it is the (chi-square) bound on variation distance found in many textbooks, e.g. Levin, Peres and Wilmer, Markov Chains and Mixing Times, Chapter 12. As far as the platform's catalog shows, neither (1.9) nor (1.10) has a machine-checked proof. The platform already has the spectral decomposition of a reversible chain and the identity between the two forms of total variation, both proved; this mission links them to the variation distance bound in the exact form used by the geometric-bounds literature. The diagonal bound (milestone 5) and the reversibility identity (milestone 2) are reusable statements about reversible chains in their own right.
The Cauchy–Schwarz step and the reversibility identity are finite-sum manipulations. The difficulty is in the spectral step. One has to show that, apart from the eigenvalue (whose eigenfunction is constant and contributes exactly to ), every eigenvalue in the decomposition has modulus at most , and that the remaining weights at sum to . This uses that is a simple eigenvalue, which needs irreducibility. Without irreducibility the bound fails. A second eigenvalue equal to would contribute with no decay, while , a maximum over eigenvalues different from , does not see it.
A naive approach that bounds entry by entry and sums gives a factor depending on rather than on ; the point of (1.9) is that the constant is only. For (1.10) the matrix is an infinite series in , and the decomposition has to be carried through the series, each eigenvalue contributing .
The objects are the published MarkovMixing definitions (Levin–Peres–Wilmer layer): the chain is a real matrix P : Matrix V V ℝ on a Fintype V with IsStochastic P, MarkovMixing.Irreducible P, IsStationary P π (π is a probability vector with πP = π) and DetailedBalance P π. These four hypotheses are the paper's standing assumption of §1A; every statement of the mission carries all of them, and no other hypothesis.
tvDist (rowDist P n x) π, the supremum over subsets; is heatKernel P t x.lambdaStar P, the supremum of over real eigenvalues ; is lambdaTwo P, the supremum of real eigenvalues . For an irreducible reversible chain these are the paper's and .A formalization that assumed milestone 3 or milestone 5 as a hypothesis of the goal, or that replaced by a free parameter bounded by hypothesis, would trivialize the goal and is excluded.
Needed infrastructure: finite-dimensional spectral theory for self-adjoint operators on (available through the proved MarkovMixing.spectral_representation), simplicity of the eigenvalue for irreducible chains, Cauchy–Schwarz for finite sums, and termwise manipulation of the Poisson series for (1.10). Proofs of any milestone, and of the simplicity of the top eigenvalue as a separate lemma, are welcome.