100.yaml

1:
  title  : The Irrationality of the Square Root of 2
  decl   : irrational_sqrt_two
  author : mathlib
2:
  title  : Fundamental Theorem of Algebra
  decl   : complex.exists_root
  author : Chris Hughes
3:
  title  : The Denumerability of the Rational Numbers
  decl   : rat.denumerable
  author : Chris Hughes
4:
  title  : Pythagorean Theorem
  decl   : euclidean_geometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
  author : Joseph Myers
5:
  title  : Prime Number Theorem
6:
  title  : Gödel’s Incompleteness Theorem
7:
  title  : Law of Quadratic Reciprocity
  decls  :
    - legendre_sym.quadratic_reciprocity
    - jacobi_sym.quadratic_reciprocity
  author : Chris Hughes (first) and Michael Stoll (second)
8:
  title  : The Impossibility of Trisecting the Angle and Doubling the Cube
9:
  title  : The Area of a Circle
  links  :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/9_area_of_a_circle.lean
  author : James Arthur, Benjamin Davidson, and Andrew Souther
10:
  title  : Euler’s Generalization of Fermat’s Little Theorem
  decl   : nat.modeq.pow_totient
  author : Chris Hughes
11:
  title  : The Infinitude of Primes
  decl   : nat.exists_infinite_primes
  author : Jeremy Avigad
12:
  title  : The Independence of the Parallel Postulate
13:
  title  : Polyhedron Formula
14:
  title  : Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + ….
  decl   : has_sum_zeta_two
  author : Marc Masdeu, David Loeffler
15:
  title  : Fundamental Theorem of Integral Calculus
  decls  :
    - interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_right
    - interval_integral.integral_eq_sub_of_has_deriv_right_of_le
  author : Yury G. Kudryashov (first) and Benjamin Davidson (second)
16:
  title  : Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem)
  author: Thomas Browning
  links :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/16_abel_ruffini.lean
17:
  title  : De Moivre’s Formula
  decl   : complex.cos_add_sin_mul_I_pow
  author : Abhimanyu Pallavi Sudhir
18:
  title  : Liouville’s Theorem and the Construction of Transcendental Numbers
  author : Jujian Zhang
  decl   :  liouville.transcendental
19:
  title  : Four Squares Theorem
  decl   : nat.sum_four_squares
  author : Chris Hughes
20:
  title  : All Primes (1 mod 4) Equal the Sum of Two Squares
  decl   : nat.prime.sq_add_sq
  author : Chris Hughes
21:
  title  : Green’s Theorem
22:
  title  : The Non-Denumerability of the Continuum
  decl   : cardinal.not_countable_real
  author : Floris van Doorn
23:
  title  : Formula for Pythagorean Triples
  decl   : pythagorean_triple.classification
  author : Paul van Wamelen
