100 theorems

Freek Wiedijk maintains a list tracking progress of theorem provers in formalizing 100 classic theorems in mathematics as a way of comparing prominent theorem provers. Currently 80 of them are formalized in Lean. We also have a page with the theorems from the list not yet in Lean.

1. The Irrationality of the Square Root of 2 #

Author: mathlib

theorem irrational_sqrt_two :
Irrational √2

docs, source

2. Fundamental Theorem of Algebra #

Author: Chris Hughes

theorem Complex.exists_root {f : Polynomial ℂ} (hf : 0 < f.degree) :
∃ (z : ℂ), f.IsRoot z

docs, source

3. The Denumerability of the Rational Numbers #

Author: Chris Hughes

instance Rat.instDenumerable :
Denumerable ℚ

docs, source

4. 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

6. Gödel’s Incompleteness Theorem #

Author: Shogo Saito

results

website

7. Law of Quadratic Reciprocity #

Author: 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

9. The Area of a Circle #

Authors: James Arthur, Benjamin Davidson, and Andrew Souther

theorem Theorems100.area_disc (r : NNReal) :
MeasureTheory.volume (Theorems100.disc ↑r) = ↑NNReal.pi * ↑r ^ 2

docs, source

10. Euler’s Generalization of Fermat’s Little Theorem #

Author: Chris Hughes

theorem Nat.ModEq.pow_totient {x n : ℕ} (h : x.Coprime n) :
x ^ n.totient ≡ 1 [MOD n]

docs, source

11. The Infinitude of Primes #

Author: Jeremy Avigad

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

docs, source

14. Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. #

Authors: Marc Masdeu, David Loeffler

theorem hasSum_zeta_two :
HasSum (fun (n : ℕ) => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6)

docs, source

15. Fundamental Theorem of Integral Calculus #

Author: 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

16. Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem) #

Author: Thomas Browning

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

docs, source

17. De Moivre’s Formula #

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

18. Liouville’s Theorem and the Construction of Transcendental Numbers #

Author: Jujian Zhang

theorem Liouville.transcendental {x : ℝ} (lx : Liouville x) :
Transcendental ℤ x

docs, source

19. Four Squares 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

20. All Primes (1 mod 4) Equal the Sum 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

22. The Non-Denumerability of the Continuum #

Author: Floris van Doorn

theorem Cardinal.not_countable_real :
¬Set.univ.Countable

docs, source

23. Formula for Pythagorean Triples #

Author: Paul van Wamelen

theorem PythagoreanTriple.classification {x y z : ℤ} :
PythagoreanTriple x y z ↔ ∃ (k : ℤ) (m : ℤ) (n : ℤ), (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

docs, source

24. The Independence of the Continuum Hypothesis #

Author: Jesse Michael Han and Floris van Doorn

result

website

see the README file in the linked repository.

25. Schroeder-Bernstein 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

26. Leibniz’s Series for Pi #

Author: Benjamin Davidson

theorem Real.tendsto_sum_pi_div_four :
Filter.Tendsto (fun (k : ℕ) => ∑ i ∈ Finset.range k, (-1) ^ i / (2 * ↑i + 1)) Filter.atTop (nhds (Real.pi / 4))

docs, source

27. Sum of the Angles of a Triangle #

Author: Joseph Myers

theorem EuclideanGeometry.angle_add_angle_add_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 p2 p3 : P} (h2 : p2 ≠ p1) (h3 : p3 ≠ p1) :
EuclideanGeometry.angle p1 p2 p3 + EuclideanGeometry.angle p2 p3 p1 + EuclideanGeometry.angle p3 p1 p2 = Real.pi

docs, source

30. The Ballot Problem #

Authors: Bhavik Mehta, Kexing Ying

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

docs, source

31. Ramsey’s Theorem #

Author: Bhavik Mehta

result

34. Divergence of the Harmonic Series #

Authors: Anatole Dedecker, Yury Kudryashov

theorem Real.tendsto_sum_range_one_div_nat_succ_atTop :
Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, 1 / (↑i + 1)) Filter.atTop Filter.atTop

docs, source

35. 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

36. Brouwer Fixed Point Theorem #

Author: Brendan Seamas Murphy

result

37. The Solution of a Cubic #

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

38. Arithmetic Mean/Geometric Mean #

Author: Yury G. Kudryashov

theorem Real.geom_mean_le_arith_mean_weighted {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) :
∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i

docs, source

39. Solutions to Pell’s Equation #

Authors: 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.

40. Minkowski’s Fundamental Theorem #

Authors: Alex J. Best, 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

42. Sum of the Reciprocals of the Triangular Numbers #

Authors: Jalex Stark, Yury Kudryashov

theorem Theorems100.inverse_triangle_sum (n : ℕ) :
∑ k ∈ Finset.range n, 2 / (↑k * (↑k + 1)) = if n = 0 then 0 else 2 - 2 / ↑n

