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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
When replenishment takes several periods, an inventory decision commits stock before the demand that will consume it is known. Too much stock incurs holding costs; too little loses sales. An optimal decision can depend on the entire pipeline of outstanding orders. A rule with only two adjustable parameters is easier to implement, but its simplicity alone gives no guarantee on the cost it can incur.
Capped base-stock policies combine an inventory-position target with a maximum order quantity. The class was introduced and analyzed by Xin (2021). The present target is the finite-lead-time guarantee in Linwei Xin's Capped Base-Stock Policies: A 2.33-Approximation, specifically the author-supplied manuscript with source label thm-main. A public listing of the paper identifies the July 17, 2026 working paper; the supplied text is the authoritative version for this formalization.
Periods are discrete. Demand is a sequence of independent, identically distributed nonnegative real random variables with finite, strictly positive mean . The deterministic lead time is an integer . Holding and lost-sales rates are and .
At the beginning of period , is on-hand inventory and are outstanding orders, with due immediately. That arrival is received, an order is placed, demand is realized, and costs are charged. The new order arrives periods later. The equations are
Here . Unfilled demand is lost rather than backlogged. With , the period cost is . Initial inventory and every pipeline coordinate are zero. A nonanticipative policy chooses orders using only information available before the current demand; policies may depend on the entire observed past and on independent private randomization.
For a policy , its long-run expected average cost is
The capped rule is for finite . Write . Ordinary base stock is already included by taking ; no infinite order cap is required.
For and , set
Empty sums are zero. The lower certificate is
The pair is feasible. Both horizon constraints are retained. With
the goal is Theorem 1's complete assertion:
The exact rational constant is used; the title's 2.33 is a rounded description. Multiplicative inequalities also make sense when the optimal cost is zero.
Five supporting targets reproduce selected source statements: Proposition 1's lower-certificate bound; Proposition 2's finite-cap cost conclusion; Lemma 2's bound on a consecutive block in the greedy recursion; Proposition 3's ordinary-base-stock cost bound; and Proposition 4's two-branch inequality. The finite-cap and ordinary-base-stock parameters remain exactly and , respectively. Labels accompany the printed numbering so the supplied source is unambiguous.
The result gives a uniform cost guarantee for this policy class across all positive holding and penalty rates, every positive integer lead time, and arbitrary nonnegative demand laws with finite positive mean. It bounds the infimum of costs over the policy parameters; it does not by itself provide an algorithm for selecting parameters or assert that the infimum is attained. At the displayed coefficient is 2, while its uniform upper bound is .
The manuscript supplies mathematical proofs. This mission asks for checked proofs of their formal statements. Compiling the declarations confirms that they are well formed, not that the claims are proved. A completed development would provide reusable delayed-inventory dynamics, measurable history policies, average-cost optimization objects, finite-horizon demand envelopes, and policy-comparison results.
The pipeline carries consequences of past decisions across multiple demand periods. Nonanticipativity and independence must be stated precisely before expectation and convexity arguments can be used. Also, existence of a stationary distribution alone does not identify its expected cost with a long-run cost from an empty initial system. The manuscript invokes stationary results from prior inventory work, including Xin and Goldberg (2016), and uses stationary CBS quantities in intermediate arguments. Their needed hypotheses and connections to the original objective require proof within a complete development.
The two cost bounds depend on both coordinates of a feasible lower-certificate pair. Losing either horizon constraint changes that certificate. Replacing it with an arbitrary scalar lower bound or assuming the policy comparisons would remove substantive parts of the result.
Stock, orders, and demand take arbitrary nonnegative real values. Time is represented from zero in the operational model, corresponding to period one in the manuscript. The formal representation uses a canonical probability model with independent demand coordinates and an independent uniform private seed; measurable time-dependent decision functions use only preceding demands and that seed. Connecting arbitrary standard-Borel randomized controls to this canonical realization is a representation obligation. The zero-start optimum ranges over these general history policies, not only stationary or capped policies.
Expected nonnegative costs, their upper limits, and cost infima are represented in the extended nonnegative reals. Thus a policy with infinite expected cost does not acquire a fictitious zero value through a totalized real integral. The finite-horizon envelope expectations use the original integrable demand law. The greedy lemma uses integer-indexed sequences so subtraction of earlier times has no natural-number truncation; its blocks are nonempty, as required to define their maximum.
Definitions contain no unproved facts. In particular, stationarity, convergence from the empty initial state, lower bounds, and upper policy comparisons are not fields assumed by the model. Contributions to these intermediate obligations and to any of the five source targets support the central theorem.
thm-main), Proposition 1 (lemma-lb), Proposition 2 (prop-finite-cap-bound), Lemma 2 (lem-greedy-window), Proposition 3 (prop-base-stock-bound), Proposition 4 (lem-two-branch). Source SHA-256: f353793c255e1ebed5f3ec541037284bd926183e3e5b71941f13e79c2d67cb7a.Every introductory number theory course opens with the same fact: the integers factor into primes in exactly one way. Euclid's Elements (Book IX, Proposition 14) already proves a form of it for the case of two factorizations sharing no further structure, but the theorem is not stated in full generality — with existence and uniqueness as a single package — until Gauss's Disquisitiones Arithmeticae (1801, Art. 16). Every standard modern treatment restates it as the opening theorem of the subject: Hardy & Wright, An Introduction to the Theory of Numbers (Theorem 2), and Apostol, Introduction to Analytic Number Theory (1976, Theorems 1.9–1.10), both prove it in the first chapter, before anything else is developed. The reason is structural, not pedagogical convenience: gcd, lcm, multiplicative functions, the notion of "the" prime factorization of an integer, and the entire multiplicative structure of depend on it being true. Mathlib itself packages the general statement as UniqueFactorizationMonoid, of which is one instance — this mission asks for the classical, elementary argument specific to , in the two-part shape every textbook gives it.
A prime is a natural number whose only divisors are and (Mathlib's Nat.Prime). A factorization of is represented here as a multiset of natural numbers — an unordered collection that tracks multiplicity but not order, so that two factorizations differing only by a reordering of their factors are already identified as the same multiset, with no separate permutation argument needed. Write for the product of the elements of with multiplicity, under the convention that the empty multiset has product . The theorem concerns multisets all of whose elements are prime.
For every nonzero there is exactly one multiset of primes whose product is . This is the capstone: existence and uniqueness combined into the single statement every textbook eventually asserts.
Every nonzero natural number is a product of primes (Apostol, Theorem 1.9). This alone says nothing about how many such multisets there might be.
Any two multisets of primes with the same product are equal (Apostol, Theorem 1.10). Combined with Milestone 1, this gives the Goal.
The result itself. Unique factorization is what makes "the prime factorization of " a well-defined object rather than a choice. Every downstream elementary and analytic number theory construction leans on it: and computed via shared prime exponents, multiplicative arithmetic functions (, , ) defined by their values on prime powers, the Euler product for , and -adic valuations. Without it, none of these constructions are canonical.
Formalizing it. The general statement is already machine-checked in Mathlib as an instance of UniqueFactorizationMonoid (and concretely realized for via Nat.factors/Nat.factors_unique), so this is not open mathematics. What this mission asks for is the specific, elementary two-lemma argument — strong induction for existence, Euclid's lemma plus strong induction for uniqueness — spelled out for with the Multiset representation used here, rather than a one-line appeal to the packaged Mathlib result. A solution that simply repackages Nat.factors_unique and its companions is a legitimate route (nothing here is designed to block it), but the more valuable contribution is the self-contained classical proof, since that is what a reader of Apostol or Hardy & Wright expects to see reconstructed.
For existence, ordinary induction on does not immediately work: if is composite, with , and the inductive hypothesis is needed for both and at once, neither of which is simply . The fix is strong (well-founded) induction on , splitting into the prime case (trivial single-element multiset) and the composite case (combine the two multisets for and ).
For uniqueness, the natural first attempt — "cancel a common prime factor from both sides and recurse" — silently assumes that the same prime appears in both multisets, which is exactly what needs to be proved. The step that actually does the work is Euclid's lemma: if a prime divides a product , it divides one of the factors of . This is not a restatement of primality (irreducibility, "no nontrivial divisors") but a genuinely separate fact about that requires either Bézout's identity or a well-ordering argument to establish; conflating "prime" with "has this divisibility property" is the standard trap for a first attempt at this proof.
The statement is specific to (not or a general UniqueFactorizationMonoid), and factorizations are represented as Multiset ℕ rather than List ℕ up to permutation — this is a deliberate choice that folds "unique up to reordering" directly into multiset equality. The hypothesis is , not : the case is included, and its unique witness is the empty multiset, since the empty product is and no nonempty multiset of primes (each ) can have product . is excluded because no multiset of natural numbers has product under this convention (every prime is , and the empty product is ), so no factorization of exists to be unique.
No auxiliary platform Definitions are required — the statement is expressed entirely in terms of Nat.Prime and Multiset.prod from Mathlib. Reusable contributions welcome beyond the two milestones: an explicit construction of the canonical sorted List ℕ factorization (Nat.factors-style) connecting this multiset formulation to the more computational list representation, or a generalization of the uniqueness argument to an explicit statement and proof of Euclid's lemma as a standalone milestone.
Mathlib.RingTheory.UniqueFactorizationDomain, https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/UniqueFactorizationDomain.htmlDiophantine equations ask for integer solutions to arithmetic equations. One family of questions starts with a set of positive integers and imposes the same condition on every pair: their product, increased by one, must be a square. The question is how many distinct integers can satisfy all those conditions together. It connects a simple definition with a global restriction on simultaneous integer solutions.
The paper There is no Diophantine quintuple, by Bo He, Alain Togbé, and Volker Ziegler, resolves the nonexistence question for sets of five elements. This mission targets its headline result, Theorem 1 in Section 1. The mathematical theorem is proved in the paper; the remaining goal is a complete Lean proof of that result.
A perfect square is an integer of the form for a natural number . A Diophantine -tuple is a set of distinct positive integers such that the product of any two different members, plus one, is a perfect square. Here records the number of elements, not a bound on their sizes. A Diophantine quintuple would have exactly five members (definition in Section 1).
Write those five integers as . Positivity means for every index. Distinctness means whenever . The square condition requires a possibly different square root for each pair. There is no requirement that the ten square roots coincide, be distinct, or satisfy an additional ordering condition.
The theorem concerns positive integers. Replacing them by rational numbers changes the question. Likewise, allowing zero changes the admissible objects, and allowing repeated entries ceases to represent a five-element set. These domain choices are explicit in the formal target.
The single goal is the following nonexistence statement:
This is Theorem 1 of the paper. The mission's goal is the existing declaration no_diophantine_quintuple.
The integers are unrestricted in size. The target does not fix the smallest entry, require a particular triple among the entries, or assume that an entry falls below a numerical search threshold. A proof must cover every quintuple satisfying the stated domain conditions.
The result rules out an entire class of simultaneous square equations. As an immediate consequence, any set of distinct positive integers satisfying the same pairwise condition has at most four elements: a larger set would contain five distinct members that inherit the condition. This consequence explains why the five-element statement also constrains larger configurations.
A completed formalization would supply a reusable theorem that can be invoked whenever five distinct positive integers and their pairwise square witnesses arise. It would turn the informal nonexistence claim into a checked contradiction from precisely those hypotheses. The published statement is currently open for a Lean proof; its successful compilation verifies that the statement is well formed, not that the theorem has been proved.
Testing examples cannot establish this target by itself. Any computation with a fixed search limit addresses only a bounded collection, while the statement quantifies over all positive integers. A formal proof that uses a finite computation must also establish why the computation covers every possible case.
The conditions are simultaneous: each entry participates in four pairwise equations. Solving or excluding one isolated pair does not by itself settle whether all ten equations can hold together. The paper's proof overview in Section 2 describes the arithmetic estimates and computational components behind its result. Formalizing those components entails checking their hypotheses and connecting their conclusions to the unrestricted goal.
The Lean declaration represents the entries by a function a : Fin 5 → Nat. It places the existence of that function under a negation and includes three conditions: every value is positive, different indices have different values, and every pair of different indices has a natural-number square witness.
The square condition is written for all unequal indices. This is equivalent to the usual condition for increasing pairs because multiplication is commutative. No increasing ordering of the five values is imposed. A development using sorted entries must justify its connection to this unrestricted indexed representation.
The root statement needs only Lean's core natural numbers, finite index type, arithmetic, and logic. It introduces no custom predicate whose meaning could hide additional assumptions. A complete proof may use Mathlib and reusable supporting results about integer arithmetic, squares, and the arithmetic tools required by the chosen argument. Supporting declarations should state their hypotheses explicitly and ultimately connect to this exact root theorem. Contributions establishing the known result, including an alternative rigorous proof, are within scope.
Two-dimensional lattice models admit topological defects whose energetic cost competes with their configurational multiplicity. The later stages of a finite vortex argument therefore need a trustworthy bridge from a prescribed vorticity to the least quadratic energy of a compatible field. This mission isolates that bridge. It does not attempt a phase-transition theorem; it establishes only the finite-dimensional variational identity on which a later, model-specific energy estimate can rest.
The algebra belongs to finite discrete Hodge theory. A finite cochain complex supplies a differential from degree one to degree two and an adjoint codifferential in the reverse direction. A normalized Green operator inverts the degree-two Laplacian on realizable vorticities and annihilates the harmonic obstruction. Such finite-complex harmonic methods go back at least to Beno Eckmann's 1944 treatment of harmonic functions and boundary-value problems on complexes. The vortex motivation comes from the energy--entropy mechanism discussed by Kosterlitz and Thouless for two-dimensional systems, but no claim from their thermodynamic analysis is included here.
Let be finite-dimensional real inner-product spaces. A finite Hodge complex consists of linear maps
together with specified adjoints and , and the cochain relation . The degree-two Laplacian is
The vorticity space is . A normalized degree-two Green owner supplies a unique self-adjoint linear map satisfying both inverse identities with the orthogonal projector onto that range, taking values in the range, and vanishing on .
For a realizable source , define the canonical one-cochain
The physical vortex normalization scales the prescribed vorticity by , so the canonical physical field is . For a coupling , the quadratic energy of is
For every realizable and every field satisfying , establish
The equality is required for every real . Its unscaled components assert the exact Poisson equation, closedness and orthogonality of the residual, the Pythagorean norm decomposition, and the identity
For , conclude
Two controls are part of the target boundary: zero coupling must not identify a unique minimizer, and zero vorticity must not imply that the underlying field or its positive-coupling energy vanishes.
The result separates universal finite linear algebra from geometry that depends on a particular lattice. Once a periodic square torus is registered as a finite Hodge complex, a later theorem may specialize the Green quadratic form to dipole charges and investigate its dependence on separation. Entropy can then be compared with a genuine energy inequality without redefining energy through the desired conclusion.
Formalizing this layer provides reusable interfaces for Poisson solvability, orthogonal residuals, exact quadratic energy splitting, and the nonnegative-coupling lower bound. It also makes normalization errors visible: the factor in the source and the factor in the energy force the coefficient . The underlying Green-owner infrastructure already has a machine-checked implementation in LeanProofs; the propositions in this mission are new proof obligations derived from that interface.
The central issue is not an asymptotic estimate. It is maintaining the exact relationship among the Laplacian sign, the orthogonal projector, the Green normalization, adjointness, and the physical scaling. A proof that silently projects a non-realizable source changes the problem. A proof that divides by loses the case. A proof that treats zero vorticity as a zero-field assertion discards closed and harmonic residuals. Each of these shortcuts is ruled out by the formal target or its controls.
The Lean development uses arbitrary finite-dimensional real inner-product spaces rather than a concrete torus. All maps are continuous only through finite-dimensional linear structure; there is no measure theory, probability, or limiting process. A source is explicitly required to lie in . The exact decomposition permits every real , while the inequality requires . Existence of a Green owner is supplied as data; this mission neither constructs a second inverse nor changes the existing normalization.
The mission does not define integer charge, torus distance, plaquette winding, or a concrete lattice Laplacian. It proves no logarithmic Green estimate, cosine-energy comparison, entropy bound, Gibbs statement, vortex proliferation result, thermodynamic limit, BKT transition, or universal jump. In particular, the target cannot be satisfied by choosing a convenient torus size or hard-coding a Green kernel: it is group-generic finite-dimensional algebra conditional on the stated Hodge and Green structures.
Contributions are welcome on the independent Poisson, orthogonality, norm, scaling, and control nodes. A later mission can add the square-torus realization and the separate analytic capacity estimate needed for a sharp logarithmic lower bound.
dbf503b2909cc17787d40a21eb75a0c9354cc6ef. https://github.com/MonumentalSystems/LeanProofs/commit/dbf503b2909cc17787d40a21eb75a0c9354cc6efFor every integer
, there exists a prime p such that
An almost complex structure gives every tangent space of a smooth manifold the linear algebra of a complex vector space, but it need not come from complex-valued coordinate charts. The gap between these two notions is a global differential-geometric question, not a change of terminology. Granja and Milivojević describe the following as “a major open problem in differential geometry”: whether every closed almost complex manifold of dimension at least six admits an integrable complex structure (Introduction, p. 1). This mission records that question as an open conjecture, not as an established theorem.
Fix an integer . Let be a connected, compact, Hausdorff, second-countable smooth manifold without boundary and of real dimension . An almost complex structure on is a smooth field
of real-linear maps satisfying for every and . This condition forces even real dimension, but by itself supplies no complex coordinate charts.
A complex structure of complex dimension is an atlas with values in whose transition maps are complex differentiable. Such an atlas induces an integrable almost complex structure. The target concerns existence on the underlying smooth manifold: the complex structure obtained may induce a different almost complex structure from the supplied . It does not claim that every chosen almost complex structure is integrable.
Here “closed” means compact and without boundary. Connectedness is explicit because it is part of the standing manifold convention in the cited 2022 source. The lower bound is on real dimension: , equivalently .
For every and every closed connected smooth real -manifold ,
“Compatible” means that the underlying real smooth structure of the complex atlas is smoothly equivalent to the given smooth structure on the same topological space. No claim of uniqueness, equality with the original atlas, or integrability of the supplied is made.
The real six-dimensional case is essential. Since carries an almost complex structure, the conjecture would imply that its underlying smooth manifold carries some complex structure. That special case remains unresolved; restricted nonexistence results, such as results imposing compatibility with a particular metric, do not decide the unrestricted existence question.
A positive solution would replace a pointwise tangent-bundle reduction by genuine holomorphic coordinates for every manifold in the stated class. It would in particular settle the existence question for . A negative solution would identify additional global obstructions to complex atlases that are invisible to the existence of an almost complex structure.
The formalization isolates a reusable smooth almost complex structure on top of Mathlib’s tangent-bundle and manifold APIs, while making the desired complex atlas explicit. This prevents the central distinction from being hidden inside an unconstrained predicate named “integrable.” It also exposes the compatibility between the original real smooth atlas and the real atlas underlying the complex charts, which future work on characteristic classes, Nijenhuis tensors, and concrete six-manifolds can reuse.
The equation is fiberwise algebra. Integrability requires local complex coordinates whose overlaps are holomorphic, equivalently the vanishing condition identified by Newlander and Nirenberg. Smooth variation of does not make that differential condition automatic. Thus simply viewing each tangent space as a complex vector space does not construct a complex manifold.
The six-sphere shows why the dimension threshold cannot be treated as a routine stable-range simplification. Its known almost complex structure supplies the hypothesis in real dimension six, while no arbitrary complex atlas is known. Likewise, replacing the conclusion by a complex vector-space structure on each tangent fiber would merely repeat the hypothesis and would not address the open problem.
The namespace AlmostComplexToComplex uses Mathlib’s boundaryless Euclidean manifold model. AlmostComplexStructure n M contains a continuous real-linear map on every tangent space, the pointwise identity , and smoothness of the induced self-map of the total tangent bundle. It contains no integrability field.
The main theorem assumes the real atlas is modeled on and concludes the existence of charts modeled on . Mathlib’s IsManifold condition over at order one states complex differentiability of chart transitions. Two conditions on the identity map compare the original real atlas and the real manifold structure underlying the complex charts in both directions; an unrelated smooth structure therefore cannot satisfy the conclusion merely by being placed on the same carrier type.
This is a chart-level interface, not yet a development of analytic integrability theory. Mathlib at the pinned revision has no ready-made almost-complex/Nijenhuis package connecting the structure above to the Newlander–Nirenberg criterion. The target does not assert that the supplied is integrable or homotopic to the one induced by the resulting atlas. A dedicated milestone is also outside this minimal draft because faithfully constructing the standard sphere and its known almost complex structure would require additional sourced infrastructure; no surrogate special case is inserted.
In 1999 Artzner, Delbaen, Eber and Heath asked what a risk measure ought to satisfy, wrote down four axioms, and observed that the industry standard of the day -- Value-at-Risk -- fails one of them. The failing axiom is subadditivity: merging two positions should never require more capital than holding them apart. VaR can violate it, so under VaR a diversified book can appear riskier than its parts.
That observation did not stay academic. It is the reason the Basel framework moved its market-risk capital standard from Value-at-Risk to Expected Shortfall. Few results in mathematical finance have had a more direct regulatory consequence, and the mathematics is elementary enough to state completely.
A position is a payoff X : Fin (n+1) -> R across finitely many equally-weighted states, and a
risk measure rho sends it to the capital that must be added to make it acceptable. Following
Definition 2.4 of the paper, rho is coherent when it is translation-invariant, subadditive,
positively homogeneous and monotone. Nonemptiness of the state space is carried in the index type
so the worst case is always attained; no probability measure is needed for these four axioms,
which is faithful to the paper -- Artzner et al. state T, S, PH and M without reference to one.
Value-at-Risk is defined here at an integer tolerance k rather than a probability level, which
keeps the quantile unambiguous on a finite space: VaR X k is the least capital leaving at most
k states in loss, corresponding to level k/(n+1).
The mission's goal theorem is the negative result: Value-at-Risk is not subadditive. A witness
is 25 equiprobable states with X losing 100 in state 0 alone and Y losing 100 in state 1
alone. Each has one losing state in twenty-five, so at tolerance k = 1 both have VaR = 0;
their sum loses in two states, exceeding the tolerance, so VaR (X+Y) 1 = 100 > 0 + 0. The
witness was checked numerically before this mission was drafted; what is open is the Lean proof.
The milestones establish the positive contrast on the same footing: worst-case risk, the most conservative measure, satisfies all four axioms, so the failure is specific to VaR rather than inherent to risk measurement.
P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent Measures of Risk, Mathematical Finance 9 (1999) 203-228. Axioms T, S, PH and M are Definition 2.4; the failure of subadditivity for VaR and the diversification consequence are discussed in Section 3.
An approximation result must specify both the allowed approximants and the error being controlled. Matching finitely many values is different from approximating a function everywhere with one error bound. Polynomial approximation on a closed interval provides a model: finitely described functions can approach an arbitrary continuous function uniformly, without assuming that the function has derivatives or a convergent power-series expansion. Lebl, Theorem 11.7.1.
The broader question replaces polynomials with a collection of continuous functions closed under algebraic operations. The relevant issue is which properties of that collection guarantee approximation of every continuous function. This distinguishes a useful approximation family from one that cannot detect some points or cannot approximate nonzero values at a particular point. The six targets follow the real and complex approximation results in §11.7 of Jiří Lebl’s Basic Analysis, Volume II. Source section.
A metric space is a set with a nonnegative, symmetric distance that vanishes exactly when and satisfies the triangle inequality. It is compact if every cover by open sets has a finite subcover. Let be either the real numbers or the complex numbers , and write for the continuous functions from to . Products, sums, and scalar multiplication of functions are taken pointwise. The notation denotes polynomials in one indeterminate with coefficients in , and for real endpoints .
A non-unital function algebra contains the zero function and is closed under these three operations. It need not contain the constant function . It separates points if, whenever , some satisfies . It vanishes nowhere if, for each , some satisfies . The witness may depend on ; one everywhere nonzero function is not specified. A complex algebra is self-adjoint if it contains the pointwise complex conjugate of every member. These conventions retain the source’s non-unital setting. Lebl, Definitions 11.7.5, 11.7.7, and 11.7.15.
Uniform convergence of to means
Here is real absolute value or complex modulus. On compact , the closure in uses this uniform topology; saying that is dense means . Mathlib’s compact-domain convergence interface.
The first four statements supply approximation, normalization, closure, and interpolation results. The final two state density, with the complex result as the goal. No approximation rate or degree bound is prescribed.
Theorem 11.7.1. For and for , respectively,
The real clause requires real coefficients. Complex polynomials are evaluated at the complex embedding of the real argument. Source theorem.
Corollary 11.7.4. For ,
Proposition 11.7.6. For compact metric and either scalar field,
Proposition 11.7.11. For an arbitrary set , without topology, let be an algebra separating points and vanishing nowhere. Then
Both scalar fields belong to this single target. Source proposition.
Theorem 11.7.12. For compact metric ,
Theorem 11.7.16, complex Stone–Weierstrass. For compact metric ,
The density conclusion turns structural conditions on an approximation family into a statement about every continuous target function. Exact interpolation only controls specified values at two points; density controls all points simultaneously to any positive tolerance. The normalized absolute-value result retains a constraint on every approximating polynomial, rather than obtaining normalization only in the limit.
These are established theorems, not open conjectures. Mathlib already has machine-checked polynomial approximation, unital Stone–Weierstrass results, and non-unital algebra infrastructure. The six source-level statements also have standalone proofs checked in the pinned Lean environment. The contribution is an explicit textbook-facing non-unital formulation, with both scalar fields and the source’s normalization and interpolation clauses retained. It is not a claim to the first formalization of Stone–Weierstrass. Polynomial approximation, Stone–Weierstrass library.
Point separation alone does not say that an algebra can approximate a nonzero value everywhere it is requested. A family may distinguish pairs of points while all its members vanish at one fixed point. Nor does interpolation at a pair of points establish a uniform error bound over an entire compact domain. These are distinct quantifier requirements.
Requiring would remove the source’s non-unital case instead of resolving it. Likewise, complex scalar multiplication does not itself impose closure under conjugation. The formal difficulty is to preserve all these distinctions while connecting bundled algebras, continuous maps, and uniform closure. A direct use of the library’s unital theorem has an additional hypothesis that is absent here. Library theorem hypotheses.
Namespace LeblRA uses NonUnitalSubalgebra, ContinuousMap, real and complex polynomials, TendstoUniformly, and topological closure. Domains are arbitrary universe-polymorphic types, with metric and compactness structures only where the source requires them. The interpolation target has neither. Conjugation is the pointwise star operation on complex continuous maps.
The conventional algebra structure includes zero, but not an assumed unit. Empty compact spaces are allowed. Polynomial sequence indices start at zero. The interval approximation theorem permits arbitrary endpoints, including a singleton or an empty interval; the absolute-value corollary assumes and includes . Neither finite-dimensional approximation spaces nor degree bounds are imposed. Replacing density by a finite-domain special case, adding a constant-one hypothesis, or assuming density itself would change the targets.
Reusable infrastructure includes non-unital subalgebras and their closures, polynomial evaluation, compact-domain uniform convergence, and real/complex continuous function spaces. The environment is Lean 4.29.0-rc3 with Mathlib revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Source-faithful alternative proofs and reusable interfaces between these existing structures are welcome; extra alias definitions are unnecessary. Non-unital algebra structures, topological closures.
777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, 2026. Polynomial approximation, Stone–Weierstrass and zero-preserving continuous maps, non-unital algebra closures.Analysis often produces a sequence of candidate functions rather than a finished function. A useful existence theorem must say when some candidates approach a single limit everywhere with a common error bound. Ordinary boundedness is insufficient: Lebl gives bounded continuous functions on a closed interval with no uniformly convergent subsequence. The missing condition concerns how consistently the functions respond to nearby inputs. Examples 11.6.2–11.6.4.
The Arzelà–Ascoli theorem answers this question for continuous complex-valued functions on a compact metric domain. Its uses include existence questions for differential equations and compactness properties of integral operators, both discussed in the source section. These applications require control of entire functions, not merely convergence at isolated points. Differential-equation application, integral-operator application.
The four targets follow §11.6 of Jiří Lebl’s Basic Analysis, Volume II, a textbook treatment of equicontinuity and compactness for uniform convergence. Author’s book page.
A metric space is a set with a distance that is nonnegative, symmetric, vanishes exactly when , and satisfies the triangle inequality. It is compact when every cover by open sets has a finite subcover. Here denotes the complex numbers, their absolute value, and the function at index . Write for the continuous functions.
The sequence is pointwise bounded if each input has its own bound, and uniformly bounded if one bound works for every input and index:
It is uniformly equicontinuous when
Thus cannot depend on the function index or the points. These are the source’s distinct boundedness and common-continuity conditions. Definition 11.6.1, Definition 11.6.6.
A subsequence has the form , where is strictly increasing. Pointwise convergence to means convergence to separately for every . Uniform convergence means that for each there is one such that for every and every . A subset is dense if its closure is all of .
The supporting targets distinguish countable domains, a necessary continuity condition, and the density property of compact metric spaces. The final target combines the hypotheses into uniform-convergence compactness; no quantitative rate is prescribed.
Proposition 11.6.5. For an arbitrary countable set , without any topology or continuity assumption,
Proposition 11.6.7. For compact metric ,
Proposition 11.6.8. Every compact metric space satisfies
Theorem 11.6.9, Arzelà–Ascoli. Suppose is compact metric, , and the sequence is pointwise bounded and uniformly equicontinuous. The complete conclusion is
Both the global bound and the subsequence conclusion are required. The limit belongs to , so its continuity is explicit. Source theorem.
The result supplies a uniform limit under hypotheses that concern individual inputs and a shared continuity condition. It therefore identifies a usable replacement for boundedness alone in a space of functions. The distinction matters downstream: retaining only pointwise convergence would not provide a common error bound across the domain, and assuming uniform boundedness in advance would discard one of the theorem’s conclusions. Lebl, Theorem 11.6.9.
These are established theorems, not open conjectures. Mathlib already contains machine-checked general Arzelà–Ascoli results, compactness and convergent-subsequence infrastructure, and the countable-dense-set interface. The four source-level statements also have ordinary local Lean proofs checked against their exact types. The contribution is a faithful textbook-facing formulation that keeps the distinct hypotheses, quantifier order, arbitrary countable domain, and both capstone conclusions visible. It is not a claim to the first formalization of Arzelà–Ascoli. Mathlib Ascoli development, countable dense subsets.
Convergence at every point does not automatically mean uniform convergence. A permissible index threshold may depend on the point, and different pointwise limits may require different subsequences. Likewise, separate continuity of every does not give a single valid for all . Replacing these statements with their uniform versions silently changes the problem. Lebl’s bounded sequence on already rules out the naive implication from bounded continuous functions to a uniformly convergent subsequence. Example 11.6.3.
The formal challenge is to retain these distinctions across the representations of functions, convergence, and compactness. In particular, the countable-domain proposition must not acquire a compactness assumption, while the capstone must not acquire global bounds as an extra premise.
The development uses namespace LeblRA, arbitrary universe-polymorphic domain types, Lean’s complex numbers, and zero-based natural-number indices. Zero-based indexing only reindexes the source’s sequence starting at one. A strictly increasing map is represented by StrictMono; pointwise limits use Tendsto at atTop, uniform limits use TendstoUniformly, and density uses Dense. Finite and empty domains remain allowed.
The boundedness and equicontinuity hypotheses are written as explicit quantifiers, not new custom definitions. No claim may be replaced by a finite-domain special case, a vacuous hypothesis, or a statement that assumes its uniform conclusion.
Reusable infrastructure consists of complex norms, metric and compact spaces, continuous maps, uniform convergence, equicontinuity, and sequence compactness. The pinned environment is Lean 4.29.0-rc3 with Mathlib revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Source-faithful alternative proofs and explicit equivalences between the raw conditions and library predicates are welcome; applications beyond the four numbered targets are outside this scope. Uniform-convergence interface, sequence compactness.
777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, 2026. General Ascoli theorems, uniform convergence, topological bases and separability.Writing a positive integer as a sum of two squares is an elementary question with a precise general answer. Some integers have such a representation and others do not; checking a few small inputs does not explain the distinction. A criterion expressed through prime factorization instead decides the question for every positive integer. This project follows Section 5.7 of William Stein's Elementary Number Theory: Primes, Congruences, and Secrets, including the section's supporting statements and one subsequent exercise. The selected material connects divisibility, coprimality, algebraic identities, and rational approximation within a single classical topic. The source is the author-hosted January 2017 text, using its numbering rather than the numbering of earlier drafts.
A two-square representation of an integer consists of integers satisfying . Either coordinate may be zero or negative. A representation is primitive when the greatest common divisor of its coordinates is one; this restricts representations, not the definition of representability itself. For a positive integer and a prime , the prime exponent is the exponent of in the prime factorization of . The congruence means that division of by four leaves remainder three.
The approximation statement uses a real number , a positive integer , and a reduced fraction , where is an integer, is a positive integer, and their greatest common divisor is one. These conventions agree with Stein's section and its definition of primitive representations.
The supporting targets retain their complete source statements. Lemma 5.7.4 concerns every positive integer with a prime divisor :
Equation (5.7.1) is the integer identity
Lemma 5.7.5 states that, for every real and positive integer , some reduced fraction satisfies
The capstone, Theorem 5.7.1, is the complete equivalence
for every positive integer . Both implications are required. These four statements are located on printed pages 117–120 of the source PDF.
Exercise 5.11, on printed page 122, is an optional downstream target:
It describes gaps among represented integers and is not a prerequisite milestone for the capstone.
The criterion replaces a search for coordinates with a finite condition on the factorization of an input. It applies to composite integers as well as primes and distinguishes the exponent of a prime divisor from the mere presence of that divisor. The primitive obstruction also explains why a claim about coprime coordinates must not be confused with a claim that excludes all representations. The composition identity supplies an explicit statement of multiplicative closure, while the exercise gives a uniform restriction on consecutive runs. These are the consequences and accompanying results presented in Stein's treatment.
The mathematics is established, not an open research problem. Important formal ingredients already exist in Mathlib: the sum-of-two-squares development includes the arithmetic criterion and primitive obstruction, and the Diophantine approximation development supplies the bounded-denominator result. The work here is a source-aligned collection of exact theorem interfaces and independently checked proofs. Reusing those results does not claim a new proof of the classical mathematics or an exact transcription of Stein's argument.
A finite list of successful representations cannot establish an assertion about every positive integer. Similarly, a restriction on primitive representations is insufficient to settle general representability, because a nonprimitive pair is still a valid representation. The capstone must account for prime exponents and both directions of the equivalence simultaneously. The approximation result has its own coupled requirements: obtaining a small denominator without the stated error bound, or a good approximation with an uncontrolled denominator, does not meet the target. These distinctions are explicit in the source statements.
The namespace is SteinENT. Inputs use natural numbers, with positivity hypotheses wherever the source uses positive integers. Coordinates and all subtraction in the composition identity use integers. Prime exponents use Nat.factorization; primitivity uses Int.gcd x y = 1. Approximation witnesses use Lean's rational type, whose canonical numerator and positive denominator already express a reduced fraction. The error inequality is an inequality of real numbers. The gap exercise allows every integer starting point, including negative ones.
No hypothesis assumes the desired representation or restricts the capstone to a bounded test range. There is no additional definition that hides a proof obligation, and no separate alias item for primitivity. Standard Mathlib arithmetic, rational approximation, and tactic libraries provide reusable infrastructure. Complete alternative proofs are welcome when they preserve these interfaces, including the explicit positive-input boundary and unrestricted integer coordinates.
Formalization status, 29 September 2026: the main theorem and all nine linked milestones are Proved, with zero Open leaves. The selected proof uses the now-Proved Philippon Theorem 2.1 and the completed Weierstrass application bridges. The linked statements retain their explicit formalization conventions and intermediate variants.
Algebraic independence measures whether several complex numbers satisfy a polynomial relation with rational coefficients. For two numbers, independence means that no nonzero polynomial in two variables vanishes at that pair. This is stronger than asking that each number separately be transcendental: two transcendental numbers can still satisfy a polynomial relation with each other. The distinction matters when describing the arithmetic information carried jointly by periods, lattice invariants, and values of analytic functions.
The completed target is Theorem 1 of Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions (2026). It concerns ten numbers attached to a complex lattice and two evaluation points. The conclusion selects an algebraically independent pair from those ten entries; it does not specify that the pair must consist of two particular function values. The mathematical result is published, and this mission now supplies its checked Lean proof. A source comparison on 29 September 2026 checked the main theorem’s hypotheses, ten values, full-period quasi-period normalization and pair-independence conclusion. The main statement needs no correction.
Take complex numbers that are linearly independent over the real numbers. Their integer linear combinations form the period lattice
The formal representation is Mathlib's PeriodPair. Its lattice determines the Weierstrass elliptic function and invariants , using Mathlib's existing definitions. Thus the lattice, function, and invariants are linked by their construction; they are not unrelated parameters.
The Weierstrass zeta function is fixed by the lattice series
This is the normalization in DLMF equation 23.2.5. For a lattice element , its quasi-period is represented by
Both arguments lie outside the lattice. Relating this fixed increment to the increment at an arbitrary regular point is part of the established analytic infrastructure. The normalization concerns the full period ; references using half-periods require the corresponding factors of two, as in DLMF equation 23.2.11.
Let belong to . Suppose are linearly independent over and
Define the indexed tuple
The proved conclusion is
These are the hypotheses and conclusion of the paper's Theorem 1. No algebraicity assumption is imposed on or , and the conclusion does not assert independence of all ten entries.
The initial supporting targets are the two identities used in §4 of the paper. For , write . They assert
and
The statements preserve the paper's multiplied-out forms. They do not require . These targets supply reusable identities; proving them alone does not establish the arithmetic conclusion of Theorem 1.
| Milestone | Linked result |
|---|---|
| Equation (5) — zeta addition identity | Proved |
| Equation (6) — elliptic addition identity | Proved |
| Lemma 6 — entire regularization and interpolation bounds | Proved |
| Lemma 8 — bounded auxiliary polynomial (formal-grid variant) | Proved |
| Appendix A.2 — Weierstrass model realization (application bridge) | Proved |
| Appendix A.2 / Lemma A.1 — subgroup degrees (application bridge) | Proved |
| Proposition A.1 — zero estimate on the mission’s rank-one grid | Proved |
| Lemma 9 — bounded-order nonvanishing on the enlarged grid | Proved |
| Lemma 10 — nonzero small arithmetic elements (linear-degree variant) | Proved |
The grid and degree variants are described in the linked statements. The two application bridges identify the Weierstrass objects with the general group-theoretic objects used by Philippon’s theorem.
The completed goal certifies that every period pair and every triple satisfying the stated hypotheses yields an independent pair in the precise ten-entry tuple. In particular, a proof must handle arbitrary complex lattice invariants and arbitrary admissible evaluation points. A result for a preferred lattice, algebraic arguments, or a predetermined choice of indices would leave the requested statement unresolved.
The definitions provide a reusable interface for elliptic zeta values: a canonical series, a fixed quasi-period convention, and an explicit finite-family independence predicate. The main theorem and all nine milestones have checked proofs; the theorem pages record their accepted submissions and dependencies.
The central difficulty in the proof is passing from identities of analytic functions to exclusion of rational polynomial relations among selected complex values. Periodicity and the addition identities describe how values are related, but do not by themselves rule out algebraic dependence. Consequently, finishing the elementary function interface is only one part of the development.
The development also addresses a concrete analytic obligation in the chosen representation. An infinite-sum expression is a total Lean term even before summability is proved. Using it as the canonical analytic zeta function requires the appropriate convergence and differentiation results. The classical convergence statement is recorded in DLMF §23.2(ii); it is not introduced as an extra hypothesis of the main theorem.
All custom declarations use the namespace WeierstrassEllipticZeta. The lattice intersection is an equality of -submodules of . Rational linear independence and real linear independence have different roles: the first constrains the three inputs to the theorem, while the second is built into the period pair. Neither is replaced by numerical noncollinearity checks or approximate arithmetic.
The ten values form a Fin 10 family. The selected pair uses Mathlib's AlgebraicIndependent over , so repeated numerical values cannot supply an independent pair merely by occupying different indices. The existing assumptions imply that both evaluation points are outside the lattice; no extra exclusion hypothesis is needed for the goal. Supporting addition identities state their pole exclusions explicitly because Lean's totalized division also assigns values at zero denominators.
The linked intermediate targets identify the variants sufficient for the completed main proof: Lemma 8 uses the stated formal-grid formulation; Proposition A.1 concerns the mission’s rank-one grid; and Lemma 10 uses linear coordinate-degree bounds rather than the source’s sharper O(N/log N) bounds. These distinctions are explicit in the milestone statements. They do not add assumptions to the main theorem. Further contributions can simplify the checked proofs, improve these intermediate bounds, or extend the general results beyond the existing mission target.
Theorem 1 with only individual pole exclusions is an Open follow-up target. It retains the same nonzero period, rational linear independence, and ten-entry algebraic-independence conclusion, while replacing the lattice-intersection hypothesis with .
This extension is an additional deduction to formalize, not a numbered result of the paper, and no mathematical novelty is claimed. Its planned proof combines the completed Theorem 1 with a separate Chudnovsky period theorem and an arithmetic lemma recovering the quasi-period of an integer combination. These additional dependencies remain to be formalized. The mission's completed main goal and nine paper-related milestones continue to record the original scope.
Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, pinned revision 0df444a360eaa60ab8c11dca51a86af692955474 (Lean 4.33.1).(a) In a tennis match, you are the favorite, and win each point independently with probability . Let be odd positive integers greater than . You have the choice between playing a best-of- (i.e., you play points and whoever wins the majority of points wins the match), or a best-of- of best-of-'s (i.e., the match is won by winning the majority of "sets", and each "set" is won by winning the majority of points). Prove that your probability of winning the match is strictly greater by playing the best-of-.
(b) We now consider two generalizations: are odd positive integers, while is any positive integer, with all integers being greater than . You have the choice between playing a best-of-, or a best-of- of "sets", which are best-of-'s of "games", …, which are best-of-'s of "points". In both cases, now that may be even, it is possible for the players to tie, in which case the match winner is determined by an independent fair coin. Prove again that your probability of winning the match is strictly greater by playing the best-of-.
(c) We consider a further generalization where each completed "set" counts toward the match score in an independently random way:
with and , so players are still incentivized to win sets (previously we had , ). This random scoring rule is applied once per completed set, at the outermost layer only: the games and points inside a set are decided by plain majorities, with no randomness, and only the set's final result is scored. If you choose to play the best-of-, then each individual point counts as a set and is subject to the same randomness with probabilities . Prove that your probability of winning the match is still strictly greater by playing the best-of- (the fair-coin-on-ties convention continues).
(d) Continue from part (c), but change the fair-coin-on-ties convention so that you only win the match if you have a strictly greater match score than your opponent. Assuming , prove that your probability of winning the match is strictly greater by playing the best-of-.
Florian E. Dorner and Moritz Hardt, Don't Label Twice: Quantity Beats Quality when Comparing Binary Classifiers on a Budget, ICML 2024. arXiv:2402.02249 (v3, 8 April 2026).
The paper asks how to spend a fixed budget of noisy crowdworker labels when comparing two binary classifiers: one label each for many data points, or several labels per data point aggregated by majority vote. It proves, via Cramér's theorem, that one label each is asymptotically optimal, and states the finite-sample version as an open conjecture (Section 5, Conjecture 1), still open in the April 2026 revision. Its Section 3 displays the finite-sample inequality for the independent, homogeneous-label case and verifies it numerically over about five billion parameter settings.
Part (d) of this mission with one level of sets is that Section 3 inequality in tennis language. A point is a single crowdworker label being correct ( is the label accuracy); a set is a data point, whose test label is the majority of its labels; and the scoring rule is what the two classifiers do with that label. Writing for the worse classifier's accuracy and for the better one's, a set is scored to its winner when the better classifier alone matches the test label, ignored when the two classifiers agree, and scored to its loser when the worse classifier alone matches:
so that , and always holds because two classifiers of accuracy at least agree on at least half the data. Substituting into the paper's Proposition 1 recovers its gap-indicator probabilities exactly: , . The paper's inequality also allows and , which parts (c)–(d) exclude only because the inequality can fail to be strict at there; for the same argument covers those edge cases. The paper's Conjecture 1 as literally stated concerns a correlated-error setting (its Section 3.2) and is not claimed here.
Parts (a)–(c) go beyond the paper's setting: arbitrary nesting depth, a fair-coin tie rule, and no constraint on the ignore rate . The hypothesis in part (d) cannot be dropped: with one level, , , , , the single best-of-3 finishes strictly ahead with probability while three single points do so with probability .
"Greater than " is read as and each odd; the list of set sizes in (b)–(d) is nonempty. Laws are functions and every probability is a finite sum — no measure theory. The goal theorem is the conjunction of the four parts.
The Hardy--Littlewood circle method is the principal analytic tool for counting solutions to additive equations in integers. Introduced by Hardy and Ramanujan for the partition function and developed by Hardy and Littlewood in their Partitio Numerorum series (1920--1928), it produces asymptotic formulae for the number of representations of a large integer as a sum of terms drawn from a prescribed set — -th powers, primes, values of a polynomial.
Its engine is an estimate for exponential sums. If a sum , where , exhibits cancellation for every not well approximable by a rational with small denominator, the method delivers an asymptotic formula; if it does not, the method stalls. Weyl's inequality (Weyl 1916) was the first such estimate and remains the standard one for moderate .
A short timeline of the estimate this mission targets. Weyl (1916) proved the inequality below with the exponent , in the course of his work on uniform distribution. Hardy and Littlewood (1920--1928) built the circle method on it, obtaining for Waring's problem. Vinogradov (1935) replaced Weyl differencing by his mean value theorem, superior for large , reducing the bound to ; Wooley's efficient congruencing (2012) and the Bourgain--Demeter--Guth decoupling theorem (2016) settled the main conjecture of Vinogradov's mean value theorem. For small — and as the entry point to the subject — Weyl's inequality is still the right tool, and it is the natural first capstone for a formalization of the method.
For a real number write
the standard additive character of : it satisfies , , and exactly when .
For a real number write for the distance from to the nearest integer. It is periodic with period , vanishes exactly on , satisfies the triangle inequality, and is at most .
Given a finite set , its generating function is . The basic identity of the subject is
a consequence of the orthogonality relation .
A Weyl sum of degree is . The whole difficulty is to bound it for in the minor arcs — those admitting no rational approximation with small.
Fix . For every there is a constant such that whenever , , and ,
The intermediate targets, weakest first, are the milestone list: the counting identity, the Weyl differencing (squaring) step, the Farey covering with coprime numerator, the divisor bound , Hua's fourth-moment inequality for , and the degree-two case of the inequality itself.
The result itself. Weyl's inequality is what makes the minor arcs negligible. Applied with in the range it gives a power saving over the trivial bound , and integrating that saving over the minor arcs shows their contribution is smaller than the main term produced by the major arcs. Every classical application of the circle method — the asymptotic formula in Waring's problem, Vinogradov's three primes theorem, the Birch--Davenport theory of forms in many variables — passes through an estimate of this shape. Without it the method produces an identity, not a theorem.
Formalizing it. Mathlib currently contains the analytic prerequisites — Fourier characters on AddCircle, Dirichlet's approximation theorem, Abel summation, Gauss sums — but no circle-method apparatus whatsoever: no Weyl sums, no arc dissection, no singular series, no mean value estimates. This mission supplies the first layer. The foundational tier is already machine-checked: 53 theorems covering the character , the norm , the geometric sum bound , both orthogonality relations, both forms of Dirichlet's theorem, and the basic theory of , are published on the platform with verified proofs and may be imported freely. What remains open is the combinatorial and analytic core listed in the milestones. None of the milestone statements is currently formalized anywhere, to the best of our knowledge.
The obvious approach fails immediately. One would like to sum by comparing it to the linear case, where the geometric series gives outright. But for the summand is not a geometric progression and there is no closed form.
Weyl's device is to square and difference: , and the substitution turns the inner polynomial into one of degree in . Iterating times reduces to a linear sum, at the cost of raising the estimate to the power — which is why the saving is so weak for large , and why Vinogradov's method eventually supersedes it.
The genuine obstacles in a formalization are: (i) bookkeeping the shifted ranges produced by each differencing step, which are not and must be handled uniformly; (ii) the divisor bound , needed to count the for which the resulting linear coefficient is close to an integer, and which is not currently in Mathlib in this form; (iii) tracking the -dependent constants through iterations without the informal notation.
Statements are given over the Prove2Me default environment (Lean v4.30.0, Mathlib c5ea003), in the shared namespace CircleMethod, and build on two published definitions: CircleMethod_char (the character e and the norm nrm) and CircleMethod_genfun (the generating function f).
Conventions this mission commits to:
nrm θ = |θ - round θ|. Mathlib's round breaks ties upwards, so round is not an odd function; the characterisation to use is minimality, nrm θ ≤ |θ - n| for every integer n, which is published as CircleMethod.nrm_le.Finset.range N, that is , and is a natural number. Hypotheses 0 < N and 0 < q are stated explicitly rather than left implicit.∀ ε > 0, ∃ C > 0, ∀ …, X ≤ C * Y, with the constant quantified outside the parameters it may depend on and inside nothing else. Solvers should not weaken this by allowing to depend on , or .Real.rpow), not natural powers.Nat.Coprime a.natAbs q, which is the correct notion for a possibly negative numerator.One trivialising formalization to rule out: the goal must not be read with permitted to depend on , since then makes it vacuous. The quantifier order in the Lean statement already forbids this, and solvers should preserve it exactly.
Contributions welcome on any milestone independently; the divisor bound and the Farey covering are self-contained and need no other milestone. Both are reusable well beyond this mission.
Chapter 5 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) carries the minimum norm theory of Chapter 3 (Mission I of this series) from Hilbert space to arbitrary real normed spaces. The inner product is gone, so orthogonal projection is no longer available; its role is taken over by the Hahn–Banach theorem, in two classical forms. The extension form generalizes the projection theorem and yields a duality principle equating a minimum norm problem in a space with a maximization problem in its dual ; the geometric form (separating hyperplanes) extends that duality from subspaces to convex sets. These duality theorems are the backbone of the optimization theory in the remainder of the book — conjugate functionals (Ch. 7) and Lagrange duality (Ch. 8) both trace back to them.
Throughout, is a real normed linear space. A linear functional on is bounded if for some constant and all ; the least such is the norm . The (normed) dual is the space of bounded (equivalently, continuous) linear functionals with this norm; denotes . A functional is sublinear when and for . Vectors and are aligned when , and orthogonal when ; for , the complement consists of the functionals vanishing on , and for , consists of the vectors annihilated by every member of . A hyperplane is a maximal proper linear variety; closed hyperplanes are the level sets of nonzero bounded functionals. The support functional of a convex set is .
The goal is §5.13 Theorem 1 (Minimum Norm Duality): if has distance from a convex set with support functional , then
the maximum on the right being achieved by some ; and if the infimum is achieved by , then is aligned with .
The milestones trace the chapter's route there: boundedness continuity (§5.2); the Hahn–Banach theorem in sublinear form (§5.4 Theorem 1) with its norm-preserving extension and norming-functional corollaries; the annihilator identity for closed subspaces (§5.7 Theorem 1); the two subspace duality theorems and the alignment characterization of best approximations (§5.8 — the chapter's principal results); and the geometric form: Mazur's separation theorem, the support theorem, and Eidelheit's separation theorem (§5.12).
The §5.8 duality theorems are the exact normed-space analogue of the projection theorem: existence transfers to the dual problem (minimum norm problems should be formulated in a dual space to guarantee solutions — the chapter's methodological moral), orthogonality becomes alignment, and infinite-dimensional problems with finitely many constraints reduce to finite-dimensional dual problems. The geometric form underpins all of convex duality.
All results are classical and proved in the source. Mathlib contains the Hahn–Banach extension theorem and point/convex separation theorems, so several milestones are exercises in connecting Luenberger's formulations to existing library lemmas; the two §5.8 duality theorems, the alignment corollary, and the §5.13 convex duality theorem have no direct Mathlib counterpart and are the mission's genuinely new content.
Degenerate cases are the trap throughout. In §5.8 Corollary 1 the "only if" direction fails literally when is dense and (then and no nonzero aligned functional exists); the formalization therefore carries the hypothesis . In the separation theorems the strict inequality holds only on the interior of the convex set — on the set itself only survives — and nonemptiness hypotheses (of the interior, of , of the variety) are what make the "nonzero functional" claims true; dropping any of them creates false statements in trivial spaces. In §5.13 the support functional may take the value , so the dual maximum is formalized by two quantified inequalities (the witness achieves ; no admissible functional exceeds ) rather than by a real-valued supremum. The infimum in the primal problems need not be attained — attainment appears only as a hypothesis in the alignment clauses.
Real scalars throughout. The dual space is represented concretely as continuous linear maps X →L[ℝ] ℝ, and annihilators are written as explicit quantified conditions rather than named subspaces. Five notions the chapter needs and Mathlib lacks are published as definitions and used by the statements rather than inlined: alignment (), the support functional (, valued in the extended reals since it may be infinite), the total variation of a function on an interval, the normalized space , and the Riemann–Stieltjes integral (defined relationally, so that no existence claim is built into the definition). The Minkowski functional needed for Mazur's theorem is Mathlib's gauge. Minimum distances are infima ⨅ over coerced sets or submodules; in §5.8 Theorem 2 the dual-side supremum is a real sSup over , which is nonempty and bounded. Sublinearity in §5.4 is hypothesized exactly as in the source (subadditivity plus positive homogeneity plus continuity). Linear varieties are parametrized as with a Submodule ℝ X. No completeness of is assumed anywhere — the chapter's results are genuinely about normed spaces, and Hahn–Banach needs no completeness. The concrete dual of (§5.5) is in scope, and carries most of the mission's new infrastructure: Mathlib has the property of bounded variation (eVariationOn) but no total-variation norm, no normalized space , and no Riemann–Stieltjes integral — its StieltjesFunction is the different object of a monotone right-continuous function inducing a Borel measure, and its Riesz–Markov–Kakutani development represents positive functionals on by measures, not bounded functionals on by functions of bounded variation. This mission therefore publishes those notions as definitions and states the representation theorem in both directions. §5.3 (the Riesz–Fréchet theorem, i.e. self-duality of Hilbert space) is the one omission: Mathlib's InnerProductSpace.toDual already provides it. §5.6 (second dual, reflexivity) is definitional and likewise present in Mathlib.
The traveling salesman problem — visit cities by the cheapest round trip — is the most widely known problem in combinatorial optimization, and its central open question concerns a linear program. The subtour-elimination relaxation (the Held–Karp bound) replaces tours by fractional edge weights, and both in theory and in practice (it powers the lower bounds inside the Concorde solver) it is remarkably close to the true optimum. How close, in the worst case, is the integrality gap of the relaxation: the supremum of over metric instances. Explicit instance families push the gap up to ; the best proven upper bound sits just barely below . The 4/3 conjecture — the gap is exactly — has been the benchmark question of approximation algorithms for four decades.
An instance on cities is a cost function assigning to each ordered pair of cities a real cost , required to be a metric cost: symmetric (), zero on the diagonal (), and satisfying the triangle inequality . Nonnegativity follows; distinct cities at distance zero are allowed, as usual for metric TSP.
A tour visits every city exactly once and returns to its start. Formally a tour is given by an ordering: a permutation of the cities, traversed as and back to ; its cost is the sum of the costs of consecutive steps, and — written tspOpt c — is the minimum over all orderings.
The subtour-elimination (Held–Karp) relaxation replaces the tour by a fractional edge weight for each pair of cities. A weight vector is feasible (IsHeldKarp x) when it is symmetric with zero diagonal, has entries in , gives every city fractional degree two (), and crosses every nontrivial cut at least twice: for every set of cities other than and all cities, . The Held–Karp bound hkValue c is the infimum of over feasible (the double sum counts each edge twice, hence the ). The incidence vector of any tour is feasible, so always.
Together with the known lower-bound families this says the integrality gap is exactly . The goal carries no algorithm and no constant to improve: it is the terminal statement of the ladder, open in both directions (a proof or a counterexample instance would each settle it).
Five results over the same definitions: the relaxation is valid (); instance families force the gap arbitrarily close to ; tree doubling gives ; Wolsey's theorem gives , the classical upper bound; and the Karlin–Klein–Oveis Gharan record for some (FOCS 2022). The last milestone is a statement-level target: its known proof (max-entropy sampling, strongly Rayleigh polynomials) is far beyond current formalization practice, so the mission's usable proving frontier remains Wolsey — the milestone records the state of the art as a formal statement.
The 4/3 conjecture is the reference open problem of approximation algorithms: the quality of the subtour LP calibrates every algorithmic advance on TSP, and the conjectured extremal instances guide the search for better rounding schemes. The bound is also what practical solvers actually compute — branch-and-cut on this LP solves instances with tens of thousands of cities — so the conjecture is a statement about the observed tightness of the world's most-used combinatorial lower bound.
Nothing in this circle exists in any proof assistant: Mathlib has no TSP, no LP relaxations, no polyhedral combinatorics of tours. The mission's milestones force the base layer into existence — tours over Equiv.Perm, cut constraints over Finset, and, for the upper bounds, the parity and tree arguments (spanning trees against the LP, T-joins for the bound) whose infrastructure is reusable for matching theory and network design far beyond TSP.
The naive plan — round the LP solution to a tour — has no known analysis losing less than in general, and the half-integral extremal instances show the hard cases are structured and simple-looking at once. Christofides' matching argument is provably stuck at against the LP; forty years of work moved the constant by , and that advance needed an entirely new probabilistic toolkit. On the other side, no instance family with ratio above has ever been found despite extensive computational search over small instances (Benoit–Boyd and successors). Both directions of the goal are genuinely open territory.
The Lean model commits to: cities Fin n; costs c : Fin n → Fin n → ℝ with IsMetricCost (symmetry, zero diagonal, triangle inequality — nonnegativity is derived, and semimetrics are included as in the standard statement of the conjecture); tours as orderings π : Equiv.Perm (Fin n) traversed cyclically via finRotate, so every permutation denotes a Hamiltonian cycle and every Hamiltonian cycle is denoted; both optimal values as sInf over nonempty, bounded-below sets of reals, so they are genuine minima for n ≥ 3. The hypothesis 3 ≤ n is load-bearing: for n ≤ 2 the degree-2 constraints are infeasible, sInf ∅ = 0 by convention, and the bounds would be false — every theorem therefore carries it.
Welcome contributions: the milestones in any order — held_karp_le_opt is the natural entry point (the tour's incidence vector crosses every cut at least twice); integrality_gap_lower_bound needs the three-path instance family and a case analysis on its tours; tree_doubling_bound needs spanning trees against the LP; wolsey_bound adds the T-join/parity argument and is the summit. Reusable infrastructure — spanning tree polytopes, T-joins, Eulerian traversals, cut lemmas — is welcome as platform theorems. Graph-TSP (), path TSP, and asymmetric TSP are deliberately left to future missions; the Karlin–Klein–Oveis Gharan bound is stated as a milestone, but its sampling machinery is expected to arrive, if ever, as shared infrastructure built over many contributions.
Chapter 4 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) develops linear least-squares estimation as an application of the Hilbert space projection theorem formalized in Mission I of this series. The chapter's centerpiece is the classical Gauss–Markov theorem: among all linear unbiased estimators of an unknown parameter vector from noisy linear measurements, the estimator has minimum variance — componentwise, not merely in trace. This result is foundational for statistics and econometrics, and its Hilbert-space derivation is the cleanest known.
Measurements are modeled as , where is an -dimensional data vector, a known matrix () with linearly independent columns, an unknown -dimensional parameter vector, and a random -vector of measurement errors with and covariance , positive definite. A linear estimate is for a constant matrix ; it is unbiased when for every , which holds iff . The optimality criterion is the error second moment , and the book's key observation (p. 85) is that the problem splits into independent minimum norm problems, one per component, each solvable by the dual approximation theorem of Mission I.
Formally, randomness is carried by an abstract probability space: a measure space with a probability measure, random vectors as functions with explicit integrability hypotheses for all first and second moments, and .
The goal is §4.4 Theorem 1 (Gauss–Markov): with ,
with error covariance
Milestones: the deterministic least-squares estimate (§4.3 Theorem 1); the book's deterministic reduction — minimize the diagonal entries of subject to (p. 85); the minimum-variance estimate for random (§4.5 Theorem 1); and the information-form identities and (§4.5 Corollary 2).
The Gauss–Markov theorem justifies weighted least squares as the optimal linear unbiased procedure and is the standard benchmark against which biased and nonlinear estimators are measured. The minimum-variance estimate of §4.5 is the Bayesian counterpart with prior covariance ; the information-form identities connect the two and exhibit Gauss–Markov as the limit . Mission III builds the recursive (Kalman) estimator directly on these results.
All results are classical and proved in the source. Mathlib has mature measure-theoretic integration but, to date, no Gauss–Markov theorem and no linear estimation theory; the matrix milestones (trace reduction, information form) are also absent as stated. The probabilistic statements here are deliberately phrased with elementary integrals of products of real-valued components — no Bochner integration of vector-valued maps — so they are approachable with MeasureTheory.integral alone.
The subtlety is bookkeeping, not depth. Unbiasedness must be encoded as the algebraic constraint (the book proves the equivalence with for all ); the componentwise variance claim is strictly stronger than the trace claim and requires the per-component minimum norm argument, not a single matrix inequality. Positive definiteness of enters through invertibility of , which itself needs the linear independence of the columns of — dropping either hypothesis makes the goal false. In the probabilistic statements every integral needs an integrability hypothesis; the drafts supply integrability of all pairwise products of components, from which integrability of every derived expression follows.
Random vectors are plain functions Ω → Fin m → ℝ on a MeasurableSpace Ω with a probability measure μ; second moments are hypotheses of the form ∫ ω, ε ω i * ε ω j ∂μ = Q i j with explicit Integrable assumptions; no independence, Gaussianity, or distributional assumptions are used anywhere. Matrices are Matrix (Fin m) (Fin n) ℝ with Mathlib's Matrix.PosDef, nonconstructive inverse ⁻¹, and mulVec. Norms on parameter space are written as explicit finite sums of squares, avoiding any ambiguity between Euclidean and supremum norms on pi types. The estimators under comparison are strictly linear (, no affine offset), exactly as in the source; §4.5's affine extension (its Problem 6) is out of scope.
Luenberger's Optimization by Vector Space Methods (Wiley, 1969) organizes a large part of optimization theory around a single geometric idea: minimum norm problems in inner product spaces, solved by orthogonal projection. Chapter 3 is the technical heart of that program. Its projection theorem and normal equations underlie least-squares data fitting, Fourier approximation, minimum-energy control, and the whole statistical estimation theory of Chapter 4 — which Missions II and III of this series formalize on top of the present one.
Throughout, spaces are real. A pre-Hilbert space is a real vector space with an inner product inducing the norm ; a Hilbert space is a complete pre-Hilbert space. Vectors are orthogonal when ; for a subset , the orthogonal complement is the set of vectors orthogonal to every element of . Given , their Gram matrix is and its determinant is the Gram determinant. A linear variety is a translate of a subspace .
The goal is §3.10 Theorem 2, the dual approximation problem: for linearly independent and constants , among all satisfying the constraints
there is a unique vector of minimum norm, and it has the form
The milestone list follows the chapter's own development: the projection theorem in its pre-Hilbert form (§3.3 Theorem 1) and classical form (§3.3 Theorem 2), the orthogonal decomposition with (§3.4 Theorem 1), the normal equations and Gram matrices (§3.6), the Gram determinant formula for the minimum distance (§3.6 Theorem 1), best approximation by Fourier sums over orthonormal families (§3.7, §3.9), minimum norm over a linear variety (§3.10 Theorem 1), and the extension from subspaces to closed convex sets with its variational inequality characterization (§3.12 Theorem 1).
The dual approximation theorem converts an infinite-dimensional constrained minimum norm problem into an linear system — the book's model example of finite reduction, applied there to minimum-energy control of a motor (§3.11) and, in Chapter 4, to every linear estimation problem: least squares, Gauss–Markov, and recursive (Kalman) estimation are all instances of these results in a Hilbert space of random variables.
All results here are classical and proved in the source; the mission's product is a faithful machine-checked development with reusable statements. Mathlib already contains close relatives of several milestones (orthogonal projection onto complete subspaces, Submodule.orthogonal), so part of the work is connecting the book's formulations to that library; the Gram determinant distance formula and the dual approximation theorem itself have no direct Mathlib counterpart.
The individual milestones are standard Hilbert space theory. The care is in the statements, not tricks: the pre-Hilbert version of the projection theorem asserts uniqueness and the orthogonality characterization without existence, while existence requires completeness and closedness — conflating the two versions produces unprovable or vacuous statements. The Gram determinant formula requires the Gram matrix of the extended family , where index bookkeeping (Fin.snoc) is easy to get wrong. In §3.12 the variational inequality replaces the equality characterization valid for subspaces; the inequality direction is a known trap.
The development commits to: real scalars (the book allows complex; this series does not), an abstract space H : Type with [NormedAddCommGroup H] [InnerProductSpace ℝ H] and [CompleteSpace H] exactly where the source assumes a Hilbert space; subspaces as Submodule ℝ H with explicit IsClosed hypotheses; finite families as Fin n → H; Gram matrices as Matrix (Fin n) (Fin n) ℝ via Matrix.of; minimum distances as infima (⨅) over coerced submodules. Best approximation statements are phrased as explicit inequalities ‖x - m₀‖ ≤ ‖x - m‖ rather than through any projection operator, so they are usable without choosing Mathlib's orthogonalProjection API. Statements deliberately carry no more hypotheses than the source: §3.3 Theorem 1 and the normal equations hold in any real inner product space; completeness appears only where existence is claimed.
Proofs are expected to lean on Mathlib's inner product space library; contributions of reusable bridging lemmas (e.g. between ⨅-formulations and orthogonalProjection) are welcome as child lemmas via proof sketches.
A graph is -degenerate if every nonempty subgraph of has a vertex of degree at most . Erdős conjectured — this is Erdős problem #146 — that every fixed bipartite -degenerate graph satisfies
The conjecture was known in several cases: when one bipartition class has maximum degree at most , for -degenerate blow-ups of trees, and, for , for grids and certain critical 2-degenerate graphs. The best general bound was the weaker of Alon, Krivelevich and Sudakov.
This mission carries a complete Lean 4 formalisation refuting it at .
Theorem. There exist a fixed connected bipartite 2-degenerate graph and constants such that
for all sufficiently large . Since the conjectured bound at is , the excess is polynomial rather than constant, so the conjecture fails outright. A related conjecture of Erdős (problem #113) asserts that a bipartite graph is 2-degenerate if and only if ; Janzer had already disproved the reverse implication, and this result refutes the forward one.
The construction. The counterexample is built in layers: starting from a layer of size , each subsequent layer is , and every vertex is joined to its two parents . The result is connected, bipartite and 2-degenerate by construction, and is related to the complete degenerate graphs of Grzesik, Janzer and Nagy.
The lower bound comes from a sampled Hamming-ball graph. With , two disjoint copies are joined whenever their Hamming distance is at most , and each vertex is retained independently with probability . The two parameters are governed by the thresholds
and the construction needs a sampling exponent with . The lower threshold controls exclusion of the layered graph; the upper one controls whether the sampled host has more than edges.
Exclusion runs on a conditional-entropy functional over parent and child arrays. An array of conditional entropy has at most realisations, while requiring its children to survive sampling costs — which dominates the possible parent arrays whenever . An embedding of would therefore have to raise a bounded entropy potential by a fixed amount at each layer, which is impossible after enough layers. A second-moment argument shows the sampled graph still has edges, and padding extends the construction to every sufficiently large order.
The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers", Sections 1.2 and 5–8), and re-verified in this environment: every node is proved from [propext, Classical.choice, Quot.sound] alone, and each staged statement's elaborated type was checked to be identical to the original declaration's. The mission is offered as a curated, closed campaign whose definitions and lemmas — binary entropy and the pair kernel, the layered construction, the Hamming-ball host and its retention measure — are reusable foundations for further work in extremal graph theory.
This is the companion result to Erdős problem #180, the Erdős–Simonovits compactness conjecture, which is formalised in the same source chapter and published as a separate mission.
Erdős and Simonovits conjectured that forbidding a finite family of graphs cannot reduce the extremal number by more than a constant factor compared with forbidding one of its members: for every finite nonempty family whose members all contain a cycle, there should be some and with for all large . The cycle hypothesis is essential — the folklore family already defeats the original formulation — and the corrected conjecture is Erdős problem #180.
This mission carries a complete Lean 4 formalisation refuting it, and refuting it quantitatively: there is a finite family of connected bipartite graphs, each containing a cycle, with
The two bounds are separated by a polynomial factor , so no member can dominate the family up to any constant. The family is , where and are the admissible quotients of two properly -coloured templates built from the subdivisions of and . The upper bound comes from counting short paths in an -free graph: excluding bounds the number of vertices that fail to be centres of a subdivided , and excluding forces those vertices to form a vertex cover. The lower bound comes from incidence graphs of symplectic generalized quadrangles , with the characteristic of the underlying field chosen to suit the forbidden member — even for , odd for — which is exactly the freedom a family bound does not have.
The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers"), re-verified in this environment. Every node is proved; the mission is offered as a curated, closed campaign whose definitions and lemmas are reusable foundations for further work in extremal graph theory.
How fast do multicolour Ramsey numbers grow? Write for the least such that every colouring of the edges of with colours contains a monochromatic triangle. The classical bounds, essentially unimproved for decades, place between and , and Erdős asked repeatedly whether the truth is closer to the exponential lower end — his Problem 183 asks whether , i.e. whether the growth is genuinely superexponential.
This mission carries a complete Lean 4 formalisation resolving that question in the affirmative, with an explicit bound: for all sufficiently large , from which follows, together with the matching two-sided estimate pinning the sharp coefficients. The argument is constructive: it builds triangle-free colourings by a recursive palette construction whose colour count grows fast enough to beat every exponential.
The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science, re-verified in this environment. Every node is proved — the mission is offered as a curated, closed campaign whose milestones map the attack path and whose lemmas are reusable foundations for further work on multicolour Ramsey theory.
Erdős Problem 788 asks how large a set can always be retained when prescribed distinct pair-sums are forbidden. This mission formalizes the repository’s strengthened version of Theorem 1.1: an explicit lower bound valid for every , an eventual quantitative upper bound, the conclusion , and the exact affirmative answer to the original upper-bound question.
Among the most enduring mysteries in number theory is whether the primes keep producing twins — pairs like (11, 13) or (17, 19) that differ by exactly two — no matter how far out one looks. The general form was set down by Alphonse de Polignac in 1849, and the first deep theorem came from Viggo Brun in 1915, who proved that the reciprocals of the twin primes converge to a finite value, now called Brun's constant; in doing so he invented modern sieve theory and showed that twins must thin out even if there are infinitely many. Hardy and Littlewood went further, conjecturing a precise density of about 2C₂·x/(ln x)² for the count of twins below x. For nearly a century the infinitude itself stood untouched, until Yitang Zhang's stunning announcement on 17 April 2013 that some gap below 70 million recurs infinitely often — the first finite bound ever proved. A Polymath collaboration led by Terence Tao, together with James Maynard's independent multidimensional sieve, soon drove that bound down to 246, where it still stands. Closing the gap all the way to 2 — the twin prime conjecture itself — remains open. This mission states it cleanly: the set of primes p for which p + 2 is also prime is infinite.
Formulated in 1985 by Joseph Oesterlé and David Masser as an arithmetic distillation of Szpiro's conjecture on elliptic curves, the abc conjecture makes a deceptively simple claim about coprime triples with a + b = c: the three numbers cannot all be built from many repeated small primes at once, so c can only rarely exceed rad(abc)^(1+ε). Dorian Goldfeld called it 'the most important unsolved problem in Diophantine analysis,' and for good reason — a single proof would cascade through number theory, delivering Fermat's Last Theorem for all large exponents almost for free, along with Roth's theorem, the Mordell–Faltings theorem, the Fermat–Catalan conjecture, infinitely many non-Wieferich primes, and all but finitely many counterexamples to Beal's conjecture. Since 2012 Shinichi Mochizuki has claimed a proof via inter-universal Teichmüller theory, published in 2021, but the community has not accepted it: in 2018 Peter Scholze and Jakob Stix identified a gap they regarded as fatal. A precise formal statement gives everyone a shared, machine-checkable target around which to organize verified progress.
Classification of countable structures asks whether objects have the same structure and whether one problem can supply definable invariants for another. Borel reducibility makes this comparison precise: a Borel map must preserve and reflect isomorphism. A class is Borel complete when every countable-structure isomorphism problem reduces to it. Friedman and Stanley introduced a hierarchy of bounded-rank tree problems and asked whether receiving every countable level already forces completeness. The question is stated in their original paper, page 899. Friedman–Stanley, 1989.
The relevant chronology distinguishes that general question from particular examples:
A countable relational language has at most countably many symbols, each with finite arity. A structure on the natural numbers assigns a truth value to each symbol and each tuple of the appropriate length. Nullary symbols are allowed. The resulting countable product of two-point spaces has its canonical Borel sigma algebra. Two structures are isomorphic when a single permutation of the natural numbers preserves all relation values.
An invariant Borel class is a Borel subset of that structure space closed under isomorphism. Borelness of the class does not assert Borelness of its isomorphism relation. Graphs are simple undirected graphs on the fixed vertex set of natural numbers.
For relations and , the notation means that some measurable map between their specified Borel code spaces satisfies
for every pair of source points. Neither relation is assumed Borel merely by writing this comparison.
The benchmark is equality on Cantor space . At successors, compares enumerated countable sets of classes, with a distinct empty-set code; order and repetitions are ignored. At nonzero countable limits, the benchmark is a coordinatewise product along a fixed increasing cofinal sequence of smaller ordinals. Codes remain actual measurable sequence spaces, rather than quotient spaces of invariants.
The goal is Theorem 1.2 of the supplied manuscript, not Question 1.1, which shares its numbering counter. There should be one fixed countable language and one invariant Borel class such that
and, including the theorem's additional conclusion,
Here denotes bounded-rank rooted well-founded tree codes, including finite and empty trees. The manuscript compares its product-limit benchmarks with the usual hierarchy conventions in Proposition 4.13 and with the original tree hierarchy in Proposition 4.15. No identification of ordinal indices between different presentations is asserted.
The milestones retain the source's attack path: the classical Borelness of bounded-rank tree isomorphism from Friedman–Stanley Section 1.2.1; Proposition 3.6 on invariant real-valued graph parameters; Theorem 4.1 on cofinality of Polishable subgroup coset relations; and Proposition 4.15 comparing the original tree hierarchy with the product-limit tower. The first is published background; the other three are targets from the proposed research draft.
The target distinguishes being above every countable benchmark from being universal for all countable-structure classification problems. In the source's sentence formulation, it would give a negative answer to the question restated by Shelah and Ulrich. The structure-class formulation is the goal here; the infinitary-sentence corollary and the appendix's forcing and thickness claims are outside this mission.
The requested formalization is open. Local compilation validates the definitions and theorem interfaces, with explicit open-target placeholders; it does not verify the proposed mathematical proof. A completed development would provide reusable code-space constructions, ordinal-indexed comparison relations, bounded-tree interfaces, and permutation-group coset machinery.
The quantifier ranges over every countable ordinal, while the language and target class must remain fixed. Results restricted to finitely many jumps, or even to the omega level, do not settle this claim. The distinction between countable sets and countable multisets is also substantive: the original tree codes retain multiplicities, while the set jump forgets them. Friedman–Stanley, Section 1.2.
The class of structures must itself be Borel and invariant. Replacing that requirement by Borelness of its isomorphism graph changes the problem. Individual reductions may depend on the ordinal; the theorem does not require a single Borel selection of reductions over all codes for countable well-orders.
The Lean language bundle represents actual relational structures on by Boolean truth tables. The source allows functions and constants to be represented by relations; no structural axioms are imposed on the ambient space. A proposed target class must supply its own Borelness and invariance. Empty languages and empty classes are admitted by the interfaces, and no nontriviality is hidden in those definitions.
The tower uses native ordinal recursion below , equality on Cantor space, option-valued sequence codes for the set jump, and dependent countable products at limits. Fundamental sequences are fixed once; their strict increase and cofinality in the countable range are proved in the definition layer. This commits to the manuscript's product-limit presentation.
Tree codes are prefix-closed subsets of finite natural-number sequences. Isomorphisms are actual node bijections preserving and reflecting immediate parenthood. A global bound is expressed by an ordinal ranking into the bound, strictly decreasing along children; the empty tree has height zero and a single vertex height one. This specifies reverse-tree height explicitly and does not conflate the original convention with the separate leaf-zero padding convention. Finite and infinite branch multiplicities are retained.
The coset interface uses the actual group of permutations of with its standard Polish topology and the source convention . No normality or closedness of the image subgroup is assumed. Contributions developing the ordinal, measurable-space, tree, and topological-group prerequisites are welcome.
FriedmanStanleyQuestion.tex, Theorem 1.2; Proposition 3.6; Theorem 4.1; Propositions 4.13 and 4.15. Author field empty; no public manuscript URL supplied.Borel reducibility compares classification problems by asking whether one can assign invariants for one problem using the equivalence classes of another. The comparison is sensitive to the definability of the assignment: the coding map must be Borel measurable and must preserve and reflect equivalence. It is a standard organizing principle in invariant descriptive set theory, where the objects being classified often live in Polish spaces. Marker's course notes introduce this perspective and the underlying descriptive set theory.
An upper bound for a family of equivalence relations is a single relation receiving a Borel reduction from every member of that family. The distinction between countable unions of compact sets and countable unions of closed sets is essential here. Rosendal's work established universal behavior for the more restrictive compact-union setting. The present target asks how far the closed-union class can be bounded when the target may have arbitrary Borel complexity. Rosendal, 2005.
The relevant chronology is:
A Polish space is a topological space admitting a complete compatible metric and a countable dense subset. An set is a countable union of closed sets. A binary relation has an graph when its set of related pairs is in the product topology. A Borel equivalence relation is an equivalence relation whose graph belongs to the Borel sigma algebra generated by that product topology.
For equivalence relations on and on , write if there is a Borel measurable map satisfying
The domain and target sigma algebras are the Borel sigma algebras of the specified topologies. All Polish source spaces are admitted, including spaces that are neither compact nor sigma-compact.
For a subgroup of a group , the coset relation is exactly when , with classes . The subgroup need not be normal. For a real linear subspace, the additive convention is exactly when .
The main target is precisely Theorem 1 of the supplied note:
In Lean the assertion is stated for every Polish target . The target graph may belong to any Borel level.
Two new supporting milestones retain the source numbering. Lemma 2 is the category-transfer statement: for standard-Borel parameters and countably many jointly Borel families of continuous group homomorphisms, a common Borel upper bound for the coset relations outside a generated-subgroup membership set forces that membership set to be Borel. Corollary 4 states that the counterexamples can be coset relations of real linear subspaces in one fixed real . The earlier -target obstruction is a separate, already-published reference milestone.
The main statement rules out a single Borel classifier for the whole class, even when no fixed bound is imposed on the complexity of that classifier's graph. This is stronger than requiring the proposed upper bound itself to have an graph. The supplied note also draws consequences for higher levels of the Borel hierarchy; those consequences are outside the present goal.
The formalization would connect topological groups, descriptive set theory and real Banach-space coset relations in a reusable Lean development. The earlier reference result already has an accepted machine-checked proof. The new theorem and its new milestones are open formal statements: successful compilation of their interfaces checks their well-formedness and does not supply their proofs.
Increasing the permitted complexity of the target changes the problem materially. The earlier theorem's hypothesis on the target graph no longer applies. For the category-transfer milestone, the individual reductions are only assumed to exist; a Borel selection of them is not part of the hypotheses. For the Banach-space milestone, an algebraic linear image need not be closed, and the source imposes injectivity without assuming a closed range or a bounded inverse. These distinctions must survive the formalization.
The mission reuses the public definitions of graphs, Borel maps and relation reductions from the earlier mission. New definitions specify Borel graphs explicitly using borel (X × X), upper bounds over all Polish sources represented in Lean's ordinary type universe, algebraically generated subgroups, and native real lp with exponent . Targets are universe-polymorphic. Empty targets and empty Polish source spaces are included.
The category-transfer parameter space carries its given standard Borel structure. Group factors carry their own Polish group topologies; joint measurability uses the product of the parameter sigma algebra and each group's Borel sigma algebra. Generated subgroups are algebraic closures under group operations. No normality, compactness, sigma-compactness or measurable selection hypothesis is added.
The definitions contain no proof placeholders. The three new theorem interfaces deliberately use the platform's open-target placeholder. Contributions proving these targets or developing their measurable-category and Banach-space prerequisites are welcome. Baire-category coding, analytic separation, countable closed covers and the tensor-image analysis are reusable infrastructure needed by a complete development.
UniversalBorelEquivalence-20261101.tex; no public manuscript URL was supplied.