The following are the theorems from this list proved so far in the Isabelle proof assistant.

If you have proved additional ones or know of any, please so I can add them here.

1. Square Root of 2 is Irrational

theorem sqrt_prime_irrational:
  "prime p  sqrt (real p)  "

2. Fundamental Theorem of Algebra

lemma fundamental_theorem_of_algebra:
  assumes nc: "¬ constant (poly p)"
  shows "z::complex. poly p z = 0"

3. Denumerability of the Rational Numbers

instance rat :: countable
proof
  show "to_nat::rat  nat. inj to_nat"

4. Pythagorean Theorem

lemma pythagoras_verbose:
  "((A1::real) - B1) * (C1 - B1) + (A2 - B2) * (C2 - B2) = 0  
  (C1 - A1) * (C1 - A1) + (C2 - A2) * (C2 - A2) =
  ((B1 - A1) * (B1 - A1) + (B2 - A2) * (B2 - A2)) + (C1 - B1) * (C1 - B1) + (C2 - B2) * (C2 - B2)"

lemma pythagoras: 
  defines ort:"orthogonal  (λ(A::point) B. fst A * fst B + snd A * snd B = 0)"
       and vc:"vector  (λ(A::point) B. (fst A  - fst B, snd A - snd B))"
      and vcn:"vecsqnorm  (λA::point. fst A ^ 2 + snd A ^2)"
 assumes o: "orthogonal (vector A B) (vector C B)"
 shows "vecsqnorm(vector C A) = vecsqnorm(vector B  A) + vecsqnorm(vector C B)"

5. Prime Number Theorem

lemma PrimeNumberTheorem: "(λx. pi x * ln (real x) / (real x)) ----> 1"

http://www.andrew.cmu.edu/user/avigad/isabelle/NumberTheory/PrimeNumberTheorem.html

6. Gödel’s Incompleteness Theorem

theorem Goedel_I:
  assumes "¬ {}  Fls"
  obtains δ where
      "{}  δ IFF Neg (PfP ⌈δ⌉)"
      "¬ {}  δ"
      "¬ {}  Neg δ"  
      "eval_fm e δ"
      "ground_fm δ"

theorem Goedel_II:
  assumes "¬ {}  Fls"
    shows "¬ {}  Neg (PfP Fls)"    

http://afp.sourceforge.net/entries/Incompleteness.shtml

7. Law of Quadratic Reciprocity

