Formalized mathematics, verified by machine.
Browse community projects, take on Lean challenges, and get your proofs checked automatically by the Lean comparator.
- projects
- 236
- open problems
- 231
- solvers
- 0
- points awarded
- 0
Showing 1–60 of 236
p3group
Formalization of the classification of groups of order (p^3) in Lean 4
multi-hole-with-helpers regression example
Regression test for trusted-helper support in multi-hole problems. Exercises three failure modes the generator used to have: (1) helpers at root namespace (`rootHelper`) must not get a spurious `open`; (2) the helper na…
Bounded gaps between primes
Zhang's bounded-gaps theorem, sharpened by Maynard and the Polymath8 project: for every `n` there exist primes `p < q` with `n ≤ p` and `q - p ≤ 246`, the post-Polymath bound recorded by Knill. Equivalently, infinitely …
Wigner semicircle law
For an iid family X i j : Ω → ℝ of mean-0, variance-1 real random variables (parameterised over upper-triangular pairs i ≤ j), the empirical spectral measure of the real-symmetric matrix W_n / √n (with W_n(i, j) = X (mi…
Wiener–Lévy theorem
The Wiener–Lévy theorem, the analytic functional calculus for the Wiener algebra: if f lies in the Wiener algebra (`InWienerAlgebra f := Summable (fourierCoeff f)`) and φ is complex-analytic on an open neighbourhood U o…
Wiener's 1/f theorem
Wiener's lemma for the circle algebra: if a continuous function f on the additive circle has absolutely summable Fourier coefficients (i.e. lies in the Wiener algebra, `InWienerAlgebra f := Summable (fourierCoeff f)`) a…
Wiener's atom-detection formula
§66 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. Wiener's atom-detection formula states that for a probability measure μ on the circle ℝ/2πℤ, the Cesàro averages (1/N) ∑_{k=1}^N |μ̂_k|² of the squared F…
Wieferich's theorem g(3) = 9
Every natural number is a sum of nine cubes, and nine is necessary (23 is not a sum of eight cubes): the k=3 case of the Hilbert–Waring problem, g(3) = 9. The trusted helper IsSumOfCubes (non-hole) fixes 'sum of k cubes…
Whitney embedding theorem (strong form, dimension 2n)
Every smooth n-manifold (n ≥ 1, Hausdorff, second-countable) admits a smooth embedding into ℝ^(2n). The smooth-embedding triple — smooth, topological embedding (mathlib's `IsEmbedding`), and immersion (`mfderiv` injecti…
Weinstein conjecture in dimension three (Taubes 2007)
Every Reeb vector field of a contact form on a closed smooth 3-manifold has a closed periodic orbit. Mathlib lacks contact-geometry API and a manifold exterior derivative, so the encoding fixes dα by the intrinsic coord…
Weak Morse inequalities
§40 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement; the boxed main theorem is the strong Morse inequality). For a Morse function f on a closed smooth finite-dimensional Hausdorff manifold M,…
Watanabe's disproof of the 4-dimensional Smale conjecture
Resolves [Kir97, Problems 4.34 and 4.126] negatively: the 4-dimensional generalized Smale conjecture (O(5) ↪ Diff(S⁴) is a homotopy equivalence, equivalently Diff(D⁴ rel ∂) is contractible) is false. Watanabe showed πₖ(…
Wang-Zahl: the three-dimensional Kakeya conjecture
Every compact subset K of Euclidean three-space that contains a unit line segment in every unit direction has Hausdorff dimension 3. The trusted IsKakeya definition includes compactness, explicitly quantifies over norm-…
Seventeen wallpaper groups (Pólya–Niggli 1924)
There are exactly 17 wallpaper groups, the discrete cocompact subgroups of the planar Euclidean motion group E_2, counted up to affine equivalence. Discreteness is encoded as a properly discontinuous action on ℝ² — loca…
von Neumann double commutant theorem
The classical double commutant theorem: for a unital *-subalgebra of bounded operators on a complex Hilbert space, equality with the double commutant is equivalent to closedness in the weak operator topology and to clos…
variable-binder minimal example
Regression for https://github.com/leanprover/lean-eval/issues/276. The theorem inherits implicit binders from a preceding `variable` declaration, which the extractor must re-emit in the generated workspace.
Upper bound theorem for geometric simplicial spheres (Stanley 1975)
Among finite (d − 1)-dimensional simplicial spheres with n vertices, the cyclic polytope C(n, d) maximises every face number f_k. The Lean encoding `FiniteSimplicialSphere d` uses mathlib's `Geometry.SimplicialComplex ℝ…
Spencer-Szemerédi-Trotter unit-distance upper bound
For a finite set P ⊆ ℝ² write ν(P) for the number of unordered pairs at Euclidean distance 1, and ν(n) = max over n-point sets. Erdős posed the unit-distance problem in 1946 alongside the dual distinct-distances problem…
Uniformization theorem for Riemann surfaces
Uniformization theorem for Riemann surfaces
Tverberg's theorem
Any (r-1)(d+1)+1 points in ℝ^d can be partitioned into r parts whose convex hulls share a common point. Trusted helper HasTverbergPartition (non-hole). Mathlib has Radon's theorem (the r=2 case) but not Tverberg. Candid…
General recursive equals Turing computable
The Turing–Kleene equivalence (total form): a total function f : ℕ → ℕ is recursive (Computable) iff it is computed by some Turing machine (mathlib's FinTM2 model, TM2Computable) under the standard binary encoding encod…
Trace Cayley-Hamilton / Newton identity
The Newton trace recurrence for the coefficients of the characteristic polynomial: k cₖ + ∑_{j=1}^k tr(Aʲ) c_{k-j} = 0, where χ_A(X) = Xᴺ + c₁ Xᴺ⁻¹ + ⋯ + c_N. The helper charpolyDescendingCoeff packages cₖ as the degree…
Topological classification of surfaces
A compact connected surface with boundary is homeomorphic to one of the representative surfaces that we formalize.
Thue–Siegel–Roth theorem (irrationality measure ≤ 2 for algebraic irrationals)
Every irrational algebraic real is Diophantine: for every ε > 0 there exists C > 0 with C / q^(2+ε) < |x − p/q| for every p ∈ ℤ and q ∈ ℤ_{>0}. Equivalently, the irrationality measure of an algebraic irrational is at mo…
Avila-Jitomirskaya Ten Martini Problem
The theorem constructs the almost Mathieu operator as an actual Mathlib continuous linear endomorphism of `lp (fun _ : Int => Complex) 2`; `IsAlmostMathieuOperator` fixes it by the standard coordinate formula, rather th…
Szemerédi's theorem
§37 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (first additional statement of the section, generalizing Roth's theorem from 3-APs to k-APs). Every subset of ℕ of positive upper density contains arbitra…
Symplectic matrices have determinant 1
§39 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. For any commutative ring R and 2n × 2n symplectic matrix A over R (A * J * Aᵀ = J with J = [[0, -I], [I, 0]]), det A = 1. Taking determinants of AᵀJA = J…
Catalan generating function via compositional inversion
The compositional inverse of X - X² is the generating function for Catalan numbers. This is a classical application of Lagrange inversion in enumerative combinatorics, connecting formal power series inversion to Dyck pa…
Sturm separation theorem
Between consecutive zeros of one solution of a second-order linear homogeneous ODE, any linearly independent solution has exactly one zero.
Sturm's theorem
§97 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The number of distinct real roots of a squarefree real polynomial in an open interval equals the drop in the number of sign variations of its Sturm chain…
Strong Subadditivity of von Neumann Entropy
This fact is 'equivalent' to other facts such as the joint convexity of quantum relative entropy. First proved in 1973 by E.H. Lieb and M.B. Ruskai, but at least half-a-dozen alternate proofs have been published, with v…
Strong Mason conjecture for matroid independent sets
For a finite Mathlib `Matroid`, `independentSetCount M k` is exactly the number of independent `k`-element subsets of its ground set. The theorem is the division-free form of ultra-log-concavity of these counts: if the …
Local stable/unstable sets at a hyperbolic fixed point (set-level Hadamard–Perron)
For a C¹ map f : ℝⁿ → ℝⁿ with an invertible hyperbolic fixed point x₀ (no eigenvalue of dfₓ₀ on the unit circle, plus invertibility to exclude the degenerate zero-eigenvalue case), some open neighbourhood U ∋ x₀ carries…
Topological sphere theorem (Berger–Klingenberg–Rauch)
A closed, simply-connected, strictly quarter-pinched (sectional curvature in (1,4]) smooth Riemannian d-manifold (d ≥ 2) is homeomorphic to the standard d-sphere. Trusted helpers IsMetricCompatible, curv (Riemann curvat…
Differentiable sphere theorem (Brendle–Schoen)
Under the same hypotheses as the topological sphere theorem (closed, simply-connected, strictly quarter-pinched, d ≥ 2), the manifold is diffeomorphic to the standard d-sphere (Brendle–Schoen 2007, via Ricci flow). Shar…
230 space groups (Fedorov 1891 / Schoenflies 1891)
In dimension 3 there are exactly 230 space groups (orientation-preserving affine equivalence), 219 if enantiomorphic pairs are identified (general affine equivalence), and 65 of the 230 are Sohncke groups — those whose …
Solvable extensions ↔ solvable groups (the missing converse in Abel–Ruffini)
§58 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement). For F : Field of characteristic zero and a nonzero p : F[X], every root of p in AlgebraicClosure F lies in solvableByRad F (AlgebraicClos…
Sobolev embedding theorem (Morrey regime)
If n < p, 0 < α ≤ 1, and r + α < k − n/p, then every W^(k,p)(ℝⁿ) function has a C^(r,α) representative. Weak-derivative Sobolev spaces W^(k,p) are defined via the distributional pairing ∫ f · D^m φ = (−1)^|m| ∫ g · φ on…
Pannwitz–Kuperberg quadrisecant theorem
Every smooth knot that is not the unknot has a quadrisecant (a line meeting it in four points). Trusted helpers (IsSmoothKnot, IsUnknotted, HasQuadrisecant, …) are non-holes. Mathlib has no knot theory. The Fáry–Milnor …
Smale conjecture (Hatcher) in relative parameterized form
Hatcher's 1983 theorem that Diff(S3) is homotopy equivalent to O(4), stated in the relative-parameterized-family form (families on a compact manifold-with-boundary X whose boundary already factors through O(4) deform re…
Shannon capacity of the pentagon
Lovász's computation: the Shannon capacity of the five-cycle C₅ is √5. The helpers IsIndependent, independenceNumber, strongPower, and HasShannonCapacity encode the capacity as the limit of (α(Gᵏ))^{1/k}, modelling leng…
Shafarevich's theorem on solvable Galois groups
Every finite solvable group is realizable as a Galois group over ℚ: the solvable case of the inverse Galois problem. Mathlib has IsSolvable and the Galois correspondence, but nothing about realizability — no embedding p…
Shafarevich's relation-rank bound
For a number field F and odd prime p, with G = Gal(F^{un,p}/F) the Galois group of the maximal unramified pro-p extension, the relation rank r(G) = dim_{𝔽_p} H²(G; 𝔽_p) is finite and r(G) ≤ d(G) + (r₁ + r₂ - 1) + δ_p(…
Radial symmetry for positive semilinear Poisson solutions
Radial symmetry for positive semilinear Poisson solutions
Schreier's conjecture: outer automorphism group of a finite simple group is solvable
For every finite non-abelian simple group S, Out(S) := Aut(S)/Inn(S) is solvable. The statement requires the normality of Inn(S) ⊴ Aut(S), which is supplied by a local instance with a one-line proof (the conjugate of co…
Schoenflies theorem
§48 of Knill's 'Some Fundamental Theorems in Mathematics'. Strong form: every Jordan curve in the plane is the image of the unit circle under some self-homeomorphism of ℝ². This is the faithful encoding of Knill's prose…
Schläfli classification of regular polytopes
§42 of Knill's 'Some Fundamental Theorems in Mathematics'. Schläfli's dimension-by-dimension enumeration of the regular convex polytopes: p_3 = 5 (Euclid XIII — the five Platonic solids), p_4 = 6 (Schläfli's six regular…
Schauder fixed-point theorem
§60 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement). The Banach-space generalization of Brouwer: every continuous self-map of a nonempty compact convex subset of a real Banach space has a fi…
Sard's theorem (critical-set image has measure zero)
For a smooth map f : ℝᵐ → ℝⁿ, the image of the rank-deficient locus {x | rank df(x) < m ∧ rank df(x) < n} has Lebesgue measure zero. This is Knill's specific phrasing — the standard textbook Sard theorem uses the larger…
Runge's theorem
Basic Runge approximation theorem for compact subsets of ℂ. The statement uses polynomials p q : ℂ[X] and requires q to be nonvanishing on K, expressing rational functions with no poles on K. This does not include the s…
Rouche theorem via zero counting
Phrases Rouché's theorem as equality of multiplicity-counted zero counts for f and f + g on the closed disk of radius R.
Rokhlin lemma
§109 of Knill's 'Some Fundamental Theorems in Mathematics'. Every aperiodic measure-preserving automorphism of a standard Borel probability space admits, for every height n and every ε > 0, a measurable tower base B suc…
Riesz's rising sun lemma
Every continuous real function on a compact interval has the rising-sun property: the shadow set is open, empty iff the function is antitone, else a disjoint union of open intervals with f(c_n) ≤ f(d_n). Trusted helpers…
Lagarias criterion is equivalent to RH
Lagarias' elementary divisor-sum criterion stated using Mathlib's RiemannHypothesis, harmonic numbers, and sigma notation.
Sard's regular-value corollary
For a smooth f : ℝᵐ → ℝ, almost every c ∈ ℝ is a regular value (every point of f⁻¹(c) has nonzero derivative). The measure-theoretic heart of the regular-value form of Sard's theorem; the main critical-set-null Sard the…
Ramanujan–Petersson conjecture for the τ-function (Deligne's theorem)
τ(n) is the n-th q-expansion coefficient of mathlib's modular discriminant ModularForm.discriminant = η²⁴, the normalised cusp form of weight 12 and level 1; the module proves τ(1) = 1 as a sanity check. Ramanujan (1916…
Radon transform: Fourier-slice diagonalization and pseudo-inversion
The Fourier slice theorem diagonalizes the Radon transform (1D Fourier of a projection = a 2D-Fourier slice), and the transform has a left inverse on Schwartz functions. Trusted helpers radon, fourier1, fourier2 (non-ho…
Entrywise exponential of a PSD matrix is PSD
Part of the Schur-Polya-Loewner theory of entrywise functions preserving PSD. The proof uses the Schur product theorem iteratively: exp_⊙(A) = ∑ A^{⊙k}/k!, each Hadamard power is PSD, and the convergent series of PSD ma…