42 famous theorems in ProofPower
Freek Wiedijk is tracking progress on automated proofs of a list of "100 greatest theorems". 42 of the theorems on the list have been proved so far in ProofPower. The statements of these theorems are listed below. Most of the theorems are taken from the ProofPower-HOL mathematical case studies. See the case studies web page for more information, including documents in PDF format that give the definitions on which the theorems depend.
1. The Irrationality of the Square Root of 2

xl-gft
sqrt_2_irrational_thm
⊢ ¬Sqrt 2. ∈ ℚ

3. The Denumerability of the Rational Numbers

xl-gft
ℚ_countable_thm
⊢ ∃f : ℕ → ℝ• ∀x• x ∈ ℚ ⇒ ∃p•f p = x

4. Pythagorean Theorem

xl-gft
pythagoras_thm
⊢ ∀u v : GA• u v ⇒ (u - v)^2 = u^2 + v^2

9. The Area of a Circle

xl-gft
area_circle_thm
⊢ ∀r• 0. < r ⇒ {(x, y) | Sqrt(x^2 + y^2) ≤ r} Area π * r ^ 2

11. The Infinitude of Primes

xl-gft
prime_infinite_thm
⊢ ¬ Prime ∈ Finite

15. Fundamental Theorem of Integral Calculus

xl-gft
int_deriv_thm
⊢ ∀a b sf f•
ftbrfttaba < b
fttab(∀x• a < x ∧ x < b ⇒ (sf Deriv f x) x)
fttab(sf Cts a) ∧ (sf Cts b)
fttab(f Int sf b - sf a) (ClosedInterval a b)

17. De Moivre's Theorem

xl-gft
de_moivre_thm
⊢ ∀ x m• (Cos x, Sin x) ^ m = (Cos (ℕℝ m * x), Sin (ℕℝ m * x))

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

xl-gft
two_squares_thm
⊢ ∀p m•
fttabp ∈ Prime
fttabp = 4*m + 1
fttab∃a b• p = a^2 + b^2

22. The Non-Denumerability of the Continuum

xl-gft
ℝ_uncountable_thm
⊢ ∀X: ℕ → ℝ• ∃x• ∀m• ¬x = X m

23. Formula for Pythagorean Triples

xl-gft
pythagorean_triples_thm
⊢ ∀a b c: ℕ•
ftbrfttaba^2 + b^2 = c^2
fttab∃m n d•
ftbrfttabfttab{a; b} = {d*n*(2*m + n); 2*d*m*(m + n)}
ftbrfttabfttabc = d*(m^2 + (m + n)^2)fttab

25. Schroeder-Bernstein Theorem

xl-gft
schroeder_bernstein_thm
⊢ ∀a b f g• f ∈ a b ∧ g ∈ b a ⇒ ∃h• h ∈ a b

30. The Ballot Problem

