1000+ theorems

Freek Wiedijk started the 1000+ theorems project tracking progress of theorem provers in formalizing named theorems on wikipedia, as a way of comparing prominent theorem provers. Currently 37 of them are formalized in Lean. We also have a page with the theorems from the list not yet in Lean.

To make updates to this list, please make a pull request to mathlib after editing the yaml source file. This can be done entirely on GitHub, see "Editing files in another user's repository".

: Pythagorean theorem #

Author: Joseph Myers

theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 p2 p3 : P) :
dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 ↔ EuclideanGeometry.angle p1 p2 p3 = Real.pi / 2

docs, source

: Binomial theorem #

Author: Chris Hughes

theorem add_pow {R : Type u_1} [CommSemiring R] (x y : R) (n : ℕ) :
(x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)

docs, source

: Mean value theorem #

Author: Yury G. Kudryashov

theorem exists_deriv_eq_slope (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) :
∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a)

docs, source

: De Moivre's theorem #

Author: Abhimanyu Pallavi Sudhir

theorem Complex.cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) :
(Complex.cos z + Complex.sin z * Complex.I) ^ n = Complex.cos (↑n * z) + Complex.sin (↑n * z) * Complex.I

docs, source

: Gödel's incompleteness theorem #

Author: Shogo Saito

: Solutions of a general cubic equation #

Author: Jeoff Lee

theorem Theorems100.cubic_eq_zero_iff {K : Type u_1} [Field K] (a b c d : K) {ω p q r s t : K} [Invertible 2] [Invertible 3] (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3) (hp : p = (3 * a * c - b ^ 2) / (9 * a ^ 2)) (hp_nonzero : p ≠ 0) (hq : q = (9 * a * b * c - 2 * b ^ 3 - 27 * a ^ 2 * d) / (54 * a ^ 3)) (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
a * x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔ x = s - t - b / (3 * a) ∨ x = s * ω - t * ω ^ 2 - b / (3 * a) ∨ x = s * ω ^ 2 - t * ω - b / (3 * a)

docs, source

: Independence of the continuum hypothesis #

Authors: Floris van Doorn and Jesse Michael Han

: Intermediate value theorem #

Authors: Rob Lewis and Chris Hughes

theorem intermediate_value_Icc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) :
Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b

docs, source

: Wilson's theorem #

Author: Chris Hughes

theorem ZMod.wilsons_lemma (p : ℕ) [Fact (Nat.Prime p)] :
↑(p - 1).factorial = -1

docs, source

: Ptolemy's theorem #

Author: Manuel Candales

theorem EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a b c d p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hapc : EuclideanGeometry.angle a p c = Real.pi) (hbpd : EuclideanGeometry.angle b p d = Real.pi) :
dist a b * dist c d + dist b c * dist d a = dist a c * dist b d

docs, source

: Stirling's theorem #

Authors: Moritz Firsching and Fabian Kruse and Nikolas Kuhn and Heather Macbeth

theorem Stirling.tendsto_stirlingSeq_sqrt_pi :
Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds √Real.pi)

docs, source

: Quadratic reciprocity theorem #

Authors: Chris Hughes (first) and Michael Stoll (second)

theorem legendreSym.quadratic_reciprocity {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) :
legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

docs, source

theorem jacobiSym.quadratic_reciprocity {a b : ℕ} (ha : Odd a) (hb : Odd b) :
jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a

docs, source

: Cantor's theorem #

Authors: Johannes Hölzl and Mario Carneiro

theorem Function.cantor_surjective {α : Type u_4} (f : α → Set α) :
¬Function.Surjective f

docs, source

: Solutions of a general quartic equation #

Author: Thomas Zhu

