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?
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).
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.
Brouwer's fixed point theorem says that a continuous map of a closed simplex into itself has a fixed point. Many existence questions in game theory and mathematical economics produce instead a point-to-set mapping: to each point it assigns a whole set of admissible responses, for instance the set of best replies of a player to the others' strategies. Such a set need not be a single point, and no continuous single-valued selection need exist. Kakutani's 1941 note, A generalization of Brouwer's fixed point theorem, gives the fixed point theorem for this setting, and shows on the same three pages that it implies two results of J. von Neumann: an intersection theorem for two closed subsets of a product of convex sets, and the minimax theorem.
Timeline, as the paper records it:
Let with its Euclidean norm, and let . Kakutani writes for the family of all closed convex subsets of ; as printed, it contains the empty set. A point-to-set mapping of into assigns to each a closed convex set .
is upper semi-continuous (in the paper's sense) when
This is a sequential closed-graph condition. The paper remarks that for a closed it is equivalent to the graph being closed in .
An -dimensional closed simplex is the convex hull of affinely independent points of . A fixed point of is a point with .
Let be nonempty, bounded, closed and convex, and let be upper semi-continuous on with every value , , a nonempty closed convex subset of . Then
Milestones 8 and 9 stand off the goal's proof path: the paper proves Theorem 2 from the Corollary, using milestone 8 to check upper semi-continuity.
The Corollary is the form in which Kakutani's theorem is used: existence of equilibrium points in -person games (Nash), of competitive equilibria (Arrow–Debreu), and of solutions of generalized games and variational inequalities all reduce to a fixed point of a point-to-set mapping with nonempty closed convex values on a compact convex set. Theorem 2 in turn gives the minimax theorem (the paper's Theorem 3) in a few lines.
The results are classical and their proofs are known; what is missing is a machine-checked version. Mathlib does not contain Kakutani's theorem, and on Prove2Me the theorem is not posed. Brouwer's theorem is proved on the platform (AGT.brouwer_fixed_point) and enters as a reference milestone. Theorem 3 is already proved on the platform as a special case of Sion's minimax theorem (FamousTheorems.sion_minimax_theorem, Mathlib's Sion.minimax) and is therefore not posed here. A related open platform statement, Debreu's 1952 fixed point lemma for a contractible polyhedron with contractible values and a closed graph (SocialEquilibrium.Existence.fixed_point_of_contractible_polyhedron), generalizes Theorem 1 on polyhedra but not the Corollary, since a bounded closed convex set need not be a polyhedron. Once proved, the goal is the standard entry point for formalized equilibrium existence results.
Brouwer's theorem needs a continuous single-valued map, and a point-to-set mapping with closed convex values need not admit a continuous selection: the mapping on equal to for , at and for is upper semi-continuous and has none. So the obvious route, select and apply Brouwer, fails; any proof must pass through approximations and a limit in which the graph condition and the convexity of the limiting value both enter. The approximation step needs a family of triangulations of the simplex with mesh tending to zero, which Mathlib does not provide. The transfer from a simplex to a general convex set needs a continuous retraction, which uses convexity and closedness of in Euclidean space.
EuclideanSpace ℝ (Fin m), included. A point-to-set mapping is a total function Φ : E → Set E; only its values on are constrained.IsClosedConvexSubset S A is the paper's (, closed, convex) and admits as printed. Nonemptiness of the values (and of , and of in Theorem 2) is a separate, labelled hypothesis: with , or , the printed hypotheses hold and there is no fixed point, while the paper's proof picks "an arbitrary point from ".IsUpperSemicontinuous S Φ is the paper's sequential condition, with sequences in and limit . It is not Berge's open-neighbourhood upper hemicontinuity.ContinuousOn ψ S', MapsTo ψ S' S and ψ x = x on ; "clearly an upper semi-continuous point-to-set mapping of into " is stated as three conclusions; "closed subset of " is closedness in (the same for closed ); is ; " in " is the product .The alternating direction method of multipliers (ADMM) solves problems of the form subject to by alternating a minimization in , a minimization in and a dual ascent step. Its practical appeal, as surveyed by Boyd, Parikh, Chu, Peleato and Eckstein in Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers (Foundations and Trends in Machine Learning, 2011, doi:10.1561/2200000016), rests on the fact that each of these minimizations is often trivial to carry out: a projection, a linear solve, or a componentwise formula. Chapter 4 of the book, "General Patterns", catalogues the cases that recur in every later application (lasso, basis pursuit, sparse inverse covariance selection, consensus and sharing problems). This mission formalizes the statements of that chapter, culminating in the identification of the update for an penalty with soft thresholding.
Vectors live in with the Euclidean norm . An extended-real-valued function is given by its effective domain and its finite values there. Fix a penalty parameter , a matrix and a vector . The -update of ADMM (p. 25) is
where "argmin" denotes a minimizer over . When the right-hand side, as a function of , is the proximity operator (§4.1).
The chapter evaluates in four situations:
The soft thresholding operator (§4.4.3, p. 32) is, for ,
applied componentwise to vectors.
For , and , a vector minimizes over if and only if
The statement gives both that the soft-thresholded vector is a minimizer and that it is the only one.
The results of this chapter are what make ADMM an implementable algorithm rather than a conceptual one. Soft thresholding is the -update of the lasso (§6.4), of distributed -regularized regression (§8.2) and of sparse inverse covariance selection (§6.5); projections are the updates of every constrained problem in Chapter 5; the linear-system form (4.1) and the KKT system are the updates of least squares and quadratic programming. Every later chapter of the book cites these identities without proof, so a formal library of them is the substrate on which formal statements about specific ADMM instances can be built.
None of these statements is open as a mathematical question: all are classical facts of convex analysis. The book states them without proof (the goal is justified by a reference to subdifferential calculus in Rockafellar's Convex Analysis). This mission poses their formal statements as Lean proof goals. The matrix inversion lemma already has a machine-checked proof on the platform (the Woodbury identity) and is reused. A related but distinct statement, that singular value shrinkage is the proximity operator of the nuclear norm (Cai, Candès and Shen, 2010), is posed separately on the platform and is not this mission's target.
The goal objective is not differentiable, so setting a gradient to zero does not apply; the minimizer sits exactly on the kink of whenever . A proof has to handle the three regimes of and must establish global optimality, not only stationarity, together with uniqueness. Passing from the vector problem to the scalar ones requires the separability statement, which is a statement about minimizers of sums over a product domain, not about any particular function. For the quadratic milestones, the difficulty is linear-algebraic: showing that invertibility of forces positive definiteness, and, for the equality-constrained case, that a minimizer exists and depends affinely on even when is rank deficient and the KKT matrix is singular.
Vectors are EuclideanSpace ℝ (Fin n), so ‖·‖ is ; matrices are Matrix (Fin p) (Fin n) ℝ acting through Matrix.toEuclideanLin. The conventions committed to are:
IsXUpdate, IsProx and IsProjection say " is a minimizer"; no choice function is used. Where the book says "the solution", the theorems state an equivalence " is a minimizer equals the formula", which gives existence and uniqueness at once.lam, since λ is a Lean keyword); for the soft thresholding identities (implicit in the book, where , and false for ); in (4.2), as on the page; symmetric positive semidefinite (Matrix.PosSemidef); invertibility of in (4.1); closed, convex and nonempty for the projection; nonemptiness of for the existence part of §4.2.5; of arbitrary rank.The trivializing formalization to avoid is stating the goal as the subgradient condition , or as agreement of the three formulas for : the goal is global minimality and uniqueness of the soft-thresholded vector for the objective. Not formalized: the flop counts and caching remarks of §§4.2.1–4.2.4 and the iterative-solver discussion of §4.3, which make no mathematical claim.
Contributions welcome: proofs of any milestone; the general block-separability statement of §4.4.1; a lemma connecting IsProx with Mathlib's orthogonal projection onto complete convex sets.
Infinite-horizon dynamic programming with positive (nonnegative) costs and no discounting, or with discount factors that do not make the Bellman operator a contraction, is the setting of Blackwell's and Strauch's positive and negative programming models and of many deterministic control and reachability problems. In this regime the classical contraction argument is unavailable: the optimal cost may be infinite at some states, value iteration may fail to converge to it, and an optimal policy may fail to exist. Chapter 5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), treats these problems in an abstract framework, a single monotone mapping , so that one set of theorems covers stochastic control with additive or multiplicative costs and minimax control. The chapter is the book version of Bertsekas, "Monotone mappings with application in dynamic programming", SIAM J. Control Optim. 15 (1977).
The chapter's last structural result answers a practical question: when value iteration is run from the terminal cost, do the minimizing controls it computes at each stage lead to an optimal stationary policy?
The abstract monotone model consists of a state space , a control space , nonempty constraint sets , a terminal function , and a mapping defined for , and , which is monotone: implies .
A selector is a function with ; a policy is a sequence of selectors, and it is stationary if all are equal. The operators are
the cost of a policy is , is the cost of the stationary policy , and the optimal cost is . A policy is optimal if .
Assumption I (uniform increase) is for all , ; under it the sequence defining is nondecreasing, so the limit exists in . Assumption I.1 says commutes with limits of nondecreasing sequences above , and I.2 says that for some , for all and . Assumptions D, D.1, D.2 are the mirror images (uniform decrease, continuity along nonincreasing sequences below , and a lower shift bound).
The DP algorithm (value iteration) generates ; for and the level sets
collect the controls that keep the stage- cost below .
Let I, I.1 and I.2 hold, let be a Hausdorff space, and let be compact for all , and . Then (a) some policy satisfies
(b) for every such policy, has an accumulation point whenever ; and (c) any that picks such an accumulation point at those states, and any admissible control where , defines an optimal stationary policy:
In the order of the mission's milestone list: Lemma 3.1 (compact sublevel sets give a minimum), Proposition 5.2 (Bellman's equation under I, I.1, I.2), Proposition 5.4 (a stationary policy is optimal iff ), Proposition 5.10 (under the compactness hypothesis, and a stationary optimal policy exists), Proposition 5.6 (-optimal policies from approximate attainment, with explicit constants and ), Corollaries 5.3.1 and 5.7.1 (Bellman's equation and -optimal policies under D, D.2 with finite and ), and Propositions 5.14 and 5.15 (the multiplicative-cost and minimax models satisfy I, I.1, I.2 or D, D.1/D.2 with explicitly named scalars).
Proposition 5.10 alone gives existence of an optimal stationary policy; Proposition 5.11 identifies one. It says that the minimizers computed by value iteration, which any implementation produces anyway, converge (along subsequences, state by state) to optimal controls. This is the abstract form of the classical results for deterministic and stochastic positive-cost problems with compact control sets, and through Propositions 5.14 and 5.15 it applies to multiplicative (risk-sensitive) costs and to minimax control without new arguments.
Lemma 3.1, Propositions 5.1–5.5, 5.7–5.10, Lemmas 5.1–5.2 and Corollaries 5.2.1, 5.3.2 are already formalized and proved on the platform, in the MonotoneDP.Increase and MonotoneDP.Decrease developments built from the 1977 paper; this mission reuses their model and assumption definitions and links Lemma 3.1, Proposition 5.2 and Proposition 5.10 as milestones. Propositions 5.4 (in the book's stronger form, with policies optimal state by state), 5.6, 5.11, 5.14, 5.15 and Corollaries 5.3.1, 5.7.1 are new here. All are proved in the book; none has a machine-checked proof yet.
The obvious route to (c) is to pass to the limit in . That fails twice. First, need not converge, and different subsequences may have different limits; the statement is about an arbitrary accumulation point, and in a general Hausdorff space accumulation points are not limits of subsequences. Second, is not assumed continuous in at all: the only regularity in is compactness of the level sets , and the only regularity in is I.1 along monotone sequences. States with need separate treatment, because there the level sets give no control on .
For Corollaries 5.3.1 and 5.7.1 the difficulty is that D.1 is not assumed; the replacement uses finiteness of and essentially, and both hypotheses are needed.
Functions are S → EReal. The model, Assumptions I, I.1, I.2, D, D.1, D.2 and the epigraph sets used by Proposition 5.10 are the published definitions MonotoneDP_Increase_Model, MonotoneDP_Increase_Assumptions, MonotoneDP_Increase_Epigraph, MonotoneDP_Decrease_Model and MonotoneDP_Decrease_Assumptions. In them is the limit (limUnder) of the policy compositions, which exists under I or D; is the iterate T^[k]; the composition applies first; the model requires nonempty and ; "I.2 holds" is the existence of a scalar , and results that name the scalar take it as a parameter. An accumulation point of a sequence in is a cluster point (MapClusterPt), not a limit; in Proposition 5.11(c) the conclusion includes that is admissible. is computed pointwise in and equals where does.
The book computes in with . Mathlib's EReal gives , so the two mappings of Section 2.3 use the series' shared definitions, which follow the book's convention: the expected value on a countable (expect, positive and negative parts summed in , when the positive part diverges) and the sum inside the minimax supremum (badd, when either summand is ), both from BertsekasShreve.FiniteHorizon.SpecificModels. Propositions 5.14 and 5.15 quantify over every model whose and are these mappings; such models exist because the mappings are monotone.
A formalization in which or is introduced as an arbitrary fixed point of , or in which (c) assumes that is a limit of , would make the goal trivial or different; both are ruled out by the definitions above.
Contributions welcome: proofs of the milestones, and reusable EReal infrastructure (limits of monotone sequences, series of nonnegative extended reals) that the Part I chapters of the book share.
A stochastic process is reversible when a film of it run backwards is statistically indistinguishable from the film run forwards. For Markov processes in equilibrium this distributional symmetry has an algebraic counterpart, the detailed balance conditions, and that counterpart is what makes large classes of queueing networks, migration processes, loss networks, clustering processes and population-genetics models solvable in closed form. F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) builds the whole theory of product-form equilibria on this link, and Chapter 1 sets it up.
The criterion that bears Kolmogorov's name goes back to A. Kolmogorov, "Zur Theorie der Markoffschen Ketten" (Math. Annalen 112, 1936), who showed that reversibility of a chain can be read off its transition probabilities around closed cycles. Kelly's Chapter 1 (§§1.1–1.7) states the criterion for chains (Theorem 1.7) and processes (Theorem 1.8), together with the detailed-balance characterization (Theorems 1.2, 1.3), the cut and tree lemmas (1.4, 1.5), the monotonicity of relative entropy (Theorem 1.6), truncation and rate alteration (Lemma 1.9, Corollary 1.10), and the description of the time-reversed process (Theorems 1.12–1.14). This mission is the first in a series covering the book.
Let be a finite state space. A continuous-time Markov process , , is specified by transition rates , , with Kelly's convention . Its generator is the matrix with off the diagonal and , and its transition matrices are . The rates are irreducible if every state can be reached from every other through transitions of positive rate. An equilibrium distribution is a collection of positive numbers summing to one that satisfy the equilibrium equations
The stationary process with rates and equilibrium distribution has finite-dimensional distributions
It is reversible (Kelly, p. 5) if has the same distribution as for all . The rates satisfy detailed balance with if for all , and Kolmogorov's cycle condition if
for every finite sequence of states . The discrete-time analogue replaces rates by a stochastic matrix and by the matrix power , .
For a stationary, irreducible Markov process on a finite state space,
The left side is a statement about the joint laws of the process at all finite sets of times; the right side involves the rates alone, not even the equilibrium distribution.
Theorem 1.8 is the working test for reversibility throughout the book and the queueing literature: a model's reversibility, and with it a product-form equilibrium obtained by solving detailed balance, can be decided by checking a finite list of cycles in its transition diagram. Theorem 1.3 converts the distributional property into equations that later chapters solve explicitly; Theorems 1.12 and 1.13 underlie the treatment of quasi-reversible queues and networks in Chapter 3; Lemma 1.9 and Corollary 1.10 produce the equilibria of loss systems and queues with shared buffers.
The algebraic content of several of these results is already proved on the platform at the level of rates: detailed balance implies the equilibrium equations, the reversed rates preserve , truncation preserves detailed balance, and Kolmogorov's criterion is equivalent to detailed balance for two-way communicating rates. What is not formalized anywhere is the process-level statement: that these conditions are equivalent to the time-reversal symmetry of the finite-dimensional distributions built from . This mission supplies that layer, which connects the rate identities to the probabilistic notion they are meant to capture.
The rate-level identities are short; the difficulty is the passage between them and the process. Reversibility constrains the joint law at every finite set of times, and that law is built from the matrix exponential , whose entries are not explicit functions of the rates. Relating the two requires the analytic facts about for a generator (stationarity of , the semigroup property, behaviour as , strict positivity of the entries for under irreducibility) that Mathlib does not yet provide for Markov generators, together with bookkeeping for tuples of times given in arbitrary order, with ties. For Theorem 1.8 a positive, normalized equilibrium has to be produced from the cycle condition alone, on rates that may vanish in one direction only: two-way communication is not a hypothesis, so the platform's proved rate-level criterion does not apply directly. A first attempt that defines reversibility as detailed balance avoids all of this and proves nothing new; it is excluded below.
The state space is a Fintype with decidable equality; Kelly allows a countable state space, and this restriction is stated in every item. Rates are q : S → S → ℝ with 0 ≤ q j k for j ≠ k and q j j = 0 as hypotheses. The transition matrices are NormedSpace.exp (t • generator q). Time sets are ℝ (processes) and ℤ (chains). Finite-dimensional distributions are defined for arbitrary finite tuples of time points by sorting them with Tuple.sort. Equilibrium means positive, summing to one, and satisfying (1.3) (resp. ), and every theorem takes the equilibrium distribution of the stationary process as a hypothesis. Existing platform definitions are reused: FullBalance, DetailedBalance and reversedRates from KellyStochasticNetworks_Balance, the stochastic-matrix vocabulary of mm_basic, and truncatedRates from KellyStochasticNetworks_LossNetwork.
Reversibility is not defined as detailed balance or as equality of with its reversed rates: under such a definition Theorems 1.2 and 1.3 would be tautologies and Theorem 1.8 would be the already proved rate-level criterion. It is the distributional definition of p. 5. Kolmogorov's condition ranges over all sequences of all lengths, repetitions allowed, and two-way communication is not assumed.
A complete development needs the matrix exponential of a generator (positivity, the semigroup property, the derivative at , and ), which is reusable for any finite-state continuous-time Markov chain, and a lemma on reversing sorted tuples. Lemma 1.1 (a general stationary process) and Lemma 1.11 (a non-stationary reversal) are not included. Proofs of any milestone, and generalizations to countable state spaces, are welcome.
Project scheduling with cumulative resources models production and logistics projects in which activities fill and empty storage: an activity withdraws material from an inventory when it starts and deposits its output when it completes, and every inventory must stay between a safety stock and a storage capacity. Neumann, Schwindt and Zimmermann treat this model in §2.12 of Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2) and use it in their process-industry applications.
Before any optimization, a scheduler must know whether a feasible schedule exists at all. Theorem 2.12.1 of the book answers the complexity of this question: it is NP-complete, and it stays NP-complete when the project network has no cycles. The contrast with renewable resources (machines, workers) is the point of the theorem: with renewable resources, the feasibility problem is NP-complete as well (Theorem 2.3.13, after Bartusch, Möhring and Radermacher, 1988), but an acyclic network always admits a feasible schedule when every requirement is within capacity.
The mission also collects the two other reductions the book proves in full: Proposition 2.5.4 (recognizing whether an activity lies in some minimal delaying alternative, the branching object of the book's branch-and-bound procedures, is NP-complete) and Proposition 3.4.2 (maximizing weighted start-time deviations, a resource-levelling objective, is NP-hard without any resource constraints).
A project has activities with ; activity is the project beginning and the project completion. Activity has a duration , with . The project network has arc set ; an arc with integer weight imposes the temporal constraint on the start times. A schedule is a real vector with and ; it is time-feasible if it meets every temporal constraint.
Cumulative resources carry integer demands : depletes units at the start , replenishes units at the completion , and is the initial stock. The inventory at time is
With safety stock and storage capacity (integers, by (2.12.1)), is feasible if it is time-feasible and for every and every . The decision problem of asks whether a feasible schedule exists.
For renewable resources with capacities and requirements , a set is forbidden if for some . A delaying alternative for is a set such that is not forbidden; it is minimal if no proper subset of is one.
In there are no resources, schedules must also satisfy , and the objective here is with weights .
NP and NP-completeness are taken in the sense of Cook's Turing-machine formulation, with instances written in binary.
Assuming PARTITION is NP-complete,
are both NP-complete.
The goal follows from milestones 1 and 3 together with the transfer of NP-completeness along (on the platform as CookPvsNP.npComplete_of_polyReducible).
The result. Theorem 2.12.1 explains why the book's methods for cumulative resources enumerate precedence relations between depleting and replenishing activities (minimal surplus and shortage sets, Theorem 2.12.4) instead of relying on a constructive feasibility test: unless P = NP, no polynomial algorithm decides feasibility, even for acyclic networks, where the renewable-resource case is trivial. Proposition 2.5.4 does the same for the branching scheme of §2.5, and Proposition 3.4.2 places the resource-levelling objectives of Chapter 3 among the hard ones.
Formalizing it. The three results are proved in the book, as short reductions whose delicate steps are left implicit: the polynomial size of a certificate for real-valued schedules, the handling of instances outside the construction (odd sums, empty index sets, oversized items), and the passage from an optimization problem to its decision version. None of the three reductions is machine-checked anywhere known. The mission states them against a single Turing-machine model and a single binary encoding, reusing the published definitions CookPvsNP_defs, so that the reductions compose with the Cook–Levin development already on the platform.
The mathematical content of the reductions is short; the difficulty is in the complexity-theoretic layer. Two steps resist the obvious argument.
First, NP membership. The book's certificate is a schedule, and a schedule is a real vector: it is not a string. A verifier needs a finite certificate of polynomial length, and it is not immediate that a feasible instance has a feasible schedule with small rational (or integer) start times, since the inventory constraints involve strict orderings between event times.
Second, polynomial-time computability in a concrete Turing-machine model. The transformation must compute, on a one-tape machine, binary codes of sums and halves of the input sizes, an arc list of quadratic length, and must map malformed strings to fixed no-instances. Informal "clearly polynomial" arguments have to become explicit machine constructions or a reusable library of closure properties.
The Lean development fixes the following conventions.
Fin (n + 2), with the completion Fin.last (n + 1); resources are Fin m. Start times are real.A trivializing formalization is ruled out: the languages contain only codes of well-formed instances, the encoding is injective, and the hypotheses on the source problems are true theorems, so the goal cannot hold vacuously or by a degenerate encoding.
A complete development needs closure properties of polynomial-time computable functions in Cook's model (composition, binary arithmetic, list manipulation), transitivity of , and a small-certificate lemma for systems of difference constraints with strict and non-strict inequalities. These are reusable for every NP-hardness proof stated in the same framework. Contributions to any of them, to the instance-level milestones 2, 4, 5 and 7, or to the NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT in this model, are welcome.
Many questions about polynomial equations — which equations can be solved by radicals, which geometric constructions are possible with ruler and compass, how the roots of a polynomial are related — become questions about the symmetries of a field extension. The fundamental theorem of Galois theory, going back to Évariste Galois, is the dictionary that makes this possible: for a finite Galois extension it matches intermediate fields with subgroups of a finite group, so that questions about fields become questions in finite group theory. The same dictionary underlies Kummer theory and class field theory, and it is the step that turns the unsolvability of the general quintic (Abel–Ruffini) into a statement about solvable groups.
This mission follows the Wikipedia article Fundamental theorem of Galois theory (revision 1345286594): its main statement, its list of properties of the correspondence, three of its worked examples, and its section on the infinite case.
A field extension is a field with a field inside it; it is finite when is finite-dimensional as an -vector space, of dimension . An intermediate field is a field with . The automorphism group is the group of field automorphisms of with for every .
The two maps of the correspondence are:
The extension is Galois when it is normal and separable; for a finite extension this is equivalent to . When is Galois, is written .
For an infinite algebraic Galois extension, carries the Krull topology: the coarsest topology for which each restriction map , with a finite Galois subextension and discrete, is continuous.
For a finite extension ,
The result. The correspondence turns the lattice of intermediate fields of a finite Galois extension into the (reversed) lattice of subgroups of a finite group, with degrees matching indices and normal subextensions matching normal subgroups. This is the tool used to classify subfields, to compute Galois groups of explicit polynomials, and to prove that solvability by radicals corresponds to solvability of the Galois group.
Formalizing it. The theorems are classical, and Mathlib contains formal proofs of the general finite and infinite correspondences (for example IsGalois.intermediateFieldEquivSubgroup and the InfiniteGalois namespace). This mission's contribution is a statement set indexed by the source: the converse direction ("only if Galois") as the goal, the non-Galois behaviour, each listed property, and the concrete examples of the article. The explicit examples require genuine computation: degrees of towers, minimal polynomials, and counting subgroups and subfields.
The general statements reduce to Artin's theorem and a degree count, but the non-Galois milestone asks for four separate claims about injectivity and surjectivity, each needing the correct direction of Artin's theorem. The examples cannot be settled by a general principle: showing that has exactly five intermediate fields, or that the splitting field of has degree , requires irreducibility arguments and an explicit transfer through the correspondence. Showing that has no non-trivial automorphism requires knowing that the other two roots of are not real.
All statements use Mathlib's IntermediateField F E, IntermediateField.fixedField, IntermediateField.fixingSubgroup, the automorphism group E ≃ₐ[F] E, and IsGalois (normal and separable). Finite means FiniteDimensional F E. Subgroups in the finite statements range over all subgroups; in the infinite case the Krull topology is Mathlib's standard topology on E ≃ₐ[F] E. Degrees are Module.finrank, orders are Nat.card, and the index is Subgroup.index. The concrete fields of the examples are taken inside (for and , with the real cube root) or as the abstract splitting field (for ). The quotient milestone takes the normality of and of as instance hypotheses; they are equivalent by milestone 5, so neither is vacuous.
The article's Example 3 (the anharmonic group acting on ) and the "Applications" section are out of scope for this first mission. No new definitions are needed; contributions of proofs for any milestone are welcome.
Planar flows are tame: the Poincaré–Bendixson theorem says that a bounded forward orbit in the plane tends to a fixed point or a periodic orbit. From dimension three on this fails, and the long-time behavior of a flow has to be described through sets rather than single orbits. Chapter 8 of Gerald Teschl's graduate text Ordinary Differential Equations and Dynamical Systems (AMS GSM 140, 2012; author's preliminary version at mat.univie.ac.at) develops two tools for this. The first is the attracting set produced by a trapping region, the device used to show that the Lorenz equation (Lorenz 1963) has an attractor. The second is volume: Liouville's formula for volumes measures how a flow expands or contracts phase space, which shows that the Lorenz attractor has Lebesgue measure zero, and in the special case of a Hamiltonian system gives Liouville's theorem, that the flow preserves volume. Liouville's theorem, with Poincaré's recurrence theorem as its companion, underlies Hamiltonian mechanics and equilibrium statistical mechanics.
This mission states those results for the local flow of a vector field on an open subset of , as in the book.
Let be open and of class . An integral curve of is a differentiable on an open interval with . For each there is a unique maximal one through at time , defined on the open interval . Its value at time is , the flow. The flow is local: may be bounded.
For , the -limit set is the set of for which there are and with . The stable and unstable sets of are , where is the distance to a set. A set is invariant if it contains the full orbit of each of its points. An invariant is attracting if is a neighborhood of . A trapping region is an open connected with compact closure such that for all .
The divergence of is . On phase space , a Hamilton function defines Hamilton's equations , , whose right-hand side is the Hamiltonian vector field . The Lorenz equation is , , with . Volume is Lebesgue measure.
For on an open , with the flow of on , every measurable and every time at which all points of are alive satisfy
The result itself. Liouville's theorem is the basic structural fact of Hamiltonian dynamics. It rules out asymptotically stable equilibria and attractors of positive measure for Hamiltonian systems. It makes Lebesgue measure invariant, which is the starting point of ergodic theory for mechanical systems. Combined with Theorem 8.11, it gives recurrence for any Hamiltonian motion confined to a bounded energy region. Lemma 8.8 is the quantitative version for arbitrary flows: for the Lorenz equation it gives , so the attractor from Lemma 8.5 has measure zero. Lemmas 8.5 and 8.6 produce attractors and show that they contain the unstable manifolds of their points.
Formalizing it. All of these results are classical and proved in the book. Mathlib has the change-of-variables formula, Poincaré recurrence for conservative measure-preserving maps (MeasureTheory.Conservative), and an -limit set for global flows (omegaLimit). It has no flow of a nonlinear ODE with its differentiable dependence on initial conditions, no volume formula along such a flow, and no Hamiltonian formalism. The mission asks for those pieces in the book's local-flow setting, with its hypotheses made explicit.
Lemma 8.8 and Theorem 8.10 need the flow map to be a diffeomorphism of the set of points alive at time onto its image. They also need its Jacobian to satisfy the first variational equation , whose determinant obeys Liouville's formula for linear systems. None of this is available for a general vector field in Mathlib, which provides local existence and uniqueness of integral curves but not differentiability of the flow in the initial condition. Differentiating under the integral also needs uniform control on a compact set of initial points. That is why Lemma 8.8 asks the closure of , not just , to be alive at . Without that, can have infinite volume (, , ).
Lemmas 8.5 and 8.6 are point-set topology. The obstacle there is the local flow: every statement about must first establish that the points involved are alive at time . The book avoids this by assuming completeness at the start of the chapter. For Lemma 8.7, the Liapunov function from the text has , not , so convergence to the origin requires the Krasovskii–LaSalle argument, not a plain Liapunov one.
is EuclideanSpace ℝ (Fin n) and phase space is EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with points , momenta first. volume on it is Lebesgue measure on . The flow is a pair satisfying IsMaximalFlow, which makes the unique maximal integral curve on . Nothing assumes . The chapter's standing completeness assumption is replaced by explicit aliveness hypotheses, and these are implied by completeness. The explicit readings are:
A trivializing formalization is excluded. The goal is not stated for a complete or globally Lipschitz flow, not for sets of measure zero or bounded open sets only, and not with assumed. It must be proved for the flow of built from itself.
A complete development needs differentiability of the flow in the initial condition and the first variational equation. It also needs Liouville's formula for linear systems, and change of variables for the flow map. Each is reusable beyond this mission; contributions of any of them as separate lemmas are welcome.
Mathlib/Dynamics/Ergodic/Conservative.lean. https://github.com/leanprover-community/mathlib4Almost every existence theory for elliptic, parabolic and hyperbolic partial differential equations works in Sobolev spaces: function spaces defined through weak derivatives and integrability rather than classical differentiability. Energy methods produce solutions whose derivatives are known only to be square-integrable. Sobolev embedding theorems are what turn that information back into integrability or continuity of the solution itself, and they are used at every step of the regularity theory.
This mission covers Chapter 3, §3.1–3.8 of J. K. Hunter's graduate lecture notes Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): weak derivatives, the spaces , approximation by test functions, and the two embedding regimes and .
Timeline. S. L. Sobolev proved the embedding for in 1938 by potential-theoretic methods. E. Gagliardo (1958) and L. Nirenberg (1959) independently gave the elementary proof, including , that the notes follow. The inequality behind it, for products of functions of variables, is also known as the Loomis–Whitney inequality (1949). C. B. Morrey (1940) proved the Hölder estimate for . The sharp constants were found by Federer–Fleming and Maz'ya (1960, , equivalent to the isoperimetric inequality) and by G. Talenti (1976, ).
Throughout, carries Lebesgue measure and the Euclidean norm , and is open. A test function is infinitely differentiable, and its support is a compact subset of . For a multi-index with , .
A locally integrable has weak derivative if
The Sobolev space , for and , consists of the whose weak derivatives , , exist and lie in . It is normed by , with the maximum of the suprema when .
For the Sobolev conjugate is , so that . For , is the gradient, its Euclidean length, and . The Hölder seminorm is .
For , and every ,
The goal's constant is explicit, and it is not the sharp one. A later sharp constant (Talenti's) would strengthen the goal but would not invalidate it.
The result. Theorem 3.28 is the quantitative core of the embedding . Density (Theorem 3.24) extends it to all of , giving Theorem 3.31. From there, extension operators and Rellich–Kondrachov compactness follow, and with them the existence and regularity of weak solutions to elliptic equations (Chapters 4–6 of the same notes). Morrey's inequality is the complementary statement for and yields continuity of Sobolev functions. Without these estimates, a weak solution obtained by the Lax–Milgram or Galerkin method carries no pointwise or integrability information.
Formalizing it. Mathlib contains a Gagliardo–Nirenberg–Sobolev inequality for compactly supported functions with a non-explicit constant (MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, restated on the platform as FamousTheorems.gagliardo_nirenberg_sobolev and included here as a reference item). Mathlib has no weak derivatives in the integral form used here, no spaces on open sets, no density theorem for them, no embedding, and no Morrey inequality. This mission asks for the explicit constant, the Loomis–Whitney-type product inequality in the form the proof uses, and the first results on Sobolev spaces built from integral-form weak derivatives.
The explicit constant cannot be read off Mathlib's existing inequality, whose constant is defined through its own proof. It has to come from the one-dimensional bound (Lemma 3.26) combined with the product inequality (3.10). Theorem 3.27 is an induction on dimension in which Hölder's inequality is applied on sections of and then integrated over the remaining coordinate. Expressing " with the th coordinate omitted" and Fubini across those splittings of is the bulk of the measure-theoretic bookkeeping. For the argument has to be applied to , which is only .
Theorems 3.24 and 3.31 need weak derivatives to commute with mollification and cutoff. They also need the weak derivative of a limit to be identified, and completeness of . None of this is available for the integral-form definition. Morrey's inequality needs averages over balls and polar-coordinate integration.
EuclideanSpace ℝ (Fin n) with volume. Coordinates are 0-based (i : Fin n), and multi-indices are Fin n → ℕ. is ‖gradient f x‖, which equals the operator norm of fderiv ℝ f x. norms are eLpNorm in , with real exponents coerced by ENNReal.ofReal.ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞). ContDiff ℝ ⊤ means analytic in current Mathlib, and using it for test functions would leave only the zero function, making every function weakly differentiable. A test function on has HasCompactSupport φ and tsupport φ ⊆ Ω, so the test class is all of . A smaller class would trivialize weak differentiability, and this formalization rules that out.MemW k p Ω f is membership in . sobolevNorm is the norm of Definition 3.23, valued in and built from a chosen weak derivative (unique a.e.). For it uses the essential supremum.Line search methods for unconstrained minimization of a smooth function choose a direction and a step and set . Classical rules (Armijo, Wolfe) insist that every step decrease . For quasi-Newton and conjugate gradient directions this monotonicity requirement often forces short steps, and nonmonotone line searches, which only ask for a decrease relative to some reference value built from past iterates, have been used since Grippo, Lampariello and Lucidi (1986) to let such methods take longer steps.
Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum of recent function values used by Grippo et al. with a weighted average of all past function values. The paper proves two results: global convergence to stationary points (the companion mission) and, the subject of this mission, R-linear convergence of the function values when is strongly convex.
Timeline:
Fix parameters , and . Write and . The Nonmonotone Line Search Algorithm (NLSA) keeps weights and reference values :
with chosen freely at each step. A step is accepted either by the nonmonotone Wolfe conditions
or by the nonmonotone Armijo rule , where is a trial step and is the largest integer such that the first inequality holds and . With one recovers the monotone rules.
The direction assumption asks for constants with and . The function is strongly convex with constant if
Let be the minimizer, , , and the set of points within distance of .
Let be strongly convex with minimizer , let be Lipschitz continuous on bounded sets, let , let the directions satisfy the direction assumption at every iteration, and let for all . Then there is with
The goal fixes no value of : it asserts only the existence of a linear rate.
In the paper's order of use:
Here is a Lipschitz constant of on . A further result on the same definitions is Theorem 3.2: if converges R-linearly with ratio inside a compact convex set on which is strongly convex, then the sufficient decrease condition with reference value holds for all large .
Theorem 3.1 shows that averaging past function values costs nothing in the rate: on strongly convex functions the nonmonotone method keeps the linear rate of monotone descent, for any direction sequence satisfying the direction assumption (steepest descent, L-BFGS with bounded condition numbers, and so on). Theorem 3.2 is the converse side: for weights close enough to 1, the averaged test eventually accepts the steps of any R-linearly convergent iteration of this kind. The paper contrasts this with the max-based test of Grippo et al.
These results are proved in the paper. As far as the platform catalogue shows, no line search with the Wolfe conditions or a nonmonotone reference value has been formalized. The only related item is a monotone backtracking gradient descent rate, which is a different theorem. Machine-checked proofs would give reusable Lean statements of the nonmonotone Wolfe and Armijo rules and of the averaged reference value. They would also give the explicit constants , and in checked form, and a checked record of the repair of the printed statement described below.
The obvious argument would show that contracts at each step. It fails: the method is nonmonotone, and may exceed . The quantity that contracts is , and only is controlled by the line search. The contraction must be derived by relating to in two regimes, and the second regime needs a bound on from the gradient at the previous iterate. That bound requires the Lipschitz constant on a region containing every point the line search examines, which is why the region and the step bound enter. In Lean, the sufficient decrease (3.6) also rests on the step-length lower bounds of Lemma 2.1 for both rules, including the integer-exponent Armijo rule with its maximality condition.
Conventions:
EuclideanSpace ℝ (Fin n), is ContDiff ℝ 1, and is ⟪gradient f x, d⟫_ℝ.IsGreatest.Repair of the printed statement: the paper's direction assumption holds only for all sufficiently large , but Theorem 3.1 concludes (3.5) for each , and its proof uses the assumption at every . As printed the theorem is false: with the Wolfe step gives , which violates (3.5) at whenever . The goal therefore requires the direction assumption for every .
The step bound "there exists with " is stated with the algorithm's parameter. For the Armijo rule this holds by construction. The Wolfe rule does not use , so nothing is lost.
Trivializing formalizations are ruled out:
A complete development needs:
The NLSA definitions are reusable by any later mission on nonmonotone line searches. Proofs of the milestones in any order are welcome, as are a proof of the counterexample to the printed statement and a proof that the platform theorem ConvexOptimization.strong_convexity_quadratic_lower_bound implies (3.4).
In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first rounds.
The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.
Fix a dimension and an unknown parameter . In round the learner is given a nonempty decision set , chooses , and observes the reward
There is a filtration such that is -measurable and is -measurable and conditionally -sub-Gaussian: for all , with fixed.
For a regularization parameter let and let be the regularized least-squares estimate. With and a known bound , the confidence ellipsoid is
The OFUL algorithm chooses, in round , a pair maximizing over . The pseudo-regret is , where .
If , for all , and , then for every , with probability at least ,
For any positive definite , and : with probability at least , for all ,
With probability at least , for all (first claim). If , then with probability at least , for all , (second claim, stated here for ).
Theorem 3 bounds the regret of OFUL by with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.
All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases , , of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.
The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix , which is itself built from the adaptively chosen actions; a bound for each fixed does not give it.
Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed for , so sums over are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy ) requires; this is an added hypothesis. Every "with probability at least , for all " is stated as an outer-measure bound on the failure event, with the time quantifier inside the event. is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.
OFUL is a predicate on the whole process: in every round the chosen pair maximizes over , with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward is the supremum over , finite because of the reward bound.
Two corrections to the printed Theorem 3 are made and disclosed. The printed is replaced by , which is what the determinant–trace bound gives; for the corrected bound implies the printed one. The hypothesis is added: for the printed logarithm can be negative, and the printed bound would then assert . In the second claim of Theorem 2, is added, because at the claim does not follow from the first claim and the paper's proof is not available.
The goal is a probability bound over the noise, not the pathwise statement "if for all then ". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same as the conclusion.
Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on , log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general and , and reusable determinant lemmas are all welcome.
A cooperative game with transferable utility assigns to every coalition of players the total payoff the coalition can secure on its own. Two solution concepts for such games go back to the foundations of game theory: the core, the set of payoff divisions no coalition can improve upon, and the stable set (von Neumann–Morgenstern solution), a set of divisions that is internally consistent and externally absorbing under the relation of domination. For general games the two concepts behave badly: the core may be empty, stable sets may fail to exist (Lucas 1968), and when they exist there are usually many of them.
Lloyd Shapley's paper Cores of Convex Games (Int. J. Game Theory 1, 1971) isolates a class of games, the convex games (supermodular characteristic functions), on which all of this becomes well behaved. Convex games arise in cost allocation, in bankruptcy and airport problems, in scheduling and sequencing games, and in any setting with increasing returns to cooperation; the supermodular functions behind them are the same objects studied as polymatroid rank functions in combinatorial optimization (Edmonds 1970). For such games the paper shows that the core is nonempty, that its faces fit together in a rigid combinatorial pattern, that its vertices are exactly the marginal-contribution vectors, and that the core is the unique stable set.
Let be a finite set of players. A game is a function from subsets of to the reals with . It is convex if
A payoff vector is , and . It is feasible if . The core is the set of feasible with for every ; in particular on .
For a nonempty coalition , the face is the set of core points with ; by convention , and . The family is the core configuration. It is complete if no is empty, and regular if and
For an ordering of the players, is the set of the first players, and the marginal vector pays each player its marginal contribution .
A payoff vector is dominated by if some nonempty coalition has and for all . A set of feasible vectors is stable if every feasible vector is either a member of or dominated by a member of , but not both.
The goal contains both halves of the page's statement: stability of the core, and uniqueness ("the unique von Neumann–Morgenstern solution").
The mission also states Theorem 3 (p. 19), the vertices of a regular core are exactly the marginal vectors , as a further item that is not on the path to the goal.
The result. Theorem 8 gives, for a natural and widely occurring class of games, a complete answer to the existence and uniqueness questions for von Neumann–Morgenstern solutions, which are open or negative in general. Theorems 3 and 5 describe the core of a convex game explicitly as the polytope spanned by the marginal vectors, the combinatorial description that underlies later work on the Shapley value, the Weber set, and the polymatroid greedy algorithm. Theorem 5 is the geometric characterization of supermodularity through the face structure of the core.
Formalizing it. All results in this mission are proved in the paper; none has a machine-checked proof on the platform. Theorem 4 is already stated on the platform (as part of a statement that also puts every marginal vector and the Shapley value in the core) and enters the mission as an existing item. The remaining work is a formal development of face configurations of the core, of stable sets and domination, and of the passage from supermodularity to the geometry of the core. The definitions of stable set and domination are general and reusable for any transferable-utility game.
The internal half of stability is immediate from the definitions: a core point cannot be dominated by any vector satisfying a coalition constraint . Uniqueness also follows from two short observations. The substance is external stability: every feasible vector outside the core must be dominated by a core point, and the dominating vector has to be produced explicitly. The obvious attempt, raising the payoffs of one violated coalition and leaving the other coordinates of unchanged, does not in general produce a core point, and nothing in the definition of the core alone controls how the core meets the hyperplane of a given coalition; that control is what the face theory of §3 is about. For non-convex games the external half genuinely fails, so no argument that ignores convexity can succeed.
Players are Fin n (a relabelling of the paper's finite set ), a game is f : Finset (Fin n) → ℝ, payoff vectors are Fin n → ℝ, and is ∑ i ∈ S, a i. The existing platform definitions Supermodularity.Cooperative.IsConvexGame ( plus supermodularity on all subsets), Core, InitialCoalition and GreedyPayoff (the marginal vectors, orderings being permutations of Fin n) are reused; the reused Theorem 4 statement is Supermodularity.Cooperative.convex_game_core_and_shapley.
Conventions committed to:
IsConvexGame.Fin (m + 1).Set.extremePoints ℝ.A formalization in which the dominating coalition may be empty, in which regularity omits , or in which the goal asserts stability without uniqueness does not state the paper's theorem and is ruled out.
Welcome contributions: proofs of the milestones in any order, general lemmas about faces of polytopes cut out by set-function inequalities, and reusable API for domination and stable sets.
Which sets of positive integers are forced to contain long arithmetic progressions? Van der Waerden (1927) showed that in any finite colouring of some colour class does; Erdős and Turán (1936) asked for a density version, which became Szemerédi's theorem. Erdős then proposed the strongest natural size condition: divergence of the reciprocal sum. Erdős Problem #3 (erdosproblems.com/3) asks whether every with contains arbitrarily long arithmetic progressions. Erdős attached one of his largest prizes to it. The primes are the motivating example: , so a positive answer would contain the Green–Tao theorem.
Timeline.
The problem is open for every .
A set is an arithmetic progression of length if and for some (for the size condition forces ). For , denotes the largest size of a subset of containing no arithmetic progression of length . A set has divergent reciprocal sum if .
For every ,
This is the formal-conjectures statement erdos_3 with its answer(sorry) instantiated to the conjectured answer yes. A disproof of the goal on the platform settles the problem negatively.
A positive answer would be a common strengthening of Szemerédi's theorem and the Green–Tao theorem, obtained from a single size condition with no arithmetic structure. Through the reduction milestone, it is closely tied to the quantitative theory of : bounds of the shape for every would suffice. Formalizing the milestones would also give reusable Lean statements of Szemerédi-type theorems in a common language.
Divergence of is a very weak condition: such sets can have density zero, and the natural approach through requires bounds just past . For this barrier was only broken in 2020. For the best known bounds (Leng–Sah–Sawhney) save only a power of in the exponent, far from what is needed. The Green–Tao method uses pseudorandom majorants specific to the primes and does not apply to arbitrary sets.
All statements import the published definition file Erdos142Basic, which reproduces the formal-conjectures definitions IsAPOfLengthWith, IsAPOfLength and the counting function r k N (over ). The reciprocal-sum hypothesis is ¬ Summable (fun a : A ↦ 1 / (a : ℝ)); the element , if present, contributes . "Arbitrarily long" is written as ∃ᶠ k in atTop, which is equivalent to "every length" because sub-progressions of progressions are progressions. Bounds stated in the literature with are written without a multiplicative constant and with "for all sufficiently large "; the constant can be absorbed into the exponent. Contributions formalizing partial summation over sets of naturals and the equivalence of the "frequently" and "for every " forms are welcome.
A recurring question in high-dimensional statistics is how tightly a scalar quantity built from many random inputs concentrates around its mean, even as the number of inputs grows without bound. Two classical answers organize the whole toolkit: martingale methods, which control a sum of dependent increments one conditional step at a time, and Gaussian-specific isoperimetry, which shows that essentially any regular (Lipschitz) function of a high-dimensional Gaussian vector concentrates as tightly as a single Gaussian coordinate, regardless of dimension. This mission formalizes one representative theorem from each line: the general martingale Bernstein bound (Wainwright, High-Dimensional Statistics, 2019, Theorem 2.19) and the Gaussian concentration of Lipschitz functions (Theorem 2.26), following Chapter 2 of the same book.
A random variable with mean is sub-Gaussian with parameter (Definition 2.2) if for all ; it is sub-exponential with parameters (Definition 2.7, a strictly milder condition) if the same bound holds only for , with the convention so that recovers the sub-Gaussian case exactly.
A sequence , adapted to a filtration , is a martingale difference sequence if each is -measurable and . Such sequences arise throughout statistics via the Doob martingale construction: given a function of independent variables , setting telescopes to , converting a deviation question about into a martingale concentration question.
A function is -Lipschitz with respect to the Euclidean norm if for all (Eq. (2.38)).
Let be i.i.d. standard Gaussian and be -Lipschitz with respect to the Euclidean norm. Then is sub-Gaussian with parameter at most , and hence
The bound is dimension-free: it depends on only through 's Lipschitz constant, not the ambient dimension itself.
For any differentiable and convex , for independent — the interpolation identity Theorem 2.26's proof is built on.
Given a martingale difference sequence with a per-index sub-exponential conditional moment-generating-function bound for , the sum is itself sub-exponential with parameters , and satisfies the two-regime concentration inequality of Eq. (2.28): sub-Gaussian for small deviations, sub-exponential for large ones. This is the chapter's central general-purpose martingale concentration tool.
Theorem 2.19 is the source of two of the most-cited concentration inequalities in the field —
the Azuma–Hoeffding inequality (Corollary 2.20) and the bounded-differences/McDiarmid
inequality (Corollary 2.21), both already faithfully covered elsewhere on the platform
(azuma_hoeffding_two_sided, bounded_diff_martingale_two_sided) and included here as
kind: reference milestones rather than redrafted. Theorem 2.26's Gaussian Lipschitz
concentration is separately significant: it is the tool behind dimension-free operator-norm
bounds for random matrices, concentration of the empirical spectral distribution, and much of
the machinery of Chapters 5 and 6 of the same book.
Formalizing it. No faithful prior art exists on the platform for either the martingale
Bernstein bound or Lipschitz-Gaussian concentration itself (a fresh search for "martingale
Bernstein," "sub-exponential martingale," "Gaussian interpolation," and "Lipschitz
concentration" returned no hits; the existing Vershynin-book item
HighDimProb.Isoperimetry.lipschitz_concentration_sphere concentrates a Lipschitz function on
the sphere, a different underlying space and a different proof from Theorem 2.26's Gaussian
vector). Both goal-adjacent theorems and the Gaussian interpolation lemma are drafted here as
open goals (:= by sorry); the two Azuma–Hoeffding/bounded-differences corollaries are reused
from the platform's existing, already-proved formalizations.
The naive approach to Theorem 2.26 — try to bound directly via a Lipschitz-type argument in — has no obvious route to a dimension-free bound, since a union bound over coordinates (or over an -net of the domain) picks up a factor that grows with . The resolution, Lemma 2.27's interpolation identity, instead exploits a special structural fact about the Gaussian distribution — its rotation invariance — to replace the nonlinear quantity with the linear, and hence exactly computable, Gaussian quantity , at the mild cost of a non-optimal constant. Theorem 2.19's difficulty is bookkeeping rather than a conceptual obstruction: the recursive conditioning step (Eq. (2.29)) must be iterated exactly times while keeping track of the interplay between the two parameters per difference, and Proposition 2.9's two-regime tail bound (small-deviation sub-Gaussian behavior, large-deviation sub-exponential behavior) must be carried through unchanged into the final statement — dropping either regime understates what the theorem proves.
Expectations are Bochner integrals against an explicit probability measure, with integrability
required as an explicit hypothesis in IsSubGaussian and IsSubExponential (Mathlib's Bochner
integral silently returns for a non-integrable function, which this mission's definitions
rule out as a trivializing formalization). The sub-exponential condition's domain restriction
|λ| < 1/α is realized as the disjunction α = 0 ∨ |λ| < 1/α, since Lean's real division
convention 1/0 = 0 is exactly backwards from the book's own stated 1/0 = +\infty convention
for the degenerate sub-Gaussian case.
" independent" (Lemma 2.27, Theorem 2.26) is formalized via Mathlib's
HasGaussianLaw predicate together with explicit coordinatewise mean-zero and
identity-covariance hypotheses, which together pin down the standard multivariate normal law,
plus IndepFun. The inner product is realized as
fderiv ℝ f (X ω) (Y ω), the Fréchet derivative applied to — equal to
by the Riesz representation of the gradient on a
Hilbert space, avoiding the need to separately construct a gradient vector field.
Theorem 2.19's printed parameter pair for part (a), "," is formalized
as : Definition 2.7 parametrizes the sub-exponential MGF bound
by (with appearing in the exponent), so a literal transcription of the printed
pair's first entry would silently square the effective parameter and make part (a), read
literally, inconsistent with part (b)'s own tail-bound formula (which the book derives from
part (a) via the general sub-exponential tail bound, Proposition 2.9). The corrected pairing is
the one the book's own proof actually establishes; see MODERATION_NOTES.md for the full
derivation.
Out of scope for this mission: Proposition 2.5 (plain Hoeffding for a sum of independent sub-Gaussians), used in the book only as background for Theorem 2.26's proof and not redrafted, since the goal theorem's own statement does not depend on it once Lemma 2.27 is in hand.
Call cube-free if no triple has all seven of , , , , , , inside . The triple is unconstrained, so a degenerate one counts. Write for the largest size of a cube-free subset.
The conjecture. for every .
This is Conjecture 5.1 of Jason Long and Adam Zsolt Wagner, The largest projective cube-free subsets of , arXiv:1810.01225. It has been open since October 2018, and a 2026 journal paper still names it as conjectured: Yuchen Meng, On Cube-Free Problems, Electron. J. Combin. 33(1) (2026) #P1.16.
The bound is sharp, and the extremal set is explicit: , the odd residues together with those congruent to 4 mod 8. Its size is . In the layer language of Long and Wagner this is .
The conjecture holds for unions of layers. That is Long-Wagner Theorem 1.10 at , and it is the largest class on which the conjectured constant is proved.
For arbitrary sets the best published unconditional bound is . Meng calls this bound "quite trivial" and gives it in one paragraph for every cyclic group, so it should not be read as progress toward . The residual gap is exactly , that is elements.
Small values are , , , , , , , matching from on.
State those values honestly. They come from solver searches, Gurobi in Long and Wagner for and an independent SAT reproduction. The SAT half that matters, the unsatisfiability of "a cube-free set of size 81 exists at ", is a solver claim with no proof certificate checked and no kernel check behind it. The witness half is verified: a set of exactly 80 elements was produced and re-checked cube-free. So is solid and is not certified. Nothing in this mission rests on either.
The goal item is the conjecture itself, for , and it is open. Every other item is a milestone that is proved mathematics, and the two closed instances and are stated separately because they are the only cases of the goal that a proof assistant has actually settled here.
The chain runs: the base case mod 8 by exhaustion, monotonicity under subsets, the bridge between the membership form and the Finset form of the forbidden configuration, sharpness, the odd-residue tight case, the layer-union theorem, the two-thirds bound, and then and .
Six definitions live in one definition item, Def_Z2nCubeFreeLayers: HasCube, CubeFree, config, ConfigFree, layerIdx and IsLayerUnion. layerIdx is written through the 2-adic valuation rather than through a congruence, because the congruence form leaves in no layer at all and needs the last layer special-cased.
CubeFree and ConfigFree are two encodings of the same condition and they are not definitionally equal, because config collapses duplicates on a degenerate triple. Their equivalence is a milestone rather than an assumption.
The Lagrange spectrum describes the asymptotic quality of rational approximation to irrational real numbers. The Markov spectrum is defined through minima of indefinite binary quadratic forms. Freiman determined the exact starting point of the maximal half-line contained in each spectrum.
This mission aims to formalize his theorem that this half-line is , where
The formalization must establish membership of every real number at least , including the endpoint, and show that no half-line starting below is contained in either spectrum.
The sources are Freiman's Russian monograph and an accompanying detailed reconstruction of its proof, with an English translation, exact computational certificates, and verification scripts. The project follows Freiman's continued fraction construction, incorporating the corrections and supplementary arguments established in the report.
The intended result is a complete Lean 4 proof. Its scope includes the equivalence of the classical and continued fraction definitions of the spectra, the infinite constructions that realize spectral values, and the exact finite calculations used in the argument.
Start with README.md and PROOF_GUIDE.md in the package. The files formalization/MISSION.md and formalization/MILESTONES.md describe the scope and proposed stages of the formalization. For reproducing the report, use the PDF and sources contained in the ZIP.
References to the report in the individual source fields use its printed page numbers.
A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is bounded.
Feghali, Lucke, Paulusma, and Ries answered that question negatively. Their conference paper appeared at ISAAC 2023, and the version of record was published in Algorithmica in 2025. The paper proves NP-completeness for bipartite graphs of arbitrarily prescribed girth and bounded maximum degree. A central input, Lemma 5, is a stronger structural existence statement: for every girth threshold there is an immune -regular bipartite graph of at least that girth, and it has a perfect matching.
This is therefore a ResearchPaper mission, not a new open-problem mission. Its goal is to formalize the published theorem and its graph-theoretic consequence. Repository candidate constructions and finite arithmetic audits remain separate and are not credited as solving the problem.
For a finite simple graph and a vertex set , the associated cut consists of all edges with one endpoint in and one in . The cut is nontrivial when both shores are nonempty. It is a matching cut when each vertex is incident with at most one crossing edge. A graph is called immune in the cited paper when it has no matching cut.
The girth is the length of a shortest simple cycle; forests have infinite girth. A graph is -regular when every vertex has exactly fourteen neighbors. Bipartiteness is witnessed by a partition into two independent sides. A perfect matching pairs every vertex with one adjacent partner.
The original OPG wording has a literal one-vertex boundary ambiguity: with nonempty shores required, has no matching cut, average degree zero, and infinite girth. The research-paper target avoids that vacuity by constructing connected graphs with at least two vertices, exact degree fourteen, and arbitrarily large finite girth.
The main theorem follows the paper's structural lemma:
The graph may depend on . The existence quantifier does not request an efficient algorithm or a numerical order bound.
A supporting theorem removes the perfect-matching and bipartite fields and records the direct substantive counterexample family:
Thus choosing refutes the intended universal assertion that some girth threshold works for every graph of average degree below .
The theorem shows that large girth and bounded degree do not force matching cuts. The examples are highly nontrivial: they are connected, regular, bipartite, and can have arbitrarily large girth. This separates local tree-like structure from the global expansion that prevents a matching cut.
Within the paper, the immune graphs serve as gadgets for hardness reductions. The journal theorem states that, for every , Matching Cut is NP-complete even for bipartite graphs of girth at least and maximum degree at most . Formalizing Lemma 5 supplies the graph-theoretic core needed to reconstruct that result without forcing this mission to formalize an entire complexity-theory reduction in its first stage.
Large girth alone makes bounded neighborhoods look like trees, and trees have many matching cuts. Immunity must therefore come from global expansion rather than short local cycles. The paper obtains the required family from Lubotzky–Phillips–Sarnak Ramanujan graphs and combines spectral and isoperimetric bounds to show that every nontrivial cut has too many crossing incidences to be a matching.
A formal proof must bridge several exact interfaces: existence of suitable primes, the finite Cayley-graph construction, bipartiteness and regularity, the girth lower bound, the spectral-to-isoperimetric inequality, and Hall's theorem for the perfect matching. None of these can be replaced by a finite sample or an asymptotic slogan.
Graphs are finite and simple. Connectedness is nonempty mutual graph reachability. A simple cycle is a cyclic list of at least three distinct vertices; girth at least means every such cycle has length at least , so forests satisfy every threshold. A matching cut requires both shores nonempty and is encoded by the condition that every vertex has at most one crossing neighbor. A perfect matching is represented by an adjacent involution.
The main theorem explicitly requires at least two vertices, although exact 14-regularity already forces nontrivial order; the redundant bound documents exclusion of the ambiguity. The mission does not claim that the frozen OPG contract was well-posed at order one. It formalizes the paper's substantive counterexample family and the consequence for the intended question.
Candidate files in the associated repository explore alternative bounded-degree constructions and integer counts. They are candidate_only and are not proof dependencies. Contributions should follow the published Lemma 5 and its cited inputs, or provide a separately sourced proof of the same declaration. The later maximum-degree-60 NP-completeness theorem is welcome as a future extension after the finite complexity framework is fixed.
[VM-STATUS-20260908-R05-PROVED]
Status update (2026-09-08): The root theorem
OPG500Counterexample.eight_vertex_counterexampleis now Proved by an accepted Prove2Me submission. All six milestones are proved and the root has zero open leaves. The accepted proof has also been independently rebuilt with Lean 4.33.1 / Mathlib0df444a360eaa60ab8c11dca51a86af692955474. The historical text below describes the mission as it stood before formal closure.
Peripheral cycles occupy a distinguished place in structural graph theory. A cycle is peripheral when it is induced and does not separate the graph after its vertices are removed. Tutte proved in 1963 that the peripheral cycles of a finite 3-connected graph generate its binary cycle space. This theorem links a local, visibly embedded kind of cycle to the global algebraic structure of all cycles.
Weighted geodesic cycles provide a different generating family. Georgakopoulos and Sprüssel proved in 2009 that, for every finite graph with positive edge lengths, every cycle is a binary sum of weighted geodesic cycles whose lengths do not exceed the length of the original cycle. In the same paper they posed Problem 3: can the edges of every finite 3-connected graph be assigned positive lengths so that every weighted geodesic cycle is peripheral? A positive answer would recover Tutte's generation theorem through metric structure.
The present target tests the opposite possibility on one explicitly specified graph with eight vertices. A candidate argument and finite certificates are available in the frozen OPG-500 research repository, but those artifacts are explicitly marked candidate_only: they are neither a published counterexample nor a machine-checked resolution. The purpose of the formal target is to determine whether the proposed universal obstruction survives complete definition, proof, and statement-faithfulness checks.
Let be a finite simple graph. A positive edge-length assignment is a function
such that for every edge . The length of a finite path or cycle is the sum of the lengths of its edges.
A simple cycle is -geodesic when, for every pair of vertices on , at least one of the two – arcs of has length equal to the shortest-path distance between and in . Equivalently, there is no – path in whose length is strictly smaller than both – arcs of . The definition concerns vertices of the cycle and permits ties between shortest paths.
A simple cycle is peripheral when it is induced and deleting all of its vertices leaves a connected graph or the empty graph. This is vertex deletion, not edge deletion.
Fix the graph on vertices . The vertices induce . For each , set and join to exactly the three core vertices other than . The four vertices are pairwise nonadjacent. Thus the frozen edge set is
The labels and edge set are part of the statement and are not interchangeable with earlier candidate labelings without an explicit isomorphism.
Formalize the following statement for the fixed graph :
The existential cycle may depend on . The universal quantifier includes all strictly positive real assignments, including assignments with tied shortest paths. This is the stable target; finite samples and rational specializations are subordinate checks rather than replacements for it.
The development should also formalize the finite weighted geodesic-cycle generation theorem of Georgakopoulos and Sprüssel, the exact 3-connectivity and peripheral-cycle classification of , the required shortest-path and tight-subgraph statements, the finite cycle-space rank statements, and the finite minimum/descent principle used to select a cycle outside a closed binary span. These targets should remain separate declarations so that their assumptions and reuse boundaries are visible.
A proof of the main target would give a negative answer to the finite problem by exhibiting a 3-connected graph for which no positive edge weighting can make all geodesic cycles peripheral. It would not contradict Tutte's theorem: peripheral cycles may still generate the cycle space even though they cannot be made to contain every geodesic cycle for any weighting. The distinction between these two generation mechanisms is part of the mathematical content.
A formal development would add more than a checked final sentence. It would provide reusable definitions for positively weighted finite graphs and vertex-geodesic cycles, a precise treatment of the two arcs between cycle vertices, explicit deletion semantics for peripheral cycles, and finite cycle-space infrastructure. It would also separate purely finite graph facts from statements quantified over arbitrary real weights. The candidate repository currently supplies finite enumeration and abstract Lean fragments, but no existing artifact checks this full dependency chain.
Until the complete main theorem is verified, the eight-vertex graph remains a candidate obstruction and the original problem remains unresolved by this development.
The central difficulty is the universal quantification over real edge lengths. Testing many integer or rational vectors cannot cover it. Shortest paths need not be unique, so an argument that silently perturbs the weights or assumes unique geodesics can change which cycles are geodesic. Every strict and weak inequality must therefore agree with the source definition, including tie cases.
The graph is small but the semantic boundary is not. A formal cycle representation must expose the two cycle arcs for every vertex pair without admitting malformed or repeated-vertex objects. The peripheral predicate must combine inducedness with connectivity after vertex deletion and must classify all cycles, not only a selected family of triangles. Finally, finite cycle-space computations and rank inequalities must be connected to actual paths and weighted geodesicity; a propositional or enumerative certificate alone does not establish that bridge.
The Lean development will use Fin 8 for the vertices of and a SimpleGraph representation for adjacency. Weights will be functions on the edge subtype, so values on nonedges cannot affect the theorem. All weights are real and strictly positive. Paths and cycles are finite and simple; arbitrary walks do not count as target witnesses. Geodesicity is vertex-based and includes tied shortest paths. Peripheral cycles use inducedness and vertex deletion, with a connected-or-empty remainder.
The main theorem must retain the quantifier order “for every weighting, there exists a cycle.” It may not be weakened to rational weights, finitely many tested assignments, nonnegative weights, one selected weighting, edge-geodesicity, or the assertion that only four named core triangles fail to be peripheral. Definitions must be sorry-free, and nontrivial mathematical claims must be theorem declarations with separately checked proofs.
Reusable contributions include finite weighted-path length, shortest-path attainment in finite positive graphs, the equivalence of the two geodesic formulations, cycle-arc APIs, vertex-deletion connectivity, binary edge-vector encodings, and finite descent outside a closed span. Graph-specific finite certificates are welcome only when their checker is represented in Lean or their conclusions are otherwise proved in the kernel.
a41fe59b4535851ea55f6e868e938b9aaf81e924. https://github.com/vibemathing/problem-opg-500-geodesic-cycles/tree/a41fe59b4535851ea55f6e868e938b9aaf81e924A modular form has a complex L-function whose critical values carry arithmetic information. To compare those values in p-adic families, their transcendental period factors must first be removed. The remaining algebraic numbers can then be embedded into a p-adic field. The result sought here is a single bounded measure encoding the critical values of all twists by characters of p-power conductor. This is the existence and interpolation theorem underlying the cyclotomic p-adic L-function (one of the most fundamental objects of Iwasawa theory).
The reference is the famous paper of Mazur, Tate and Teitelbaum, Chapter I, especially §§10–14 (MTT); but for simplicity we are treating only the ordinary case here (not the more general finite-slope case), and not attacking the results later in MTT (exceptional-zero conjectures, etc).
Fix a prime , a positive integer , and a weight . Let be a normalized cuspidal Hecke eigenform of weight on with nebentypus and Fourier coefficients (necessarily algebraic). Fix embeddings and . No condition is imposed. The character is extended by zero on nonunits modulo .
The form is ordinary when . The ordinary root is the root of
with . This convention also covers the case: if , then and the unit root is (MTT I.§12).
A measure means a continuous -linear functional on the continuous functions . It is a bounded p-adic measure, rather than a positive real-valued measure. The Lean representation is Mathlib's AbstractMeasure on (PadicInt p)ˣ.
The two periods and normalize the signed modular integrals. Write
and use for sign . A period system specifies nonzero periods, algebraic normalized values for , and finite generation over of the lattice generated by these values. Period rationality and finite generation are separate mathematical obligations, combining Manin–Shimura rationality with the module-of-values construction in MTT I.§2; see also the explicit treatment of general eigenforms in Williams, §11.7.
The goal is to construct an ordinary root, a period system, and a measure with the following interpolation property. Let be a primitive Dirichlet character of conductor , where , and let . Put . With the positive-exponential Gauss sum , define the algebraic number by
The required identity is
where all algebraic character values in the following expression are transported by :
This is the scalar period-normalized form of MTT I.§14. At both character values at vanish, leaving . At the primitive character is the character of modulus one, and both Euler factors remain. The latter case is included explicitly.
Seven milestones isolate period rationality and its finite lattice; existence and uniqueness of the ordinary root; the distribution relation for polynomial disk moments; uniform boundedness of constant disk masses; unique extension to a measure with every critical polynomial moment; the complex Birch–Mellin identity; and the deduction of interpolation from the two signed measures. Their source locations are recorded individually. The period milestone combines two standard inputs; the boundedness and extension milestones specialize the MTT construction to slope zero.
The result supplies the analytic input for studying p-adic special values and their variation. It also supplies reusable infrastructure for normalized modular integrals, rational period systems, finite-order twists, and bounded measures on p-adic units. The classical existence theorem is known. The work proposed here is to prove the stated Lean theorems and connect the existing Mathlib analytic and algebraic infrastructure. Local compilation establishes that the declarations are well-typed; the mission statements remain unproved targets.
Listing algebraic critical values does not establish that one bounded measure interpolates them. Values on nested residue disks must satisfy compatibility, and ordinary boundedness must control the extension to continuous functions. Polynomial moments of positive degree must agree with that same extension. The unramified character requires its own Euler-factor calculation; simply applying the ramified formula at conductor one loses factors. On the complex side, rationality requires genuine periods of the modular form, not arbitrary chosen scaling constants. These are the obligations represented by the milestones.
The cusp form is Mathlib's analytic CuspForm, with Fourier coefficients tied to its width-one q-expansion. The nebentypus transformation law and every prime Hecke eigenvalue equation are written explicitly. The prime Hecke operator includes both its translated sum and its second term; when the prime divides the level, the second term vanishes. The complex twist is the finite-translate expression for , and its critical L-value is defined by the actual Mellin integral. Neither an arbitrary L-value table nor the desired measure is an input assumption.
The embeddings share the abstract algebraic closure of ; there is no asserted continuous map from to . The algebraic bridge in each interpolation identity is existential and constrained by a complex equality. Test functions are existential continuous maps constrained pointwise to equal the specified character or disk function; this makes their continuity part of the conclusion instead of an unproved definition. All primes, including , are allowed. Natural-number subtractions occur only in theorem contexts with and .
The signed projections use a factor of . Their normalized measures are added, and the period sign is . These conventions fix the powers, sign, Gauss sum, and periods in the displayed interpolation formula. Periods are not asserted to be canonical integral periods; rescaling by algebraic constants changes the normalization. Exceptional-zero derivative formulas, positive-slope distributions, tame-conductor twists, and Iwasawa main conjectures are outside this mission.
Adam McKenna closed this mission on 13 September 2026 following Unit distances in convex polygons, by Liam Kruer, Jensen Kohlmeyer, and Liam Price. Their construction gives strictly convex point sets with Ω(n log log n) unit-distance pairs and arbitrarily large minimum unit-distance degree, answering both questions and the general fixed-k version of Problem 97 negatively.
Paper and complete Lean source. All credit for the counterexample and its formalization belongs to those authors. Adam McKenna prepared the Prove2Me adapters.
Do not start further proof attempts or solver runs for the affirmative conjectures. Existing statements, conditional lemmas, partial proofs, and milestones remain as historical work. The owner has authorized closure assuming the external result is correct; individual theorem pages report Prove2Me verification status.
The mission is to prove the combined open goal
for finite point sets in strictly convex position in the Euclidean plane.
Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every nonempty convex-independent finite set then has a vertex with at most three neighbors at each positive radius, in particular at radius . Delete that vertex and preserve convex independence. Apply the same step to every subset created by deletion until no points remain. Charge each unordered unit-distance pair to the first endpoint deleted. Each deleted vertex receives at most three charges, so an -point set determines at most unordered unit-distance pairs. This gives the Problem 96 bound and therefore . The package uses this one-way dependency; it does not seek a reverse implication.
Let be finite. Strict convex position means that every point of is an extreme point of the convex hull of . For , the pinned multiplicity at radius counts points with . Problem 97 asks for a point where no radius has four such other points. Problem 96 counts unordered pairs at distance , then takes the supremum over convex-independent -point sets.
The historical progression is part of the setting. Erdős’s 1946 paper posed an earlier three-neighbor version. His 1987 account reports Danzer’s convex nonagon in which every vertex has three equidistant witnesses, and asks about four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex configuration with the same unit distance at every vertex, placing the local question beside the unit-distance problem.
The Problem 97 target is the canonical statement that every nonempty finite convex-independent has no four-equidistant-point property:
The Problem 96 target is the canonical asymptotic statement
where is the supremum of the unordered unit-distance counts determined by convex-independent -point sets. The bound is asymptotic; the Problem 97 route would give the stronger explicit bound for every natural number .
The package records a formal proof route joining a pinned geometric obstruction to a global extremal bound. A successful Problem 97 proof would immediately settle Problem 96 with the explicit constant , while preserving the combinatorial meaning of the count. It also separates the historical three-neighbor constructions from the still-open four-neighbor assertion.
The source proof reduces Problem 97 to strong induction on . Its counting engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib (2013). This engine forces every counterexample to have at least nine points; a finite geometric analysis excludes exactly nine points; and the remaining step must produce a removable vertex for every larger minimal counterexample. The removable-vertex statement carries the induction hypothesis that every strictly smaller nonempty convex 4-equidistant set is contradictory. That large-cardinality geometric step remains open, so both headline targets remain open. Finite computational certificates can support local cases but do not replace the universal geometric statement.
Problem 97 is open, so the mission also records the parallel negative route.
The source formalization calls a nonempty convex-independent
finite set with the four-equidistant property a
Problem97.IsCounterexample.
Constructing one such set would refute Problem 97 and therefore refute the
mission's affirmative conjunction, regardless of whether Problem 96 remains
true. The counterexample milestone keeps this resolution path visible beside
the nonexistence proof. A successful witness must use exact coordinates or
exact algebraic data from which Lean verifies both strict convex position and
the four-equidistant property; a numerical approximation or a realizable
incidence pattern alone is insufficient.
Problem 96 has its own negative route. Because its claim is asymptotic, one finite convex configuration cannot refute it. A counterexample must instead give convex-independent point sets at arbitrarily large cardinalities whose unit-distance counts exceed every proposed linear constant. The mission tracks this superlinear-family statement separately, together with a reduction from it to the exact negation of Problem 96. This keeps both possible outcomes visible: a direct or Problem-97-derived linear upper bound, and an explicit family proving that no such bound exists.
The canonical source is pinned at commit
757d852766f377f7c1a0ffeeef6d3526bc0cb7a4. It contains the formal source
statements for Problem 97
and Problem 96.
The source repository reports closed proofs of the conditional bridge to the bound
(conditional three-times bound),
the counting milestone
(nine-point counting bound),
and the exact nine-point exclusion
(exact nine-point exclusion theorem).
The remaining large-cardinality milestone is the
removable-vertex step,
with its minimality hypothesis retained. The current platform mission contains
accepted transfers of the counting argument, the conditional bridge, and the
exact nine-point exclusion, while the removable-vertex step remains open. Its definitions make
convex independence and the positive-radius condition explicit; no theorem is
assumed inside a definition. Singletons and two-point sets are included in
Problem 97, while Problem 96's counting definitions also include the empty set.
The source repository uses Lean v4.27.0; these mission statements target the
platform's v4.33.1. Source-proof transfer and revalidation remain separate work.
The Lean declarations and proofs are this project's own formalization. The
Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical
provenance; they do not indicate that a paper proof was imported or
machine-checked directly.
These source results establish the intended dependency graph: the P97 universal
root feeds low-unit-degree extraction, strong induction, and then the P96
supremum bound. The platform mission records those contracts and milestones;
it does not claim to have transplanted their proof bodies.
The milestones include the two canonical roots, their conditional bridge, the
|A| ≥ 9 count, the n = 9 exclusion, the |A| > 9 removable-vertex step,
the documented Danzer nine-point three-neighbor example, the parallel goal of
constructing a Problem 97 counterexample, and the superlinear-family route to
a counterexample to Problem 96.