docs, source

44. The 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

45. The Partition Theorem #

Authors: Bhavik Mehta, Aaron Anderson

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

docs, source

46. The Solution of the 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

49. The 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

51. Wilson’s Lemma #

Author: Chris Hughes

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

docs, source

52. The Number of Subsets of a Set #

Author: mathlib

theorem Finset.card_powerset {α : Type u_1} (s : Finset α) :
s.powerset.card = 2 ^ s.card

docs, source

54. Königsberg Bridges Problem #

Author: Kyle Miller

theorem Konigsberg.not_isEulerian {u v : Konigsberg.Verts} (p : Konigsberg.graph.Walk u v) (h : p.IsEulerian) :
False

docs, source

55. Product of Segments of Chords #

Author: Manuel Candales

theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi {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}) (hapb : EuclideanGeometry.angle a p b = Real.pi) (hcpd : EuclideanGeometry.angle c p d = Real.pi) :
dist a p * dist b p = dist c p * dist d p

docs, source

57. Heron’s Formula #

Author: Matt Kempster

theorem Theorems100.heron {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 p2 p3 : P} (h1 : p1 ≠ p2) (h2 : p3 ≠ p2) :
let a := dist p1 p2; let b := dist p3 p2; let c := dist p1 p3; let s := (a + b + c) / 2; 1 / 2 * a * b * Real.sin (EuclideanGeometry.angle p1 p2 p3) = √(s * (s - a) * (s - b) * (s - c))

docs, source

58. Formula for the Number of Combinations #

Author: mathlib

theorem Finset.card_powersetCard {α : Type u_1} (n : ℕ) (s : Finset α) :
(Finset.powersetCard n s).card = s.card.choose n

docs, source

theorem Finset.mem_powersetCard {α : Type u_1} {n : ℕ} {s t : Finset α} :
s ∈ Finset.powersetCard n t ↔ s ⊆ t ∧ s.card = n

docs, source

59. The Laws of Large Numbers #

Author: Sébastien Gouëzel

theorem ProbabilityTheory.strong_law_ae {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (X : ℕ → Ω → E) (hint : MeasureTheory.Integrable (X 0) μ) (hindep : Pairwise ((fun (x1 x2 : Ω → E) => ProbabilityTheory.IndepFun x1 x2 μ) on X)) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) :
∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))

docs, source

60. Bezout’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

62. Fair Games Theorem #

Author: Kexing Ying

theorem MeasureTheory.submartingale_iff_expected_stoppedValue_mono {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) :
MeasureTheory.Submartingale f 𝒢 μ ↔ ∀ (τ π : Ω → ℕ), MeasureTheory.IsStoppingTime 𝒢 τ → MeasureTheory.IsStoppingTime 𝒢 π → τ ≤ π → (∃ (N : ℕ), ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ

docs, source

63. Cantor’s Theorem #

Author: mathlib

theorem Cardinal.cantor (a : Cardinal.{u}) :
a < 2 ^ a

docs, source

64. L’Hopital’s Rule #

Author: Anatole Dedecker

theorem deriv.lhopital_zero_nhds {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ} (hdf : ∀ᶠ (x : ℝ) in nhds a, DifferentiableAt ℝ f x) (hg' : ∀ᶠ (x : ℝ) in nhds a, deriv g x ≠ 0) (hfa : Filter.Tendsto f (nhds a) (nhds 0)) (hga : Filter.Tendsto g (nhds a) (nhds 0)) (hdiv : Filter.Tendsto (fun (x : ℝ) => deriv f x / deriv g x) (nhds a) l) :
Filter.Tendsto (fun (x : ℝ) => f x / g x) (nhdsWithin a {a}ᶜ) l

docs, source

65. Isosceles Triangle Theorem #

Author: Joseph Myers

theorem EuclideanGeometry.angle_eq_angle_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 p2 p3 : P} (h : dist p1 p2 = dist p1 p3) :
EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p3 p2

docs, source

66. Sum of a Geometric Series #

Author: Sander R. Dahmen (finite) and Johannes Hölzl (infinite)

theorem geom_sum_Ico {α : Type u} [DivisionRing α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) :
∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)

docs, source

theorem NNReal.hasSum_geometric {r : NNReal} (hr : r < 1) :
HasSum (fun (n : ℕ) => r ^ n) (1 - r)⁻¹

docs, source

67. e is Transcendental #

Author: Jujian Zhang

result

website

68. Sum of an arithmetic series #

Author: Johannes Hölzl

theorem Finset.sum_range_id (n : ℕ) :
∑ i ∈ Finset.range n, i = n * (n - 1) / 2

docs, source

69. Greatest Common Divisor Algorithm #

Author: mathlib

def EuclideanDomain.gcd {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) :
R