theorem Theorems100.quartic_eq_zero_iff {K : Type u_1} [Field K] (a b c d e : K) {p q r s u v w : K} [Invertible 2] (ha : a ≠ 0) (hp : p = (8 * a * c - 3 * b ^ 2) / (8 * a ^ 2)) (hq : q = (b ^ 3 - 4 * a * b * c + 8 * a ^ 2 * d) / (8 * a ^ 3)) (hq_nonzero : q ≠ 0) (hr : r = (16 * a * b ^ 2 * c + 256 * a ^ 3 * e - 3 * b ^ 4 - 64 * a ^ 2 * b * d) / (256 * a ^ 4)) (hu : u ^ 3 - p * u ^ 2 - 4 * r * u + 4 * p * r - q ^ 2 = 0) (hs : s ^ 2 = u - p) (hv : v ^ 2 = 4 * s ^ 2 - 8 * (u - q / s)) (hw : w ^ 2 = 4 * s ^ 2 - 8 * (u + q / s)) (x : K) :
a * x ^ 4 + b * x ^ 3 + c * x ^ 2 + d * x + e = 0 ↔ x = (-2 * s - v) / 4 - b / (4 * a) ∨ x = (-2 * s + v) / 4 - b / (4 * a) ∨ x = (2 * s - w) / 4 - b / (4 * a) ∨ x = (2 * s + w) / 4 - b / (4 * a)

docs, source

: Dirichlet's theorem on arithmetic progressions #

Author: David Loeffler, Michael Stoll

theorem Nat.setOf_prime_and_eq_mod_infinite {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) :
{p : ℕ | Nat.Prime p ∧ ↑p = a}.Infinite

docs, source

: Bertrand's postulate #

Authors: Bolton Bailey and Patrick Stevens

theorem Nat.bertrand (n : ℕ) (hn0 : n ≠ 0) :
∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n

docs, source

: Cayley–Hamilton theorem #

Author: Kim Morrison

theorem Matrix.aeval_self_charpoly {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
(Polynomial.aeval M) M.charpoly = 0

docs, source

: Abel–Ruffini theorem #

Author: Thomas Browning

theorem AbelRuffini.exists_not_solvable_by_rad :
∃ (x : ℂ), IsAlgebraic ℚ x ∧ ¬IsSolvableByRad ℚ x

docs, source

: Fundamental theorem of arithmetic #

Author: Chris Hughes

theorem Nat.primeFactorsList_unique {n : ℕ} {l : List ℕ} (h₁ : l.prod = n) (h₂ : ∀ p ∈ l, Nat.Prime p) :
l.Perm n.primeFactorsList

docs, source

instance Int.euclideanDomain :
EuclideanDomain ℤ

docs, source

instance EuclideanDomain.to_principal_ideal_domain {R : Type u} [EuclideanDomain R] :
IsPrincipalIdealRing R

docs, source

class UniqueFactorizationMonoid (α : Type u_2) [CancelCommMonoidWithZero α] extends IsWellFounded α DvdNotUnit :
Prop

docs, source

theorem UniqueFactorizationMonoid.factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {f g : Multiset α} (hf : ∀ x ∈ f, Irreducible x) (hg : ∀ x ∈ g, Irreducible x) (h : Associated f.prod g.prod) :
Multiset.Rel Associated f g

docs, source

it also has a generalized version, by showing that every Euclidean domain is a unique factorization domain, and showing that the integers form a Euclidean domain.

: Lagrange's four-square theorem #

Author: Chris Hughes

theorem Nat.sum_four_squares (n : ℕ) :
∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

docs, source

: Solutions to Pell's equation #

Author: Mario Carneiro (first), Michael Stoll (second)

theorem Pell.eq_pell {a : ℕ} (a1 : 1 < a) {x y : ℕ} (hp : x * x - Pell.d✝ a1 * y * y = 1) :
∃ (n : ℕ), x = Pell.xn a1 n ∧ y = Pell.yn a1 n

docs, source

theorem Pell.exists_of_not_isSquare {d : ℤ} (h₀ : 0 < d) (hd : ¬IsSquare d) :
∃ (x : ℤ) (y : ℤ), x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

docs, source

In pell.eq_pell, d is defined to be a*a - 1 for an arbitrary a > 1.

: Fermat's theorem on sums of two squares #

Author: Chris Hughes

theorem Nat.Prime.sq_add_sq {p : ℕ} [Fact (Nat.Prime p)] (hp : p % 4 ≠ 3) :
∃ (a : ℕ) (b : ℕ), a ^ 2 + b ^ 2 = p

docs, source

: Ramsey's theorem #

Author: Bhavik Mehta

: Stone–Weierstrass theorem #

Authors: Scott Morrison and Heather Macbeth

theorem ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints) :
A.topologicalClosure = ⊤

