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.
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?
Let be a finite connected graph. In Bernoulli bond percolation each edge is independently retained with probability and deleted otherwise, and one writes for the probability that vertices and lie in the same component of the resulting random subgraph. Comparing such connection probabilities is a basic and genuinely hard problem: computing them exactly is -hard.
The bunkbed graph is built from two copies of , joined by vertical edges called posts above a chosen set of transversal vertices. Percolation is performed on the two copies while every post is retained. Writing for a vertex in the lower copy and for its counterpart upstairs, Kasteleyn conjectured in 1985 that being connected within a level is always at least as likely as crossing between levels.
The conjecture is intuitively compelling — crossing levels appears to require "using up" a post — and it resisted proof for forty years. A short timeline:
Section 7 of the source is a candid account of a large-scale machine-learning-guided search that failed to find a counterexample, and of why the problem is unusually ill-suited to experimental testing.
Fix a finite graph with vertex set and edge set , and a retention function (the uniform case is ). A configuration is a subset of open edges, occurring with probability
and is the total probability of those for which and are connected in .
Given , the bunkbed graph has vertex set . Its edges are a copy of in each level together with a post for every . In bunkbed percolation the two level-copies are percolated independently while all posts are retained; denotes the resulting connection probabilities.
For the gadget on vertices,
The result itself. A forty-year-old conjecture in percolation theory is false, and prior positive results are thereby sharpened rather than superseded: it becomes interesting to delimit exactly which families of graphs do satisfy the inequality. The refutation also settles the Counting, Weighted, Alternative and Computational variants listed in §8.1, and shows the random-cluster analogue cannot be pushed from down to .
Formalizing it. Nothing here is open; the mission produces machine-checked versions of published results, and as a by-product the first percolation theory in Lean. Mathlib currently contains no percolation of any kind — no connection probabilities, no bunkbed graph, no hypergraph percolation. That infrastructure is reusable far beyond this mission. The source itself notes (§8.2) that its central combinatorial lemma was independently verified by computer; a formal proof would replace that check with a certificate.
The obvious approach — exhibit a small graph and compute both probabilities — is hopeless, and the source explains why at length. A graph with edges has configurations; for the counterexample here the probability gap is on the order of , so no sampling argument can detect it, and exact enumeration is out of reach. Section 7 records a substantial computational search that found nothing and, in hindsight, could not have.
The proof is instead structural, and its difficulty is concentrated in one place. Hollom's refutation of the hypergraph version cannot be transferred directly, because a single -hyperedge cannot be simulated by bond percolation on any gadget graph. The source's answer is to prove a robust version of Hollom's lemma (Lemma 3.3) which survives the inexact simulation that gadget graphs do provide, and this robustness is what Lemma 4.1's inequality quantifies. Lemma 3.3 is proved by constructing a weight-preserving involution on a refined configuration space — the technical heart, and the milestone a solver should expect to spend the most effort on.
The development commits to the following conventions.
ℚ and evaluate by #eval, and small instances close by decide.Finset and realised through SimpleGraph.fromEdgeSet; connectivity is Mathlib's SimpleGraph.Reachable.Sym2 V → ℚ), since the gadget genuinely needs two different weights: its spokes are retained with probability and its path edges with probability .0 is the lower copy; posts over T are unconditionally present and are not percolated. The two levels are percolated independently.IsPlanar, no Euler formula, no Kuratowski. Building one is a larger project than this mission. The formalized statement of Theorem 1.2 is therefore strictly weaker than the published one, and the goal is instead the negation of the conjecture, which is exactly the source's own "In particular, the BBC is false." Contributions adding planarity are welcome and would strengthen the milestone.Infrastructure. Mathlib supplies SimpleGraph, boxProd, Reachable with a DecidableRel instance, fromEdgeSet, edgeFinset and Finset.powerset. It supplies no percolation, so this mission ships two definition files: Bernoulli bond percolation with the bunkbed construction and the five triple-partition probabilities, and hypergraph percolation with Hollom's hypergraph and the Wierman–Ziff five-state model. One known gap: Mathlib's Reachable decision procedure enumerates walks and is far too slow to evaluate the -configuration check of Lemma 3.1 by decide. A solver will want a linear-time reachability procedure together with a proof that it agrees with Reachable; that is itself a worthwhile reusable contribution.
The tensor product of chain complexes is a basic construction in homological algebra and in the theory of quantum CSS codes. If and are finite based chain complexes over a finite field, their tensor product is graded by total degree,
Each complex carries a basis-dependent homological distance: is the least Hamming weight of a degree- cycle that is not a boundary, with when the degree- homology vanishes. A natural candidate for the distance of the tensor product is therefore
Every nonzero pair of homology classes in complementary degrees gives a pure-tensor class of the corresponding product weight, so one always has . The substantive question is whether this upper bound is always sharp.
In the preprint Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates, posted in 2018 and subsequently published in Physical Review Letters, Zeng and Pryadko proved that the bound is sharp when one factor is a binary one-complex. Their exact formula is Eq. (13) of the arXiv version and is the capstone theorem of the Prove2Me mission Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates. The present formalization is a direct sequel: it retains the same definitions and degree conventions while examining what happens when the one-complex restriction is removed.
Zeng and Pryadko later considered arbitrary finite chain complexes over arbitrary finite fields in Minimal distances for certain quantum product codes and tensor products of chain complexes, published in 2020. In the corresponding arXiv preprint, Conjecture 18 asserts the unrestricted equality
The conjecture is appealing because it would make tensor-product distance completely compositional: the degreewise distances of the two factors would determine the distance of their product. The obstruction is that a homology class in need not have a minimum-weight representative supported in a single bidegree. A representative spread across several summands of the total complex can be lighter than every pure-tensor representative. The purpose of this formalization is to turn that observation into a concrete, machine-checked counterexample to Conjecture 18 while preserving the valid one-complex theorem as a sharply delimited special case.
The common foundation is recorded in the Prove2Me entry Based binary chain complexes and homological distance. In particular, the boundary in degree is a map , and
The one-complex result is separately available as Eq. (13) — Exact distance with a one-complex. The construction below uses exactly the same notion of distance, but both tensor factors are genuine three-term complexes.
Begin with binary CSS check maps
assumed surjective and satisfying . Suppose there are logical vectors such that
The check maps determine two dual three-term complexes
Their degree-two tensor space has three bidegree summands, corresponding to , , and . Under the natural matrix identifications, consider the element whose three blocks are
The CSS orthogonality relations make this element a cycle. Its pairing with the chosen logical vectors certifies that it is not a boundary. Its Hamming weight is exactly , whereas the componentwise candidate in degree two reduces to
Consequently, any CSS datum satisfying
produces the strict inequality . For orientation, a binary quantum Golay CSS presentation with parameters has , giving the numerical comparison . The formal proof must supply an explicit CSS instance and verify its algebraic and distance properties, rather than relying on the parameter notation alone.
The first milestone proves the general certificate: for every CSS datum satisfying the hypotheses above, the element is a nontrivial degree-two cycle of weight , and the componentwise minimum is .
The second milestone constructs and verifies one explicit CSS datum for which . This is the step that turns the general mechanism into an actual counterexample.
The capstone packages the construction as the direct existential statement
Thus the final theorem is not conditional on the existence of suitable code data: it exhibits finite based binary chain complexes for which the equality proposed in Conjecture 18 fails.
The counterexample concerns only the unrestricted passage from a one-complex factor to two arbitrary bounded complexes. It does not conflict with Zeng and Pryadko's Eq. (13), whose one-complex hypothesis rules out the three-bidegree interaction used here.
The broader literature also indicates why additional structure matters. Bravyi and Hastings introduced homological-product codes and analyzed logical representatives in product constructions; Audoux and Couvreur developed tensor products of CSS codes through chain-complex methods. More recently, Akhmechet et al. discussed the Zeng–Pryadko conjecture in the structured setting of complexes derived from Khovanov homology, while Berthusen et al. restated it as Conjecture 5.1 in their study of automorphism gadgets. Golowich and Guruswami obtained strong distance guarantees for iterated homological products under expansion and local-testability hypotheses. These results are compatible with the proposed counterexample: they concern special families or impose hypotheses that are absent from Conjecture 18.
Besides settling the unrestricted statement, the formalization isolates a reusable obstruction. It shows precisely how a low-weight class assembled across several bidegrees can evade a formula based only on the degreewise distances of the factors. This distinction should help guide corrected formulations in which an exact product formula, or a useful lower bound, is recovered from additional geometric, expansion, or local-testability assumptions.
The main formal issues are mathematically substantive rather than presentational: the proof must respect the endpoint conventions for the boundary maps, distinguish a cycle from a non-boundary, compare finite weights with -valued distances, and verify a concrete strict-gap instance. Making each of these points explicit is especially important here, because an indexing shift or a merely conditional existence statement would no longer constitute a refutation of the conjecture as stated.
A quantum circuit of depth built from gates of fan-in at most two cannot let an output wire depend on more than input wires. The argument is folklore and takes a paragraph on paper: the causal cone of the measured wire grows by at most a factor of two per layer. Formalizing it exposes a subtlety that the paper argument hides, and that is what this mission is about.
Define the backward cone step of a wire set through a layer by adjoining the support of every gate of that meets . There is a choice here: test each gate against the incoming set , or against the partially accumulated cone. Testing against the accumulator over-approximates, and the doubling bound fails. Testing against the incoming set gives the bound — but is only correct when the gates within a layer act on pairwise disjoint wires.
Without that hypothesis (LayerOk) the semantic statement is false, and the counterexample is
small: on three wires, the single layer [cnot 2 1, cnot 1 0] has cone around wire
, yet wire ends up holding . So the cone under-approximates
the true dependence. This mission's development carries LayerOk throughout, and the
counterexample is recorded in the source.
Layered circuits over on wires, with states as amplitude functions on bit-strings and no tensor products anywhere. On top of that:
acceptProb is a genuine probability in ;The semantic half is proved in the Heisenberg picture. The measurement observable is conjugated backwards through the circuit and its support tracked: a gate meeting the support enlarges it by that gate's own wires, and a gate missing it commutes with the observable and cancels against its own adjoint. That cancellation is the reason the non-cascading cone step is correct, and it is why unitarity of the gate set is needed at the -dimensional level rather than gate by gate. Supporting this is a small reusable algebra of local operators: locality is monotone, closed under adjoint and product, and disjointly supported operators commute.
The published depth bound assumes each input wire lies in the syntactic cone of the output. That is weaker than saying the wire matters. Milestone 1 asks for the semantically honest version, stated in terms of genuine functional dependence; the bridge is the semantic cone theorem already in the development.
Beyond that, the natural continuations are the same argument for fan-in- gates (), for geometrically local circuits where cone growth is linear rather than exponential, and ultimately the Bravyi–Gosset–König separation — which needs machinery (non-local games, magic squares) that this development deliberately does not build.
When exact dynamic programming is intractable, practice runs on approximations: one-step and multistep lookahead with a cost-to-go surrogate, open-loop feedback control, and rollout — the algorithm that improved backgammon programs and became a conceptual ancestor of Monte-Carlo tree search and modern policy improvement schemes. Chapter 6 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) gives the basic guarantees: performance bounds for limited lookahead (Props. 6.3.1–6.3.2), superiority of open-loop feedback control over open-loop control (Prop. 6.2.1), and the cost-improvement theory of rollout on discrete deterministic problems (Props. 6.4.1–6.4.3). These are the theorems that make "approximate DP" more than a heuristic.
Two frameworks. For the stochastic bounds (§6.2–6.3): the basic finite-horizon model of Mission I of this series (BertsekasDPModel), its policy cost recursion, and the open-loop cost of a fixed control sequence (BertsekasDPOpenLoopCost). For rollout (§6.4.1): a graph search problem — a finite digraph with destination set and terminal costs on destinations (BertsekasGraphSearch); a base heuristic producing from every node a path to a destination (BertsekasBaseHeuristic), with projection and heuristic cost ; the rollout algorithm repeatedly moves to a neighbor minimizing (BertsekasIsRolloutRun). is sequentially consistent if its paths have the tail property (Def. 6.4.1), sequentially improving if (Def. 6.4.2).
For sequentially improving and any terminating rollout run :
— BertsekasDP.rollout_sequential_improvement (goal, Prop. 6.4.2). Milestones: Props. 6.4.1 (termination under sequential consistency with the book's tie-breaking), 6.4.3 (exact cost identity via the defects ), 6.3.1, 6.3.2 (lookahead bounds), 6.2.1 (OLFC).
Prop. 6.4.2 is the "rollout never hurts" theorem — the formal warrant for policy improvement by simulation, with Prop. 6.3.1 its stochastic counterpart (via Example 6.3.1 the rollout of any policy improves that policy). Prop. 6.3.2 is the robustness version that quantifies the cost of inexact minimization, used for CEC bounds. Formalizing the chapter yields a reusable graph-search + base-heuristic vocabulary and connects it to the Mission I stochastic model. Everything here is proved in the book; the formal versions are new.
The rollout proofs are elementary but exact: the min formula (6.37) requires tracking the running minimum along the run, and the IsLeast membership half forces identifying which neighbor value is attained. Termination under sequential consistency (6.4.1) is the delicate one — it fails without the tie-breaking convention (the book gives a cycling counterexample), so the formal statement carries the convention explicitly and the proof must extract a termination measure from "strict decreases are finitely many, plateaus shorten the heuristic path". The stochastic bounds are clean backward inductions over the Mission I recursion.
Graph search: finite node type, arcs as ordered pairs, vertex costs only (no arc costs — the book's reduction absorbs them into destination costs); heuristic paths as lists; rollout runs as lists (finite, complete runs) except 6.4.1, where the run is an infinite sequence absorbed at destinations so that termination is a genuine claim. Ties in neighbor selection are allowed everywhere except where 6.4.1's convention pins them. Stochastic side: state-independent constraint sets for OLFC (as in §6.2); restricted lookahead sets per Eq. (6.19); all statements at the level of the Mission I model.
An LLM agent acting in an environment spends most of its wall-clock time waiting. Each step — a model call, a tool or MCP request, a browser action, sometimes a human reply — must complete before the next can be issued, and the round trips dominate end-to-end latency: a chess game between two reasoning agents runs for hours, and an operating-system tuning task for tens of minutes. When a training or prompt-optimization loop repeats such a run thousands of times, the waiting is the cost.
Speculative actions (Ye, Ahuja, Liargkovas, Lu, Kaffes, Peng, ICLR 2026) transplants a classical systems idea — speculative execution in microprocessors, and speculative decoding for LLM inference — to the agent's environment loop. A cheap, fast speculator guesses the action a slow, authoritative actor is about to produce, the guess is used to launch the next environment call early, and the work is committed only when the actor's real action confirms the guess. The interface stays sequential and lossless; the internals run in parallel.
What makes this a formalization target rather than an engineering report is the paper's §5 cost–latency analysis. Speculating more branches buys hit probability but costs tokens, and the paper derives closed-form expressions for both sides of that trade — a self-contained piece of applied probability sitting underneath a systems paper. This mission asks for those expressions, machine-checked.
Fix a horizon and index steps . At each step a policy maps the state to an API call; the actor executes it with latency , while the speculator proposes candidate actions with latency , where (the speculator is faster in expectation). A speculative branch hits when the action it guesses implies the same next call the actor's true action would have implied; branches hit independently across steps with probability .
Two knobs define the two regimes analyzed. Breadth : at each step, launch independent one-step speculations in parallel, each immediately followed by a real call. At least one of the succeeds with probability
Depth: follow a single branch, extending it whenever a speculative or real call returns and pruning subtrees the actor contradicts.
The quantity driving both results is , the expected number of hits by round . A hit consumes the following step's speculation window — after a correct guess the next call is already cached, so no new speculation is launched there — which yields the two-term recursion
Write for the latency and token cost of strictly sequential execution, and for their speculative counterparts. In the depth regime latencies are taken deterministic: for a real call, for a speculative one.
The goal theorem is the finite-horizon latency ratio for breadth-focused speculation (Proposition 1), with abbreviated :
The supporting targets, ordered as the analysis builds them:
The analysis is what turns speculation from a trick into a tunable system. Proposition 1 and Theorem 4 are governed by the same quantity , so a practitioner who can estimate hit probability can choose offline against a latency/cost budget rather than by trial. The 50% ceiling is a genuine negative result — it says breadth alone cannot do better, and motivates the depth regime, where the ceiling becomes 1. Theorem 3 explains why confidence-based branch selection is cheap in practice: the whole dynamic program collapses to one scalar continuation value, so a runtime system sorts confidences and adds branches greedily in per step.
The paper's proofs are pen-and-paper and, as far as we are aware, none of these results has a machine-checked proof. Three parts reward formalization specifically. The recursion's closed form is derived by a characteristic-equation argument with a particular solution that collides with the homogeneous part — routine but error-prone. The per-hit saving is an honest two-dimensional integral over independent exponentials. And Theorem 6's cost expression is stated in the paper with a floor function and then immediately replaced by an approximation, so formalizing it forces a decision about which claim is actually being asserted (see Formalization scope).
The obvious first move on the recursion — guess a constant particular solution — fails, because is a root of the characteristic polynomial and a constant trial collides with the homogeneous family; the particular solution is linear in , and the coefficient comes out of matching both initial conditions, not one.
The interesting hypothesis is the one the recursion's shape encodes and the prose states only in passing: a hit at round removes the speculation window at round . Drop it and the recursion becomes one-term and the answer changes.
For the per-hit saving, the difficulty is analytic rather than algebraic: the inner antiderivative of must be handled, and the outer integral runs over an unbounded interval, so integrability has to be established rather than assumed.
The asymptotic statements need the oscillating term controlled uniformly — it is bounded, not vanishing termwise in an obvious way — before the prefactor can be taken to zero.
Everything is over . The model lives in one definition bundle,
Def_SpecActions_model, in namespace SpecActions; the mission's Lean names match the
prose symbols ( is hits, is phit, is kt).
The model is formalized at the level the paper's own proofs use: and
are defined by the expressions Appendix A derives for them
(specTime, specCost, and their depth analogues), and the theorems assert the
algebraic and asymptotic identities relating those quantities. Deriving those
expressions from a measure-theoretic model of the execution trace is deliberately not
in scope — with one exception: milestone 2 states the per-hit saving as a genuine
iterated integral against the exponential densities, so the one probabilistic step the
paper actually computes is formalized as an integral rather than assumed.
Conventions a solver should know before starting:
hits takes (the per-step hit probability ), not the per-branch ;
phit relates the two, and Thm_SpecActions_phit_bounds supplies the
range facts the other statements assume.Reusable beyond this mission: the two-term linear recursion solved in milestone 1, and
the computation for independent exponentials, which is a standard
fact absent from Mathlib. Contributions extending the model toward an actual measure on
execution traces — deriving specTime rather than defining it — are welcome as
follow-on work.
Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code over a finite field has a dual code consisting of the words orthogonal to all words of under the standard coordinatewise bilinear form.
The MacWilliams identity states that the full Hamming-weight distribution of is determined by that of through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's The Theory of Error-Correcting Codes. The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.
This development isolates the arbitrary- Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.
Let be a finite field of cardinality , let be a finite coordinate type, and let a word be a function . A linear code is an -linear subspace of the word space. The standard bilinear form is
and the dual code is
The Hamming weight is the number of coordinates at which is nonzero. Writing , the homogeneous Hamming weight enumerator of is the integer-coefficient polynomial
Thus the coefficient of is the number of codewords of weight . The Lean development represents this object symbolically in MvPolynomial (Fin 2) ℤ; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.
For a primitive complex additive character of , define
The first milestone states that when and otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.
For every word and all , the second milestone records the full character-weighted transform of the Hamming monomial:
This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.
The capstone is the following equality of integer polynomials:
This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula
The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.
The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.
The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in ; and the final result is most reusable as an equality of symbolic polynomials over . The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.
The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.
The coordinate type is an arbitrary finite type rather than only Fin n; its cardinality plays the role of the code length. A word is CodingTheory.Word F ι := ι → F, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.
The polynomial CodingTheory.hammingWeightEnumeratorPolynomial has coefficients in and variables indexed by Fin 2. Variable records zero coordinates and variable records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.
The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to . The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.
Counting the trees on a fixed, labeled vertex set is one of the oldest enumeration problems in graph theory. Cayley stated the count in 1889 while enumerating isomers of saturated hydrocarbons — each tree corresponds to a possible carbon skeleton — and the same number reappears throughout combinatorics as the number of spanning trees of the complete graph , a special case of Kirchhoff's Matrix–Tree Theorem, and as the base case against which more refined tree-counting results (trees with a prescribed degree sequence, forests, spanning trees of general graphs) are measured.
Several independent proofs of the count are known — a direct recursive argument, a determinant computation via the Matrix–Tree Theorem, a double-counting argument on increasing trees — and each exposes a different piece of structure. This mission formalizes the proof via Prüfer sequences, due to Prüfer (1918): an explicit, computable bijection between labeled trees and certain finite sequences, presented here following Gross and Yellen, Graph Theory and Its Applications, 3rd ed. (CRC Press, 2018), Section 3.7, pp. 157–162.
Fix and take the vertex set to be (formalized as Fin n).
A labeled tree on vertices is a simple graph on this vertex set that is
connected and acyclic (Mathlib's SimpleGraph.IsTree). Two labeled trees are the same
exactly when their edge sets coincide — the two 4-vertex trees in Figure 3.7.1 of the
source are both paths but are different labeled trees, since the labels sit on
different vertices.
A Prüfer sequence of length is any sequence of labels drawn from , repetitions allowed (so there are of them, by the rule of product).
The encoding of a tree (Algorithm 3.7.1, p. 157) builds its Prüfer sequence by repeating, times: find the leaf (degree-one vertex) with the smallest label among those not yet removed, record the label of its neighbor, then delete that leaf. The decoding of a sequence (Algorithm 3.7.3, p. 159) reverses this: it rebuilds the tree edge by edge, at each step joining the smallest label not yet used and not appearing later in the sequence to the next label in the sequence, finishing by joining the two labels left over.
This is the weakest stable statement: it is exactly the count Cayley identified, phrased without reference to any particular proof method, so it is not tied to properties of Prüfer sequences beyond what is needed to establish the count.
The identity itself is foundational: it is the base case of Kirchhoff's Matrix–Tree Theorem (which computes the analogous count for spanning trees of an arbitrary graph as a cofactor of its Laplacian) and it appears as an ingredient in random graph theory (counting spanning trees of bounds the number of ways a random graph process can build a tree) and in the analysis of algorithms on trees, where the Prüfer encoding itself is used as a compact serialization of a labeled tree.
The result has been proved by hand for over a century, and its most classical proof (the
one formalized here) has not, to this project's knowledge, appeared as a
machine-checked Lean proof; Mathlib's Combinatorics.SimpleGraph library has the tree
and acyclicity infrastructure this mission builds on, but not the Prüfer bijection or
the count itself. Formalizing it here means constructing the encoding and decoding maps
explicitly as computable, total recursive functions, and proving they are mutually
inverse — the mission's four milestones below are exactly the four supporting results
the source uses for this.
The obvious first attempt is to define the encoding by structural recursion, peeling one
leaf per step, but this immediately runs into a dependent-typing obstacle: after
deleting a vertex, the "remaining graph" naturally lives on a smaller vertex type, so
a naive recursive definition changes type at every step and the final sequence's type
(length ) is not visible to the recursion by construction. The formalization here
sidesteps this by keeping the ambient vertex type fixed at Fin n throughout and
tracking the shrinking set of "active" vertices as an ordinary Finset (Fin n)
parameter, so the recursion is on a natural number step-counter rather than on the type
itself; the price is that every step's "leaf" and "neighbor" must be picked out by an
explicit Finset.filter/Finset.min computation whose well-definedness (there is
always a smallest active leaf, and it always has a unique active neighbor) is exactly
the content of Propositions 3.7.1 and 3.7.3 below, rather than something the type system
gives for free. The inverse direction has the dual issue in reverse: decoding recurses
structurally on the sequence while tracking a shrinking label set, and showing the two
recursions undo each other (Proposition 3.7.4) requires the same induction run in both
directions simultaneously.
Trees are SimpleGraph (Fin n) satisfying Mathlib's SimpleGraph.IsTree; no alternate,
weaker notion of "tree" is used. Prüfer sequences are functions Fin (n - 2) → Fin n
(equivalently, by Fintype.card_fun, exactly the count needed) rather than
List or Vector, so that the final counting step is immediate once the bijection is
established. The encoding and decoding functions (pruferEncode, pruferDecode) are
supplied as noncomputable definitions in Definitions.Def_GYGraphTheory — noncomputable
only because Prop-level decidability of a general SimpleGraph.Adj is classical, not
because the algorithm is non-constructive; every step is the literal Prüfer procedure,
junk-valued (defaulting to label 0) outside its intended domain in exactly the way a
hand proof would say "this step is meaningless once fewer than two active vertices
remain." The four milestones give the precise faithful statements of the source's
Propositions 3.7.1, Corollary 3.7.2, Proposition 3.7.3, and Proposition 3.7.4; the goal
theorem is the immediate corollary once all four are in hand, via Fintype.card_congr
and Fintype.card_fun. A trivializing formalization is not available here: IsTree is
Mathlib's standard, non-vacuous notion, and the milestones pin down pruferEncode
and pruferDecode to the source's specific algorithm rather than leaving the bijection's
existence as a free black box. Beyond the four milestones, a full development needs:
basic Finset/List manipulation lemmas relating pruferPeel's step-indexed recursion
to pruferDecodeAux's list-indexed recursion (reusable in any future mission touching
Prüfer-style encodings); and the final cardinality argument tying the bijection to
n ^ (n - 2). Contributions connecting this formula to Mathlib's general Matrix–Tree
machinery (if and when it exists) would be a natural, welcome extension but are out of
scope for this mission.
The weak pentagon problem asks for a five-label structure on the edges of every triangle-free cubic graph. Although its wording resembles proper edge coloring, properness is not part of the conjecture. Instead, each individual color class must meet enough odd cycles that deleting that class leaves a bipartite spanning graph. The problem connects odd-cycle transversals, cut structure, and homomorphisms to a fixed sixteen-vertex graph.
Robert Šámal recorded the conjecture on the Open Problem Garden in 2007. DeVos and Šámal proved that sufficiently high-girth subcubic graphs map to the Clebsch graph, with an explicit girth threshold in their theorem; that does not cover all triangle-free cubic graphs. The mission separates the general existence question from two exact reformulations that can be verified independently.
Let be a finite simple triangle-free cubic graph. A five-edge coloring here is any symmetric assignment
It need not be proper or surjective. For a color , delete all edges with label while retaining every vertex. The coloring is a weak-pentagon coloring when each of the five resulting spanning graphs is bipartite.
Equivalently, each color class is an odd-cycle edge transversal: it meets the edge set of every simple odd cycle. The cycles are not required to be induced. This last distinction matters because an odd cycle may have a chord in the original graph and still survive in a deleted-edge spanning subgraph.
A second representation uses the sixteen four-bit vectors. Two vectors are adjacent when their Hamming distance is three or four. This graph is a model of the Clebsch graph. A graph homomorphism sends every edge of to an adjacent pair in this target.
The root target is
No condition is imposed on adjacent edges receiving different labels.
For every fixed graph and fixed five-edge labeling,
This theorem is graph-general: triangle-freeness and cubicity delimit the root but are not needed for the equivalence.
For every finite simple graph ,
where has vertex set and edges at Hamming distance three or four. The statement concerns existence of some coloring and some homomorphism; it does not preserve an arbitrarily prescribed coloring.
The root theorem would establish a uniform parity decomposition for all triangle-free cubic graphs. The transversal form makes every odd cycle use all five colors. The homomorphism form replaces edge labels and five separate bipartitions by one bounded vertex certificate, allowing structural and computational methods to share an exact target.
Formalization prevents several nearby but inequivalent conjectures from being conflated. A weak-pentagon coloring can be improper. Checking only induced odd cycles of the original graph is insufficient. Mapping to a five-cycle is stronger and fails even for familiar positive examples. The explicit four-bit model also avoids relying on the name “Clebsch graph” without fixing its adjacency convention.
The equivalences reorganize the problem but do not create the required object. Five odd-cycle transversals must be pairwise compatible as color fibers; finding one small transversal is not enough. Local deletion and gluing methods must preserve existence of a whole homomorphism, not one chosen boundary assignment.
High-girth results leave finitely many short-cycle configurations only when the girth hypothesis is present. Triangle-free graphs may still contain overlapping five- and seven-cycles, and naive local recoloring can repair one odd cycle while breaking another color complement. Minimum-counterexample arguments also require care because deleting vertices preserves subcubicity but not cubicity.
Colors are Fin 5. The coloring stores a symmetric value on ordered endpoint pairs, with nonedge values ignored. Cubic means every neighbor set has extended cardinality exactly three. A simple odd cycle is a cyclic list of at least three distinct vertices of odd length; it need not be induced. Bipartiteness is witnessed by a Boolean side assignment after one color is deleted.
The sixteen-vertex relation is defined directly on four-bit functions by Hamming distance, so its cardinality and adjacency are not hidden behind an imported graph name. The repository's transversal proof, normalization, and local homomorphism studies are candidate_only; the mission publishes their clean statements as proof obligations. Contributions may close either equivalence, formalize known high-girth results, prove restricted graph classes, or attack the root. A finite benchmark or a failure of one extension strategy is not a counterexample to the conjecture.
The dichromatic number of a digraph is the directed analogue of chromatic number: vertices of one color may be adjacent, but each color class must induce an acyclic digraph. The Two Color Conjecture asks whether every orientation of a planar graph has dichromatic number at most two. It is a natural directed-coloring counterpart to planar graph coloring, with the key difference that forbidden monochromatic objects are directed cycles rather than undirected edges.
Critical-digraph theory gives general degree restrictions on minimal counterexamples, and Li and Mohar proved two-colorability under the additional hypothesis that the directed girth is at least four. The unrestricted planar-orientation problem permits directed triangles, so that theorem is a genuine partial result rather than a solution. The project candidate develops the elementary least-order-counterexample consequences needed before any planar structural argument.
Let be a finite simple planar graph. An orientation assigns exactly one direction to every edge of , with no loops, parallel arcs, or pair of opposite arcs. For , the induced digraph retains every arc whose two endpoints lie in .
A two-coloring is a map
It is valid when both induced digraphs and contain no directed cycle. The color classes need not be independent and either color may be unused.
Planarity belongs to the underlying undirected graph. Lean represents it by an injective straight-line embedding with noncrossing nonincident edges. Directed reachability is reflexive, so a singleton orientation is strongly connected under the usual length-zero convention, although it is also acyclic and hence cannot be a counterexample.
The goal is
Disconnected graphs and empty color classes are included.
A supporting theorem states that every counterexample of minimum vertex order is nonempty and strongly connected, and its underlying graph has minimum degree at least three:
The minimum is taken over the full class of finite planar orientations, not over one embedding or an arc-minimal subclass.
A stronger open milestone asks whether every vertex of such a least-order counterexample has at least two incoming and at least two outgoing neighbors. This is recorded separately because it is stronger than the degree-three conclusion and its repository proof remains candidate_only.
The root theorem would establish a universal two-color bound for planar orientations while allowing directed triangles and arbitrary local degree. A counterexample would demonstrate a sharp obstruction specific to directed cycles, not visible to ordinary planar coloring.
The formalized minimal-counterexample package is reusable regardless of the ultimate answer. Strong connectivity permits arguments inside one component, while the degree and semidegree restrictions narrow discharging configurations and finite searches. Encoding the full induced color classes prevents an invalid shortcut in which only a selected acyclic spanning subdigraph is checked.
Deleting a low-degree vertex is safe only if a valid coloring of the smaller graph can be extended without creating a monochromatic directed cycle through the restored vertex. For a chosen color, obstruction depends on both an incoming and an outgoing neighbor of that color together with a directed return path in the old color class. Merely seeing same-colored in- and out-neighbors is not sufficient.
Strongly connected components can be colored separately because their condensation is acyclic, but that observation only reduces a minimal counterexample to one component. Planarity alone does not eliminate directed triangles or the return paths that block both colors. Results assuming directed girth at least four therefore leave the central case untouched.
A directed graph is a binary relation, coupled to a SimpleGraph by an orientation predicate that requires exactly one direction on every edge and forbids arcs on nonedges. A directed cycle is a cyclic list of at least three distinct vertices. A color class is acyclic when no such list lies entirely in that class. Strong connectivity is nonempty mutual reflexive-transitive reachability.
The least-order predicate quantifies over every smaller finite planar orientation in the same universe. It does not assert that a counterexample exists. Consequently, its structural theorems may be true vacuously if the root conjecture is true; the read-back must expose that conditional form.
Repository arguments, finite tables, and transport receipts are not machine-checked proofs. Contributions may formalize component gluing, exact vertex-extension criteria, degree or semidegree restrictions, planar reducible configurations, or the root. Any stronger minimum-degree claim must remain distinct from the admitted degree-three target until proved.
Quantum query algorithms are known to beat classical ones on problems with algebraic structure -- period finding, hidden subgroups, forrelation. No such speedup is known for a problem with no structure at all. Aaronson and Ambainis proposed making that observation into a theorem, and reduced it to a question with no quantum content: a statement about bounded low-degree polynomials on the Boolean cube (Aaronson--Ambainis 2009).
The question has resisted since. A timeline of what is actually established:
The cases that are settled are settled under structural hypotheses -- block-multilinearity, complete boundedness, symmetry, Boolean range. The general statement is open.
Let be a positive integer. The Boolean cube is , carrying the uniform distribution; a point is identified with the real vector it names, so a real multivariate polynomial in variables has a value at each cube point. For a function on the cube write
The variance of is . Writing for with its -th bit flipped, the influence of coordinate on is
These are the combinatorial forms of both quantities, as used in the source; no Fourier--Walsh expansion is required to state anything below. The degree of is its total degree as a polynomial. Call bounded when at every cube point -- a condition imposed only on the cube, not on all of .
The goal is the conjecture in the shape stated by its authors: there is an absolute constant such that for all , all , every polynomial of degree at most that is bounded on the cube, and every with , some coordinate satisfies
The constant is quantified outermost and may depend on nothing. That uniformity is the entire content: bounds that degrade exponentially in are already known, and a goal naming a specific exponent would be superseded by the next improvement.
The result itself. Aaronson and Ambainis prove that the conjecture implies that the acceptance probability of any bounded-error -query quantum algorithm on a Boolean input can be approximated, to small error on all but a small fraction of inputs, by a classical algorithm making queries. Quantum speedups would then require structure in a precise sense. The conjecture also has purely classical content, asserting that boundedness plus low degree forces variance to concentrate on some single coordinate rather than spread across all . Without it, no such concentration is known at any rate polynomial in .
Formalizing it. The conjecture is open, so this mission does not formalize a known proof of the goal. What it produces is a machine-checked statement of the conjecture together with formalizations of the partial results above, each currently existing only on paper. The milestone chain also yields reusable infrastructure for analysis of Boolean functions, of which Mathlib currently contains none: no Fourier--Walsh expansion, no influence, no variance on the cube.
The elementary bound is the Poincare inequality on the cube, , which yields a coordinate with influence at least . This is tight for the dictator and depends on , so it says nothing: the conjecture demands a bound free of entirely.
The natural repair is the route available when takes only the values and . A Boolean-valued polynomial of degree depends on boundedly many coordinates, which immediately produces an influential one. That argument does not survive relaxing the range to the interval : a bounded real-valued polynomial of low degree need not depend on boundedly many coordinates, and every known substitute loses a factor exponential in . Closing the gap between exponential and polynomial dependence on is the difficulty, and it is where all of the partial results stop.
Polynomials are MvPolynomial (Fin N) ℝ and degree is Mathlib's totalDegree, so the
statement needs no bespoke notion of degree. Expectation is a finite sum scaled by
rather than a measure-theoretic integral, keeping every definition elementary. Bit flipping
is Function.update x i (!x i). Boundedness is asserted at cube points only. Variance and
influence are the combinatorial definitions above, published as the definition
AaronsonAmbainis.
Three points close off degenerate readings. The exponent of the source is rendered as an existentially quantified natural number with no leading multiplicative constant, since admitting one weakens the claim. Taking that exponent to be would demand influence at least and is therefore not a trivializing choice, while larger exponents only weaken the bound; the content is that some fixed exponent suffices for all and at once. The hypothesis is universally quantified over , which is equivalent to the source's exact-degree form because the smallest admissible gives the strongest conclusion. The cases and are vacuous, since fails for a constant polynomial.
A complete development needs, beyond the published definitions, a Fourier--Walsh layer with Parseval's identity, the level- machinery used by the partial results, and -- for the completely bounded case -- operator-space norms on multilinear forms. All of the Boolean-analysis material is reusable well beyond this mission. Contributions of any milestone are welcome, as are alternative formalizations of the definitions in function-level rather than polynomial-level form.
Out of scope: the quantum simulation consequence is not formalized here. Stating it requires a formal quantum query model, which no Lean library currently provides.
Circular coloring refines ordinary vertex coloring by placing colors on a cycle and measuring separation modulo the palette size. It records information that an ordinary chromatic-number bound can lose, and it interacts sharply with planarity, forbidden short cycles, and degree constraints. OPG-401 asks for a specific bound at the intersection of those themes: whether triangle-free planar graphs of maximum degree three always admit a circular coloring of ratio .
The question appears on Xuding Zhu's open-problem page and in the Open Problem Garden record. Nearby theorems on fractional coloring do not settle it: fractional chromatic number and circular chromatic number are distinct parameters, so the known fractional bounds for subcubic triangle-free graphs cannot simply be substituted for a circular-coloring proof. Work on circular recoloring likewise studies connectivity between colorings that already exist and does not supply the missing universal existence theorem.
For integers , a -coloring of a finite simple graph is a map
such that the shortest cyclic distance between and is at least for every edge . Equivalently, using representatives in , the modular difference lies between and , inclusive. The circular chromatic number is the infimum of the ratios for which such a coloring exists.
The root domain consists of all finite simple graphs that are planar, triangle-free, and subcubic. Disconnected and empty graphs are included. Planarity is represented by an injective straight-line drawing with no vertex in the interior of an edge and no intersection between nonincident edges. For finite simple graphs this is the standard straight-line form of planarity.
The central target is
This is exactly the claim in a form suitable for finite Lean data.
A reusable finite milestone freezes the local palette arithmetic. For , let be the colors at cyclic distance at least seven from . For all ,
This includes equal colors, antipodal colors, tied symmetries, and all twenty residues. It is the exact obstruction encountered when extending a coloring over a deleted degree-two vertex while preserving every old color. The repository artifact supporting this formulation is only candidate_only; the mission publishes the statement as an open formal target rather than claiming it as proved.
A proof of the root theorem would give the requested sharp circular-coloring guarantee uniformly over a broad planar graph class. It would also separate the circular problem from nearby fractional results by constructing the stronger cyclic palette assignment itself. A counterexample, if one exists, would have to survive the combined restrictions of planarity, triangle-freeness, and maximum degree three, and would identify a genuine boundary for local extension methods.
Formalization adds two concrete assets. First, the cyclic-distance convention is fixed once, avoiding common errors involving directed residues, unrestricted integer lifts, or truncated subtraction. Second, graph reductions can be checked against a precise preservation obligation: deleting a vertex does not help unless the chosen coloring of the smaller graph has compatible boundary colors. The mission therefore welcomes both global structural arguments and verified finite boundary classifications, but finite enumeration alone is not accepted as a proof for arbitrary graph order.
The obvious induction on vertices fails at degree two. A coloring of need not extend over : if its two neighbors receive colors at cyclic distance at least seven, their two allowed sets can be disjoint. The local table characterizes this failure exactly but does not guarantee that a different coloring of has favorable boundary values. Recoloring, reducible configurations, and planar discharging must therefore interact without silently assuming universal extension or connectivity of the recoloring graph.
A second source of difficulty is parameter confusion. Bounds for fractional colorings do not automatically yield -colorings, and a theorem about mixing existing circular colorings does not prove existence. Any proposed bridge must be stated and verified explicitly.
Lean represents colors by Fin 20 and uses the minimum of the two directed modular differences as cyclic distance. Edge compatibility includes both the lower bound and the formal upper bound . Triangle-freeness is literal absence of three mutually cyclic adjacent vertices, and subcubic means every neighbor set has extended cardinality at most three.
The definition bundle contains no theorem and no sorry. Draft theorem items contain exactly one := by sorry. The local candidate computations and GitHub transport records are provenance, not evidence that either theorem is proved. A complete contribution may formalize the finite palette table, a faithful reducible configuration, a recoloring lemma with all quantifiers exposed, or the root theorem. Every claimed universal reduction must retain finiteness, simplicity, planarity, triangle-freeness, and the degree bound.
A star edge coloring is a proper edge coloring with an additional local restriction: no path or cycle of four edges may use only two colors. It sits between ordinary proper edge coloring and strong edge coloring. The problem is local enough to admit finite obstruction searches, but global enough that independently valid local colorings may fail to fit together.
Dvořák, Mohar, and Šámal proved in 2013 that every subcubic multigraph has a star edge coloring with seven colors and conjectured that six always suffice. The Open Problem Garden records the simple-graph version as OPG-37271. The value six would be best possible because the complete bipartite graph has star chromatic index six.
Subsequent work has proved the six-color bound under additional hypotheses. Lei, Shi, and Song proved it for subcubic multigraphs with maximum average degree less than and obtained a five-color result below . Casselgren, Granholm, and Raspaud proved the conjecture for cubic Halin graphs and several bipartite families. These results leave the unrestricted finite subcubic case as the target of this mission.
Let be a finite simple undirected graph. An edge coloring assigns to each unordered edge of one color from a finite palette. It is proper if two distinct edges incident with the same vertex always have different colors.
A simple path of four edges has five pairwise distinct vertices and consecutive edges . It is bichromatic in a proper coloring exactly when the first and third edges have the same color and the second and fourth edges have the same color. The path need not be induced: additional chords do not remove it. A four-cycle has four pairwise distinct vertices and is bichromatic under the analogous alternating equalities, including the closing edge.
A coloring is a star edge coloring when it is proper and contains neither type of bichromatic four-edge configuration. The star chromatic index is the least palette size admitting such a coloring. A graph is subcubic when every vertex has at most three neighbors.
The main target is the exact OPG-37271 assertion for finite simple graphs:
In the Lean statement, this is expressed directly as the existence of a coloring by Fin 6; no separate minimization operator is needed.
The first literature milestone is the established seven-color theorem:
Formalizing this result provides a checked baseline and infrastructure that a six-color argument can reuse.
The second literature milestone records both sides of the exact value
Thus the mission cannot be completed by weakening the goal to a larger universal constant.
A proof would determine the universal star chromatic-index bound for graphs of maximum degree three and would match the known lower-bound example . A counterexample, if one exists, would separate six from the established seven-color bound and identify the first genuinely seven-chromatic subcubic graph.
The formalization contributes a reusable definition of star edge coloring on Mathlib finite simple graphs. In particular, it fixes several conventions that are easy to blur in informal or computational work: forbidden paths have four edges rather than four vertices; they are simple but need not be induced; four-cycles are checked separately; and properness is not inferred merely from the absence of an alternating four-edge pattern. These definitions can support certified bounded searches, verified coloring certificates, and later formalizations of sparse or planar special cases.
The current research repository contains candidate-only local extension criteria and finite certificates. They may motivate future milestones, but they are not treated here as proofs of the conjecture, as admitted evidence, or as replacements for the literature milestones.
A direct greedy coloring argument can fail at a newly inserted edge because a color may be forbidden either by an adjacent edge or by a bichromatic four-edge path created several incidences away. Deleting a low-degree vertex and coloring the remaining graph therefore does not guarantee that the old coloring extends without recoloring. Explicit small configurations already witness failure of this zero-recoloring strategy while remaining globally six-colorable.
The known seven-color proof has one extra color available to break such interactions. Reaching six requires coordinating local recolorings or extracting stronger structure from a minimal counterexample. Finite searches can test configurations and produce certificates, but bounded verification alone cannot establish the universal quantifier over all finite graphs.
The mission uses SimpleGraph with an arbitrary finite vertex type. Edges are unordered edge-set elements, and palettes are the labeled finite types Fin k. The graph need not be connected, cubic, planar, or nonempty; isolated vertices and the empty graph are included. “Subcubic” means degree at most three, not degree exactly three.
A forbidden path is represented by five pairwise distinct vertices and four consecutive adjacencies. It is not required to be induced. A forbidden cycle is represented separately by four pairwise distinct vertices and four cyclic adjacencies. Under the properness hypothesis, equality of opposite edge colors is precisely the bichromatic alternating pattern.
A complete development should supply the known seven-color theorem, certify the exact value for , and then address the six-color goal. Contributions formalizing faithful special cases or reusable extension lemmas are welcome, but sampled graph families and successful SAT searches remain finite evidence unless converted into a general Lean proof.
ddc49c1978a196490702150bb75264793a658457. RepositoryThe Fourier series of a periodic function decomposes it into sinusoidal components, but the partial sums of that series need not converge to the function even when the function is continuous: du Bois-Reymond exhibited in 1873 a continuous -periodic function whose Fourier partial sums diverge at a point. Fejér's 1904 theorem repairs this failure by replacing the partial sums with their Cesàro (arithmetic) averages: for every continuous periodic function, these averages converge to the function, uniformly, with no smoothness hypothesis beyond continuity. This was the first universally valid summation method for Fourier series, and its underlying technique — averaging against a kernel whose mass concentrates at the origin — became the template for what is now called a good kernel or approximate identity, the basic device used throughout harmonic analysis (heat-kernel smoothing, Poisson summation, Fourier-inversion arguments) [Stein & Shakarchi, 2003].
Timeline.
Let be continuous and -periodic, i.e. for every . Its -th Fourier coefficient, for , is
Its -th partial sum is , and its -th Cesàro (Fejér) mean is the arithmetic average of the first partial sums,
This is the full 1904 statement: no restriction to pointwise convergence, and no extra regularity assumed on beyond continuity.
The result itself. Fejér's theorem gives the first universally valid summation method for the Fourier series of a continuous function, closing the gap left open by pointwise convergence tests that need extra regularity. It also yields, essentially for free, a proof of the Weierstrass approximation theorem on the circle — the trigonometric polynomials are dense in the continuous -periodic functions under the uniform norm — and it is the historical prototype of the good-kernel/approximate-identity method underlying Poisson summation, heat-kernel smoothing, and Fourier-inversion arguments.
Formalizing it. Mathlib currently has no infrastructure for this at all. Mathlib.Analysis.Fourier.AddCircle defines Fourier coefficients on the circle and proves convergence (Parseval's identity, via the orthonormal Fourier basis), but it has no notion of a partial sum, no Dirichlet or Fejér kernel, and no pointwise or uniform convergence result for Fourier series of any kind. This mission builds that classical convergence theory — the Fejér kernel, its closed form and positivity, the good-kernel estimates, and the uniform convergence theorem itself — from first principles.
The obvious first attempt is to bound termwise from the individual Fourier coefficients. This fails outright: a continuous function's Fourier coefficients need not be absolutely summable, which is exactly the mechanism behind du Bois-Reymond's divergence example. The real difficulty is representing as a convolution,
against the Fejér kernel , and then proving is a good kernel: nonnegative, integrating to over one period, and — the genuinely quantitative step — with its mass outside any fixed neighborhood of vanishing as . That last estimate needs the closed form
which carries a removable singularity at that must be handled carefully, together with a genuine decay estimate — via a lower bound on — valid uniformly outside any fixed -neighborhood of the origin.
is complex-valued, and only continuity together with exact -periodicity is assumed — no differentiability, no bounded variation, no realness. Uniform convergence is stated with Mathlib's TendstoUniformly. The period is fixed at , matching the classical circle-group convention, rather than a general ; the -periodic statement is a routine rescaling of this one and is not separately targeted here. One route to a trivializing formalization is worth ruling out explicitly: assuming any extra regularity on (differentiability, bounded variation, Lipschitz continuity) would let the uniform-convergence conclusion follow from the much easier Dirichlet-kernel estimates, and would no longer be Fejér's theorem — the entire content of the result is that continuity alone suffices.
The needed infrastructure is the four definitions above (Fourier coefficient, partial sum, Cesàro mean, Fejér kernel) and the milestone lemmas below, culminating in the goal. The Fejér kernel's closed form, positivity, and good-kernel estimates are reusable well beyond this mission: directly for a Lean proof of the Weierstrass approximation theorem on the circle, and for any future development that needs an explicit approximate identity on the circle group. Contributions are welcome at every milestone; the concentration estimate is the analytic heart of the mission and a natural place to start.
In 1956 Kelly answered a question that looks like gambling and is really about information: if a channel gives you a noisy advance signal about a sequence of bets, how much is that signal worth? His answer was that the maximum exponential rate of growth of a gambler's capital equals the rate of transmission over the channel -- so information rate and capital growth rate are the same quantity in different units. The betting fraction that achieves it is now called the Kelly criterion, and it is the basis of a large practical literature on position sizing.
The result is short, entirely explicit, and has no analytic subtleties -- which makes it a good formalization target and a surprising gap: the platform currently has fifteen missions on bandit algorithms and none on optimal growth.
This mission formalizes the simplest case of Kelly's Section 4: an even-money bet with no
track take, won independently with probability p and lost with probability q = 1 - p. A
gambler stakes a fixed fraction l of current wealth on each bet, so wealth is multiplied by
1 + l on a win and 1 - l on a loss. The exponential rate of growth is
Kelly shows this is maximised at l = p - q, with maximum value 1 + p log p + q log q in
bits. We state G in nats (natural logarithm), so the maximum carries an additive log 2;
dividing by log 2 recovers Kelly's bit-valued form, which is exactly 1 - H(p) for the
binary entropy H. The maximiser is unaffected by the choice of base.
The goal theorem is that l = 2p - 1 maximises G over the admissible range (-1, 1) when
the bet is favourable (p > 1/2). Milestones supply the maximum value (Kelly's
information-rate identity), the admissibility of the maximiser, and the concavity that makes
the first-order condition sufficient.
J. L. Kelly Jr., A New Interpretation of Information Rate, Bell System Technical Journal
35 (1956) 917-926, Section 4 ("the simplest case"). The growth-rate expression and the
maximiser l = p - q are stated there; the maximum value in bits is Kelly's eq. for G_max.
The identity and maximiser were checked numerically before drafting: for p = 0.55, 0.6, 0.7,
0.9 the claimed maximum matches log 2 + p log p + q log q to six decimals, and a grid search
over (-1, 1) at 1e-5 resolution returns 2p - 1 in every case.
Positive-definite functions sit at a crossroads of harmonic analysis, probability, and machine learning. A function is positive-definite if, for every finite family of points and complex coefficients , the Hermitian quadratic form is real and nonnegative. This single algebraic condition is exactly what makes realizable as: the covariance kernel of a stationary stochastic process; the characteristic function of a random variable (up to normalization); a valid Mercer/RBF kernel in machine learning; or a valid random-features/spectral density in random-feature kernel approximation methods.
Bochner's theorem (1932) is the structural reason all of these examples work: it says positive-definiteness is not merely a necessary condition for such a representation, but exactly characterizes it. A continuous, normalized () function is positive-definite if and only if it is the Fourier–Stieltjes transform of some probability measure on — i.e. is the characteristic function of a random variable. This mission asks for a machine-checked proof of that theorem, together with its most useful corollary: the case where is additionally Lebesgue-integrable, so that has an explicit continuous density given directly by the ordinary Fourier transform of .
Fix IsPositiveDefinite f as above, for (not restricted to real-valued kernels — the standard, fully general statement). A positive-definite function is automatically Hermitian-symmetric, (IsPositiveDefinite.conj_neg), which is exactly what makes a representation by a genuine (positive) probability measure possible, rather than a signed or complex one. The theorem works with f continuous and normalized. No further hypothesis (in particular, no integrability of f) is assumed for the general representation theorem: the representing measure need not be absolutely continuous (e.g. for a periodic , is a discrete measure supported on the harmonics of the period — this is Herglotz's 1911 theorem, the periodic special case). Under the extra hypothesis that f is Lebesgue-integrable, the representing measure becomes absolutely continuous with a continuous density: this density is fourierTransform f, the (real part of the) Fourier transform of f — automatically real-valued, again by Hermitian symmetry — and Fourier inversion recovers f from it.
The central representation theorem: no integrability hypothesis on , so may be any probability measure, not necessarily a density.
L¹ (density) caseThe special case where the representing measure of the goal theorem is absolutely continuous with an explicit density — the form most directly usable in applications. Provable independently of the general goal theorem via classical Fourier-inversion machinery, so it is a natural, self-contained first target.
Bochner's theorem is one of the load-bearing structural results of 20th-century harmonic analysis: it underlies Bochner–Minlos-type theorems for random fields, the entire theory of stationary Gaussian processes, kernel methods in statistics and machine learning, and (via its periodic specialization, Herglotz's theorem) the spectral theory of stationary time series. Formalizing it gives the platform a reusable, general-purpose characterization of positive-definite functions that any future mission on kernel methods, random features, or characteristic functions can build on directly.
The general representation theorem is the harder target: the standard proof (see the Wikipedia article linked below) constructs, from f, a strongly continuous unitary representation of on a Hilbert space via a GNS-type construction, then invokes Stone's theorem and the spectral theorem to extract the representing measure — a substantial functional-analytic argument, since f need not be integrable and need not have a density. The L¹ milestone is comparatively more tractable: it can be attacked directly via Mathlib's existing Fourier-transform and Fourier-inversion machinery for integrable functions, plus the elementary fact (already available for reuse: IsPositiveDefinite.conj_neg) that a positive-definite function is Hermitian-symmetric.
IsPositiveDefinite is formalized exactly as the finite Hermitian-form condition above, over Fin n → ℝ point families and Fin n → ℂ coefficients, matching the standard convention in the literature, with f : ℝ → ℂ — the fully general, complex-valued statement, not restricted to real-valued kernels. fourierTransform f ξ is defined as the real part of ∫ Complex.exp(-i2πξ x) * f(x) dx; this is provably the exact (not merely real-part-of) Fourier transform once f is positive-definite, since Hermitian symmetry forces the integral to be real already.
A space group describes the rigid motions compatible with a periodic spatial symmetry. The classification concerns possible symmetry types, rather than the size or shape of a particular drawing of a crystal. The classical three-dimensional numbers are 230, 219 when mirror-related types are identified, and 65 for the orientation-preserving subfamily. These are the three numbers recorded in Oliver Knill’s survey, §94, “Crystallography,” p. 41. Keeping their conventions separate matters: changing which coordinate transformations are allowed changes what counts as the same type.
The target is the known classification result selected by LeanEval v1, not an unsolved classification conjecture. Its authoritative specification is the declaration LeanEval.Geometry.SpaceGroupsProblem.space_groups. The accompanying benchmark manifest attributes the classification independently to Fedorov and Schoenflies in 1891. The work requested here is a machine-checked proof of that fixed statement.
For a natural number , let with its Euclidean inner product. A Euclidean isometry is an invertible affine distance-preserving transformation of this space. The objects being counted are subgroups of this full motion group. In the benchmark’s definitions, is discrete when, for every point and every real , the set of its elements satisfying is finite.
Such a group is crystallographic when it also contains translations by the members of some linearly independent family of vectors. Translation by means exactly that the transformation sends every to . These conditions specify the underlying groups directly; they do not start with a list of previously classified examples. Although the structure field containing the translation condition is called cocompact, its actual content is the existence of these independent translations, not a separately assumed compact quotient.
An affine equivalence between two groups is an invertible affine map whose conjugation carries the first group’s set of transformations onto the second’s. It need not be an isometry. An orientation-preserving affine equivalence additionally requires the determinant of that affine map’s linear part to be positive. Separately, an individual isometry preserves orientation when its own linear part has positive determinant. The Sohncke subfamily restricts the groups themselves: every element of a group must preserve orientation. This is distinct from restricting the map used to compare two groups, as explicitly distinguished by the source definitions and notes.
Write for crystallographicCountOP d, for crystallographicCount d, and for crystallographicCountOPOnly d. They count, respectively, orientation-preserving affine classes of all crystallographic groups, arbitrary affine classes of all crystallographic groups, and orientation-preserving affine classes within the all-elements-orientation-preserving subfamily. The sole goal is
This is the exact benchmark conjunction, in its original order. None of its three components is optional, and they are not separate theorem targets. There are no milestones or auxiliary theorem items.
The result gives finite and exact answers for the specified spaces of symmetry types, while retaining the distinction between orientation of a coordinate change and orientation of every symmetry in a group. The difference between 230 and 219 reflects the identification of mirror-related types described in Knill, §94; the 65 count answers a different question, concerning the restricted subfamily. Neither a single count nor a list that silently merges the equivalence conventions establishes the full assertion.
The formalization would add a proof connecting these numerical claims to the actual groups and class subsets specified in Lean. The benchmark source currently supplies the statement with an unproved placeholder. This draft likewise supplies a statement, not a proof or a claim that the benchmark is solved.
A finite catalog can have 230 entries without representing every crystallographic group, and different entries can still represent the same affine class. Thus checking the length of a catalog alone does not establish the source’s cardinality assertion. The difficulty is the mathematical connection between concrete descriptions and all groups admitted by the definitions, with precisely the required equivalence relations. The restricted 65-count must also respect the condition on every group element, rather than just a label attached to an example.
The Lean representation is EuclideanSpace ℝ (Fin d), with affine isometries and affine equivalences from Mathlib. The three source counting functions use Set.encard in the extended natural numbers . More precisely, each counts the set of subsets obtained as the class of some admissible group; it does not count representatives with multiplicity. Consequently, the displayed finite equalities include finiteness, which is not assumed beforehand.
One reusable definition bundle contains exactly the source’s model spaces, translation and discreteness predicates, crystallographic-group subtype, orientation predicate, two conjugacy relations, and three counting functions. Their declarations are preserved, including definitions for every natural dimension; only the theorem fixes . Definitions for group actions, affine conjugation, and these class subsets can be used independently of this particular count. Contributions must establish the fixed goal with these meanings. Replacing the groups by a hard-coded finite type, defining a count to be its desired answer, or importing an unproved classification into the definition bundle would not establish this target.
296b7491ec989d21bcf8636a9a69231a1e5d1d25. Exact Lean source; manifest with historical bibliography.A finite allocation problem begins with a list of permitted choices. Each recipient may use some resources but not others, and a resource may be assigned at most once. Knowing that every recipient has an available resource is insufficient: several recipients may all depend on the same small pool. A useful theorem must decide whether the compatibility pattern permits all requirements to be met simultaneously.
This mission develops the matching results in the chapter on systems of distinct representatives in D. Yogeshwaran's Discrete Mathematics—Lecture Notes, §6.1. Its endpoint allows different recipients to require different numbers of resources. The classical one-resource problem, the regular-graph case, and the case in which a bounded number of assignments may remain unfilled are retained as separate source-numbered results. The project concerns established theorems, not a new conjecture about the existence of matchings.
A finite simple graph consists of a finite set of vertices and unordered pairs of distinct vertices called edges. A bipartition is a pair of disjoint sets whose union is the vertex set, such that every edge joins a vertex in to a vertex in . The left vertices represent recipients and the right vertices represent resources. An edge records that the resource is permitted for that recipient. These graph conventions follow Definition 1.1 of the notes.
For a vertex , the neighbor set contains the vertices joined to . For a set of vertices, write . A matching is an edge set in which no vertex is used twice. It is complete on if every left vertex is used, and perfect if every vertex is used. A subgraph may retain selected edges of the original graph. Its degree counts the retained neighbors of .
A demand is a natural number attached to each . Unlike a complete ordinary matching, the capstone may assign more than one resource to a recipient. Resources still have capacity one, and a demand may be zero.
The ordinary matching criterion is Theorem 6.2:
The development also includes Exercise 6.3, asserting that a -regular bipartite graph has a perfect matching when . Proposition 6.4 states the quantitative deficit version:
The capstone is the prescribed-degree equivalence of Exercise 6.5:
This statement retains the entire demand function and does not fix a uniform demand, restrict demands to positive values, or replace integral selections by real weights.
The set-theoretic interface is Corollary 6.9. A finite family of arbitrary sets has a system of distinct representatives, meaning an injective choice , exactly when
Only the index family is finite; the sets themselves may be infinite.
The demand criterion characterizes feasibility entirely in terms of the original compatibility graph and the requested multiplicities. Its necessity identifies an obstruction to any assignment, while its sufficiency asserts that no other obstruction exists. The deficit theorem gives a quantitative statement when complete coverage is unavailable. The regular case gives a distinct consequence for graphs described through their degrees, rather than through a separately supplied collection of neighborhood inequalities. These are the respective contents of Exercises 6.3 and 6.5 and Proposition 6.4.
Mathlib already provides finite-family and graph versions of Hall's theorem in its Hall development and graph interface. The source-aligned development therefore reuses established infrastructure. Its additional work consists of connecting exact graph degrees and edge counts to the source statements, retaining the deficit and zero-demand cases, and supplying an arbitrary-set representatives interface. Local proofs of the five theorem statements have been checked in Lean 4.29.0-rc3 with Mathlib 777aaa6.
Independent local choices do not guarantee a matching: different choices can collide at one resource. Replacing distinct selections by nonnegative real allocations would change the conclusion. Counting total demand alone also misses obstructions carried by proper subsets of recipients.
Several representation issues matter even after the mathematics is known. A left-saturating matching need not be perfect. A subgraph's vertex set may omit isolated ambient vertices. Cardinality conventions for infinite sets can turn a superficially plausible formula into a different assertion. Finally, a theorem that assumes all neighborhood inequalities has not established those inequalities merely because a graph is regular. The individual interfaces must distinguish these obligations rather than hide them inside a definition.
The graph results use finite vertex types and native SimpleGraph and Subgraph objects. Both disjointness and coverage of the bipartition are explicit. Local-finiteness instances supply finite neighbor enumerations; they impose no further restriction on finite graphs. The complete-matching predicate combines the native matching condition with inclusion of the prescribed vertex set.
Degrees in the capstone are cardinalities of finite subgraph neighbor sets. The deficit conclusion counts unordered subgraph edges. Natural subtraction is truncated at zero, an equivalent convention for these nonnegative cardinality lower bounds. Empty graphs, empty index families, and zero demands remain admissible. In the representatives theorem, arbitrary sets are measured by extended cardinality; infinity is never replaced by zero.
The reusable outputs are the source-aligned graph statements, the complete-matching interface, the prescribed-degree equivalence, and the arbitrary-set representatives criterion. Equivalent proofs and clearer reusable interfaces are within scope. Placeholder conclusions, extra assumptions that exclude the difficult cases, and fractional substitutes for the integral capstone are not.
Ramsey theory asks for the smallest number such that every graph on vertices contains either a clique of size or an independent set of size . Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is exactly the distinction between a graph and its complement, and their growth controls constructions used in derandomization and in the theory of Boolean functions.
This mission formalizes the paper that started the probabilistic method as a systematic tool: Erdős's 1947 proof that . It is also the natural companion to the platform's Sipser–Gács–Lautemann mission: the union-bound argument formalized here is the same counting technique that drives the Lautemann lemma used to place in .
Timeline. Ramsey proved in 1928 that is finite; Erdős and Szekeres gave the first upper bounds in 1935; Erdős's 1947 paper supplied the exponential lower bound by a one-page counting argument, introducing the probabilistic method. Better constants for specific regimes followed (Lovász local lemma 1975, Spencer 1977), but no general lower bound beyond is known today.
Fix an integer and put . A graph is a pair with an irreflexive symmetric relation on ; here vertices are labeled . A subset of size is a clique if every two distinct vertices of are adjacent, and an independent set if every two distinct vertices of are non-adjacent. A -set that is either a clique or an independent set is monochromatic: it is monochromatic in the two-coloring of the complete graph on in which an edge is colored by the graph (present) or its complement (absent).
The ambient probability space is the uniform distribution over all graphs on labeled vertices — equivalently, each of the possible edges is present independently with probability . This space has exactly elements.
A graph with no monochromatic -set is a graph with neither a -clique nor an independent -set. The mission's goal, "the Ramsey number satisfies ", is formalized as the bare existence of such a graph on vertices, without defining the Ramsey number itself.
i.e. there exists a graph on labeled vertices that contains no monochromatic -set.
The goal follows by combining the three steps: the pair count is the sum over bad events in the union-bound principle, and the count estimate makes that sum smaller than the graphs.
The result. The lower bound is exponential, matching (up to the constant in the exponent) the best known upper bound from Erdős–Szekeres. It shows that the Ramsey function, despite being finite, grows genuinely fast — and the proof's method became more influential than the bound: the probabilistic method now permeates combinatorics, graph theory, and theoretical computer science (random graphs, discrepancy, property testing, derandomization).
Formalizing it. Mathlib currently contains no Ramsey theory at all: no definition of a Ramsey number and no lower bound. This mission closes that gap with the foundational result, in a way that is deliberately elementary — no measure theory, no randomness: the "probabilistic" argument is re-expressed as exact counting, which is why the statements are fully formalizable in Mathlib today. The union-bound principle (target 2) is a reusable lemma for future probabilistic-method formalizations, and the monochromatic-set infrastructure (targets 1 and 3) is the natural base layer for a future definition of the Ramsey number .
The central difficulty is that the bad events — "the -set is monochromatic" — overlap heavily: a typical graph contains many monochromatic -sets, so the union bound must be crude enough to survive the overlap. Concretely, the estimate holds for but fails for ; the naive "take one vertex more" step is where the argument breaks. A solver who tries to strengthen the bound will find the exponent is tight.
A second difficulty is purely formal: the uniform distribution over graphs has to be eliminated. The mission's statements do this by counting graphs with a fixed monochromatic -set ( of them) and applying the union-bound principle, so no probability theory enters the formalization.
Representation. Graphs are SimpleGraph (Fin N): a relation on labeled vertices. A candidate set is a Finset (Fin N) of cardinality ; "monochromatic" is IsClique ∨ IsIndepSet on the graph; "no monochromatic -set" is the predicate NoMonoK. All counting is cardinality of finite sets; monoCount N k G is the number of monochromatic -sets of .
Conventions. uses natural-number division, so for odd the graph lives on vertices — the standard reading of . The hypothesis is explicit. The theorem quantifies existence over all graphs; it does not define the Ramsey number (a definition item for it, with the re-stated bound , is a natural follow-up contribution).
Reusability. The union-bound principle, the monochromatic--set machinery, and the pair-count bound are all reusable beyond this mission. Welcome contributions: defining ramseyNumber and restating the bound as ; the Erdős–Szekeres upper bound as a companion mission; applications of the same principle elsewhere.
This mission is not a duplicate of existing platform content, and the choice of target is deliberate:
0df444a) contains no Ramsey-number theory at all — nothing in Combinatorics/SimpleGraph, no ramseyNumber-style definition. This mission seeds that subfield with reusable infrastructure: the monochromatic-set model, the finite union-bound (probabilistic-method) principle, and the double-counting bound are all general-purpose lemmas, not one-off steps.Erdos183 mission concerns multicolour triangle Ramsey numbers and is driven by recursive palette constructions — a different Ramsey parameter and a different technique. The classical 2-colour diagonal bound formalized here appears nowhere on the platform as a proved statement.0df444a) asks, eventually in , for ; its upper half is already proved as ramsey_theory_upper_bound. The lower half is exactly what this mission's goal supplies: once ramsey_lower_bound is proved, closing that open problem reduces to a translation between the graph formulation used here (SimpleGraph / NoMonoK) and the edge-colouring formulation (ramseyDiag) used there, plus the eventual-quantifier wrapper.Around 1637 Pierre de Fermat wrote, in the margin of his copy of Diophantus' Arithmetica, that no -th power with splits as a sum of two like powers, and that he had a proof the margin was too narrow to hold. The claim resisted every generation of number theorists that attacked it, and the machinery built during those attacks — cyclotomic fields, ideal theory, class numbers, elliptic curves, modular forms, Galois representations — became a large part of modern algebraic number theory. The statement itself is elementary enough to explain to a schoolchild; nothing about its proof is.
Timeline. Fermat himself proved the case by infinite descent, as a corollary of the fact that the area of a right triangle with integer sides is never a perfect square. Euler treated in his Vollständige Anleitung zur Algebra (1770), by a descent in that assumed a unique-factorization property later supplied by others. Dirichlet and Legendre settled between 1825 and 1830, Dirichlet added in 1832, and Lamé published in 1839. In 1847 Kummer made the decisive structural step: introducing ideal numbers to repair the failure of unique factorization in , he proved the theorem for every regular prime exponent — those not dividing the class number of , a condition he characterized by divisibility of Bernoulli numerators. Irregular primes were left open, and the elementary programme stalled there for over a century.
The route that closed the problem came from a different direction. The modularity conjecture of Taniyama (1955), refined by Shimura and given conceptual support by Weil (1967), predicted that every elliptic curve over arises from a modular form. Hellegouarch and then Frey (1985) attached to a hypothetical solution the curve , whose ramification behaviour is too tame for a curve of its conductor. Serre made this precise as the epsilon conjecture, and Ribet proved it in 1986: modularity of semistable elliptic curves over implies Fermat's Last Theorem. Wiles proved that modularity statement, with the key Hecke-algebra input supplied jointly with Taylor, in two 1995 Annals of Mathematics papers. Breuil, Conrad, Diamond and Taylor removed the semistability hypothesis in 2001.
Fix a natural number and natural numbers . A Fermat triple of exponent is a triple of strictly positive naturals with
For such triples are everywhere, and for they are the Pythagorean triples, parametrized by . The assertion at issue is that from upward there are none at all: the hypothesis and the positivity hypotheses , , are exactly what is needed, since and the degenerate triples with a zero entry both produce solutions.
Two standard reductions organize any attack. First, if is a triple of exponent and , then is a triple of exponent ; since every is divisible by or by an odd prime , the general statement follows from the cases and an odd prime. Second, for a prime exponent one may assume , and the classical literature then splits on whether (case I) or (case II).
This is the mission's single goal, referenced as the published platform theorem fermat_last_theorem. It fixes no exponent, no congruence class, and no auxiliary structure: any complete argument, classical or modern, discharges it.
The result itself. As a Diophantine statement, Fermat's Last Theorem is a closed case; its value now lies in what proving it required. The proof established the modularity of semistable elliptic curves over , made modularity lifting ("") a standard technique, and turned Galois deformation theory into a working tool. Those consequences — not the non-existence of Fermat triples — are what the surrounding mathematics uses daily; the Fermat statement is the compact certificate that the machinery works.
Formalizing it. The theorem is proved but not formally verified end to end, and that gap is the mission. Machine-checked proofs exist for the small exponents and for Kummer's regular-prime case: Mathlib carries the general statement together with the cases and , and the flt-regular project verified the regular-prime theorem in Lean 4. No formal proof of the full theorem exists in any system; Buzzard's ongoing FLT project at Imperial College is building one by reducing the statement to results known to experts by the late 1980s. Contributions here need not follow that route — a complete Lean proof of any single case not yet covered, or of any structural ingredient (level lowering, modularity lifting, the properties of the Frey curve), is a genuine advance, and the platform's sketch mechanism is the natural way to record such a reduction.
The naive attacks fail for identifiable reasons, and a solver should rule them out before spending time on them. Congruence and descent arguments of the kind that settle depend on the arithmetic of a specific small ring and do not generalize: the descent step needs unique factorization in or a substitute, and unique factorization fails there for all but finitely many . Kummer's ideal-theoretic repair recovers the argument exactly when is regular, and no argument in that family is known to handle irregular primes; the irregular primes are moreover infinite in number, so no finite computation closes them. Parity, size, and modular-arithmetic obstructions have all been shown insufficient, since the equation has solutions modulo every prime power for suitable triples. The only known complete proof passes through modularity, which means the formal development needs elliptic curves over , their Galois representations, modular forms and Hecke algebras, level-lowering, and a modularity lifting theorem — none of which is a shortcut around the difficulty, all of which is where the difficulty actually lives.
The target is stated over , so no truncated subtraction enters the statement and no sign analysis is hidden in it; the equivalent formulations over and over follow by clearing denominators and moving terms, and a solver who prefers to work over must supply that bridge. Exponentiation is Monoid.npow on , and plays no role because . The hypotheses , , are all load-bearing and none of them is vacuous, so the statement admits no trivializing reading: dropping any one makes it false, and every hypothesis is satisfiable, so the conclusion cannot be reached by contradiction from the assumptions alone. Mathlib does not contain Fermat's Last Theorem, so the goal cannot be discharged by citing a library lemma.
A complete development will want: the reduction from general to and odd prime exponents; the coprimality normalization; cyclotomic fields, class groups, and the regularity criterion for the Kummer line of attack; and, for the modular route, Weierstrass curves over , conductors and minimal models, Galois representations attached to torsion points, modular forms and Hecke operators, and the level-lowering and modularity-lifting statements. Most of that infrastructure is reusable well beyond this mission and is welcome as separate published theorems and definitions. Partial contributions are welcome in either style: a direct proof of a single exponent, or a sketch that reduces the goal to child lemmas with statements that stand on their own.
flt-regular), Lean 4 formalization. https://github.com/leanprover-community/flt-regularFor a square matrix A over a commutative semiring, subtraction and determinant arguments are generally unavailable. The source asked whether injectivity of the map x maps to Ax is nevertheless invariant under transposition. The case n=2 was known, with n=3 presented as the first open size.
This mission turns CUHK-Shenzhen AI Math Problem 20, Transpose symmetry for injectivity over semirings, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
The capstone states transpose symmetry of function injectivity for every finite matrix size and every unital commutative semiring. In the current Prove2Me snapshot both the general theorem and the dimension-two supporting theorem are published and marked Proved. This mission concerns a resolved result, not an open general declaration. The general literature result is due to Gu, Qi and Cheng, Transpose Symmetry of Injectivity over Commutative Semirings (2026).
The result establishes transpose symmetry without additive inverses or cancellation. The current formal artifacts already record the finite-dimensional statement over arbitrary unital commutative semirings; users should inspect those exact statements and proof records before selecting extensions. The literature status and formal proof status are both resolved for the linked targets.
Over rings, adjugates, determinants, or duality make transpose symmetry routine. Over semirings, equality of alternating sums cannot be rearranged by subtraction, additive cancellation need not hold, and linear duals do not reflect injectivity. The successful proof must encode parity-separated minors and use injectivity itself to cancel vectors rather than scalars.
This mission is historical and solved in the literature. A Prove2Me solution can reconstruct the paper's proof with independently authored Lean code: isolate the even/odd minor algebra, verify the top separation identity, descend through matrix sizes, and derive coefficient equality. Generalizations to nonunital semirings and the parallel surjectivity theorem are natural follow-up nodes, provided their exact hypotheses match the paper.
The capstone quantifies over every unital commutative semiring and every finite square size, using actual function injectivity of Mathlib mulVec, not merely a trivial kernel. The extra sizes zero, one and two do not weaken the original size-at-least-three question. Both linked theorem items are now Proved on Prove2Me. This update does not copy or redistribute any external repository source, and does not change the published Lean statements or proof identities.
The linked dimension-two theorem is Proved. The general goal is also Proved. Any further generalization, such as a nonunital version or a surjectivity statement, would be a separately stated theorem rather than an unfinished part of either existing item.
The source problem was added July 4, 2026. Sixuan Gu, Wei Qi, and Yaoyu Cheng posted a general proof on August 17, 2026, together with a Lean formalization. The mission records that rapid resolution rather than presenting the theorem as currently unknown.
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
Dynamic programming is the backbone of stochastic optimal control, operations research, and reinforcement learning. Its cornerstone — that the backward recursion of Bellman computes the optimal cost of a finite-horizon stochastic control problem — is stated as Proposition 1.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., Athena Scientific, 2005), the standard graduate text on the subject. Every convergence result for value iteration, every performance bound for approximate DP, and every correctness proof for a planning algorithm ultimately leans on this proposition. A machine-checked version of it — over a clean, reusable model of the basic problem — is the natural foundation stone for formalized control theory and RL theory alike.
The basic problem (§1.2 of the book): a discrete-time system
with state , control constrained to a finite nonempty set , and disturbance drawn from a finite space with conditional probabilities . A policy is a sequence of feedback maps ; it is admissible if everywhere. Its expected cost from is
In the Lean development these are BertsekasDPModel, BertsekasDPPolicyCost (backward recursion on remaining stages), and the DP recursion BertsekasDPValue:
Section 1.6 of the book develops the minimax variant, where the disturbance is chosen antagonistically from a finite membership set ; the mission mirrors it with BertsekasMinimaxDPModel, BertsekasMinimaxPolicyCost, BertsekasMinimaxValue.
formalized as BertsekasDP.dp_algorithm_optimality: the DP value at the horizon is an IsLeast of the set of admissible policy costs. Milestones: the min–max interchange Lemma 1.6.1 (minimax_selection_interchange) and the minimax DP validity (minimax_dp_algorithm).
The proposition itself is the license to compute optimal policies stage by stage; downstream, Missions VI and VII of this series (lookahead bounds, infinite-horizon theory) consume exactly this model and recursion. Formalizing it produces the reusable model of the basic problem — the shared vocabulary for the whole series. The result is classical and proved in the book; the contribution here is a machine-checked proof over a model faithful to the book's, with the measurable-selection subtleties deliberately avoided by finiteness (see scope).
The proof is a backward induction, but the standard informal argument ("interchange expectation and minimization") must be carried out honestly: the induction hypothesis is about all states simultaneously, the minimizing control must be selected as a function of the state (choice over a finite set), and the policy-cost recursion must be related to the value recursion stage by stage. The minimax milestone needs the interchange lemma with its proviso — the classic trap is losing that hypothesis and asserting a false unconditioned interchange.
Finite disturbance space (Fintype W), finite nonempty control-constraint sets (Finset, inf'), arbitrary (possibly infinite) state space; expectations are finite weighted sums, probabilities are required to be distributions only at admissible controls. Stage data are total functions on ; only stages matter. Policies are deterministic Markov feedback maps — for this class the book's result is exactly recovered. The trivializing risks (empty constraint sets, junk beyond horizon) are ruled out by the nonemptiness field and by evaluating at exactly remaining stages. Lemma 1.6.1 is stated in the extended reals over arbitrary types with the book's finiteness-of-infimum proviso.
Restless multi-armed bandits are the standard model for allocating a scarce resource across many independently-evolving agents: N arms, each a small Markov chain, and a budget that lets you activate only a fixed fraction of them at each step. The joint problem is PSPACE-hard, so practice runs on index policies — score each arm by a priority index computed from its own local state, then activate the top ones until the budget runs out — and evaluates them by value decomposition: approximate the joint Q-function by a sum of per-arm local Q-functions, each computed from a single arm's chain. The decomposition is used everywhere from Whittle-index heuristics to modern multi-agent RL, and it is used without an error bound.
Chen and Peng (arXiv:2506.02385) supply one. Their companion mission established the general principle: the value decomposition error of a multi-agent chain is controlled by its measure of Markov entanglement, the distance from the chain's transition matrix to the nearest separable one. This mission carries that principle to the restless-bandit setting and proves that index policies are asymptotically separable — their entanglement decays like 1/sqrt(N), so the decomposition error is sublinear in N while the joint Q-function itself is of order N. The relative error vanishes as the system grows, which is exactly why the practice works.
The argument runs through the mean-field limit. Because the arms are homogeneous, the only thing that matters about a joint state is its configuration: the fraction of arms in each local state. Under an index policy the configuration evolves by a map that does not depend on N at all, and under two standard technical conditions — a uniform global attractor property and non-degeneracy — that map has a unique attracting fixed point m*. The chain of reasoning is: policy entanglement is bounded by how far the realised policy sits from the mean-field limiting policy (Proposition 1); that distance is bounded by the configuration's deviation from m* (Lemma 2/8); and the deviation concentrates at rate 1/sqrt(N) by a concentration-plus-local-stability argument adapted from Gast, Gaujal and Yan. The concentration and stability inputs (Lemmas 9, 10, 11) are results of Gast et al. and are formalized here as well, so the mission stands on its own.
The mission also formalizes the mean-field map on the whole simplex and checks it against the N-agent characterisation, which is what makes the piecewise-affine and stability analysis expressible at all.
The classical persistence problem asks which invariant tori of an integrable Hamiltonian survive a small perturbation. A resonance makes some internal angular frequencies vanish, and an almost-periodic perturbation introduces infinitely many additional forcing frequencies. Zhang, Si, and Si state a Poincaré–Treshchev persistence theorem for this combined regime: most lower-dimensional resonant tori associated with nondegenerate relative equilibria persist as infinite-dimensional invariant tori in Theorem 2.7. The formal mission targets that headline result in corrected form. It retains the paper’s nonresonance, spatial-shell, and averaged-critical-point hypotheses, while making explicit the full frequency twist and reduced-frequency parameter chart used later in the paper but absent from the printed theorem statement.
Let and . The internal variables are and , where is bounded and closed. The external forcing angles and their conjugate actions are and . The suspended Hamiltonian is
Here is real analytic near . A primitive rank- resonance lattice is represented by an integer matrix with , where the last columns generate the lattice. The adapted angles are , with and . Writing for the actual derivative of , define
The averaged potential is the zero external and zero Fourier coefficient of at . A pair is associated and nondegenerate when
Let be the subset of admitting such a , let , and trim in reduced-frequency coordinates:
The perturbation has the paper’s spatial-shell Fourier expansion over finite shells in a spatial structure . With for , each shell has a uniform analytic Fourier bound , and for some . Every nonzero admissible finite external mode satisfies
where , is the minimum shell weight containing its support, and is a nondecreasing approximation function with , , and .
Assume that is nonempty. On every sufficiently small trim , require compactness and positive -dimensional measure in the chart, injectivity of , an analytic lower-Lipschitz diffeomorphism , and nondegeneracy of every averaged critical point retained by the conclusion. Then, for every , there are , a rate as , and closed measurable nonempty sets for such that
For every and every associated nondegenerate , construct a topological embedding
that is analytic almost periodic with the same shell structure, is the image of the standard resonant torus under a local canonical transformation, is -close to that torus, and is invariant under with rotation vector .
The result combines three features that are usually separated: a positive-rank internal resonance, an infinite external frequency vector, and persistence for an asymptotically full-measure parameter set. It identifies the surviving object in the full suspended phase, including the external actions, rather than only in the finite internal fibre. The paper contains a proof of its printed theorem; the mission’s open work is a Lean proof of the corrected target. The correction exposes the parameter twist and chart assumptions on which the reduction and measure assertion depend, so a completed formalization would distinguish the theorem’s stated content from hypotheses needed to make that content mathematically controlled.
Finite-dimensional Diophantine notation does not control infinitely many external modes: admissibility, support weights, and the decay of must interact without leaving an empty mode class. Resonance also removes internal frequencies and replaces the original parameter set by a lower-dimensional surface. Its ambient Euclidean boundary is therefore unsuitable for a positive trim, and ordinary ambient volume is unsuitable for the majority statement. Finally, persistence must be expressed simultaneously as an invariant solution of the actual Hamilton equations, an analytic almost-periodic embedding, and a canonical equivalence in the suspended phase; any one of these conditions alone admits objects that do not express the theorem.
The Lean representation uses finitely supported integer external modes, a covering spatial structure, the literal shell-indexed norm, complex-neighborhood coefficient analyticity, and a separate absolute-summability guard for every infinite Fourier sum. Unit modes are provably admissible. The averaged potential, its gradient and Hessian, the internal frequency , the resonant set, and the reduced-frequency map are transparent definitions. Nonemptiness of , positive volume of every allowed , and nonempty rule out empty-set and zero-measure trivializations.
The formal target strengthens the printed assumptions only where the source’s reduction requires missing control: is injective on the retained trim, and is an analytic diffeomorphism there with a uniform lower Lipschitz bound. The boundary distance and excluded volume are both taken in the -dimensional reduced-frequency chart. The word “Cantor” is represented by closedness, measurability, nonemptiness, and asymptotically full measure; perfectness and total disconnectedness are not additional targets.
The torus lives in a genuine external-action space. Its action component has one weighted--valued shell expansion, and the Hamiltonian pairing and external action velocity carry convergence guards. A local conjugacy is a homeomorphism between open neighborhoods, fixes , is differentiable along all action directions and finitely supported external-angle directions, and preserves on those cylinder directions. Reusable contributions include spatial-shell Fourier classes, approximation functions, reduced-manifold measure interfaces, weighted infinite canonical forms, and coordinatewise Hamiltonian invariance.
The conjugate-gradient method in Luenberger's Chapter 10 is one of the most enduring consequences of Hilbert-space geometry in numerical optimization. For a bounded self-adjoint coercive operator, it solves the quadratic first-order equation Q x = b using only operator applications, inner products, and a short recurrence. Luenberger develops the method from steepest descent and conjugate directions, then proves convergence in a general real Hilbert space rather than only for finite matrices. This mission formalizes that full setting. It also repairs a practical omission in the printed recursion: division formulas are undefined after exact convergence, so the formal algorithm explicitly stops and stutters once its search direction is zero.
Let H be a complete real inner-product space and Q : H →L[ℝ] H a bounded self-adjoint operator. Constants m and M satisfy 0 < m ≤ M and
for every x. The first inequality is coercivity; together with self-adjointness it supplies the positive Q-energy. For a right-hand side b and initial point x₀, the initial residual and direction are both b - Q x₀. A conjugate-gradient state records the current iterate, residual, and direction. If the direction is nonzero, the next state uses Luenberger's alpha and beta ratios. If the direction is zero, conjugateGradientStep returns the same state, so every natural-number iterate is total and all denominators occur only on the active branch.
The root theorem VectorSpaceOpt.conjugate_gradient_converges states that there is a unique xStar satisfying Q xStar = b and that the iterate component of the guarded conjugate-gradient state tends to xStar in norm. Four milestones provide reusable structure. coercive_selfadjoint_bijective establishes existence and uniqueness for Q x = b from bounded self-adjoint coercivity. conjugate_directions_converge formalizes §10.6, Theorem 1: a complete sequence of nonzero pairwise Q-orthogonal directions produces residuals orthogonal to every earlier direction and iterates converging to the solution. cg_directions_conjugate_until_stop records the §10.8 invariants only before the explicit stopping time. cg_energy_contraction captures the uniform energy reduction factor derived from the bounds m and M.
The total algorithm is represented by conjugateGradientIterate, and its error functional is
These definitions are proposed as mission-owned reusable objects in the shared VectorSpaceOpt namespace.
The mission gives a coordinate-free verification target for an algorithm usually presented through arrays and matrices. Its theorem applies directly to finite-dimensional symmetric positive-definite systems but also retains Luenberger's infinite-dimensional perspective. The guarded recursion is suitable for later executable specializations and makes exact termination a first-class semantic event. The coercivity and conjugate-directions milestones can be reused for Galerkin methods, preconditioned variants, and other Krylov algorithms, while the energy estimate provides a natural connection to condition-number convergence rates.
Unlike a matrix-only formalization, the Hilbert-space theorem cleanly separates the geometric reason for convergence from any storage representation. It therefore complements Mathlib's existing operator and orthogonality libraries and can serve as a specification against which finite implementations are later verified. It also preserves the book's unifying theme: optimization algorithms arise from the geometry of carefully chosen inner products rather than from coordinate manipulation alone.
The difficulty is medium to high. Algebraic invariants of the three-term recurrence involve several interacting orthogonality relations and require strict control of nonzero denominators. Infinite-dimensional convergence additionally uses density of the closed span of directions and comparison of the Q-energy with the ambient norm. The theorem must move between self-adjoint continuous linear maps, scalar inner products, filters on sequences, and function iteration. Exact termination creates a case split that informal accounts routinely ignore; the formal statement must show that the zero-direction branch is stable and already represents the solution.
The proposal follows §10.6 and §10.8, pp. 291–296, and uses Chapter 10, Problem 10 on p. 309 for the coercive-invertibility dependency. All assumptions on Q, m, and M that §10.8 inherits from the preceding sections are repeated explicitly. The conjugate-directions milestone explicitly assumes every direction is nonzero and that the closed span of the directions is the whole Hilbert space. The conjugate-gradient invariants are asserted only for iterations before a zero direction occurs. Once it occurs, the state stutters by definition; the proposal never relies on Lean's totalized value for 0 / 0.
Luenberger's §10.7, Theorem 1 is not included as a literal milestone. As printed, its orthogonalization-of-moments statement omits self-adjointness of the auxiliary operator relative to the Q inner product and omits the linear-independence/nonbreakdown conditions needed to keep denominators nonzero. The mission instead isolates the Q-conjugacy invariant directly from §10.8. It does not claim finite-dimensional termination within dim H steps, floating-point stability, preconditioning, a sharp Chebyshev condition-number rate, or computability of equality tests on arbitrary Hilbert spaces.
Quadratic exterior penalties in Luenberger's §10.11 replace a constrained problem by a sequence of unconstrained minimizations. The method is simple enough to state in a few lines, yet Luenberger's convergence theorem is strikingly general: no convexity, differentiability, or convergence of the full minimizer sequence is required. If penalty weights increase to infinity and a subsequence of exact penalty minimizers converges, lower semicontinuity alone makes its limit feasible and optimal. This mission isolates that robust primal convergence result as a tractable companion to the more analytic conjugate-gradient and optimal-control missions. It offers a clean formalization target with direct relevance to nonlinear programming and approximation schemes.
Let X be a topological space, f : X → ℝ, and G : X → (Fin p → ℝ). Feasibility means G x i ≤ 0 for every component. Define the positive part componentwise and the squared violation by
For a positive weight K, the penalty objective is f x + K * v x. A sequence K n is positive, nondecreasing, and tends to +∞. The constrained problem is assumed to have a minimizer xStar, and for each n an exact global minimizer x n of the corresponding penalty objective is supplied. A limit point is represented explicitly by a strictly increasing index map phi for which x ∘ phi tends to x₀.
The root VectorSpaceOpt.quadratic_penalty_cluster_point_converges formalizes §10.11, Theorem 1. Assuming lower semicontinuity of f and v, it concludes that every stated subsequential limit x₀ is feasible, has the same objective value as xStar, and globally minimizes f over the feasible set.
Three milestones split the exact source content into reusable statements. quadratic_penalty_basic_estimates is §10.11, Lemma 1: the attained penalty values are nondecreasing, are bounded above by f xStar, and the stronger weighted violation K n * v (x n) tends to zero. penalty_cluster_point_feasible combines convergence of violations with lower semicontinuity at a subsequential limit to recover all component inequalities. penalty_cluster_point_optimal combines lower semicontinuity of f, the uniform upper bound f (x n) ≤ f xStar, feasibility of the limit, and optimality of xStar to identify the limiting objective value and global constrained optimality.
The theorem captures the essential consistency guarantee behind one of the most widely used constraint-handling methods. Its assumptions separate optimization existence from convergence: minimizers of each auxiliary problem and at least one cluster point are assumed, while the theorem identifies what any such cluster point must be. The componentwise positive-part and violation definitions are reusable for augmented Lagrangians, exact penalties, barrier comparisons, and finite inequality systems. The basic-estimates lemma is particularly useful because it requires neither topology nor continuity and exposes a quantitative fact stronger than mere feasibility residual convergence.
Because the proof target is stated over an arbitrary topological space, the mission also clarifies which parts of penalty convergence are genuinely metric and which depend only on order, finite nonnegative sums, and lower semicontinuity. This abstraction is faithful to the source's vector-space viewpoint.
The mission has moderate difficulty and relatively low infrastructure risk. The main analytic interfaces are lower semicontinuity along a convergent subsequence and real filter convergence to both zero and infinity. The basic estimates require reasoning simultaneously about minimizers for changing objectives, monotonicity of the weights, and the asymptotic product K n * v (x n). The cluster-point theorem must extract componentwise feasibility from a finite sum of nonnegative squares without assuming continuity of G. Lean's IsMinOn does not itself assert membership in the feasible set, so feasibility of the known constrained minimizer is included separately rather than hidden in prose.
The proposal covers the primal part of §10.11: Lemma 1 on p. 305 and Theorem 1 on p. 306. It makes “limit point” precise through a strictly monotone subsequence, avoiding any assumption that the full sequence converges. The weight sequence may have repeated values because the source only needs it to be nondecreasing, but every weight is positive and the sequence tends to atTop. Lower semicontinuity is required for f and the composite violation v, exactly as in the book; continuity or componentwise lower semicontinuity of G is not substituted. Existence of xStar and of every penalty minimizer is assumed rather than derived from compactness or coercivity.
The mission does not include §10.11, Lemma 2 or Theorem 2 on dual multipliers. Those results add convexity and continuity assumptions and naturally require careful treatment of an extended-real dual functional. It also does not address approximate minimizers, rates, boundedness of the sequence, existence of cluster points, equality constraints beyond their encoding as paired inequalities, or finite exactness. Keeping those extensions separate preserves the unusually weak hypotheses and clear conclusion of the cited primal theorem.
Fin-indexed vectors, subsequences, global minima on sets, and filter convergence).