docs, source

theorem EuclideanDomain.gcd_dvd {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) :
EuclideanDomain.gcd a b ∣ a ∧ EuclideanDomain.gcd a b ∣ b

docs, source

theorem EuclideanDomain.dvd_gcd {R : Type u} [EuclideanDomain R] [DecidableEq R] {a b c : R} :
c ∣ a → c ∣ b → c ∣ EuclideanDomain.gcd a b

docs, source

70. The Perfect Number 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

71. Order of a Subgroup #

Author: mathlib

theorem Subgroup.card_subgroup_dvd_card {α : Type u_1} [Group α] (s : Subgroup α) :
Nat.card ↥s ∣ Nat.card α

docs, source

72. Sylow’s Theorem #

Author: Chris Hughes

theorem Sylow.exists_subgroup_card_pow_prime {G : Type u} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact (Nat.Prime p)] (hdvd : p ^ n ∣ Nat.card G) :
∃ (K : Subgroup G), Nat.card ↥K = p ^ n

docs, source

sylow_conjugate

card_sylow_dvd

card_sylow_modeq_one

73. Ascending or Descending Sequences (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

74. The Principle of Mathematical Induction #

Author: Leonardo de Moura

inductive Nat :
Type

docs, source

Automatically generated when defining the natural numbers

75. The 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

76. Fourier Series #

Author: Heather Macbeth

def fourierCoeff {T : ℝ} [hT : Fact (0 < T)] {E : Type} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : AddCircle T → E) (n : ℤ) :
E

docs, source

theorem hasSum_fourier_series_L2 {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) :
HasSum (fun (i : ℤ) => fourierCoeff (↑↑f) i • fourierLp 2 i) f

docs, source

77. Sum of kth powers #

Authors: mathlib (Moritz Firsching, Fabian Kruse, Ashvni Narayanan)

theorem sum_range_pow (n p : ℕ) :
∑ k ∈ Finset.range n, ↑k ^ p = ∑ i ∈ Finset.range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

docs, source

theorem sum_Ico_pow (n p : ℕ) :
∑ k ∈ Finset.Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ Finset.range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

docs, source

78. The Cauchy-Schwarz Inequality #

Author: Zhouhang Zhou

theorem inner_mul_inner_self_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :
‖inner x y‖ * ‖inner y x‖ ≤ RCLike.re (inner x x) * RCLike.re (inner y y)

docs, source

theorem norm_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :
‖inner x y‖ ≤ ‖x‖ * ‖y‖

docs, source

79. The Intermediate Value Theorem #

Author: mathlib (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

80. The Fundamental Theorem of Arithmetic #

Author: mathlib (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.

81. Divergence of the Prime Reciprocal Series #

Authors: Manuel Candales (archive), Michael Stoll (Mathlib)

theorem Theorems100.Real.tendsto_sum_one_div_prime_atTop :
Filter.Tendsto (fun (n : ℕ) => ∑ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) (Finset.range n), 1 / ↑p) Filter.atTop Filter.atTop

docs, source

theorem not_summable_one_div_on_primes :
¬Summable ({p : ℕ | Nat.Prime p}.indicator fun (n : ℕ) => 1 / ↑n)

docs, source

82. Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) #

Author: Floris van Doorn

theorem Theorems100.«82».cannot_cube_a_cube {n : ℕ} :
n ≥ 3 → ∀ {s : Set (Theorems100.«82».Cube n)}, s.Finite → s.Nontrivial → s.PairwiseDisjoint Theorems100.«82».Cube.toSet → ⋃ c ∈ s, c.toSet = Theorems100.«82».Cube.unitCube.toSet → Set.InjOn Theorems100.«82».Cube.w s → False

docs, source

83. The Friendship Theorem #

Authors: Aaron Anderson, Jalex Stark, 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

85. Divisibility by 3 Rule #

Author: Kim Morrison

theorem Nat.three_dvd_iff (n : ℕ) :
3 ∣ n ↔ 3 ∣ (Nat.digits 10 n).sum

docs, source

86. Lebesgue Measure and Integration #

Author: Johannes Hölzl

def MeasureTheory.lintegral {α : Type u_5} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) :
ENNReal

docs, source

88. Derangements Formula #

Author: Henry Swanson

theorem card_derangements_eq_numDerangements (α : Type u_2) [Fintype α] [DecidableEq α] :
Fintype.card ↑(derangements α) = numDerangements (Fintype.card α)

docs, source

theorem numDerangements_sum (n : ℕ) :
↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))

docs, source

89. The Factor and Remainder Theorems #

Author: Chris Hughes

theorem Polynomial.dvd_iff_isRoot {R : Type u} {a : R} [CommRing R] {p : Polynomial R} :
Polynomial.X - Polynomial.C a ∣ p ↔ p.IsRoot a

docs, source