theorem Quadratic_Reciprocity:
     "[| p  zOdd; zprime p; q  zOdd; zprime q;
         p  q |]
      ==> (Legendre p q) * (Legendre q p) =
          (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"   

8. The Impossibility of Trisecting the Angle and Doubling the Cube

theorem impossibility_of_doubling_the_cube:
  "x^3 = 2  (Point x 0)  constructible"    

theorem impossibility_of_trisecting_angle_pi_over_3: 
  "Point (cos (pi / 9)) 0  constructible"   

http://afp.sourceforge.net/entries/Impossible_Geometry.shtml

9. The Area of a Circle

lemma circle_area:
  assumes "R  0"
  shows "emeasure lborel {z::real×real. norm z  R} = R^2 * pi"  

https://github.com/3of8/circlearea/blob/master/Circle_Area.thy

10. Euler’s Generalisation of Fermat’s Little Theorem

theorem Euler_Fermat:
  "0 < m ==> zgcd x m = 1 ==> [x^(phi m) = 1] (mod m)"  

11. The Infinitude of Primes

theorem not_finite_prime: "~ finite {p::nat. prime p}"

12. The Independence of the Parallel Postulate

http://afp.sourceforge.net/entries/Tarskis_Geometry.shtml

15. Fundamental Theorem of Integral Calculus

lemma fundamental_theorem_of_calculus:
  assumes "a  b"
  assumes f': "x. a  x  x  b  DERIV f x :> f'(x)"
  shows "Integral (a, b) f' (f(b) - f(a))"  

17. DeMoivre’s Theorem

lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"

lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"   

19. Lagrange’s Four-Square Theorem

theorem four_squares:
  "(n::int)  0   a b c d. a^2 + b^2 + c^2 + d^2 = n"

http://afp.sourceforge.net/entries/FourSquares.shtml

20. All Primes (1 mod 4) Equal the Sum of Two Squares

lemma qf1_prime_exists:
  "zprime (4*m+1)   x y. x^2 + y^2 = 4*m+1"

22. The Non-Denumerability of the Continuum

theorem real_non_denum: "¬ (f :: nat  real. surj f)"

23. Formula for Pythagorean Triples

corollary int_euclid_pyth_triples:
  " zgcd a b = 1; a  zOdd; a^2 + b^2 = c^2 
     p q. a = p^2 - q^2  b = 2*p*q  ¦c¦ = p^2 + q^2  zgcd p q=1"

http://afp.sourceforge.net/entries/Fermat4.shtml

25. Schroeder-Bernstein Theorem

lemma schroeder_bernstein:
  "[| f  inj(X,Y);  g  inj(Y,X) |] ==> h. h  bij(X,Y)"  

26. Leibnitz’s Series for Pi

theorem pi_series:
  "pi / 4 = ( k. (-1)^k * 1 / real (k*2+1))"

30. The Ballot Problem

lemma
  "valid_countings a b = (if a  b then (if b = 0 then 1 else 0) else (a - b) / (a + b) * all_countings a b)"

31. Ramsey’s Theorem

lemma ramsey: "
  (s::nat) (r::nat) (YY::'a set) (f::'a set => nat). 
  infinite YY 
   (X. X <= YY  finite X  card X = r  f X < s)
   (Y' t'. 
  Y' <= YY 
   infinite Y' 
   t' < s 
   (X. X <= Y'  finite X  card X = r  f X = t'))"

http://afp.sourceforge.net/entries/Ramsey-Infinite.shtml

34. Divergence of the Harmonic Series

theorem DivergenceOfHarmonicSeries:
  shows "¬summable (λn. 1/real (Suc n))"

35. Taylor’s Theorem

lemma taylor:
  assumes INIT: "n>0" "diff 0 = f"
  and DERIV: "( m t. m < n & a  t & t  b  DERIV (diff m) t :> (diff (Suc m) t))"
  and INTERV: "a  c " "c  b" "a  x" "x  b" "x  c" 
  shows " t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
    f x = (m<n. (diff m c / real (fact m)) * (x - c)^m) + (diff n t / real (fact n)) * (x - c)^n"     

36. Brouwer Fixed Point Theorem

lemma brouwer:
  fixes f :: "'a::euclidean_space  'a"
  assumes "compact s"
    and "convex s"
    and "s  {}"
    and "continuous_on s f"
    and "f ` s  s"
  obtains x where "x  s" and "f x = x"

37. The Solution of a Cubic

lemma cubic:
  assumes a0: "a ≠ 0"
  shows "
  let p = (3 * a * c - b^2) / (9 * a^2) ;
      q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3);
      s = csqrt(q^2 + p^3);
      s1 = (if p = 0 then ccbrt(2 * q) else ccbrt(q + s));
      s2 = -s1 * (1 + ii * csqrt 3) / 2;
      s3 = -s1 * (1 - ii * csqrt 3) / 2
  in if p = 0 then 
       a * x^3 + b * x^2 + c * x + d = 0 ⟷
           x = s1 - b / (3 * a) ∨
           x = s2 - b / (3 * a) ∨
           x = s3 - b / (3 * a)
      else
        s1 ≠ 0 ∧
        (a * x^3 + b * x^2 + c * x + d = 0 ⟷
            x = s1 - p / s1 - b / (3 * a) ∨
            x = s2 - p / s2 - b / (3 * a) ∨
            x = s3 - p / s3 - b / (3 * a))"

38. Arithmetic Mean / Geometric Mean

theorem CauchysMeanTheorem_Eq:
  fixes z::"real list"
  assumes "pos z"
  shows "gmean z = mean z  het z = 0"

http://afp.sourceforge.net/entries/Cauchy.shtml

44. The Binomial Theorem

corollary binomial:
  "(a+b::nat)^n = (k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))"

46. The Solution of the General Quartic Equation

lemma quartic:
 "(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 
  R^2 = a^2 / 4 - b + y 
  s^2 = y^2 - 4 * d 
  (D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s
                   else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) 
  (E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s
                   else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R)))
   x^4 + a * x^3 + b * x^2 + c * x + d = 0 
      x = -a / 4 + R / 2 + D / 2 
      x = -a / 4 + R / 2 - D / 2 
      x = -a / 4 - R / 2 + E / 2 
      x = -a / 4 - R / 2 - E / 2"

47. The Central Limit Theorem