24:
  title  : The Independence of the Continuum Hypothesis
  author : Jesse Michael Han and Floris van Doorn
  links  :
    result: https://github.com/flypitch/flypitch/blob/master/src/summary.lean
    website: https://flypitch.github.io/
  note   : see the `README` file in the [linked repository](https://github.com/flypitch/flypitch/).
25:
  title  : Schroeder-Bernstein Theorem
  decl   : function.embedding.schroeder_bernstein
  author : Mario Carneiro
26:
  title  : Leibniz’s Series for Pi
  decl   : real.tendsto_sum_pi_div_four
  author : Benjamin Davidson
27:
  title  : Sum of the Angles of a Triangle
  decl   : euclidean_geometry.angle_add_angle_add_angle_eq_pi
  author : Joseph Myers
28:
  title  : Pascal’s Hexagon Theorem
29:
  title  : Feuerbach’s Theorem
30:
  title  : The Ballot Problem
  author : Bhavik Mehta, Kexing Ying
  links  :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/30_ballot_problem.lean
31:
  title  : Ramsey’s Theorem
  author : Bhavik Mehta
  links  :
    result: https://github.com/b-mehta/combinatorics/blob/extras/src/inf_ramsey.lean
32:
  title  : The Four Color Problem
33:
  title  : Fermat’s Last Theorem
34:
  title  : Divergence of the Harmonic Series
  decl   : real.tendsto_sum_range_one_div_nat_succ_at_top
  author : Anatole Dedecker, Yury Kudryashov
35:
  title  : Taylor’s Theorem
  decls  :
    - taylor_mean_remainder_lagrange
    - taylor_mean_remainder_cauchy
  author : Moritz Doll
36:
  title  : Brouwer Fixed Point Theorem
  author : Brendan Seamas Murphy
  links  :
    result: https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/master/src/brouwer_fixed_point.lean
37:
  title  : The Solution of a Cubic
  author : Jeoff Lee
  links  :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/37_solution_of_cubic.lean
38:
  title  : Arithmetic Mean/Geometric Mean
  decl   : real.geom_mean_le_arith_mean_weighted
  author : Yury G. Kudryashov
39:
  title  : Solutions to Pell’s Equation
  decls  :
    - pell.eq_pell
    - pell.exists_of_not_is_square
  author : Mario Carneiro (first), Michael Stoll (second)
  note   : "In `pell.eq_pell`, `d` is defined to be `a*a - 1` for an arbitrary `a > 1`."
40:
  title  : Minkowski’s Fundamental Theorem
  decl   : measure_theory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
  author : Alex J. Best, Yaël Dillies
41:
  title  : Puiseux’s Theorem
42:
  title  : Sum of the Reciprocals of the Triangular Numbers
  author : Jalex Stark, Yury Kudryashov
  links :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/42_inverse_triangle_sum.lean
43:
  title  : The Isoperimetric Theorem
44:
  title  : The Binomial Theorem
  decl   : add_pow
  author : Chris Hughes
45:
  title  : The Partition Theorem
  author : Bhavik Mehta, Aaron Anderson
  links:
    mathlib archive: https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/45_partition.lean
46:
  title  : The Solution of the General Quartic Equation
47:
  title  : The Central Limit Theorem
48:
  title  : Dirichlet’s Theorem
49:
  title  : The Cayley-Hamilton Theorem
  decl   : matrix.aeval_self_charpoly
  author : Scott Morrison
50:
  title  : The Number of Platonic Solids
51:
  title  : Wilson’s Lemma
  decl   : zmod.wilsons_lemma
  author : Chris Hughes
52:
  title  : The Number of Subsets of a Set
  decl   : finset.card_powerset
  author : mathlib
53:
  title  : Pi is Transcendental
54:
  title  : Königsberg Bridges Problem
  links:
    mathlib archive: https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/54_konigsberg.lean
  author : Kyle Miller
55:
  title  : Product of Segments of Chords
  decl   : euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi
  author : Manuel Candales
56:
  title  : The Hermite-Lindemann Transcendence Theorem
57:
  title  : Heron’s Formula
  links :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/57_herons_formula.lean
  author : Matt Kempster
58:
  title  : Formula for the Number of Combinations
  decls  :
    - finset.card_powerset_len
    - finset.mem_powerset_len
  author : mathlib <!--Jeremy Avigad in lean 2-->
59:
  title  : The Laws of Large Numbers
  decl   : probability_theory.strong_law_ae
  author : Sébastien Gouëzel
60:
  title  : Bezout’s Theorem
  decl   : nat.gcd_eq_gcd_ab
  author : mathlib
61:
  title  : Theorem of Ceva
62:
  title  : Fair Games Theorem
  decl   : measure_theory.submartingale_iff_expected_stopped_value_mono
  author : Kexing Ying
63:
  title  : Cantor’s Theorem
  decl   : cardinal.cantor
  author : mathlib <!-- Mario and/or Johannes -->
64:
  title  : L’Hopital’s Rule
  decl   : deriv.lhopital_zero_nhds
  author : Anatole Dedecker
65:
  title  : Isosceles Triangle Theorem
  decl   : euclidean_geometry.angle_eq_angle_of_dist_eq
  author : Joseph Myers
66:
  title  : Sum of a Geometric Series
  decls  :
    - geom_sum_Ico
    - nnreal.has_sum_geometric
  author : Sander R. Dahmen (finite) and Johannes Hölzl (infinite)
67:
  title  : e is Transcendental
  author : Jujian Zhang
  links  :
    result: https://github.com/jjaassoonn/transcendental/blob/master/src/e_transcendental.lean
    website: https://jjaassoonn.github.io/transcendental/
68:
  title  : Sum of an arithmetic series
  decl   : finset.sum_range_id
  author : Johannes Hölzl
69:
  title  : Greatest Common Divisor Algorithm
  decls  :
    - euclidean_domain.gcd
    - euclidean_domain.gcd_dvd
    - euclidean_domain.dvd_gcd
  author : mathlib
70:
  title  : The Perfect Number Theorem
  links  :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/70_perfect_numbers.lean
  author : Aaron Anderson
71:
  title  : Order of a Subgroup
  decl   : subgroup.card_subgroup_dvd_card
  author : mathlib
72:
  title  : Sylow’s Theorem
  decls  :
    - sylow.exists_subgroup_card_pow_prime
  links  :
    sylow_conjugate: https://github.com/ChrisHughes24/Sylow/blob/7185e33eeb6d28ea1a423492e7b4a8634aa9723d/src/sylow.lean#L885
    card_sylow_dvd: https://github.com/ChrisHughes24/Sylow/blob/7185e33eeb6d28ea1a423492e7b4a8634aa9723d/src/sylow.lean#L925
    card_sylow_modeq_one: https://github.com/ChrisHughes24/Sylow/blob/7185e33eeb6d28ea1a423492e7b4a8634aa9723d/src/sylow.lean#L944
  author : Chris Hughes
73:
  title  : Ascending or Descending Sequences (Erdős–Szekeres Theorem)
  links  :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/73_ascending_descending_sequences.lean
  author : Bhavik Mehta
74:
  title  : The Principle of Mathematical Induction
  decl   : nat
  note   : Automatically generated when defining the natural numbers
  author : Leonardo de Moura
75:
  title  : The Mean Value Theorem
  decl   : exists_deriv_eq_slope
  author : Yury G. Kudryashov
76:
  title  : Fourier Series
  decls   :
    - fourier_coeff
    - has_sum_fourier_series_L2
  author : Heather Macbeth
77:
  title  : Sum of kth powers
  decls  :
    - sum_range_pow
    - sum_Ico_pow
  author : mathlib (Moritz Firsching, Fabian Kruse, Ashvni Narayanan)
78:
  title  : The Cauchy-Schwarz Inequality
  decls  :
    - inner_mul_inner_self_le
    - norm_inner_le_norm
  author : Zhouhang Zhou
79:
  title  : The Intermediate Value Theorem
  decl   : intermediate_value_Icc
  author : mathlib (Rob Lewis and Chris Hughes)
80:
  title  : The Fundamental Theorem of Arithmetic
  decls  :
    - nat.factors_unique
    - int.euclidean_domain
    - euclidean_domain.to_principal_ideal_domain
    - unique_factorization_monoid
    - unique_factorization_monoid.factors_unique
  author : mathlib (Chris Hughes)
  note   : "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:
  title  : Divergence of the Prime Reciprocal Series
  links  :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean
  author : Manuel Candales
82:
  title  : Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof)
  links :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/82_cubing_a_cube.lean
  author : Floris van Doorn
