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
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)
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 ^ 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 ∉ constructibleArchive 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)
theorem not_finite_prime:
infinite {p. prime p}
12. The Independence of the Parallel Postulate
Archive of Formal Proofs15. Fundamental Theorem of Integral Calculus
theorem FTC1:
[| a ≤ b; ∀x. a ≤ x ∧ x ≤ b --> DERIV f x :> f' x |] ==> Integral (a, b) f' (f b - f a)
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; 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
25. Schroeder-Bernstein Theorem
theorem Schroeder_Bernstein:
[| inj f::'a=>'b; inj g::'b=>'a |] ==> ∃h::'a=>'b. inj h ∧ surj h
theorem pi_series:
pi / 4 = (∑k. (-1)^k * 1 / real (k*2+1))
34. Divergence of the Harmonic Series
theorem DivergenceOfHarmonicSeries:
¬ summable (%n. 1 / real (Suc n))
theorem taylor:
[| 0 < n; diff 0 = f; ∀m t. m < n ∧ a ≤ t ∧ t ≤ b --> DERIV (diff m) t :> diff (Suc m) t; a ≤ c; c ≤ b; a ≤ x; x ≤ b; x ≠ c |] ==> ∃t. (if x < c then x < t ∧ t < c else c < t ∧ t < 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"
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 zArchive of Formal Proofs
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 = 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)
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
58. Formula for the number of Combinations
theorem n_subsets:
finite A ==> card {B. B ⊆ A ∧ card B = k} = card A choose k
theorem bezout:
∃d x y. d dvd a ∧ d dvd b ∧ (a * x - b * y = d ∨ b * x - a * y = d)
theorem cantor:
∃S. S ∉ range f::'a=>'a set
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
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
theorem group.lagrange:
[| group G; finite (carrier G); subgroup H G |] ==> card (rcosetsG H) * card H = order G
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
theorem MVT:
[| a < b; ∀x. a ≤ x ∧ x ≤ b --> isCont f x; ∀x. a < x ∧ x < b --> f differentiable x |] ==> ∃l z. a < z ∧ z < b ∧ DERIV f z :> l ∧ f 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 a ≤ y; y ≤ f b; a ≤ b; ∀x. a ≤ x ∧ x ≤ b --> isCont f x |] ==> ∃x≥a. x ≤ b ∧ f x = y
80. Fundamental Theorem of Arithmetic
theorem unique_prime_factorization:
Suc 0 < n ==> ∃!l. primel l ∧ nondec l ∧ prod l = n
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 Proofs89. 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
theorem abs_triangle_ineq:
¦a + b¦ ≤ ¦a¦ + ¦b¦
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)"
lemma cramer:
det A ≠ 0
==> (A *v x = b) =
(x = χ k. (det (χ i j. if j = k then b $ i else A $ i $ j) / det A))
Last modified: 10 Feb, 2009 by Gerwin Klein.