theorem (in prob_space) central_limit_theorem:
  fixes 
    X :: "nat  'a  real" and
    μ :: "real measure" and
    σ :: real and
    S :: "nat  'a  real"
  assumes
    X_indep: "indep_vars (λi. borel) X UNIV" and
    X_integrable: "n. integrable M (X n)" and
    X_mean_0: "n. expectation (X n) = 0" and
    σ_pos: "σ > 0" and
    X_square_integrable: "n. integrable M (λx. (X n x)2)" and
    X_variance: "n. variance (X n) = σ2" and
    X_distrib: "n. distr M borel (X n) = μ"
  defines
    "S n  λx. i<n. X i x"
  shows
    "weak_conv_m (λn. distr M borel (λx. S n x / sqrt (n * σ2))) 
        (density lborel std_normal_density)"

https://github.com/avigad/isabelle/blob/master/Analysis/Central_Limit_Theorem.thy#L69

49. Cayley-Hamilton Theorem

theorem Cayley_Hamilton:
  fixes A :: "'a::comm_ring_1^'nfinite^'n"
  shows "evalmat (charpoly A) A = 0"

http://afp.sourceforge.net/entries/Cayley_Hamilton.shtml

51. Wilson’s Theorem

theorem Wilson_Russ:
  "zprime p ==> [zfact (p - 1) = -1] (mod p)"   

52. The Number of Subsets of a Set

lemma card_Pow:
  "finite A  card (Pow A) = 2 ^ card A"

54. The Koenigsberg Bridges Problem