83:
  title  : The Friendship Theorem
  links  :
    mathlib archive: https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/83_friendship_graphs.lean
  author : Aaron Anderson, Jalex Stark, Kyle Miller
84:
  title  : Morley’s Theorem
85:
  title  : Divisibility by 3 Rule
  author : Scott Morrison
  decls  :
    - nat.three_dvd_iff
86:
  title  : Lebesgue Measure and Integration
  decl   : measure_theory.lintegral
  author : Johannes Hölzl
87:
  title  : Desargues’s Theorem
88:
  title  : Derangements Formula
  decls  :
    - card_derangements_eq_num_derangements
    - num_derangements_sum
  author : Henry Swanson
89:
  title  : The Factor and Remainder Theorems
  decls  :
    - polynomial.dvd_iff_is_root
    - polynomial.mod_X_sub_C_eq_C_eval
  author : Chris Hughes
90:
  title  : Stirling’s Formula
  decls  :
    - stirling.tendsto_stirling_seq_sqrt_pi
  author : mathlib (Moritz Firsching, Fabian Kruse, Nikolas Kuhn, Heather Macbeth)
91:
  title  : The Triangle Inequality
  decl   : norm_add_le
  author : Zhouhang Zhou
92:
  title  : Pick’s Theorem
93:
  title  : The Birthday Problem
  links  :
    mathlib archive: https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/93_birthday_problem.lean
  author : Eric Rodriguez
94:
  title  : The Law of Cosines
  decl   : euclidean_geometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle
  author : Joseph Myers
95:
  title  : Ptolemy’s Theorem
  decl   : euclidean_geometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical
  author : Manuel Candales
96:
  title  : Principle of Inclusion/Exclusion
  links  :
    github : https://github.com/NeilStrickland/lean_lib/blob/f88d162da2f990b87c4d34f5f46bbca2bbc5948e/src/combinatorics/matching.lean#L304
  author : Neil Strickland
97:
  title  : Cramer’s Rule
  decl   : matrix.mul_vec_cramer
  author : Anne Baanen
98:
  title  : Bertrand’s Postulate
  decl   : nat.bertrand
  author : Bolton Bailey, Patrick Stevens
99:
  title  : Buffon Needle Problem
100:
  title  : Descartes Rule of Signs