Logo

The following is a list of the theorems (from this list) proved so far in the Isabelle theorem proving enviroment.

1. Square root of 2 is irrational

theorem sqrt_prime_irrational:

  prime p ==> sqrt (real p) ∉ \<rat>

2. Fundamental Theorem of Algebra

theorem fundamental_theorem_of_algebra:

~constant(poly p) ==> ∃z::complex. poly p z = 0
	

3. Denumerability of the Rational Numbers

theorem rat_denum:

f::nat=>rat. surj f

4. Pythagorean Theorem

theorem pythagoras_verbose:

(A1 - 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)

5. Prime Number Theorem

http://www.andrew.cmu.edu/user/avigad/ - Research Project and TOCL Paper.

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⌉)"
Archive of Formal Proofs

7. Law of Quadratic Reciprocity

theorem Quadratic_Reciprocity:

  [| p ∈ zOdd; zprime p; q ∈ zOdd; zprime q; pq |]
  ==> Legendre p q * Legendre q p = -1 ^ 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

Archive of Formal Proofs

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:

  infinite {p. prime p}

12. The Independence of the Parallel Postulate

Archive of Formal Proofs

15. Fundamental Theorem of Integral Calculus

theorem FTC1:

  [| ab; ∀x. axxb --> DERIV f x :> f' x |]
  ==> Integral (a, b) f' (f b - f a)

17. DeMoivre's Theorem

theorem DeMoivre:

  cis a ^ n = cis (real n * a)

theorem DeMoivre2:

  rcis r a ^ n = rcis (r ^ n) (real n * a)

19. Lagrange's four-square theorem

theorem four_squares:

  0  n ==> ∃a b c d. a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

20. All primes (1 mod 4) equal the sum of two squares

lemma prime_1mod4_is_sum2sq:

 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; azOdd; 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

25. Schroeder-Bernstein Theorem

theorem Schroeder_Bernstein:

  [| inj f::'a=>'b; inj g::'b=>'a |] ==> ∃h::'a=>'b. inj h ∧ surj h

26. Leibnitz's Series for Pi

theorem pi_series:

  pi / 4 = (∑k. (-1)^k * 1 / real (k*2+1))
	

31. Ramsey's Theorem

Archive of Formal Proofs

34. Divergence of the Harmonic Series

theorem DivergenceOfHarmonicSeries:

  ¬ summable (%n. 1 / real (Suc n))

35. Taylor's Theorem

theorem taylor:

  [| 0 < n; diff 0 = f;
     ∀m t. m < nattb --> DERIV (diff m) t :> diff (Suc m) t; ac;
     cb; ax; xb; xc |]
  ==> ∃t. (if x < c then x < tt < c else c < tt < x) ∧
          f x =
          (∑m = 0..<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::"real^'n::finite => real^'n::finite"
    assumes "compact s" "convex s" "s ≠ {}" "continuous_on s f" "f ` s ⊆ s"
    obtains x where "x ∈ s" "f x = x" 

37. The Solution of a Cubic

theorem cubic:

  a  0==> 
  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 + \<i> * csqrt 3) / 2; 
      s3 = - s1 * (1 - \<i> * 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:

  pos z::real list ==> gmean z ≤ mean z
Archive of Formal Proofs

44. The Binomial Theorem

theorem binomial:

  (a + b) ^ n = (∑k = 0..n. (n choose k) * a ^ k * b ^ (n - k))

46. The Solution of the General Quartic Equation

theorem quartic_cases:

y ^ 3 - b * y ^ 2 + (a * c - 4 * d) * y - a ^ 2 * d + 4 * b * d - c ^ 2 = 0R ^ 2 = a ^ 2 / 4 - b + ys ^ 2 = y ^ 2 - 4 * dD ^ 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 / 2x = - a / 4 + R / 2 - D / 2x = - a / 4 - R / 2 + E / 2x = - a / 4 - R / 2 - E / 2)

47. The Central Limit Theorem

On GitHub

49. Cayley-Hamilton Theorem

theorem Cayley_Hamilton:

  fixes A :: "'a::comm_ring_1^'n::finite^'n"
  shows "evalmat (charpoly A) A = 0"
Archive of Formal Proofs

51. Wilson's Theorem

theorem Wilson_Russ:

  zprime p ==> [zfact (p - 1) = -1] (mod p)

52. The number of subsets of a set

theorem card_Pow:

  finite A ==> card (Pow A) = Suc (Suc 0) ^ 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'"

Archive of Formal Proofs

58. Formula for the number of Combinations

theorem n_subsets:

  finite A ==> card {B. BA ∧ card B = k} = card A choose k

60. Bezout's Theorem

theorem bezout:

d x y. d dvd ad dvd b ∧ (a * x - b * y = db * x - a * y = d)
	

63. Cantor's Theorem

theorem cantor:

S. S ∉ range f::'a=>'a set

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

theorem sumr_geometric:

  x ≠ 1 ==> setsum (op ^ x) {0..<n} = (x ^ n - 1) / (x - 1)

theorem geometric_sums:

  ¦x¦ < 1 ==> op ^ x sums (1 / (1 - x))

68. Sum of an Arithmetic Series

theorem arith_series_int:

  0 < n
  ==> 2 * (∑i = 0..n - 1. a + int i * d) = int n * (a + (a + int (n - 1) * d))

69. Greatest Common Divisor Algorithm

theorem 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^(n+1) - 1)"
Archive of Formal Proofs

