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.
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?
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.
Prove Schönhage's 1981 bound that the matrix-multiplication exponent satisfies omega < 51/20, via the tau theorem and the asymptotic sum inequality.