Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Chapter 9 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) develops the differential calculus of mappings . The definition of the derivative changes character: it is no longer a number but a linear transformation , the one that approximates the increment of to first order. Once that is in place, the chapter proves the two theorems that make nonlinear analysis possible: the inverse function theorem (Theorem 9.24), which says that a continuously differentiable map with invertible derivative at a point is locally invertible with a continuously differentiable inverse, and the implicit function theorem (9.28), which solves locally for in terms of .
The message of both is that a nonlinear map behaves locally like its linearization, provided that linearization is invertible and varies continuously.
This mission is the ninth in a series formalizing Rudin Chapters 1–11; it uses the completeness and compactness results of Missions II and IV and the mean value estimates of Mission V, and it prepares the change-of-variables machinery used in Mission X.
is the space of linear maps with the operator norm . A map defined on an open is differentiable at with derivative if
and — a -mapping — if it is differentiable on and is continuous. The partial derivative is the derivative of at . A map of a metric space into itself is a contraction if for some .
Let be a -mapping of an open into and suppose is invertible at some . Then there are open sets and such that
The inverse function theorem is the local classification statement of differential calculus: it says that the only local obstruction to invertibility is degeneracy of the derivative, and it is the mechanism behind coordinate changes, the rank theorem (9.32), and the change-of-variables formula for integrals in Chapter 10. The implicit function theorem is its standard reformulation and is what makes level sets of smooth maps into manifolds. Theorem 9.21 is the practical criterion for the hypothesis, since it reduces it to continuity of finitely many partial derivatives; Theorem 9.41 shows that the symmetry of second derivatives, though intuitive, requires a hypothesis; Theorem 9.19 is the several-variable substitute for the mean value theorem, whose equality form already failed in Chapter 5.
Mathlib has the Fréchet derivative, the inverse and implicit function theorems for Banach spaces, the Banach fixed-point theorem, and symmetry of second derivatives. This mission states the Rudin versions concretely in — with the explicit open sets and and the inverse mapping produced as data, rather than through a bundled local homeomorphism — and so provides a bridge between the book's formulations and the library's.
The inverse function theorem is the first theorem in the book whose proof combines several chapters at once: the contraction principle (9.23) gives local surjectivity by solving as a fixed point of ; openness of the set of invertible operators (9.8) keeps the derivative invertible near ; the mean value inequality (9.19) controls the error; and the continuity of inversion gives the regularity of . The delicate point is that all estimates must hold uniformly on a neighbourhood chosen in advance, so the order in which the neighbourhoods are shrunk matters.
For Theorem 9.41 the trap is the hypothesis: continuity of at the single point is assumed, not continuity of both mixed partials on a neighbourhood; the conclusion is existence of at that point, and it genuinely fails without some such hypothesis.
Conventions fixed by this mission:
EuclideanSpace ℝ (Fin n); linear maps are →L[ℝ] (continuous linear
maps), which in finite dimension is the same as Rudin's , with
the operator norm.HasFDerivAt, and the condition is ContDiffOn ℝ 1.HasDerivAt of the line restriction
t ↦ f (x + t • eⱼ) at t = 0, avoiding any coordinate-projection bookkeeping;
eⱼ = EuclideanSpace.single j 1.Function.Bijective, which for a continuous linear map
between finite-dimensional spaces is equivalent to the existence of a continuous linear
inverse.inv constrained on the invertible
operators, so that continuity of inversion can be stated without bundling.D1f, D2f, D21f, which
is how Rudin states the hypotheses, and the conclusion asserts existence of D₁₂f at the
point as a HasDerivAt statement.α increasing and φ(·,t) ∈ ℛ(α).Packing congruent circles into a square is a classical problem in discrete geometry: for each natural number , choose a common radius as large as possible while keeping all disks inside the square and preventing overlap. Every exact value requires two logically distinct achievements: an explicit configuration attaining the proposed radius and a proof that no configuration can do better.
The character of those proofs changes sharply with . The first cases admit short geometric arguments; later cases use contact-graph analysis, specialized case divisions, or computer-assisted global optimization with interval arithmetic. Formalizing the resulting constants therefore provides a growing benchmark for extremal geometry, real algebra, finite configurations, and verified computation in Lean.
This is an open-ended formalization mission. It begins with the exact constants currently represented by theorem-backed milestones, but it is not restricted to a fixed terminal value of . Further milestones may be added whenever an exact packing value and its rigorous optimality argument are identified and stated precisely enough for formalization.
A point is a pair of real coordinates. For points and , squared Euclidean distance is
For a real radius , a point lies in the inner square when both coordinates belong to the closed interval . This is exactly the coordinate condition saying that a closed disk of radius , centered at that point, is contained in the unit square.
The predicate requires and a family of centers in the inner square such that the squared distance between every two distinctly indexed centers is at least . Equality is allowed, so tangent disks are admitted. Radius zero is also admitted.
Define
and define the optimal covered-area fraction by
It is often convenient to use the equivalent point-separation constant , the greatest possible minimum pairwise distance among points in the unit square. The conversion is
The Lean definitions use a supremum rather than assuming in advance that an optimal packing is attained.
The mission currently contains theorem-backed milestones for the following values:
| Exact separation or area value | Proof character in the supplied notes | |
|---|---|---|
| , hence | diagonal bound | |
| minimum enclosing square of a triangle | ||
| , hence | convex hull and perimeter | |
| four-cell pigeonhole argument | ||
| case-specific geometric proof | ||
| hand proof and later computer verification | ||
| case-specific geometric proof | ||
| , hence | classical geometric proof | |
| , hence | theoretical grid-optimality proof | |
| , hence | theoretical grid-optimality proof | |
| , hence | theoretical grid-optimality proof |
For rows stated using , the corresponding milestone for uses the conversion formula above. The equalities are claims about the supremum-defined packing constants, not merely about the displayed candidate configurations.
The milestone list is intended to grow. The supplied survey notes classify and as rigorously solved in the cited literature, while distinguishing and as not rigorously closed in the cited 2021 account. Many of the computer-assisted cases do not have a simple radical expression in the supplied notes. Before such a case is linked to a Lean theorem, its primary source must provide a precise candidate value, algebraic characterization, certified enclosure, or optimal-configuration certificate that can be stated faithfully.
A new milestone should identify:
Numerical evidence and strong bounds are valuable, but they must be labeled as bounds rather than exact-value milestones. Conversely, newly published exact results for larger may be added without changing the underlying definitions.
Every exact-value milestone must connect the proposed value to Packable, r_n, and c_n. Constructing a configuration establishes only a lower bound. An upper-bound argument without attainability also does not establish equality. A complete proof must bridge both directions through the supremum definition.
The proof methods may include:
Shortcuts that redefine , , or to equal a desired answer are excluded. The constants must remain consequences of the common geometric model.
The root theorem CirclePackingConstants.c_all is the conjunction of the eleven exact-value milestones currently in the mission, covering . Its proof sketch reduces the root directly to those milestone theorems, so the mission remains open until every current exact value is proved.
The milestone theorems remain separately reusable and independently auditable. When further exact values are added, a successor aggregate theorem can extend the conjunction and become the new root without replacing the shared definitions or invalidating earlier results.
This structure allows elementary cases, historical hand proofs, and computer-assisted certificates to progress independently while remaining part of one cumulative library of exact circle-packing constants.
The Lean model uses ℝ × ℝ for points and an explicit coordinate formula for squared Euclidean distance. Disk containment is represented by inclusive coordinate inequalities. Nonoverlap is represented by a weak squared-distance inequality, so tangency is permitted. The indexing type is Fin n, and the definitions apply to every natural number, including zero.
The definition bundle contains only Point, sqDist, InInnerSquare, Packable, r_n, and c_n. Solvers may introduce normalization maps, separation bounds, explicit configurations, supremum lemmas, contact structures, certificate checkers, and radical or polynomial identities as auxiliary declarations.
A strongly regular graph with parameters is a finite simple graph on vertices in which every vertex has exactly neighbours, every pair of adjacent vertices has exactly common neighbours, and every pair of non-adjacent vertices has exactly common neighbours. For most parameter tuples the elementary counting and integrality conditions already decide existence; the interesting cases are those that survive every known feasibility test and still resist construction. The tuple is the smallest such case in the family , , and its existence has been open for more than fifty years. John Horton Conway offered $1000 for a resolution, as one of five problems posed at the 2014 DIMACS conference on Challenges of Identifying Integer Sequences (Conway, Five $1,000 Problems (Update 2017)).
Timeline of the problem and of what is known about it:
No graph with these parameters has been found, and no non-existence proof is known.
Fix a finite vertex set and a simple graph on (irreflexive, symmetric adjacency ). For vertices write for the neighbourhood of and for the set of common neighbours. The graph is strongly regular with parameters , written , when
The case says that every edge lies in exactly one triangle — equivalently, the neighbourhood of each vertex induces a perfect matching, so such graphs are locally linear. The case says that every non-adjacent pair is the pair of opposite corners of exactly one -cycle. Conway's problem asks for with these two local conditions.
Counting paths of length two from a fixed vertex gives , which for , reduces to ; with this yields . Writing for the adjacency matrix, for the identity and for the all-ones matrix, strong regularity is equivalent to the matrix identity , which for reads ; the eigenvalues of other than are then and , and integrality of their multiplicities ( and ) is one of the feasibility conditions that passes.
The goal is Mathlib's own proof_wanted conway_99 in Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean, stated verbatim: existence of a finite type carrying a strongly regular graph with parameters . A resolution in either direction is welcome — a proof settles the existence half, and a proof of the negation settles the non-existence half; the platform records the two as proof and disproof of the same statement.
for every strongly regular graph with , : the counting identity, local linearity, and the integrality restriction that cuts the family down to five non-degenerate parameter tuples.
the two members of the family that are known to exist: the rook's graph (the Paley graph on vertices) and the Berlekamp–van Lint–Seidel graph.
structural consequences for a hypothetical -graph, the last one being Wilbrink's theorem.
A graph, if it exists, is a locally linear graph of maximal density in its parameter range and a partial linear space of girth with points and lines of size ; its existence would also produce new association schemes and new examples for the general classification of strongly regular graphs. A non-existence proof would be the first case in this family ruled out by anything other than the classical feasibility conditions, and would say something new about how far local conditions (, ) constrain global structure.
Nothing in this mission is presently formalized. Mathlib defines SimpleGraph.IsSRGWith, proves the counting identity IsSRGWith.param_eq, the complement rule IsSRGWith.compl, and the matrix identity IsSRGWith.matrix_eq, and records the -graph problem as a proof_wanted. The supporting targets are of three kinds: results that are proved in the literature and only need formalizing (existence at and ; Wilbrink's non-vertex-transitivity; the integrality restriction on ); routine consequences that supply reusable infrastructure (edge and triangle counts, the spectral identity, evenness of ); and the goal itself, which is open mathematics.
The obvious approaches fail for concrete reasons. Exhaustive search is out of range: the graph has edges among pairs, and no isomorph-free generation of locally linear graphs on vertices is feasible. Algebraic constructions are blocked by Wilbrink's theorem — the graph cannot be vertex-transitive, so it is not a Cayley graph and cannot be produced by the group-theoretic constructions that yield most known strongly regular graphs, including the two that work at and . On the non-existence side, every classical feasibility test (the counting identity, integrality of the eigenvalue multiplicities, the Krein conditions, the absolute bound) is passed by , so a proof of non-existence needs an argument that does not factor through the parameters alone.
All statements are phrased with Mathlib's SimpleGraph.IsSRGWith on a Fintype vertex type with DecidableRel adjacency, and use Fintype.card, SimpleGraph.edgeFinset, SimpleGraph.cliqueFinset 3 (triangles as -cliques), SimpleGraph.adjMatrix over , and graph isomorphisms g ≃g g for automorphisms. The goal quantifies over α : Type together with a Fintype α instance, so the vertex set is finite by construction and the empty type does not satisfy the cardinality clause; the statement is therefore not vacuously satisfiable. Note that Mathlib's definition constrains only through pairs that are actually adjacent and only through pairs that are actually distinct and non-adjacent, so degenerate small graphs (the one-vertex graph, ) do satisfy IsSRGWith with , ; the supporting statements carry the cardinality hypotheses (, ) that exclude them where needed, and the degenerate degree is listed explicitly in the classification of feasible degrees.
Infrastructure a complete development needs, and which is reusable beyond this mission: interface lemmas for counting common neighbours in a strongly regular graph; the spectral theory of the adjacency matrix (multiplicities of the two non-principal eigenvalues, and their integrality), which is the missing ingredient for the classification of feasible degrees; a Lean construction of the perfect ternary Golay code and its coset graph, for the case; and decision procedures for strong regularity of an explicitly given small graph, for the case. Contributions to any of these are welcome, as are partial non-existence results (for instance, restrictions on automorphisms of prime order) submitted as separate statements.
Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.
Fix vectors with Euclidean norm . A sign vector is an : one sign per vector. Writing for the -th coordinate of the vector , the discrepancy of the family under is the largest coordinate, in absolute value, of the signed sum — that is, , the norm of the signed sum. The Komlós property at constant — KomlosBound K — says that every such family, in every and every , admits a sign vector with every coordinate of the signed sum at most in absolute value.
Set systems embed as the special case of -incidence matrices: if is an matrix of s and s in which every column has at most ones (every element lies in at most sets), the columns scaled by have norm at most one, so the Komlós property gives discrepancy — the Beck–Fiala conjecture.
The goal fixes no value of : any finite universal constant settles it, so the statement survives every improvement in the constant.
Eight results over the same definitions: Beck–Fiala's for degree- set systems; Spencer's for sets on points; Banaszczyk's for the Komlós setting; its corollary for set systems; the reduction "Komlós at implies Beck–Fiala at "; Kunisky's lower bound ; and the two 2025 Bansal–Jiang breakthroughs — for the Komlós setting, and the Beck–Fiala conjecture's bound in the regime .
The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.
None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.
Random signs lose: they give , not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least — so any proof must handle instances strictly harder than the set-system case.
The Lean model commits to: vectors as EuclideanSpace ℝ (Fin m), whose norm is the norm (the hypothesis reads ‖v i‖ ≤ 1); the conclusion written coordinatewise as ∀ j, |∑ i, ε i * v i j| ≤ K, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with ε i = 1 ∨ ε i = -1; and set systems as matrices A : Fin m → Fin n → ℝ with an entrywise hypothesis and column-degree counted by Set.ncard. Quantifier order matters everywhere: in KomlosBound K the constant is fixed before and — a depending on would make the statement the trivial bound. In beck_fiala the hypothesis is required (the degree- system has discrepancy otherwise); the Banaszczyk-form bounds use so that the bound is positive already at . In the Bansal–Jiang milestones the asymptotic and are rendered by existential constants quantified before all instances: the hidden factor becomes for some fixed (the inner shift keeps the iterated logarithm positive), and the threshold becomes for some fixed .
Welcome contributions: any milestone in any order — beck_fiala and komlos_implies_beck_fiala are self-contained finite arguments and the natural entry points; spencer_six_deviations and banaszczyk_bound each import a major technique; komlos_lower_bound needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.
Harmonic maps into singular nonpositively curved spaces arise in geometric analysis, rigidity theory, and the study of group actions on buildings. Near a point in the domain, their infinitesimal growth is measured by an order, obtained from an Almgren-type frequency quotient. For smooth targets that order is tied to familiar Taylor expansion data. Euclidean buildings are instead assembled from Euclidean apartments along reflection walls, so a map can branch through a singular link and a priori might exhibit a much less controlled spectrum of homogeneities. Breiner and Dees prove that, for maps from surfaces, this spectrum is discrete and is governed by the finite rotational Weyl group of the building. The mission formalizes their headline classification theorem, Theorem 1.1 of Breiner--Dees.
The discreteness matters because frequency information is a basic input to stratification and regularity arguments for singular harmonic maps. A finite list of possible denominators prevents homogeneities from accumulating arbitrarily and isolates rank-one behavior. The formal target makes explicit the nonconstant condition used by the source paper's tangent-map reduction. Without it, the usual numerator and denominator of the frequency quotient both vanish for a constant map, so its order is not defined.
A Euclidean Coxeter complex consists of Euclidean space together with an affine reflection group. Taking the linear parts of its affine isometries produces a finite rotational reflection group . A Euclidean building of type is a complete metric space covered by isometric Euclidean apartments whose overlaps are related by elements of the affine Weyl group; the atlas is required to contain the relevant geodesic segments, rays, and lines and to be maximal with these compatibility properties.
The domain is a connected open subset of a complex one-dimensional manifold, hence a Riemann surface domain. The formalization uses a concrete Korevaar--Schoen-style metric Sobolev energy built from normalized local difference quotients and Lebesgue area in charts. A map is harmonic when it has finite local energy and minimizes that energy against competitors with the same trace. For and small radii , the energy and boundary moment determine a frequency quotient. When its limit exists with positive denominator, that limit is the order .
For a nonconstant energy-minimizing harmonic map and any , prove that the order is defined and that there are positive integers such that
If the building has rank one, prove the sharper form
The same theorem also records the small-scale energy and positive-boundary-moment facts needed for the order to be meaningful; these are conclusions, not assumptions supplied by a solver.
The result identifies a purely algebraic constraint on an analytic singularity invariant: every denominator divides the order of the finite rotational Weyl group. In rank one, where the target is a tree or an -tree, it recovers the half-integer spectrum and its lower bound. This converts an apparently continuous local invariant into a discrete one determined by the building type.
Formalizing the theorem requires reusable infrastructure that is largely absent from current Mathlib: concrete Euclidean-building atlases, metric-valued Sobolev energy, trace and boundary-moment constructions, harmonic energy minimization, frequency quotients, and homogeneous tangent-map interfaces. The paper theorem is proved in ordinary mathematics; the open task is to replace the single sorry in the target with a machine-checked Lean proof. A completed development would provide components useful for other singular-target harmonic-map and CAT(0) formalizations.
The target is not a direct consequence of treating the building as a Euclidean vector space. A harmonic map can cross apartment walls, and a single chart need not contain the image of a punctured neighborhood. The local problem must respect both metric energy and Weyl-group compatibility. Moreover, the frequency quotient is defined through limiting analytic quantities, while the conclusion is an exact rational arithmetic classification. Bridging those levels requires controlling tangent maps and the geometry of directions in the building rather than merely proving monotonicity of the frequency.
The rank-one clause is not obtained by substituting into the general statement alone: it also asserts . The formal proof therefore must preserve the nonconstant hypothesis and the positivity information that rules out the degenerate zero-order case.
The Lean bundle fixes a complex one-dimensional manifold model for the source, a genuine complete metric target, a finite affine reflection group acting by Euclidean isometries, and an explicit building atlas. The rotational group is the image of the affine group under taking linear parts, so is not an arbitrary external number. The domain carries a point and is nonempty by construction. The map is required to be nonconstant on the domain; this is the necessary explicit repair of the printed headline, whose later reduction theorem uses the same condition.
Energy, trace, boundary moment, frequency, and order are transparent definitions tied to the supplied geometry. In particular, the caller cannot choose a zero measure or an unrelated predicate to make the target vacuous. The theorem must establish finite small-scale energy, positivity of the boundary moment, existence of the frequency limit, and its classification. Solvers may contribute supporting files for metric Sobolev estimates, tangent-map compactness, homogeneous harmonic-map classification, or finite-reflection-group lemmas, provided they preserve the exact conventions in the definition bundle.
The oldest bandit algorithm (Thompson, 1933) is also the most modern: sample a parameter from the posterior and act greedily. Chapters 34–36 of Lattimore–Szepesvári develop the Bayesian view in two crowning results. The Gittins index theorem: for infinite-horizon discounted Markov bandits, the seemingly intractable dynamic program is solved exactly by an index policy — each arm gets a retirement-value index computable arm-by-arm, and playing the largest index is Bayesian optimal. And the frequentist analysis of Thompson sampling — the goal theorem: with Gaussian posteriors, Thompson sampling on 1-subgaussian bandits achieves , exactly asymptotically optimal, alongside the minimax-grade . Together they explain why posterior sampling is both principled and practically dominant.
Is the regret of LinUCB (Mission X) an artifact of the algorithm or a law of nature? Chapters 24–25 of Lattimore–Szepesvári prove it is essentially unimprovable. On the unit ball there is a parameter with forcing — the goal theorem — and the hypercube gives the same rate. The asymptotic chapter is more striking still: for fixed finite action sets, the instance-optimal constant is characterized by an allocation program, and optimism itself is provably suboptimal — LinUCB and Thompson sampling cannot achieve it, because exploration must sometimes deliberately play actions optimism would never touch. These lower bounds define the targets for the entire linear-bandit literature.
What if the rewards are not random at all, but chosen by an adversary who knows your algorithm? Remarkably, a randomized learner can still compete with the best fixed arm in hindsight. Chapters 11–12 of Lattimore–Szepesvári develop the adversarial -armed bandit: rewards are an arbitrary fixed matrix, the learner samples , and regret is measured against . The exponential-weights algorithm Exp3, fed by importance-weighted loss estimates , achieves — the goal theorem. The companion Exp3-IX, which deliberately biases its estimator, upgrades this to a bound holding with high probability rather than only in expectation. These results are the foundation of all adversarial online learning with partial feedback.
Many questions about polynomial equations — which equations can be solved by radicals, which geometric constructions are possible with ruler and compass, how the roots of a polynomial are related — become questions about the symmetries of a field extension. The fundamental theorem of Galois theory, going back to Évariste Galois, is the dictionary that makes this possible: for a finite Galois extension it matches intermediate fields with subgroups of a finite group, so that questions about fields become questions in finite group theory. The same dictionary underlies Kummer theory and class field theory, and it is the step that turns the unsolvability of the general quintic (Abel–Ruffini) into a statement about solvable groups.
This mission follows the Wikipedia article Fundamental theorem of Galois theory (revision 1345286594): its main statement, its list of properties of the correspondence, three of its worked examples, and its section on the infinite case.
A field extension is a field with a field inside it; it is finite when is finite-dimensional as an -vector space, of dimension . An intermediate field is a field with . The automorphism group is the group of field automorphisms of with for every .
The two maps of the correspondence are:
The extension is Galois when it is normal and separable; for a finite extension this is equivalent to . When is Galois, is written .
For an infinite algebraic Galois extension, carries the Krull topology: the coarsest topology for which each restriction map , with a finite Galois subextension and discrete, is continuous.
For a finite extension ,
The result. The correspondence turns the lattice of intermediate fields of a finite Galois extension into the (reversed) lattice of subgroups of a finite group, with degrees matching indices and normal subextensions matching normal subgroups. This is the tool used to classify subfields, to compute Galois groups of explicit polynomials, and to prove that solvability by radicals corresponds to solvability of the Galois group.
Formalizing it. The theorems are classical, and Mathlib contains formal proofs of the general finite and infinite correspondences (for example IsGalois.intermediateFieldEquivSubgroup and the InfiniteGalois namespace). This mission's contribution is a statement set indexed by the source: the converse direction ("only if Galois") as the goal, the non-Galois behaviour, each listed property, and the concrete examples of the article. The explicit examples require genuine computation: degrees of towers, minimal polynomials, and counting subgroups and subfields.
The general statements reduce to Artin's theorem and a degree count, but the non-Galois milestone asks for four separate claims about injectivity and surjectivity, each needing the correct direction of Artin's theorem. The examples cannot be settled by a general principle: showing that has exactly five intermediate fields, or that the splitting field of has degree , requires irreducibility arguments and an explicit transfer through the correspondence. Showing that has no non-trivial automorphism requires knowing that the other two roots of are not real.
All statements use Mathlib's IntermediateField F E, IntermediateField.fixedField, IntermediateField.fixingSubgroup, the automorphism group E ≃ₐ[F] E, and IsGalois (normal and separable). Finite means FiniteDimensional F E. Subgroups in the finite statements range over all subgroups; in the infinite case the Krull topology is Mathlib's standard topology on E ≃ₐ[F] E. Degrees are Module.finrank, orders are Nat.card, and the index is Subgroup.index. The concrete fields of the examples are taken inside (for and , with the real cube root) or as the abstract splitting field (for ). The quotient milestone takes the normality of and of as instance hypotheses; they are equivalent by milestone 5, so neither is vacuous.
The article's Example 3 (the anharmonic group acting on ) and the "Applications" section are out of scope for this first mission. No new definitions are needed; contributions of proofs for any milestone are welcome.
Line search methods for unconstrained minimization of a smooth function choose a direction and a step and set . Classical rules (Armijo, Wolfe) insist that every step decrease . For quasi-Newton and conjugate gradient directions this monotonicity requirement often forces short steps, and nonmonotone line searches, which only ask for a decrease relative to some reference value built from past iterates, have been used since Grippo, Lampariello and Lucidi (1986) to let such methods take longer steps.
Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum of recent function values used by Grippo et al. with a weighted average of all past function values. The paper proves two results: global convergence to stationary points (the companion mission) and, the subject of this mission, R-linear convergence of the function values when is strongly convex.
Timeline:
Fix parameters , and . Write and . The Nonmonotone Line Search Algorithm (NLSA) keeps weights and reference values :
with chosen freely at each step. A step is accepted either by the nonmonotone Wolfe conditions
or by the nonmonotone Armijo rule , where is a trial step and is the largest integer such that the first inequality holds and . With one recovers the monotone rules.
The direction assumption asks for constants with and . The function is strongly convex with constant if
Let be the minimizer, , , and the set of points within distance of .
Let be strongly convex with minimizer , let be Lipschitz continuous on bounded sets, let , let the directions satisfy the direction assumption at every iteration, and let for all . Then there is with
The goal fixes no value of : it asserts only the existence of a linear rate.
In the paper's order of use:
Here is a Lipschitz constant of on . A further result on the same definitions is Theorem 3.2: if converges R-linearly with ratio inside a compact convex set on which is strongly convex, then the sufficient decrease condition with reference value holds for all large .
Theorem 3.1 shows that averaging past function values costs nothing in the rate: on strongly convex functions the nonmonotone method keeps the linear rate of monotone descent, for any direction sequence satisfying the direction assumption (steepest descent, L-BFGS with bounded condition numbers, and so on). Theorem 3.2 is the converse side: for weights close enough to 1, the averaged test eventually accepts the steps of any R-linearly convergent iteration of this kind. The paper contrasts this with the max-based test of Grippo et al.
These results are proved in the paper. As far as the platform catalogue shows, no line search with the Wolfe conditions or a nonmonotone reference value has been formalized. The only related item is a monotone backtracking gradient descent rate, which is a different theorem. Machine-checked proofs would give reusable Lean statements of the nonmonotone Wolfe and Armijo rules and of the averaged reference value. They would also give the explicit constants , and in checked form, and a checked record of the repair of the printed statement described below.
The obvious argument would show that contracts at each step. It fails: the method is nonmonotone, and may exceed . The quantity that contracts is , and only is controlled by the line search. The contraction must be derived by relating to in two regimes, and the second regime needs a bound on from the gradient at the previous iterate. That bound requires the Lipschitz constant on a region containing every point the line search examines, which is why the region and the step bound enter. In Lean, the sufficient decrease (3.6) also rests on the step-length lower bounds of Lemma 2.1 for both rules, including the integer-exponent Armijo rule with its maximality condition.
Conventions:
EuclideanSpace ℝ (Fin n), is ContDiff ℝ 1, and is ⟪gradient f x, d⟫_ℝ.IsGreatest.Repair of the printed statement: the paper's direction assumption holds only for all sufficiently large , but Theorem 3.1 concludes (3.5) for each , and its proof uses the assumption at every . As printed the theorem is false: with the Wolfe step gives , which violates (3.5) at whenever . The goal therefore requires the direction assumption for every .
The step bound "there exists with " is stated with the algorithm's parameter. For the Armijo rule this holds by construction. The Wolfe rule does not use , so nothing is lost.
Trivializing formalizations are ruled out:
A complete development needs:
The NLSA definitions are reusable by any later mission on nonmonotone line searches. Proofs of the milestones in any order are welcome, as are a proof of the counterexample to the printed statement and a proof that the platform theorem ConvexOptimization.strong_convexity_quadratic_lower_bound implies (3.4).
In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first rounds.
The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.
Fix a dimension and an unknown parameter . In round the learner is given a nonempty decision set , chooses , and observes the reward
There is a filtration such that is -measurable and is -measurable and conditionally -sub-Gaussian: for all , with fixed.
For a regularization parameter let and let be the regularized least-squares estimate. With and a known bound , the confidence ellipsoid is
The OFUL algorithm chooses, in round , a pair maximizing over . The pseudo-regret is , where .
If , for all , and , then for every , with probability at least ,
For any positive definite , and : with probability at least , for all ,
With probability at least , for all (first claim). If , then with probability at least , for all , (second claim, stated here for ).
Theorem 3 bounds the regret of OFUL by with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.
All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases , , of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.
The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix , which is itself built from the adaptively chosen actions; a bound for each fixed does not give it.
Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed for , so sums over are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy ) requires; this is an added hypothesis. Every "with probability at least , for all " is stated as an outer-measure bound on the failure event, with the time quantifier inside the event. is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.
OFUL is a predicate on the whole process: in every round the chosen pair maximizes over , with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward is the supremum over , finite because of the reward bound.
Two corrections to the printed Theorem 3 are made and disclosed. The printed is replaced by , which is what the determinant–trace bound gives; for the corrected bound implies the printed one. The hypothesis is added: for the printed logarithm can be negative, and the printed bound would then assert . In the second claim of Theorem 2, is added, because at the claim does not follow from the first claim and the paper's proof is not available.
The goal is a probability bound over the noise, not the pathwise statement "if for all then ". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same as the conclusion.
Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on , log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general and , and reusable determinant lemmas are all welcome.
Matroids and their integral generalizations, integral base polytopes, are the combinatorial structures on which the greedy algorithm is exact. Edmonds' theory relates them to submodular and supermodular set functions: a polytope is a base polytope exactly when its support function, restricted to vectors, is supermodular and the greedy formula evaluates it everywhere. Dress and Wenzel's valuated matroids (1990) and Murota's M-concave functions carry the exchange axiom from sets to functions on sets. This paper (Adv. Math. 124, 1996) sets up the resulting theory of discrete concave functions on base sets, later developed into discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003).
The question behind this mission is how the set-level correspondence between exchange and supermodularity extends to functions. Section 5 of the paper answers it with the Local Supermodularity Theorem: the exchange property of a function is a supermodularity property of its concave conjugate, holding locally at every point.
Let be a finite nonempty set, . For let be the unit vector, for let be its characteristic vector, , and . For a finite , is its convex hull.
A finite integral base set is a finite nonempty such that
A function satisfies the exchange property (EXC) (is M-concave) if for and there is with and . Write and for the maximizers of on .
The support function of is . A positively homogeneous is "matroidal" if
The concave conjugate is , the concave closure is , the subdifferential is , and the localization of at is .
For on a finite integral base set ,
The printed Theorem 5.3 has only the second condition on the right. Its "only if" direction holds as printed; its "if" direction is false without the first condition, and a separate item of the mission states the counterexample: , .
The result. Theorem 5.3 is the function-level version of Theorem 5.1. Condition (C1) is a supermodularity condition, so the theorem expresses (EXC) as "a collection of local supermodularity" properties of , in the same way that (B1) corresponds to supermodularity of a support function. In the paper this characterization of the conjugate side underlies the Fenchel-type duality of Section 6, and more generally the conjugacy between M-concave and L-convex functions in discrete convex analysis.
The formalization. No part of this theory is formalized in Lean or on this platform: base sets, (EXC), "matroidal" functions and concave conjugates of functions on base sets are all new. The mission also corrects the published statement: the reduction from localizations to base sets needs every integer point of to be a maximizer, and the concave-closure condition supplies this. A machine-checked proof would settle both the corrected theorem and the counterexample. Theorem 2.1 and Lemma 5.2 are classical but have no formal proof either.
depends only on the concave closure , so any characterization of (EXC) through alone cannot see values of below . That is why the goal needs the extra clause. The "only if" direction needs the full theory of Section 4: M-concave functions coincide with their concave closure, and all their maximizer sets are base sets. Theorem 5.1 needs the greedy algorithm on integral base polytopes, together with the fact that the base polytope of an integral supermodular function has integral vertices. Theorem 2.1 is the folklore statement that polyhedral and exchange descriptions agree, and the paper does not prove it. Eq. (5.12) needs the subdifferential of a finite minimum of affine functions to be the convex hull of the active gradients, stated globally rather than only near .
Integer vectors are V → ℤ, real vectors V → ℝ, with [Fintype V] [DecidableEq V] [Nonempty V]. A finite subset of is a Finset (V → ℤ). A function on is a total function (V → ℤ) → ℝ whose values off are never used. The mission commits to the following readings:
sInf over the subdifferential, defined by (5.8)–(5.9) exactly, not by the formula (5.12). Eq. (5.12) is stated with IsLeast, so it asserts attainment, not just the value.Fin n ≃ V along which is non-increasing. This is equivalent to "for some" such indexing. "Matroidal" includes positive homogeneity but not concavity.Trivializing formalizations are ruled out. Defining by (5.12) would reduce the goal to Theorems 4.4 and 5.1. A "matroidal" without (C2) would be satisfied by support functions of non-base sets. An taken as a supremum would reverse the sign conventions.
The development needs: the greedy algorithm and integrality for integral base polytopes, supergradients of polyhedral concave functions, and the Section 4 results of the paper (concave closure of M-concave functions, Lemma 4.3). The base-set and "matroidal" layers can be reused beyond this mission. Proofs of any milestone, of the counterexample, and a proof of the "only if" direction on its own are all welcome.
A cooperative game with transferable utility assigns to every coalition of players the total payoff the coalition can secure on its own. Two solution concepts for such games go back to the foundations of game theory: the core, the set of payoff divisions no coalition can improve upon, and the stable set (von Neumann–Morgenstern solution), a set of divisions that is internally consistent and externally absorbing under the relation of domination. For general games the two concepts behave badly: the core may be empty, stable sets may fail to exist (Lucas 1968), and when they exist there are usually many of them.
Lloyd Shapley's paper Cores of Convex Games (Int. J. Game Theory 1, 1971) isolates a class of games, the convex games (supermodular characteristic functions), on which all of this becomes well behaved. Convex games arise in cost allocation, in bankruptcy and airport problems, in scheduling and sequencing games, and in any setting with increasing returns to cooperation; the supermodular functions behind them are the same objects studied as polymatroid rank functions in combinatorial optimization (Edmonds 1970). For such games the paper shows that the core is nonempty, that its faces fit together in a rigid combinatorial pattern, that its vertices are exactly the marginal-contribution vectors, and that the core is the unique stable set.
Let be a finite set of players. A game is a function from subsets of to the reals with . It is convex if
A payoff vector is , and . It is feasible if . The core is the set of feasible with for every ; in particular on .
For a nonempty coalition , the face is the set of core points with ; by convention , and . The family is the core configuration. It is complete if no is empty, and regular if and
For an ordering of the players, is the set of the first players, and the marginal vector pays each player its marginal contribution .
A payoff vector is dominated by if some nonempty coalition has and for all . A set of feasible vectors is stable if every feasible vector is either a member of or dominated by a member of , but not both.
The goal contains both halves of the page's statement: stability of the core, and uniqueness ("the unique von Neumann–Morgenstern solution").
The mission also states Theorem 3 (p. 19), the vertices of a regular core are exactly the marginal vectors , as a further item that is not on the path to the goal.
The result. Theorem 8 gives, for a natural and widely occurring class of games, a complete answer to the existence and uniqueness questions for von Neumann–Morgenstern solutions, which are open or negative in general. Theorems 3 and 5 describe the core of a convex game explicitly as the polytope spanned by the marginal vectors, the combinatorial description that underlies later work on the Shapley value, the Weber set, and the polymatroid greedy algorithm. Theorem 5 is the geometric characterization of supermodularity through the face structure of the core.
Formalizing it. All results in this mission are proved in the paper; none has a machine-checked proof on the platform. Theorem 4 is already stated on the platform (as part of a statement that also puts every marginal vector and the Shapley value in the core) and enters the mission as an existing item. The remaining work is a formal development of face configurations of the core, of stable sets and domination, and of the passage from supermodularity to the geometry of the core. The definitions of stable set and domination are general and reusable for any transferable-utility game.
The internal half of stability is immediate from the definitions: a core point cannot be dominated by any vector satisfying a coalition constraint . Uniqueness also follows from two short observations. The substance is external stability: every feasible vector outside the core must be dominated by a core point, and the dominating vector has to be produced explicitly. The obvious attempt, raising the payoffs of one violated coalition and leaving the other coordinates of unchanged, does not in general produce a core point, and nothing in the definition of the core alone controls how the core meets the hyperplane of a given coalition; that control is what the face theory of §3 is about. For non-convex games the external half genuinely fails, so no argument that ignores convexity can succeed.
Players are Fin n (a relabelling of the paper's finite set ), a game is f : Finset (Fin n) → ℝ, payoff vectors are Fin n → ℝ, and is ∑ i ∈ S, a i. The existing platform definitions Supermodularity.Cooperative.IsConvexGame ( plus supermodularity on all subsets), Core, InitialCoalition and GreedyPayoff (the marginal vectors, orderings being permutations of Fin n) are reused; the reused Theorem 4 statement is Supermodularity.Cooperative.convex_game_core_and_shapley.
Conventions committed to:
IsConvexGame.Fin (m + 1).Set.extremePoints ℝ.A formalization in which the dominating coalition may be empty, in which regularity omits , or in which the goal asserts stability without uniqueness does not state the paper's theorem and is ruled out.
Welcome contributions: proofs of the milestones in any order, general lemmas about faces of polytopes cut out by set-function inequalities, and reusable API for domination and stable sets.
Call cube-free if no triple has all seven of , , , , , , inside . The triple is unconstrained, so a degenerate one counts. Write for the largest size of a cube-free subset.
The conjecture. for every .
This is Conjecture 5.1 of Jason Long and Adam Zsolt Wagner, The largest projective cube-free subsets of , arXiv:1810.01225. It has been open since October 2018, and a 2026 journal paper still names it as conjectured: Yuchen Meng, On Cube-Free Problems, Electron. J. Combin. 33(1) (2026) #P1.16.
The bound is sharp, and the extremal set is explicit: , the odd residues together with those congruent to 4 mod 8. Its size is . In the layer language of Long and Wagner this is .
The conjecture holds for unions of layers. That is Long-Wagner Theorem 1.10 at , and it is the largest class on which the conjectured constant is proved.
For arbitrary sets the best published unconditional bound is . Meng calls this bound "quite trivial" and gives it in one paragraph for every cyclic group, so it should not be read as progress toward . The residual gap is exactly , that is elements.
Small values are , , , , , , , matching from on.
State those values honestly. They come from solver searches, Gurobi in Long and Wagner for and an independent SAT reproduction. The SAT half that matters, the unsatisfiability of "a cube-free set of size 81 exists at ", is a solver claim with no proof certificate checked and no kernel check behind it. The witness half is verified: a set of exactly 80 elements was produced and re-checked cube-free. So is solid and is not certified. Nothing in this mission rests on either.
The goal item is the conjecture itself, for , and it is open. Every other item is a milestone that is proved mathematics, and the two closed instances and are stated separately because they are the only cases of the goal that a proof assistant has actually settled here.
The chain runs: the base case mod 8 by exhaustion, monotonicity under subsets, the bridge between the membership form and the Finset form of the forbidden configuration, sharpness, the odd-residue tight case, the layer-union theorem, the two-thirds bound, and then and .
Six definitions live in one definition item, Def_Z2nCubeFreeLayers: HasCube, CubeFree, config, ConfigFree, layerIdx and IsLayerUnion. layerIdx is written through the 2-adic valuation rather than through a congruence, because the congruence form leaves in no layer at all and needs the last layer special-cased.
CubeFree and ConfigFree are two encodings of the same condition and they are not definitionally equal, because config collapses duplicates on a degenerate triple. Their equivalence is a milestone rather than an assumption.
Euler's constant measures the gap between the harmonic numbers and the logarithm:
It appears wherever the harmonic series is compared against an integral, and it is the value at of the digamma function, , equivalently . Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown.
For and the arithmetic questions were settled long ago: both are irrational and transcendental. For , neither is known. It is not known whether is irrational, and a fortiori not whether it is transcendental, though it is universally expected to be both.
The goal theorem of this mission is transcendence,
with irrationality carried as a separate, weaker target — a proof of transcendence yields irrationality immediately, but not conversely, and irrationality alone would already be a landmark.
Progress has come in three forms, and the milestones below formalize each.
Conditional bounds on a putative denominator. If were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing to places by an algorithm built on modified Bessel functions, showed any denominator exceeds ; a continued-fraction analysis by Papanikolaou (1997) pushed this past . These are not steps toward a proof so much as a measurement of how far brute computation can go.
Disjunctive results. The strongest unconditional statements pair with the Euler–Gompertz constant
Aptekarev, building on work of Mahler and Shidlovskii, observed that at least one of and is irrational. Rivoal later strengthened this to at least one of them is transcendental. Neither argument isolates which, and that is precisely the obstruction: the Padé-approximation machinery that controls the pair does not separate them.
Irrationality criteria. Sondow, adapting Beukers' treatment of Apéry's theorem for , gave criteria equivalent to the irrationality of in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it.
Mathlib provides the constant as Real.eulerMascheroniConstant, defined as the limit of , together with the identifications and and the numeric bounds . Irrational and Transcendental ℚ are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.
The Lagrange spectrum describes the asymptotic quality of rational approximation to irrational real numbers. The Markov spectrum is defined through minima of indefinite binary quadratic forms. Freiman determined the exact starting point of the maximal half-line contained in each spectrum.
This mission aims to formalize his theorem that this half-line is , where
The formalization must establish membership of every real number at least , including the endpoint, and show that no half-line starting below is contained in either spectrum.
The sources are Freiman's Russian monograph and an accompanying detailed reconstruction of its proof, with an English translation, exact computational certificates, and verification scripts. The project follows Freiman's continued fraction construction, incorporating the corrections and supplementary arguments established in the report.
The intended result is a complete Lean 4 proof. Its scope includes the equivalence of the classical and continued fraction definitions of the spectra, the infinite constructions that realize spectral values, and the exact finite calculations used in the argument.
Start with README.md and PROOF_GUIDE.md in the package. The files formalization/MISSION.md and formalization/MILESTONES.md describe the scope and proposed stages of the formalization. For reproducing the report, use the PDF and sources contained in the ZIP.
References to the report in the individual source fields use its printed page numbers.
A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is bounded.
Feghali, Lucke, Paulusma, and Ries answered that question negatively. Their conference paper appeared at ISAAC 2023, and the version of record was published in Algorithmica in 2025. The paper proves NP-completeness for bipartite graphs of arbitrarily prescribed girth and bounded maximum degree. A central input, Lemma 5, is a stronger structural existence statement: for every girth threshold there is an immune -regular bipartite graph of at least that girth, and it has a perfect matching.
This is therefore a ResearchPaper mission, not a new open-problem mission. Its goal is to formalize the published theorem and its graph-theoretic consequence. Repository candidate constructions and finite arithmetic audits remain separate and are not credited as solving the problem.
For a finite simple graph and a vertex set , the associated cut consists of all edges with one endpoint in and one in . The cut is nontrivial when both shores are nonempty. It is a matching cut when each vertex is incident with at most one crossing edge. A graph is called immune in the cited paper when it has no matching cut.
The girth is the length of a shortest simple cycle; forests have infinite girth. A graph is -regular when every vertex has exactly fourteen neighbors. Bipartiteness is witnessed by a partition into two independent sides. A perfect matching pairs every vertex with one adjacent partner.
The original OPG wording has a literal one-vertex boundary ambiguity: with nonempty shores required, has no matching cut, average degree zero, and infinite girth. The research-paper target avoids that vacuity by constructing connected graphs with at least two vertices, exact degree fourteen, and arbitrarily large finite girth.
The main theorem follows the paper's structural lemma:
The graph may depend on . The existence quantifier does not request an efficient algorithm or a numerical order bound.
A supporting theorem removes the perfect-matching and bipartite fields and records the direct substantive counterexample family:
Thus choosing refutes the intended universal assertion that some girth threshold works for every graph of average degree below .
The theorem shows that large girth and bounded degree do not force matching cuts. The examples are highly nontrivial: they are connected, regular, bipartite, and can have arbitrarily large girth. This separates local tree-like structure from the global expansion that prevents a matching cut.
Within the paper, the immune graphs serve as gadgets for hardness reductions. The journal theorem states that, for every , Matching Cut is NP-complete even for bipartite graphs of girth at least and maximum degree at most . Formalizing Lemma 5 supplies the graph-theoretic core needed to reconstruct that result without forcing this mission to formalize an entire complexity-theory reduction in its first stage.
Large girth alone makes bounded neighborhoods look like trees, and trees have many matching cuts. Immunity must therefore come from global expansion rather than short local cycles. The paper obtains the required family from Lubotzky–Phillips–Sarnak Ramanujan graphs and combines spectral and isoperimetric bounds to show that every nontrivial cut has too many crossing incidences to be a matching.
A formal proof must bridge several exact interfaces: existence of suitable primes, the finite Cayley-graph construction, bipartiteness and regularity, the girth lower bound, the spectral-to-isoperimetric inequality, and Hall's theorem for the perfect matching. None of these can be replaced by a finite sample or an asymptotic slogan.
Graphs are finite and simple. Connectedness is nonempty mutual graph reachability. A simple cycle is a cyclic list of at least three distinct vertices; girth at least means every such cycle has length at least , so forests satisfy every threshold. A matching cut requires both shores nonempty and is encoded by the condition that every vertex has at most one crossing neighbor. A perfect matching is represented by an adjacent involution.
The main theorem explicitly requires at least two vertices, although exact 14-regularity already forces nontrivial order; the redundant bound documents exclusion of the ambiguity. The mission does not claim that the frozen OPG contract was well-posed at order one. It formalizes the paper's substantive counterexample family and the consequence for the intended question.
Candidate files in the associated repository explore alternative bounded-degree constructions and integer counts. They are candidate_only and are not proof dependencies. Contributions should follow the published Lemma 5 and its cited inputs, or provide a separately sourced proof of the same declaration. The later maximum-degree-60 NP-completeness theorem is welcome as a future extension after the finite complexity framework is fixed.
A polynomial is split if and for some and . Split polynomials are the simplest non-constant maps defined over that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into .
Say is -collapsible if there are split with , collapsible if it is -collapsible, and eventually collapsible if it is -collapsible for some . Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree : Jordi Ribes settled the cubic case of eventual collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is . For the one-step notion the picture is different — degrees and are settled, and degree is open. That one-step cubic case is this mission's goal.
Let be an algebraic number with . After an affine change of variable over one may assume is a root of a depressed cubic
with discriminant . When the cubic is totally real (three real roots); when it has one real root and a complex-conjugate pair. In the latter case write the roots as
and set , the parameter that controls the archimedean obstruction below. Scaling sends , so the single rational invariant
determines the problem up to scaling: the search space is one rational parameter, not two.
This is the weakest statement that settles the case: it fixes no bound on , and asserts only that some split exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.
The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:
The mission also carries, as a plain theorem rather than a milestone, the single open instance — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.
A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree . A disproof would be at least as informative: a single cubic admitting no split with would separate -collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.
The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing , and it is what rules out a uniform-degree approach.
Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are not proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance and the goal itself are open.
The obvious approach is to write down a split with rational roots and force by solving for the roots. This works when is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.
Suppose and is split with . Irreducibility of forces to be divisible by , hence , hence . Each factor lies on a fixed circle through and determined by , and a convexity argument on then forces
As one has , so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For the bound already gives , which is why that cubic resists the searches that settle its neighbours.
Only one step of this argument is special to cubics: the identification of the circle parameter as . For an algebraic number of any degree with a real conjugate and a non-real conjugate , irreducibility gives the same relation , the images again lie on a circle through and , and the parameter is , which specialises to in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.
In the totally real case () the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of . Whether degrees stay bounded there is itself unsettled.
Representation. IsSplit f says and for a nonzero rational and a multiset of rationals; multiplicities are therefore allowed and the roots need not be distinct. Collapsible α is stated for in an arbitrary field carrying a -algebra structure, not only for , so the results apply verbatim to a root in , in , or in . The goal theorem is stated over , with "cubic" expressed as .
Ruling out a trivialisation. Collapsible places no lower bound on and does not require the value to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: would make , impossible for an irreducible cubic dividing a polynomial that splits over . Constant is excluded by . Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.
Conventions in the archimedean milestones. In the cubic bound the parameters enter as real numbers satisfying the factorisation identity, with the normalisation ; this is not a restriction, since is determined only up to sign and the sign may be chosen. Under it , and the conclusion is with the natural-number degree.
In the general bound the corresponding normalisation is . It forces , so is genuinely non-real and , hence and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when , which the hypothesis excludes and which cannot occur for a depressed cubic with . No degree hypothesis on is needed: possessing both a real and a non-real root already forces .
Infrastructure. A complete development needs Polynomial, Multiset, minpoly, and for the archimedean bound Real.arctan, Complex.arg, and strict concavity of on . The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of of any degree.
[VM-STATUS-20260908-R05-PROVED]
Status update (2026-09-08): The root theorem
OPG500Counterexample.eight_vertex_counterexampleis now Proved by an accepted Prove2Me submission. All six milestones are proved and the root has zero open leaves. The accepted proof has also been independently rebuilt with Lean 4.33.1 / Mathlib0df444a360eaa60ab8c11dca51a86af692955474. The historical text below describes the mission as it stood before formal closure.
Peripheral cycles occupy a distinguished place in structural graph theory. A cycle is peripheral when it is induced and does not separate the graph after its vertices are removed. Tutte proved in 1963 that the peripheral cycles of a finite 3-connected graph generate its binary cycle space. This theorem links a local, visibly embedded kind of cycle to the global algebraic structure of all cycles.
Weighted geodesic cycles provide a different generating family. Georgakopoulos and Sprüssel proved in 2009 that, for every finite graph with positive edge lengths, every cycle is a binary sum of weighted geodesic cycles whose lengths do not exceed the length of the original cycle. In the same paper they posed Problem 3: can the edges of every finite 3-connected graph be assigned positive lengths so that every weighted geodesic cycle is peripheral? A positive answer would recover Tutte's generation theorem through metric structure.
The present target tests the opposite possibility on one explicitly specified graph with eight vertices. A candidate argument and finite certificates are available in the frozen OPG-500 research repository, but those artifacts are explicitly marked candidate_only: they are neither a published counterexample nor a machine-checked resolution. The purpose of the formal target is to determine whether the proposed universal obstruction survives complete definition, proof, and statement-faithfulness checks.
Let be a finite simple graph. A positive edge-length assignment is a function
such that for every edge . The length of a finite path or cycle is the sum of the lengths of its edges.
A simple cycle is -geodesic when, for every pair of vertices on , at least one of the two – arcs of has length equal to the shortest-path distance between and in . Equivalently, there is no – path in whose length is strictly smaller than both – arcs of . The definition concerns vertices of the cycle and permits ties between shortest paths.
A simple cycle is peripheral when it is induced and deleting all of its vertices leaves a connected graph or the empty graph. This is vertex deletion, not edge deletion.
Fix the graph on vertices . The vertices induce . For each , set and join to exactly the three core vertices other than . The four vertices are pairwise nonadjacent. Thus the frozen edge set is
The labels and edge set are part of the statement and are not interchangeable with earlier candidate labelings without an explicit isomorphism.
Formalize the following statement for the fixed graph :
The existential cycle may depend on . The universal quantifier includes all strictly positive real assignments, including assignments with tied shortest paths. This is the stable target; finite samples and rational specializations are subordinate checks rather than replacements for it.
The development should also formalize the finite weighted geodesic-cycle generation theorem of Georgakopoulos and Sprüssel, the exact 3-connectivity and peripheral-cycle classification of , the required shortest-path and tight-subgraph statements, the finite cycle-space rank statements, and the finite minimum/descent principle used to select a cycle outside a closed binary span. These targets should remain separate declarations so that their assumptions and reuse boundaries are visible.
A proof of the main target would give a negative answer to the finite problem by exhibiting a 3-connected graph for which no positive edge weighting can make all geodesic cycles peripheral. It would not contradict Tutte's theorem: peripheral cycles may still generate the cycle space even though they cannot be made to contain every geodesic cycle for any weighting. The distinction between these two generation mechanisms is part of the mathematical content.
A formal development would add more than a checked final sentence. It would provide reusable definitions for positively weighted finite graphs and vertex-geodesic cycles, a precise treatment of the two arcs between cycle vertices, explicit deletion semantics for peripheral cycles, and finite cycle-space infrastructure. It would also separate purely finite graph facts from statements quantified over arbitrary real weights. The candidate repository currently supplies finite enumeration and abstract Lean fragments, but no existing artifact checks this full dependency chain.
Until the complete main theorem is verified, the eight-vertex graph remains a candidate obstruction and the original problem remains unresolved by this development.
The central difficulty is the universal quantification over real edge lengths. Testing many integer or rational vectors cannot cover it. Shortest paths need not be unique, so an argument that silently perturbs the weights or assumes unique geodesics can change which cycles are geodesic. Every strict and weak inequality must therefore agree with the source definition, including tie cases.
The graph is small but the semantic boundary is not. A formal cycle representation must expose the two cycle arcs for every vertex pair without admitting malformed or repeated-vertex objects. The peripheral predicate must combine inducedness with connectivity after vertex deletion and must classify all cycles, not only a selected family of triangles. Finally, finite cycle-space computations and rank inequalities must be connected to actual paths and weighted geodesicity; a propositional or enumerative certificate alone does not establish that bridge.
The Lean development will use Fin 8 for the vertices of and a SimpleGraph representation for adjacency. Weights will be functions on the edge subtype, so values on nonedges cannot affect the theorem. All weights are real and strictly positive. Paths and cycles are finite and simple; arbitrary walks do not count as target witnesses. Geodesicity is vertex-based and includes tied shortest paths. Peripheral cycles use inducedness and vertex deletion, with a connected-or-empty remainder.
The main theorem must retain the quantifier order “for every weighting, there exists a cycle.” It may not be weakened to rational weights, finitely many tested assignments, nonnegative weights, one selected weighting, edge-geodesicity, or the assertion that only four named core triangles fail to be peripheral. Definitions must be sorry-free, and nontrivial mathematical claims must be theorem declarations with separately checked proofs.
Reusable contributions include finite weighted-path length, shortest-path attainment in finite positive graphs, the equivalence of the two geodesic formulations, cycle-arc APIs, vertex-deletion connectivity, binary edge-vector encodings, and finite descent outside a closed span. Graph-specific finite certificates are welcome only when their checker is represented in Lean or their conclusions are otherwise proved in the kernel.
a41fe59b4535851ea55f6e868e938b9aaf81e924. https://github.com/vibemathing/problem-opg-500-geodesic-cycles/tree/a41fe59b4535851ea55f6e868e938b9aaf81e924The linear feasibility problem takes a matrix and a vector and asks whether the system of linear inequalities in real unknowns
has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.
What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time . In the real-number model the input is a list of exact real numbers, each arithmetic operation (), comparison, or memory move costs one unit, and a running time may only depend on and . An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every , , and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.
For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of but not on or , covering network flows and all -constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).
For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.
The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).
Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.
Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.
The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of ; no data-independent perturbation exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).
The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.
Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:
It fixes nothing about ; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.
Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of
from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.
Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound and the perturbation estimates, Khachiyan's theorem: for integer data bounded by , every admissible ellipsoid run decides feasibility within
The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on .
Level 3 — the goal (open). A uniform program with data-independent polynomial cost:
The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.
Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function would make the statement trivially true and is not the theorem. Division is totalized as and the branch test is ; both are benign for the class of programs quantified over.
The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.
A modular form has a complex L-function whose critical values carry arithmetic information. To compare those values in p-adic families, their transcendental period factors must first be removed. The remaining algebraic numbers can then be embedded into a p-adic field. The result sought here is a single bounded measure encoding the critical values of all twists by characters of p-power conductor. This is the existence and interpolation theorem underlying the cyclotomic p-adic L-function (one of the most fundamental objects of Iwasawa theory).
The reference is the famous paper of Mazur, Tate and Teitelbaum, Chapter I, especially §§10–14 (MTT); but for simplicity we are treating only the ordinary case here (not the more general finite-slope case), and not attacking the results later in MTT (exceptional-zero conjectures, etc).
Fix a prime , a positive integer , and a weight . Let be a normalized cuspidal Hecke eigenform of weight on with nebentypus and Fourier coefficients (necessarily algebraic). Fix embeddings and . No condition is imposed. The character is extended by zero on nonunits modulo .
The form is ordinary when . The ordinary root is the root of
with . This convention also covers the case: if , then and the unit root is (MTT I.§12).
A measure means a continuous -linear functional on the continuous functions . It is a bounded p-adic measure, rather than a positive real-valued measure. The Lean representation is Mathlib's AbstractMeasure on (PadicInt p)ˣ.
The two periods and normalize the signed modular integrals. Write
and use for sign . A period system specifies nonzero periods, algebraic normalized values for , and finite generation over of the lattice generated by these values. Period rationality and finite generation are separate mathematical obligations, combining Manin–Shimura rationality with the module-of-values construction in MTT I.§2; see also the explicit treatment of general eigenforms in Williams, §11.7.
The goal is to construct an ordinary root, a period system, and a measure with the following interpolation property. Let be a primitive Dirichlet character of conductor , where , and let . Put . With the positive-exponential Gauss sum , define the algebraic number by
The required identity is
where all algebraic character values in the following expression are transported by :
This is the scalar period-normalized form of MTT I.§14. At both character values at vanish, leaving . At the primitive character is the character of modulus one, and both Euler factors remain. The latter case is included explicitly.
Seven milestones isolate period rationality and its finite lattice; existence and uniqueness of the ordinary root; the distribution relation for polynomial disk moments; uniform boundedness of constant disk masses; unique extension to a measure with every critical polynomial moment; the complex Birch–Mellin identity; and the deduction of interpolation from the two signed measures. Their source locations are recorded individually. The period milestone combines two standard inputs; the boundedness and extension milestones specialize the MTT construction to slope zero.
The result supplies the analytic input for studying p-adic special values and their variation. It also supplies reusable infrastructure for normalized modular integrals, rational period systems, finite-order twists, and bounded measures on p-adic units. The classical existence theorem is known. The work proposed here is to prove the stated Lean theorems and connect the existing Mathlib analytic and algebraic infrastructure. Local compilation establishes that the declarations are well-typed; the mission statements remain unproved targets.
Listing algebraic critical values does not establish that one bounded measure interpolates them. Values on nested residue disks must satisfy compatibility, and ordinary boundedness must control the extension to continuous functions. Polynomial moments of positive degree must agree with that same extension. The unramified character requires its own Euler-factor calculation; simply applying the ramified formula at conductor one loses factors. On the complex side, rationality requires genuine periods of the modular form, not arbitrary chosen scaling constants. These are the obligations represented by the milestones.
The cusp form is Mathlib's analytic CuspForm, with Fourier coefficients tied to its width-one q-expansion. The nebentypus transformation law and every prime Hecke eigenvalue equation are written explicitly. The prime Hecke operator includes both its translated sum and its second term; when the prime divides the level, the second term vanishes. The complex twist is the finite-translate expression for , and its critical L-value is defined by the actual Mellin integral. Neither an arbitrary L-value table nor the desired measure is an input assumption.
The embeddings share the abstract algebraic closure of ; there is no asserted continuous map from to . The algebraic bridge in each interpolation identity is existential and constrained by a complex equality. Test functions are existential continuous maps constrained pointwise to equal the specified character or disk function; this makes their continuity part of the conclusion instead of an unproved definition. All primes, including , are allowed. Natural-number subtractions occur only in theorem contexts with and .
The signed projections use a factor of . Their normalized measures are added, and the period sign is . These conventions fix the powers, sign, Gauss sum, and periods in the displayed interpolation formula. Periods are not asserted to be canonical integral periods; rescaling by algebraic constants changes the normalization. Exceptional-zero derivative formulas, positive-slope distributions, tame-conductor twists, and Iwasawa main conjectures are outside this mission.
Adam McKenna closed this mission on 13 September 2026 following Unit distances in convex polygons, by Liam Kruer, Jensen Kohlmeyer, and Liam Price. Their construction gives strictly convex point sets with Ω(n log log n) unit-distance pairs and arbitrarily large minimum unit-distance degree, answering both questions and the general fixed-k version of Problem 97 negatively.
Paper and complete Lean source. All credit for the counterexample and its formalization belongs to those authors. Adam McKenna prepared the Prove2Me adapters.
Do not start further proof attempts or solver runs for the affirmative conjectures. Existing statements, conditional lemmas, partial proofs, and milestones remain as historical work. The owner has authorized closure assuming the external result is correct; individual theorem pages report Prove2Me verification status.
The mission is to prove the combined open goal
for finite point sets in strictly convex position in the Euclidean plane.
Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every nonempty convex-independent finite set then has a vertex with at most three neighbors at each positive radius, in particular at radius . Delete that vertex and preserve convex independence. Apply the same step to every subset created by deletion until no points remain. Charge each unordered unit-distance pair to the first endpoint deleted. Each deleted vertex receives at most three charges, so an -point set determines at most unordered unit-distance pairs. This gives the Problem 96 bound and therefore . The package uses this one-way dependency; it does not seek a reverse implication.
Let be finite. Strict convex position means that every point of is an extreme point of the convex hull of . For , the pinned multiplicity at radius counts points with . Problem 97 asks for a point where no radius has four such other points. Problem 96 counts unordered pairs at distance , then takes the supremum over convex-independent -point sets.
The historical progression is part of the setting. Erdős’s 1946 paper posed an earlier three-neighbor version. His 1987 account reports Danzer’s convex nonagon in which every vertex has three equidistant witnesses, and asks about four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex configuration with the same unit distance at every vertex, placing the local question beside the unit-distance problem.
The Problem 97 target is the canonical statement that every nonempty finite convex-independent has no four-equidistant-point property:
The Problem 96 target is the canonical asymptotic statement
where is the supremum of the unordered unit-distance counts determined by convex-independent -point sets. The bound is asymptotic; the Problem 97 route would give the stronger explicit bound for every natural number .
The package records a formal proof route joining a pinned geometric obstruction to a global extremal bound. A successful Problem 97 proof would immediately settle Problem 96 with the explicit constant , while preserving the combinatorial meaning of the count. It also separates the historical three-neighbor constructions from the still-open four-neighbor assertion.
The source proof reduces Problem 97 to strong induction on . Its counting engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib (2013). This engine forces every counterexample to have at least nine points; a finite geometric analysis excludes exactly nine points; and the remaining step must produce a removable vertex for every larger minimal counterexample. The removable-vertex statement carries the induction hypothesis that every strictly smaller nonempty convex 4-equidistant set is contradictory. That large-cardinality geometric step remains open, so both headline targets remain open. Finite computational certificates can support local cases but do not replace the universal geometric statement.
Problem 97 is open, so the mission also records the parallel negative route.
The source formalization calls a nonempty convex-independent
finite set with the four-equidistant property a
Problem97.IsCounterexample.
Constructing one such set would refute Problem 97 and therefore refute the
mission's affirmative conjunction, regardless of whether Problem 96 remains
true. The counterexample milestone keeps this resolution path visible beside
the nonexistence proof. A successful witness must use exact coordinates or
exact algebraic data from which Lean verifies both strict convex position and
the four-equidistant property; a numerical approximation or a realizable
incidence pattern alone is insufficient.
Problem 96 has its own negative route. Because its claim is asymptotic, one finite convex configuration cannot refute it. A counterexample must instead give convex-independent point sets at arbitrarily large cardinalities whose unit-distance counts exceed every proposed linear constant. The mission tracks this superlinear-family statement separately, together with a reduction from it to the exact negation of Problem 96. This keeps both possible outcomes visible: a direct or Problem-97-derived linear upper bound, and an explicit family proving that no such bound exists.
The canonical source is pinned at commit
757d852766f377f7c1a0ffeeef6d3526bc0cb7a4. It contains the formal source
statements for Problem 97
and Problem 96.
The source repository reports closed proofs of the conditional bridge to the bound
(conditional three-times bound),
the counting milestone
(nine-point counting bound),
and the exact nine-point exclusion
(exact nine-point exclusion theorem).
The remaining large-cardinality milestone is the
removable-vertex step,
with its minimality hypothesis retained. The current platform mission contains
accepted transfers of the counting argument, the conditional bridge, and the
exact nine-point exclusion, while the removable-vertex step remains open. Its definitions make
convex independence and the positive-radius condition explicit; no theorem is
assumed inside a definition. Singletons and two-point sets are included in
Problem 97, while Problem 96's counting definitions also include the empty set.
The source repository uses Lean v4.27.0; these mission statements target the
platform's v4.33.1. Source-proof transfer and revalidation remain separate work.
The Lean declarations and proofs are this project's own formalization. The
Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical
provenance; they do not indicate that a paper proof was imported or
machine-checked directly.
These source results establish the intended dependency graph: the P97 universal
root feeds low-unit-degree extraction, strong induction, and then the P96
supremum bound. The platform mission records those contracts and milestones;
it does not claim to have transplanted their proof bodies.
The milestones include the two canonical roots, their conditional bridge, the
|A| ≥ 9 count, the n = 9 exclusion, the |A| > 9 removable-vertex step,
the documented Danzer nine-point three-neighbor example, the parallel goal of
constructing a Problem 97 counterexample, and the superlinear-family route to
a counterexample to Problem 96.
Applying the circle method to an additive problem about primes requires counting primes in arithmetic progressions with an error term uniform in the modulus: the modulus is not fixed in advance, it grows with the size of the numbers being represented. The Siegel–Walfisz theorem is the classical statement of that uniformity, valid for every modulus up to a fixed power of , and it is the one analytic ingredient the standard proof of Vinogradov's three primes theorem cannot do without.
The history is a sequence of partial uniformities:
The von Mangoldt function equals if is a prime power and otherwise. The Chebyshev function counts primes with weights; the prime number theorem is the assertion .
A Dirichlet character modulo is a multiplicative function , supported on the units and taking root-of-unity values there. The principal character is the indicator of the units; a character is quadratic (real) if and , and primitive if it is not induced by a character of a proper divisor of . The Dirichlet -function , defined for , extends meromorphically to , entire except for a simple pole at when is principal.
The two counting functions of the mission are the twisted von Mangoldt sum and the progression sum
related by finite character orthogonality. Write for principal and otherwise. A zero of lying inside the classical zero-free region is an exceptional zero (a Siegel zero); the set of such zeros for a given is the exceptional set , which the results below constrain to have at most one element.
The attack path follows Davenport, Multiplicative Number Theory, 3rd ed., §§14, 18, 20, 21, 22.
(1) zero_free_region (§14, pp. 88–96). There is an absolute such that for
every and every ,
with at most one exception, which is real, lies in , is a simple zero, and can occur only for quadratic non-principal .
(2) pnt_dlvp (§18, pp. 111–114). For some and all ,
(3) psi_char_of_region (§20, pp. 121–125). For a region constant there are
such that, whenever is an exceptional set for with
respect to and ,
(4) siegel (§21, pp. 126–131). For every there is
such that for every real primitive non-principal ,
(5) siegel_zero (§21, second form). For every there is
such that for every real primitive non-principal ,
(6) siegelWalfisz (§22, pp. 132–134). For every there are such
that for all , all , and all with ,
This is literally the platform proposition ThreePrimes.SiegelWalfisz.
A corollary, not a milestone, records the progression form siegel_walfisz_ap: for
and ,
Goal (three_primes, §26). There is such that every odd is a sum
of three primes. It follows from milestone (6) by the existing platform theorem
deducing ThreePrimes.ThreePrimesExistence from ThreePrimes.SiegelWalfisz. The goal
leaves unspecified rather than hard-coding a numeric threshold, so it is not
invalidated by later improvements to that threshold.
Siegel–Walfisz is the standard uniform input downstream of which sit the circle method for ternary Goldbach, the Bombieri–Vinogradov theorem, and much of sieve theory. Without it, the three primes theorem's major-arc analysis has no main term.
Platform status is the reason this mission exists. A complete, machine-checked
formalization of the three primes theorem already exists in the namespace ThreePrimes
(by user tabbott), following Vaughan, The Hardy–Littlewood Method, Ch. 3, and
Davenport §26. It is conditional: it takes Siegel–Walfisz as an explicit hypothesis
ThreePrimes.SiegelWalfisz. Discharging that hypothesis makes the three primes theorem
unconditional, and is the whole content of this mission.
Mathlib contains the analytic continuation of
(DirichletCharacter.LFunction),
its functional equation, the non-vanishing of on ,
Dirichlet's theorem, and the Chebyshev function. It does not contain the zero-free
region for , the explicit formula for , Siegel's theorem, or
Siegel–Walfisz. The platform additionally hosts the
PNT+ project contour
machinery for — Borel–Carathéodory, the
inequality, a zero-free rectangle, and MediumPNT,
. That is a template for the
analogues, not a proof of them, and its error term is weaker than the de la Vallée
Poussin form milestone (2) asks for.
The first idea is to run the argument character by character. It works for complex and breaks for real ones. The positivity device that pushes zeros off compares , and the trivial character at nearby points; when is quadratic, is principal and contributes the pole of at at exactly the height where the putative zero sits, so the inequality degrades from "no zeros" to "at most one zero" and stops there. Every later step inherits that unexcluded zero: milestone (3) can only be stated with the term present, and milestone (6) is exactly the assertion that for this term is small — which Siegel's ineffective bound supplies and nothing effective is known to.
A second shortcut, deducing uniformity from Mathlib's non-vanishing of on together with Dirichlet's theorem, also fails: those results are qualitative, carry no rate, and are not uniform in .
Sums run over with , matching Vino.vmSumChar and
ThreePrimes.SiegelWalfisz; Davenport sums over . The two differ by the single
term , negligible against every error term above. Milestone (2)
alone uses a real argument, via Mathlib's Chebyshev.psi. is Mathlib's
DirichletCharacter.LFunction, so no continuation is reconstructed.
The zero-free region is Davenport.InRegion c q s, namely
; the exceptional zero
is packaged as IsExceptionalSet c χ E: is a subsingleton, every element is a real
zero of in and can exist only for quadratic non-principal ,
and at every of the region outside . Milestone (1) adds
simplicity as for .
Milestone (3) takes the region constant as a parameter rather than importing it
from milestone (1), so the milestones can be attempted in any order. For large the
hypothesis IsExceptionalSet c χ E may be unsatisfiable for some , making the
statement vacuous there — a harmless weakening, not a falsehood, and not a trivializing
reading: milestone (1) produces a definite small with a witness for every
, so instantiating milestone (3) at that discharges the hypothesis rather than
voiding it.
Siegel's theorem is stated for χ.IsQuadratic, χ ≠ 1, χ.IsPrimitive characters, with
the conclusion a lower bound on ; since is real
for real , this is the value itself, not a weakening. The constants in milestones
(4), (5) and (6) are ineffective; the statements are plain existentials, so
ineffectivity is invisible to Lean, but no numeric constant can be extracted from
anything downstream of them.
The principal character is included in the character-form statements, with main term
(if χ = 1 then (N : ℂ) else 0); milestones (3) and (6) therefore contain the prime
number theorem itself and cannot be proved by restricting to non-principal .
Milestone (6) requires strictly, which is what makes a
genuine saving over the trivial ; with allowed it would be
empty.
Beyond the six milestones, a complete development needs Hadamard factorization for as an entire function of order , the zero-counting estimate (§16, pp. 101–103), the truncated explicit formula for (§19, pp. 115–120), Perron-type contour truncation, and the imprimitive-to-primitive reduction . All of it is reusable well beyond this mission, being the standard prerequisite for Bombieri–Vinogradov, Linnik's theorem, and effective Chebotarev. Contributions of these supporting results, of alternative routes to milestone (3) following Montgomery–Vaughan Ch. 11, of the versions, and of sharper constants are welcome.
Mathlib.NumberTheory.LSeries.DirichletContinuation.
docsPolynomial representations provide a concrete way to study modules over Lie algebras: the underlying vector space is a polynomial ring, while the Lie generators act by explicit multiplication, shift, and differential operators. Chen and Tan classify a family of modules over the symplectic Lie algebra that are free of rank one over the universal enveloping algebra of an abelian nilradical. Their paper determines the family, its isomorphism classes, its weight and simplicity criteria, its finite-length behavior at exceptional parameters, and an application to Hamiltonian Lie algebras. This mission packages those headline results into one common Lean target, corresponding to Theorems 1.1--1.3 of Chen--Tan.
The common-family formulation matters. The source does not assert three unrelated existence theorems: one explicit two-parameter family carries all of the classification, simplicity, finite-length, and Hamiltonian consequences. The Lean goal therefore quantifies that family once and requires all headline properties of the same witness.
Fix and the complex symplectic Lie algebra . The relevant maximal parabolic subalgebra has an abelian nilradical . Its enveloping algebra is a polynomial algebra in the root generators, represented formally by a multivariate polynomial ring. A rank-one free -module can consequently be modeled on that polynomial ring.
The definition bundle presents the simple Chevalley generators and their action by explicit operators depending on a scalar and a polynomial parameter . Rather than assuming that these formulas already form a representation, the target asks for a generator presentation satisfying the symplectic Lie relations and for a representation family realizing the formulas. It also formalizes module equivalence, weight spaces, simplicity, Noetherian and Artinian conditions, finite composition factors, and the Shen--Larsson construction for a Hamiltonian Lie algebra.
Prove that for every there is one generator presentation and one family
of -representations on the polynomial ring, free of rank one over the abelian nilradical, satisfying the explicit generator formulas. Prove the source's classification and isomorphism criteria, including that is a weight module exactly when is constant, and the stated simplicity criterion outside the exceptional arithmetic set
For exceptional , prove the Noetherian/Artinian and finite-composition-series conclusions and the weight/nonweight classification of the composition factors. Finally, prove that the canonical Hamiltonian Shen--Larsson construction has the exact degree-weight spaces and the source's simplicity and weight-module consequences. All clauses must be witnessed by the same family .
The result gives a complete algebraic description of a large concrete class of non-highest-weight modules. It separates the generic simple regime from an exceptional finite-length regime and shows how nonweight symplectic modules generate weight modules over an infinite-dimensional Hamiltonian Lie algebra. The explicit formulas make the family suitable for calculation, while the classification prevents duplicate parameter choices from being mistaken for genuinely different modules.
Formalization adds checks that are easy to blur in prose. In particular, the generator formulas cannot be called a Lie representation until the defining relations have been verified, and the same witness must support every later theorem. A completed proof will contribute reusable Lean infrastructure for symplectic root data, polynomial representations, module-theoretic finiteness, exact weight-space descriptions, and Hamiltonian Lie-algebra functors. The paper's proofs are known; the open task is their machine-checked reconstruction.
The first obstacle is structural rather than computational. Checking formulas on individual generators is insufficient: all Chevalley and Serre relations must hold with the correct operator order and signs, after which the action must extend to the full Lie algebra. Classification then requires controlling arbitrary rank-one-free modules, not merely verifying that the displayed examples exist.
The exceptional parameters introduce a second layer. Generic simplicity and exceptional finite length are logically different claims, and the composition-factor statement must be tied to the same parameterized representation. The Hamiltonian application adds another algebra and a tensor construction; exact weight spaces and simplicity cannot be obtained by treating the functor as an opaque interface. The Lean goal deliberately keeps these obligations inside one theorem so that separate convenient witnesses cannot satisfy different portions.
The mission works over with natural rank . The definition bundle uses concrete multivariate polynomials, matrices and linear maps, a presented symplectic Lie algebra, Lie representations, submodules, and tensor products. The exceptional set is expressed with complex coercions, so no accidental natural-number division is involved. The nilradical action, freeness, parameter equivalence, weight-space equalities, simplicity, finite-length properties, and Hamiltonian brackets are transparent propositions in the bundle.
The final theorem is a single conjunction under one existentially quantified presentation and one existentially quantified family . Several convenient corollaries can be projected from it, but they are not independent targets and do not permit different witnesses. The bundle contains no custom axioms or opaque semantic assumptions, and the only admitted term is the main theorem's sorry. Contributions may split the proof into source-numbered lemmas about generator relations, classification, exceptional submodules, or the Shen--Larsson application, provided the shared-family quantifier structure is preserved.
Moment-angle complexes are central objects in toric topology. They convert the combinatorics of a simplicial complex into a topological space assembled from disks and circles, allowing face structure to influence homotopy and homology. When the simplicial complex triangulates a sphere, the resulting space is a moment-angle manifold. Torsion in the integral homology of these manifolds is difficult to realize in low simplicial dimension, and torsion in the homology of their based loop spaces is even more constrained. Yang Han and Keke Li's Theorem 1.7 asserts that dimension four is already universal: every finitely generated abelian group can occur as a subgroup of both homology theories for one and the same simplicial -sphere.
This mission formalizes that headline existence statement. It is not restricted to a chosen finite list of groups or primes, and it requires a common simplicial sphere rather than permitting separate witnesses for ordinary and loop homology.
Let be an abstract simplicial complex on a finite vertex set . Its geometric realization is formed from probability vectors whose supports are faces of . The condition that is a simplicial -sphere means that this realization is homeomorphic to the unit sphere .
For each face , assign a copy of the closed disk at vertices in and the boundary circle at vertices outside . The associated moment-angle complex is
The all-ones point is a canonical basepoint. Write for the based loop space with the compact-open topology. For a space , the mission uses total integral singular homology
as an additive abelian group. Saying that an abelian group is a subgroup means that there is an injective additive homomorphism .
For every finitely generated abelian group , prove that there are an integer and a simplicial complex on Fin m such that and there are injective homomorphisms
The quantifier order matters: the same and the same must support both embeddings. The target concerns additive subgroups of total graded homology; it does not require the two embeddings to land in the same degree or to preserve multiplicative structures.
The theorem gives a universality statement for moment-angle manifolds over simplicial -spheres. It says that no classification by a bounded list of torsion primes or exponents can describe all such homology and loop-homology groups. Requiring both embeddings for a single connects the ordinary topology of the manifold to its based-loop topology rather than proving two unrelated existence results.
Formalizing the theorem requires reusable foundations in several areas: finite abstract simplicial complexes, geometric realization, polyhedral products, based loop spaces, integral singular homology, graded direct sums, and additive embeddings. The published article presents a human proof; this mission records its intended main theorem as an open Lean target. The definitions do not assume the existence of the required sphere or embeddings, so a solver must supply the mathematical construction and all homological consequences.
The assertion ranges over arbitrary finitely generated abelian groups, including free parts and prime-power torsion of unbounded exponent. A finite check of selected groups cannot establish the target. The same finite simplicial object must simultaneously control two different homology theories, one of which is applied to an infinite-dimensional function space. Standard library support is strongest for singular homology as a functor, while concrete calculations for moment-angle spaces and loop spaces require additional bridges.
There is also a substantial representation boundary between combinatorics and topology. The face data of , the union of disk-circle products, the homeomorphism , and the induced maps on homology must all refer to compatible spaces and basepoints. A formal solution cannot replace “simplicial sphere” by a mere Boolean flag or replace homology by an arbitrary group-valued field.
Lean represents using AbstractSimplicialComplex (Fin m). Because Mathlib's structure includes singleton faces automatically, the auxiliary face predicate explicitly restores the conventional empty face where the moment-angle union needs it. The geometric realization is the standard support-restricted probability simplex, and the sphere condition is an actual homeomorphism to the Euclidean unit -sphere.
The moment-angle space is a subtype of (Fin m → ℂ) defined by the literal disk/circle coordinate condition. The loop space consists of based continuous paths with matching endpoints and carries the compact-open topology inherited from Mathlib's path construction. Homology is singularHomologyFunctor with coefficients in , and total homology is a direct sum over all natural degrees.
The statement permits the two embeddings to occupy different degrees and makes no ring-embedding claim; these choices match the source phrase “contain as a subgroup.” It rules out vacuity by requiring an actual simplicial complex, an actual sphere homeomorphism, and injective additive maps. Contributions that isolate degree-specific refinements, compute homology of standard polyhedral products, or formalize reusable loop-space equivalences are welcome, provided they reconnect to the stated root theorem.