71. Order of a Subgroup

theorem group.lagrange:

  [| group G; finite (carrier G); subgroup H G |]
  ==> card (rcosetsG 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

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:

  [| a < b; ∀x. axxb --> isCont f x;
     ∀x. a < xx < b --> f differentiable x |]
  ==> ∃l z. a < zz < b ∧ DERIV f z :> lf b - f a = (b - a) * l

78. The Cauchy-Schwarz Inequality

theorem CauchySchwarzReal:

  vlen x = vlen y ==> ¦x · y¦ ≤ ||x|| * ||y||
Archive of Formal Proofs

79. The Intermediate Value Theorem

theorem IVT:

  [| f ay; yf b; ab; ∀x. axxb --> isCont f x |]
  ==> ∃xa. xbf x = y

80. Fundamental Theorem of Arithmetic

theorem unique_prime_factorization:

  Suc 0 < n ==> ∃!l. primel l ∧ nondec l ∧ prod l = n

83. The Friendship Theorem

theorem (in valid_unSimpGraph) friendship_thm:

assumes "!!v u. v∈V ==> u∈V ==> v≠u ==> ∃! n. adjacent v n ∧ adjacent u n"
and "finite V"
shows "∃v. ∀n∈V. n≠v --> adjacent v n"
Archive of Formal Proofs

85. Divisibility by Three Rule

theorem three_divides_nat:

n. (3 dvd n) = (3 dvd sumdig n)

86. Lebesgue Measure and Integration

Archive of Formal Proofs

89. The Factor and Remainder Theorems

theorem long_div_ring:

  g ≠ 0
  ==> Ex (%(q, r, k). lcoeff g ^ k *s f = q * g + r ∧ (r = 0 ∨ deg r < deg g))

theorem long_div_theorem:

  g ≠ 0 ==> Ex (%(q, r). f = q * g + r ∧ (r = 0 ∨ deg r < deg g))

theorem long_div_quo_unique:

  [| g ≠ 0; f = q1 * g + r1; r1 = 0 ∨ deg r1 < deg g; f = q2 * g + r2;
     r2 = 0 ∨ deg r2 < deg g |]
  ==> q1 = q2

theorem long_div_rem_unique:

  [| g ≠ 0; f = q1 * g + r1; r1 = 0 ∨ deg r1 < deg g; f = q2 * g + r2;
     r2 = 0 ∨ deg r2 < deg g |]
  ==> r1 = r2

91. The Triangle Inequality

theorem abs_triangle_ineq:

  ¦a + 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)"

97. Cramer's Rule

lemma cramer:

det A  0
==> (A *v x = b) =
    (x = χ k. (deti j. if j = k then b $ i else A $ i $ j) / det A))