xl-gft
ballot_thm
⊢ ∀m n•
ftbrfttabletfttabS = BallotCounts m n
ftbrfttabin letfttabX = {s | s ∈ S ∧ ∀ i• ℕℤ 0 < s (i+1)}
ftbrfttabin
ftbrfttab fttabS ∈ Finite
ftbrfttabfttab¬#S = 0
ftbrfttabfttabX ⊆ S
ftbrfttabfttab(n < m ⇒ #X / #S = (m - n) / (m + n))

31. Ramsey's Theorem

xl-gft
fin_exp_2_ramsey_thm
⊢ ∀a b • ∃n • ∀(V, E) •
ftbrfttab(V, E) ∈ symg ∧ V ∈ Finite ∧ #V ≥ n
fttab(∃ C • C clique_of (V,E) ∧ #C = a ∨ C indep_of (V,E) ∧ #C = b)

34. Divergence of the Harmonic Series

xl-gft
harmonic_series_divergent_thm
⊢ ∀c• ¬ Series (λm• ℕℝ (m+1) <sup>-</sup><sup>1</sup>) -> c

35. Taylor's Theorem

xl-gft
taylor_thm
⊢ ∀n f D a b•
ftbrfttaba < b
fttabD 0 = f
fttab(∀ m x• m ≤ n ∧ a ≤ x ∧ x ≤ b ⇒ D m Cts x)
fttab(∀ m x• m ≤ n ∧ a < x ∧ x < b ⇒ (D m Deriv D (m + 1) x) x)
fttab∃x• a < x ∧ x < b
fttabf b =
ftbrfttabPowerSeries (λm• D m a * ℕℝ(m!)<sup>-</sup><sup>1</sup>) (n+1) (b-a) +
ftbrfttabD (n+1) x * (b-a) ^ (n+1) * ℕℝ((n+1)!)<sup>-</sup><sup>1</sup>

38. Arithmetic Mean/Geometric Mean

xl-gft
cauchy_mean_thm
⊢ ∀A f a•
ftbrfttabA ∈ Finite ∧ ¬A = {} ∧ (∀ x• x ∈ A ⇒ 0. < f x)
fttabRoot (#A) (Π A f) ≤ Σ A f / ℕℝ(#A)

40. Minkowski's Fundamental Theorem

xl-gft
minkowski_thm
⊢ ∀A a•
ftbrfttabA ∈ Convex
fttabA ∈ Bounded
fttab¬A = {}
fttab(∀x y• (x, y) ∈ A ⇒ (~x, ~y) ∈ A)
fttabA Area a
fttaba > 4.
fttab∃i j•
ftbrfttab fttab(ℤℝ i, ℤℝ j) ∈ A
ftbrfttabfttab¬(ℤℝ i, ℤℝ j) = (0., 0.)

42. Sum of the Reciprocals of the Triangular Numbers

xl-gft
sum_recip_triangulars_thm
⊢ Series (λm• 2/((m+1)*(m+2))) -> 2.

44. The Binomial Theorem

xl-gft
binomial_thm
⊢ ∀x y n• (x + y) ^ n = Series (λm•ℕℝ(Binomial n m) * x ^ m * y ^ (n - m)) (n+1)

51. Wilson's Theorem

xl-gft
wilson_thm
⊢ ∀ p• 1 < p ⇒ (p ∈ Prime ⇔ (p - 1)! Mod p = p - 1)

52. The Number of Subsets of a Set

xl-gft
℘_finite_size_thm
⊢ ∀a• a ∈ Finite ⇒ ℘ a ∈ Finite ∧ #(℘ a) = 2 ^ #a

58. Formula for the Number of Combinations

xl-gft
combinations_finite_size_thm
⊢ ∀A n m•
ftbrfttabA ∈ Finite ∧ #A = n
fttab{X | X ⊆ A ∧ #X = m} ∈ Finite
fttab#{X | X ⊆ A ∧ #X = m} = Binomial n m

60. Bezout's Theorem

xl-gft
bezout_thm
⊢ ∀m n•
fttab0 < m ∧ 0 < n
fttab(∃a b• b*n ≤ a*m ∧ Gcd m n = a*m - b*n)
fttab(∃a b• a*m ≤ b*n ∧ Gcd m n = b*n - a*m)

63. Cantor's Theorem

xl-gft
cantor_thm
⊢ ∀f : 'a → 'a SET• ∃A• ∀x• ¬f x = A

64. L'Hospital's Rule

xl-gft
l'hopital_lim_right_thm
⊢ ∀f df g dg a b c•
ftbrfttaba < b
fttabf a = 0.
fttabg a = 0.
fttab(∀x•a ≤ x ∧ x < b ⇒ f Cts x)
fttab(∀x•a < x ∧ x < b ⇒ (f Deriv df x) x)
fttab(∀x•a ≤ x ∧ x < b ⇒ g Cts x)
fttab(∀x•a < x ∧ x < b ⇒ (g Deriv dg x) x)
fttab(∀x•a < x ∧ x < b ⇒ ¬dg x = 0.)
fttab((λx• df x * dg x <sup>-</sup><sup>1</sup>) +#-> c) a
fttab((λx• f x * g x <sup>-</sup><sup>1</sup>) +#-> c) a


xl-gft
l'hopital_lim_infinity_thm
⊢ ∀f df g dg a c•
ftbrfttabg -+#>+#
fttab(∀x•a < x ⇒ (f Deriv df x) x)
fttab(∀x•a < x ⇒ (g Deriv dg x) x)
fttab(∀x•a < x ⇒ ¬dg x = 0.)
fttab(λx• df x * dg x <sup>-</sup><sup>1</sup>) -+#> c
fttab(λx• f x * g x <sup>-</sup><sup>1</sup>) -+#> c

66. Sum of a Geometric Series

xl-gft
geometric_sum_thm
⊢ ∀n x•
ftbrfttab¬x = 1.
fttabSeries (λ m• x ^ m) (n+1) = (1. - x^(n+1)) / (1. - x)

68. Sum of an arithmetic series

xl-gft
arithmetic_sum_thm
⊢ ∀c d n•
ftbrfttabSeries (λm• c + ℕℝ m * d) n =
ftbrfttab1/2 * ℕℝ n * (2. * c + (ℕℝ n - 1.) * d)

69. Greatest Common Divisor Algorithm

xl-gft
euclid_algorithm_thm
⊢ ∀m n•
ftbrfttab0 < m ∧ 0 < n
fttabGcd m n = if m < n then Gcd m (n-m) else if m = n then m else Gcd (m-n) n


xl-gft
gcd_def
⊢ ∀m n•
ftbrfttab0 < m ∧ 0 < n
fttabGcd m n Divides m ∧ Gcd m n Divides n
fttab(∀d•
ftbrfttab fttabd Divides m ∧ d Divides n
ftbrfttabfttabd Divides Gcd m n)

71. Order of a Subgroup

xl-gft
lagrange_cosets_thm
⊢ ∀G H•
ftbrfttabG ∈ Group ∧ Car G ∈ Finite ∧ H ∈ Subgroup G
fttabCar H ∈ Finite ∧ Car(G/H) ∈ Finite ∧ #G = #H * #(G/H)

74. The Principle of Mathematical Induction

xl-gft
induction_thm
⊢ ∀ p• p 0 ∧ (∀ m• p m ⇒ p (m + 1)) ⇒ (∀ n• p n)

75. The Mean Value Theorem

xl-gft
cauchy_mean_value_thm
⊢ ∀f df g dg a b•
ftbrfttaba < b
fttab(∀x•a ≤ x ∧ x ≤ b ⇒ f Cts x)
fttab(∀x•a < x ∧ x < b ⇒ (f Deriv df x) x)
fttab(∀x•a ≤ x ∧ x ≤ b ⇒ g Cts x)
fttab(∀x•a < x ∧ x < b ⇒ (g Deriv dg x) x)
fttab(∃x• a < x ∧ x < b ∧ (dg x)*(f b - f a) = (df x)*(g b - g a))


xl-gft
mean_value_thm
⊢ ∀f df a b•
ftbrfttaba < b
fttab(∀x•a ≤ x ∧ x ≤ b ⇒ f Cts x)
fttab(∀x•a < x ∧ x < b ⇒ (f Deriv df x) x)
fttab(∃x•a < x ∧ x < b ∧ f b - f a = (b - a) * df x)

78. The Cauchy-Schwarz Inequality

xl-gft
schwarz_inequality_thm
⊢ ∀f g A•
fttabSupp f ∈ Finite ∧ Supp g ∈ Finite
fttabAbs (f .v g) ≤ Norm f * Norm g

79. The Intermediate Value Theorem

xl-gft
intermediate_value_thm
⊢ ∀f a b•
ftbrfttaba < b
fttab(∀x•a ≤ x ∧ x ≤ b ⇒ f Cts x)
fttab(∀y•
ftbrfttab fttab(f a < y ∧ y < f b ∨ f b < y ∧ y < f a)
ftbrfttabfttab∃x• a < x ∧ x < b ∧ f x = y)

80. The Fundamental Theorem of Arithmetic

xl-gft
unique_factorisation_thm
⊢ ∀m•
ftbrfttab0 < m
fttab1 e•fttab{k | ¬e k = 0} ∈ Finite ∧ {k | ¬e k = 0} ⊆ Prime
ftbrfttabfttabm = Π {k | ¬e k = 0} (λp• p ^ e p)

81. Divergence of the Prime Reciprocal Series

xl-gft
recip_primes_div_thm
fttab(∀n•{p | p ∈ Prime ∧ p ≤ n} ∈ Finite)
fttab(∀m•∃n• ℕℝ m ≤ Σ {p | p ∈ Prime ∧ p ≤ n} (λp• ℕℝ p <sup>-</sup><sup>1</sup>))

85. Divisibility by 3 Rule

xl-gft
div_3_rule_thm
⊢ ∀digits; n:ℕ•
ftbrfttab3 Divides Σ {i | i < n} (λi•digits i * 10 ^ i) ⇔
ftbrfttab3 Divides Σ {i | i < n} (λi•digits i)

89. The Factor and Remainder Theorems

xl-gft
poly_factor_thm
⊢ ∀l1 c•
ftbrfttab¬l1 = []
fttabPolyEval l1 c = 0.
fttab∃l2•
ftbrfttab fttabLength l2 < Length l1
ftbrfttabfttab(λx• PolyEval l1 x) = (λx• (x - c)*PolyEval l2 x)


xl-gft
poly_remainder_thm
⊢ ∀l1 c•
ftbrfttab¬l1 = []
fttab∃l2•
ftbrfttab fttabLength l2 < Length l1
ftbrfttabfttab(λx• PolyEval l1 x) = (λx• (x - c)*PolyEval l2 x + PolyEval l1 c)

91. The Triangle Inequality

xl-gft
triangle_inequality_thm
⊢ ∀f g•
ftbrfttabSupp f ∈ Finite ∈ Finite ∧ Supp g ∈ Finite
fttabSupp (λx• f x + g x) ∈ Finite
fttabNorm (λ x• f x + g x) ≤ Norm f + Norm g

93. The Birthday Problem

xl-gft
birthdays_thm

ftbrfttabletfttabS = {L | Elems L ⊆ {i | 1 ≤ i ∧ i ≤ 365} ∧ # L = 23}
ftbrfttabin letfttabX = {L | L ∈ S ∧ ¬L ∈ Distinct}
ftbrfttabin
ftbrfttab fttabS ∈ Finite
ftbrfttabfttab¬#S = 0
ftbrfttabfttabX ⊆ S
ftbrfttabfttab#X / #S > 1/2

96. Principle of Inclusion/Exclusion

xl-gft
size_inc_exc_thm
⊢ ∀I U A•
ftbrfttabI ∈ Finite ∧ ¬I = {}
fttab(∀i• i ∈ I ⇒ U i ∈ Finite)
fttabA = ⋃{B | ∃i• i ∈ I ∧ B = U i}
fttabℕℝ(# A) =
ftbrfttabΣ
ftbrfttab(℘I \ {{}})
ftbrfttab(λJ• ~1. ^ (#J + 1) * ℕℝ(# (⋂{B | ∃j• j ∈ J ∧ B = U j})))

99. Buffon Needle Problem

xl-gft
buffon_needle_thm

ftbrfttabletfttabS = {(θ, d) | θ ∈ ClosedInterval 0. π ∧ d ∈ ClosedInterval 0. 1.}
ftbrfttabin letfttabx_axis = {(x, y) | y = 0.}
ftbrfttabin letfttabneedle(θ, d) =
ftbrfttabfttab{(x, y) | ∃t• t ∈ ClosedInterval 0. 1.
ftbrfttabfttabfttab∧ x = t * Cos θ ∧ y = d - t * Sin θ}
ftbrfttabin letfttabX = {(θ, d) | (θ, d) ∈ S ∧ ¬needle(θ, d) ∩ x_axis = {}}
ftbrfttabin
ftbrfttab fttabX ⊆ S
ftbrfttabfttab∃x s•
ftbrfttab fttab fttab¬s = 0.
ftbrfttab fttabfttabX Area x
ftbrfttab fttabfttabS Area s
ftbrfttab fttabfttabx / s = 2. / π

100. Descartes Rule of Signs

xl-gft
descartes_rule_thm
⊢ ∀f•
ftbrfttabf ∈ PolyFunc
fttab¬f = (λx• 0.)
fttab∃k•
ftbrfttabSignChanges (Coeffs f) =
ftbrfttabΣ {r | 0. < r ∧ r ∈ Roots f} (λr• RootMultiplicity f r) + 2*k

This page was prepared as a ProofPower document by Rob Arthan and translated into HTML in collusion with Roger Jones.

up quick index

privacy policy

Created:

$Id: rda001.xml,v 1.12 2009/12/16 21:55:38 rbj Exp $

V