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• a < b ∧(∀x• a < x ∧ x < b ⇒ (sf Deriv f x) x) ∧(sf Cts a) ∧ (sf Cts b) ⇒(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• p ∈ Prime ∧p = 4*m + 1 ⇒∃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: ℕ• a^2 + b^2 = c^2 ⇔∃m n d• {a; b} = {d*n*(2*m + n); 2*d*m*(m + n)} ∧c = d*(m^2 + (m + n)^2)

 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• letS = BallotCounts m n in letX = {s | s ∈ S ∧ ∀ i• ℕ⿿ 0 < s (i+1)} in S ∈ Finite ∧¬#S = 0 ∧X ⊆ S ∧(n < m ⇒ #X / #S = (m - n) / (m + n))

 31. Ramsey's Theorem

 xl-gft fin_exp_2_ramsey_thm ⊢ ∀a b • ∃n • ∀(V, E) • (V, E) ∈ symg ∧ V ∈ Finite ∧ #V ≥ n ⇒(∃ 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) -1) -> c

 35. Taylor's Theorem

 xl-gft taylor_thm ⊢ ∀n f D a b• a < b ∧D 0 = f ∧(∀ m x• m ≤ n ∧ a ≤ x ∧ x ≤ b ⇒ D m Cts x) ∧(∀ m x• m ≤ n ∧ a < x ∧ x < b ⇒ (D m Deriv D (m + 1) x) x) ⇒∃x• a < x ∧ x < b ∧f b = PowerSeries (λm• D m a * ℕℝ(m!)-1) (n+1) (b-a) + D (n+1) x * (b-a) ^ (n+1) * ℕℝ((n+1)!)-1

 38. Arithmetic Mean/Geometric Mean

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

 40. Minkowski's Fundamental Theorem

 xl-gft minkowski_thm ⊢ ∀A a• A ∈ Convex ∧A ∈ Bounded ∧¬A = {} ∧(∀x y• (x, y) ∈ A ⇒ (~x, ~y) ∈ A) ∧A Area a ∧a > 4. ⇒∃i j• (⿿ℝ i, ⿿ℝ j) ∈ A ∧¬(⿿ℝ 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• A ∈ Finite ∧ #A = n ⇒{X | X ⊆ A ∧ #X = m} ∈ Finite ∧#{X | X ⊆ A ∧ #X = m} = Binomial n m

 60. Bezout's Theorem

 xl-gft bezout_thm ⊢ ∀m n• 0 < m ∧ 0 < n ⇒(∃a b• b*n ≤ a*m ∧ Gcd m n = a*m - b*n) ∨(∃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• a < b ∧f a = 0. ∧g a = 0. ∧(∀x•a ≤ x ∧ x < b ⇒ f Cts x) ∧(∀x•a < x ∧ x < b ⇒ (f Deriv df x) x) ∧(∀x•a ≤ x ∧ x < b ⇒ g Cts x) ∧(∀x•a < x ∧ x < b ⇒ (g Deriv dg x) x) ∧(∀x•a < x ∧ x < b ⇒ ¬dg x = 0.) ∧((λx• df x * dg x -1) +#-> c) a ⇒((λx• f x * g x -1) +#-> c) a

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

 66. Sum of a Geometric Series

 xl-gft geometric_sum_thm ⊢ ∀n x• ¬x = 1. ⇒Series (λ 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• Series (λm• c + ℕℝ m * d) n = 1/2 * ℕℝ n * (2. * c + (ℕℝ n - 1.) * d)

 69. Greatest Common Divisor Algorithm

 xl-gft euclid_algorithm_thm ⊢ ∀m n• 0 < m ∧ 0 < n ⇒Gcd 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• 0 < m ∧ 0 < n ⇒Gcd m n Divides m ∧ Gcd m n Divides n ∧(∀d• d Divides m ∧ d Divides n ⇒d Divides Gcd m n)

 71. Order of a Subgroup

 xl-gft lagrange_cosets_thm ⊢ ∀G H• G ∈ Group ∧ Car G ∈ Finite ∧ H ∈ Subgroup G ⇒Car 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• a < b ∧(∀x•a ≤ x ∧ x ≤ b ⇒ f Cts x) ∧(∀x•a < x ∧ x < b ⇒ (f Deriv df x) x) ∧(∀x•a ≤ x ∧ x ≤ b ⇒ g Cts x) ∧(∀x•a < x ∧ x < b ⇒ (g Deriv dg x) x) ⇒(∃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• a < b ∧(∀x•a ≤ x ∧ x ≤ b ⇒ f Cts x) ∧(∀x•a < x ∧ x < b ⇒ (f Deriv df x) x) ⇒(∃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• Supp f ∈ Finite ∧ Supp g ∈ Finite ⇒Abs (f .v g) ≤ Norm f * Norm g

 79. The Intermediate Value Theorem

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

 80. The Fundamental Theorem of Arithmetic

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

 81. Divergence of the Prime Reciprocal Series

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

 85. Divisibility by 3 Rule

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

 89. The Factor and Remainder Theorems

 xl-gft poly_factor_thm ⊢ ∀l1 c• ¬l1 = [] ∧PolyEval l1 c = 0. ⇒∃l2• Length l2 < Length l1 ∧(λx• PolyEval l1 x) = (λx• (x - c)*PolyEval l2 x)

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

 91. The Triangle Inequality

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

 93. The Birthday Problem

 xl-gft birthdays_thm ⊢ letS = {L | Elems L ⊆ {i | 1 ≤ i ∧ i ≤ 365} ∧ # L = 23} in letX = {L | L ∈ S ∧ ¬L ∈ Distinct} in S ∈ Finite ∧¬#S = 0 ∧X ⊆ S ∧#X / #S > 1/2

 96. Principle of Inclusion/Exclusion

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

 99. Buffon Needle Problem

 xl-gft buffon_needle_thm ⊢ letS = {(θ, d) | θ ∈ ClosedInterval 0. π ∧ d ∈ ClosedInterval 0. 1.} in letx_axis = {(x, y) | y = 0.} in letneedle(θ, d) = {(x, y) | ∃t• t ∈ ClosedInterval 0. 1. ∧ x = t * Cos θ ∧ y = d - t * Sin θ} in letX = {(θ, d) | (θ, d) ∈ S ∧ ¬needle(θ, d) ∩ x_axis = {}} in X ⊆ S ∧∃x s• ¬s = 0. ∧ X Area x ∧S Area s ∧x / s = 2. / π

 100. Descartes Rule of Signs

 xl-gft descartes_rule_thm ⊢ ∀f• f ∈ PolyFunc ∧¬f = (λx• 0.) ⇒∃k• SignChanges (Coeffs f) = Σ {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.

privacy policy

Created:

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

V