theorem Polynomial.mod_X_sub_C_eq_C_eval {R : Type u} [Field R] (p : Polynomial R) (a : R) :
p % (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)

docs, source

90. Stirling’s Formula #

Authors: mathlib (Moritz Firsching, Fabian Kruse, Nikolas Kuhn, Heather Macbeth)

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

docs, source

91. The Triangle Inequality #

Author: Zhouhang Zhou

theorem norm_add_le {E : Type u_6} [SeminormedAddGroup E] (a b : E) :
‖a + b‖ ≤ ‖a‖ + ‖b‖

docs, source

93. The Birthday Problem #

Author: Eric Rodriguez

theorem Theorems100.birthday :
2 * Fintype.card (Fin 23 ↪ Fin 365) < Fintype.card (Fin 23 → Fin 365) ∧ 2 * Fintype.card (Fin 22 ↪ Fin 365) > Fintype.card (Fin 22 → Fin 365)

docs, source

theorem Theorems100.birthday_measure :
MeasureTheory.volume {f : Fin 23 → Fin 365 | Function.Injective f} < 1 / 2

docs, source

94. The Law of Cosines #

Author: Joseph Myers

theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle {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 - 2 * dist p1 p2 * dist p3 p2 * Real.cos (EuclideanGeometry.angle p1 p2 p3)

docs, source

95. 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

96. Principle of Inclusion/Exclusion #

Authors: Neil Strickland (outside mathlib), Yaël Dillies (in mathlib)

theorem Finset.inclusion_exclusion_sum_biUnion {ι : Type u_1} {α : Type u_2} {G : Type u_3} [DecidableEq α] [AddCommGroup G] (s : Finset ι) (S : ι → Finset α) (f : α → G) :
∑ a ∈ s.biUnion S, f a = ∑ t : { x : Finset ι // x ∈ Finset.filter (fun (x : Finset ι) => x.Nonempty) s.powerset }, (-1) ^ ((↑t).card + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a

docs, source

theorem Finset.inclusion_exclusion_card_biUnion {ι : Type u_1} {α : Type u_2} [DecidableEq α] (s : Finset ι) (S : ι → Finset α) :
↑(s.biUnion S).card = ∑ t : { x : Finset ι // x ∈ Finset.filter (fun (x : Finset ι) => x.Nonempty) s.powerset }, (-1) ^ ((↑t).card + 1) * ↑((↑t).inf' ⋯ S).card

docs, source

theorem Finset.inclusion_exclusion_sum_inf_compl {ι : Type u_1} {α : Type u_2} {G : Type u_3} [DecidableEq α] [AddCommGroup G] [Fintype α] (s : Finset ι) (S : ι → Finset α) (f : α → G) :
∑ a ∈ s.inf fun (i : ι) => (S i)ᶜ, f a = ∑ t ∈ s.powerset, (-1) ^ t.card • ∑ a ∈ t.inf S, f a

docs, source

theorem Finset.inclusion_exclusion_card_inf_compl {ι : Type u_1} {α : Type u_2} [DecidableEq α] [Fintype α] (s : Finset ι) (S : ι → Finset α) :
↑(s.inf fun (i : ι) => (S i)ᶜ).card = ∑ t ∈ s.powerset, (-1) ^ t.card * ↑(t.inf S).card

docs, source

github

97. Cramer’s Rule #

Author: Anne Baanen

theorem Matrix.mulVec_cramer {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : n → α) :
A.mulVec (A.cramer b) = A.det • b

docs, source

98. Bertrand’s Postulate #

Authors: Bolton Bailey, Patrick Stevens

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

docs, source

99. Buffon Needle Problem #

Author: Enrico Z. Borba

theorem BuffonsNeedle.buffon_short {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (d l : ℝ) (hd : 0 < d) (hl : 0 < l) (B : Ω → ℝ × ℝ) (hBₘ : Measurable B) (hB : MeasureTheory.pdf.IsUniform B (Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 Real.pi) MeasureTheory.volume MeasureTheory.volume) (h : l ≤ d) :
∫ (x : Ω), BuffonsNeedle.N l B x = 2 * l * (d * Real.pi)⁻¹

docs, source

theorem BuffonsNeedle.buffon_long {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (d l : ℝ) (hd : 0 < d) (hl : 0 < l) (B : Ω → ℝ × ℝ) (hBₘ : Measurable B) (hB : MeasureTheory.pdf.IsUniform B (Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 Real.pi) MeasureTheory.volume MeasureTheory.volume) (h : d ≤ l) :
∫ (x : Ω), BuffonsNeedle.N l B x = 2 * l / (d * Real.pi) - 2 / (d * Real.pi) * (√(l ^ 2 - d ^ 2) + d * Real.arcsin (d / l)) + 1

docs, source

100. Descartes Rule of Signs #

Author: Alex Meiburg

github