lemma eulerian_split:
  assumes "nodes G1  nodes G2 = {}" "edges G1  edges G2={}" 
    "valid_unMultigraph G1" "valid_unMultigraph G2"  
    "valid_unMultigraph.is_Eulerian_trail  G1 v1 ps1 v1'"
    "valid_unMultigraph.is_Eulerian_trail  G2 v2 ps2 v2'"
  shows "valid_unMultigraph.is_Eulerian_trail nodes=nodes G1  nodes G2,
          edges=edges G1  edges G2  {(v1',w,v2),(v2,w,v1')} v1 (ps1@(v1',w,v2)#ps2) v2'"    

http://afp.sourceforge.net/entries/Koenigsberg_Friendship.shtml

58. Formula for the Number of Combinations

theorem n_subsets:
  "finite A  card {B. B  A  card B = k} = (card A choose k)"  

60. Bezout’s Theorem

lemma bezout:
  "(d::nat) x y. d dvd a  d dvd b  (a * x - b * y = d  b * x - a * y = d)"

63. Cantor’s Theorem

lemma cantor1:
  "¬ (f:: 'a  'a set. S. x. f x = S)"

64. L’Hôpital’s Rule

lemma lhopital:
  "((f::real  real) ---> 0) (at x)  (g ---> 0) (at x) 
    eventually (λx. g x  0) (at x) 
    eventually (λx. g' x  0) (at x) 
    eventually (λx. DERIV f x :> f' x) (at x) 
    eventually (λx. DERIV g x :> g' x) (at x) 
    ((λ x. (f' x / g' x)) ---> y) (at x) 
  ((λ x. f x / g x) ---> y) (at x)" 

66. Sum of a Geometric Series

lemma geometric_sums: 
  "norm c < 1  (λn. c^n) sums (1 / (1 - c))"

lemma suminf_geometric:
  "norm c < 1  suminf (λn. c^n) = 1 / (1 - c)"

68. Sum of an Arithmetic Series

lemma arith_series_int:
  "2 * (i{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"

69. Greatest Common Divisor Algorithm

lemma is_gcd: "is_gcd (gcd m n) m n"    

70. Perfect Number Theorem

theorem perfect_number_theorem:
  assumes even: "even m" and perfect: "perfect m"
  shows " n . m = 2^n*(2^(n+1) - 1)  prime ((2::nat)^(n+1) - 1)" 

http://afp.sourceforge.net/entries/Perfect-Number-Thm.shtml

71. Order of a Subgroup

theorem (in group) lagrange:
  "finite(carrier G); subgroup H G
    card(rcosets H) * card(H) = order(G)"  

72. Sylow’s Theorem

theorem sylow_thm:
  "[| prime p;  group(G);  order(G) = (p^a) * m; finite (carrier G)|]
   ==> H. subgroup H G & card(H) = p^a"

73. Ascending or Descending Sequences

lemma Erdoes_Szekeres:
  fixes f :: "_  'a::linorder"
  shows "(S. S  {0..m * n}  card S = m + 1  mono_on f (op ) S) 
         (S. S  {0..m * n}  card S = n + 1  mono_on f (op ) S)"    

74. The Principle of Mathematical Induction

theorem nat_induct:
  "⟦P 0; ⋀n. P n ⟹ P (Suc n)⟧ ⟹ P n"

75. The Mean Value Theorem

theorem MVT:
  assumes lt:  "a < b"
      and con: "x. a  x & x  b --> isCont f x"
      and dif: "x. a < x & x < b --> f differentiable (at x)"
  shows "l z::real. a < z & z < b & DERIV f z :> l &
                   (f(b) - f(a) = (b-a) * l)"

lemma MVT2:
     "[| a < b; x. a  x & x  b --> DERIV f x :> f'(x) |]
      ==> z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))"  

77. Sum of kth powers

lemma sum_of_powers:
  "(kn::nat. (real k) ^ m) = (bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0) / (m + 1)"

78. The Cauchy-Schwarz Inequality

theorem CauchySchwarzReal:
  fixes x::vector
  assumes "vlen x = vlen y"
  shows "¦xy¦  x*y"   

http://afp.sourceforge.net/entries/Cauchy.shtml

79. The Intermediate Value Theorem

lemma IVT:
  fixes f :: "'a :: linear_continuum_topology  'b :: linorder_topology"
  shows "f a  y  y  f b  a  b  
         (x. a  x  x  b  isCont f x) 
         x. a  x  x  b  f x = y"

80. Fundamental Theorem of Arithmetic

theorem unique_prime_factorization:
  "n. Suc 0 < n --> (!l. primel l  nondec l  prod l = n)" 

83. The Friendship Theorem

theorem (in valid_unSimpGraph) friendship_thm:
  assumes "v u. vV  uV  vu  ! n. adjacent v n  adjacent u n" and "finite V" 
  shows "v. nV. nv  adjacent v n"       

http://afp.sourceforge.net/entries/Koenigsberg_Friendship.shtml

85. Divisibility by Three Rule

theorem three_divides_nat:
  shows "(3 dvd n) = (3 dvd sumdig n)"

86. Lebesgue Measure and Integration

http://afp.sourceforge.net/entries/Integration.shtml

88. Derangements Formula

theorem derangements_formula:
  assumes "n  0" "finite S" "card S = n"
  shows "card (derangements S) = round (fact n / exp 1)"

http://afp.sourceforge.net/entries/Derangements.shtml

89. The Factor and Remainder Theorems

lemma long_div_theorem: 
  assumes "g  carrier P" and "f  carrier P" and "g  𝟬P"
  shows "q r (k::nat). (q  carrier P)  (r  carrier P)  
        (lcoeff g)(^)Rk P f = g P q P r 
        (r = 𝟬P | deg R r < deg R g)"

91. The Triangle Inequality

class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  assumes abs_ge_zero: "¦a¦  0"
    and abs_ge_self: "a  ¦a¦"
    and abs_leI: "a  b  - a  b  ¦a¦  b"
    and abs_minus_cancel: "¦-a¦ = ¦a¦"
    and abs_triangle_ineq: "¦a + b¦  ¦a¦ + ¦b¦"

The triangle inequality is a type class property in Isabelle. Real numbers, integers, etc are instances of this type class:

lemma abs_triangle_ineq_real: "¦(a::real) + b¦  ¦a¦ + ¦b¦"
lemma abs_triangle_ineq_int: "¦(a::int) + b¦  ¦a¦ + ¦b¦"

93. The Birthday Problem

lemma birthday_paradox:
  assumes "card S = 23" "card T = 365"
  shows "2 * card {f  extensional_funcset S T. ¬ inj_on f S}  card (extensional_funcset S T)"    

96. Principle of Inclusion/Exclusion

lemma card_UNION:
  assumes "finite A" and "k  A. finite k"
  shows "card (A) = nat (I | I  A  I  {}. (- 1) ^ (card I + 1) * int (card (I)))"

97. Cramer’s Rule

lemma cramer:
  fixes A ::"real^'n^'n"
  assumes d0: "det A  0"
  shows "A *v x = b  x = (χ k. det(χ i j. if j=k then b$i else A$i$j) / det A)"