docs, source

: Erdős–Szekeres theorem #

Author: Bhavik Mehta

theorem Theorems100.erdos_szekeres {α : Type u_1} [LinearOrder α] {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : Function.Injective f) :
(∃ (t : Finset (Fin n)), r < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ (t : Finset (Fin n)), s < t.card ∧ StrictAntiOn f ↑t

docs, source

: Cantor–Bernstein–Schroeder theorem #

Author: Mario Carneiro

theorem Function.Embedding.schroeder_bernstein {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hf : Function.Injective f) (hg : Function.Injective g) :
∃ (h : α → β), Function.Bijective h

docs, source

: Euler's partition theorem #

Authors: Bhavik Mehta and Aaron Anderson

theorem Theorems100.partition_theorem (n : ℕ) :
(Nat.Partition.odds n).card = (Nat.Partition.distincts n).card

docs, source

: Minkowski's theorem #

Authors: Alex J. Best and Yaël Dillies

theorem MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E} [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {L : AddSubgroup E} [Countable ↥L] (fund : MeasureTheory.IsAddFundamentalDomain (↥L) F μ) (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s) (h : μ F * 2 ^ Module.finrank ℝ E < μ s) :
∃ (x : ↥L), x ≠ 0 ∧ ↑x ∈ s

docs, source

: Taylor's theorem #

Author: Moritz Doll

theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x) (hf : ContDiffOn ℝ (↑n) f (Set.Icc x₀ x)) (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ x' ∈ Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1).factorial

docs, source

theorem taylor_mean_remainder_cauchy {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x) (hf : ContDiffOn ℝ (↑n) f (Set.Icc x₀ x)) (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ x' ∈ Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x') ^ n / ↑n.factorial * (x - x₀)

docs, source

: Brouwer fixed-point theorem #

Author: Brendan Seamas Murphy

in Lean 3

: Fundamental theorem of calculus #

Authors: Yury G. Kudryashov (first) and Benjamin Davidson (second)

theorem intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
HasStrictDerivAt (fun (u : ℝ) => ∫ (x : ℝ) in a..u, f x) c b

docs, source

theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E} (hab : a ≤ b) (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : ∀ x ∈ Set.Ioo a b, HasDerivWithinAt f (f' x) (Set.Ioi x) x) (f'int : IntervalIntegrable f' MeasureTheory.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a

docs, source

: Euclid's theorem #

Author: Jeremy Avigad

theorem Nat.exists_infinite_primes (n : ℕ) :
∃ (p : ℕ), n ≤ p ∧ Nat.Prime p

docs, source

: Bézout's theorem #

Author: mathlib

theorem Nat.gcd_eq_gcd_ab (x y : ℕ) :
↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

docs, source

: Bertrand's ballot theorem #

Authors: Bhavik Mehta and Kexing Ying

theorem Ballot.ballot_problem (q p : ℕ) :
q < p → (ProbabilityTheory.uniformOn (Ballot.countedSequence p q)) Ballot.staysPositive = (↑p - ↑q) / (↑p + ↑q)

docs, source

: Friendship theorem #

Authors: Aaron Anderson and Jalex Stark and Kyle Miller

theorem Theorems100.friendship_theorem {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : Theorems100.Friendship G) [Nonempty V] :
Theorems100.ExistsPolitician G

docs, source

: Euclid–Euler theorem #

Author: Aaron Anderson

theorem Theorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n) (perf : n.Perfect) :
∃ (k : ℕ), Nat.Prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1)

docs, source

: Uncountability of the continuum #

Author: Floris van Doorn

theorem Cardinal.not_countable_real :
¬Set.univ.Countable

docs, source