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) or have any other corrections, please make a pull request or contact me in some other fashion.
- Square Root of 2 is Irrational
theorem sqrt_prime_irrational: assumes "prime (p::nat)" shows "sqrt p ∉ ℚ" corollary sqrt_2_not_rat: "sqrt 2 ∉ ℚ"https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Sqrt.html
- Fundamental Theorem of Algebra
lemma fundamental_theorem_of_algebra: assumes nc: "¬ constant (poly p)" shows "∃z::complex. poly p z = 0" - Denumerability of the Rational Numbers
theorem rat_denum: "∃f :: nat ⇒ rat. surj f"https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Countable.html
- Pythagorean Theorem
lemma Pythagoras: fixes A B C :: "'a :: real_inner" assumes "orthogonal (A - C) (B - C)" shows "(dist B C) ^ 2 + (dist C A) ^ 2 = (dist A B) ^ 2" -
Prime Number Theorem
Avigad et al. formalised the elementary Erdős–Selberg proof:
definition pi :: "nat ⇒ real" where "pi x = real (card {y::nat. y ≤ x ∧ prime y})" lemma PrimeNumberTheorem: "(λx. pi x * ln (real x) / real x) ⇢ 1"http://www.andrew.cmu.edu/user/avigad/isabelle/NumberTheory/PrimeNumberTheorem.html
A formalisation by Eberl and Paulson of the shorter analytic proof is available in the AFP:
definition primes_pi :: "real ⇒ real" where "primes_pi x = real (card {p::nat. prime p ∧ p ≤ x})" corollary prime_number_theorem: "primes_pi ∼[at_top] (λx. x / ln x)"Many alternative formulations of the PNT are also available. https://www.isa-afp.org/entries/Prime_Number_Theorem.html
-
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⌉)" -
Law of Quadratic Reciprocity
theorem Quadratic_Reciprocity: assumes "prime p" "2 < p" "prime q" "2 < q" "p ≠ q" shows "Legendre p q * Legendre q p = (-1) ^ ((p - 1) div 2 * ((q - 1) div 2))"https://isabelle.in.tum.de/dist/library/HOL/HOL-Number_Theory/Quadratic_Reciprocity.html
- 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" - The Area of a Circle
theorem content_ball: fixes c :: "'a :: euclidean_space" assumes "r ≥ 0" shows "content (ball c r) = pi powr (DIM('a) / 2) / Gamma (DIM('a) / 2 + 1) * r ^ DIM('a)" corollary content_circle: "r ≥ 0 ⟹ content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Ball_Volume.html
-
Euler’s Generalisation of Fermat’s Little Theorem
lemma euler_theorem: fixes a m :: nat assumes "coprime a m" shows "[a ^ totient m = 1] (mod m)"https://isabelle.in.tum.de/dist/library/HOL/HOL-Number_Theory/Residues.html
-
The Infinitude of Primes
lemma primes_infinite: "¬finite {p::nat. prime p}"https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Primes.html
-
The Independence of the Parallel Postulate
-
Polyhedron Formula
not formalised in Isabelle yet
-
Euler’s Summation of $1 + (\frac{1}{2})^2 + (\frac{1}{3})^2 + \ldots$
theorem inverse_squares_sums: "(λn. 1 / (n + 1)²) sums (pi² / 6)"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Gamma_Function.html
A generalisation of this to all even powers is also available in the AFP:
corollary nat_even_power_sums_real: assumes n: "n > 0" shows "(λk. 1 / real (k+1) ^ (2*n)) sums ((-1) ^ (n+1) * bernoulli (2*n) * (2*pi) ^ (2*n) / (2 * fact (2*n)))"https://www.isa-afp.org/browser_info/current/AFP/Bernoulli/Bernoulli_Zeta.html
-
Fundamental Theorem of Integral Calculus
theorem fundamental_theorem_of_calculus: fixes f :: "real ⇒ 'a :: banach" assumes "a ≤ b" and "⋀x. x ∈ {a..b} ⟹ (f has_vector_derivative f' x) (at x within {a..b})" shows "(f' has_integral (f b - f a)) {a..b}"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Henstock_Kurzweil_Integration.html
-
Insolvability of General Higher Degree Equations
not formalised in Isabelle yet
-
DeMoivre’s Theorem
lemma DeMoivre: "(cis a) ^ n = cis (real n * a)" lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"https://isabelle.in.tum.de/dist/library/HOL/HOL/Complex.html
-
Liouville’s Theorem and the Construction of Transcendental Numbers
corollary transcendental_liouville_constant: "¬algebraic (standard_liouville (λ_. 1) 10)" -
Lagrange’s Four-Square Theorem
theorem four_squares: "∃a b c d::nat. n = a² + b² + c² + d²" -
All Primes (1 mod 4) Equal the Sum of Two Squares
theorem two_squares: assumes "prime (p :: nat)" shows "(∃a b. p = a² + b²) ⟷ [p ≠ 3] (mod 4) -
Green’s theorem
lemma GreenThm_typeI_typeII_divisible_region: assumes only_vertical_division: "only_vertical_division one_chain_typeI two_chain_typeI" "boundary_chain one_chain_typeI" and only_horizontal_division: "only_horizontal_division one_chain_typeII two_chain_typeII" "boundary_chain one_chain_typeII" and typeI_and_typII_one_chains_have_common_subdiv: "common_boundary_sudivision_exists one_chain_typeI one_chain_typeII" shows "integral s (λx. partial_vector_derivative (λx. (F x) ∙ j) i x - partial_vector_derivative (λx. (F x) ∙ i) j x) = one_chain_line_integral F {i, j} one_chain_typeI" "integral s (λx. partial_vector_derivative (λx. (F x) ∙ j) i x - partial_vector_derivative (λx. (F x) ∙ i) j x) = one_chain_line_integral F {i, j} one_chain_typeII" -
The Non-Denumerability of the Continuum
theorem real_non_denum: "∄f :: nat ⇒ real. surj f"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Continuum_Not_Denumerable.html
-
Formula for Pythagorean Triples
theorem nat_euclid_pyth_triples: fixes a b c :: nat assumes "coprime a b" "odd a" "a² + b² = c²" shows "∃p q. a = p² - q² ∧ b = 2 * p * q ∧ c = p² + q² ∧ coprime p q" -
The Undecidability of the Continuum Hypothesis
corollary ctm_ZFC_imp_ctm_CH: assumes "M ≈ ω" "Transset(M)" "M ⊨ ZFC" shows "∃N. M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ N ⊨ ZFC ∪ {⋅CH⋅} ∧ (∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N))" corollary ctm_ZFC_imp_ctm_not_CH: assumes "M ≈ ω" "Transset(M)" "M ⊨ ZFC" shows "∃N. M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ N ⊨ ZFC ∪ {⋅¬⋅CH⋅⋅} ∧ (∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N))" -
Schröder–Bernstein Theorem
theorem Schroeder_Bernstein: fixes f :: "'a ⇒ 'b" and g :: "'b ⇒ 'a" and A :: "'a set" and B :: "'b set" assumes "inj_on f A" and "f ` A ⊆ B" and "inj_on g B" and "g ` B ⊆ A" shows "∃h. bij_betw h A B"https://isabelle.in.tum.de/dist/library/HOL/HOL/Inductive.html
-
Leibnitz’s Series for π
theorem pi_series: "pi / 4 = (∑k. (-1)^k * 1 / real (k*2+1))"https://isabelle.in.tum.de/dist/library/HOL/HOL/Transcendental.html
-
Sum of the Angles of a Triangle
lemma angle_sum_triangle: assumes "a ≠ b ∨ b ≠ c ∨ a ≠ c" shows "angle c a b + angle a b c + angle b c a = pi" -
Pascal’s Hexagon Theorem
not formalised in Isabelle yet
-
Feuerbach’s Theorem
not formalised in Isabelle yet
-
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)"https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Ballot.html
-
Ramsey’s Theorem
lemma ramsey: fixes r s :: nat and Y :: "'a set" and f :: "'a set ⇒ nat" assumes "infinite Y" assumes "∀X. X ⊆ Y ∧ finite X ∧ card X = r ⟶ f X < s" obtains Y' t where "Y' ⊆ Y" and "infinite Y'" and "t < s" and "∀X. X ⊆ Y' ∧ finite X ∧ card X = r ⟶ f X = t" using ramsey assms by metis -
The Four Color Problem
not formalised in Isabelle yet
-
Fermat’s Last Theorem
not formalised in Isabelle yet
-
Divergence of the Harmonic Series
theorem not_summable_harmonic: shows "¬summable (λn. 1 / real (n + 1))"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Summation_Tests.html
-
Taylor’s Theorem
theorem taylor: fixes a :: real and n :: nat and f :: "real ⇒ real" assumes "n > 0" and "diff 0 = f" and "∀m t. m < n ∧ t ∈ {a..b} ⟶ (diff m has_real_derivative diff (m + 1) t) (at t)" and "c ∈ {a..b}" and "x ∈ {a..b} - {c}" shows "∃t. t ∈ open_segment x c ∧ f x = (∑m<n. (diff m c / fact m) * (x - c) ^ m) + (diff n t / fact n) * (x - c) ^ n"https://isabelle.in.tum.de/dist/library/HOL/HOL/MacLaurin.html
-
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"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Brouwer_Fixpoint.html
-
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))"https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Cubic_Quartic.html
-
Arithmetic Mean / Geometric Mean
theorem CauchysMeanTheorem: fixes z :: "real list" assumes "pos z" shows "gmean z ≤ mean z" theorem CauchysMeanTheorem_Eq: fixes z :: "real list" assumes "pos z" shows "gmean z = mean z ⟷ het z = 0" -
Solutions to Pell’s Equation
theorem pell_solutions: fixes D :: nat assumes "∄k. D = k²" obtains "x₀" "y₀" :: nat where "∀(x::int) (y::int). x² - D * y² = 1 ⟷ (∃n::nat. nat ¦x¦ + sqrt D * nat ¦y¦ = (x₀ + sqrt D * y₀) ^ n)" corollary pell_solutions_infinite: fixes D :: nat assumes "∄k. D = k²" shows "infinite {(x :: int, y :: int). x² - D * y² = 1}" -
Minkowski’s Fundamental Theorem
theorem minkowski: fixes B :: "(real ^ 'n) set" assumes "convex B" and symmetric: "uminus ` B ⊆ B" assumes meas_B: "B ∈ sets lebesgue" assumes measure_B: "emeasure lebesgue B > 2 ^ CARD('n)" obtains x where "x ∈ B" and "x ≠ 0" and "⋀i. x $ i ∈ ℤ" -
Puiseux’s Theorem
The formal Puiseux series
'a fpxsfor some coefficient type'ais defined as the type of functionsrat ⇒ 'afor which the support is bounded from below and the denominators of the support have a common denominator:definition is_fpxs :: "(rat ⇒ 'a :: zero) ⇒ bool" where "is_fpxs f ⟷ bdd_below (supp f) ∧ (LCM r∈supp f. snd (quotient_of r)) ≠ 0" typedef (overloaded) 'a fpxs = "{f::rat ⇒ 'a :: zero. is_fpxs f}" morphisms fpxs_nth Abs_fpxsIt is then shown that if
'ais an algebraically closed field of characteristic 0, then'a fpxsis also an algebraically closed field:instance fpxs :: ("{alg_closed_field, field_char_0, field_gcd}") alg_closed_field -
Sum of the Reciprocals of the Triangular Numbers
definition triangle_num :: "nat ⇒ nat" where "triangle_num n = (n * (n + 1)) div 2" theorem inverse_triangle_num_sums: "(λn. 1 / triangle_num (Suc n)) sums 2"https://isabelle.in.tum.de/library/HOL/HOL-ex/Triangular_Numbers.html
-
The Isoperimetric Theorem
not formalised in Isabelle yet
-
The Binomial Theorem
theorem binomial_ring: fixes a b :: "'a :: comm_ring_1" shows "(a + b) ^ n = (∑k=0..n. of_nat (n choose k) * a ^ k * b ^ (n - k))"https://isabelle.in.tum.de/dist/library/HOL/HOL/Binomial.html
The generalised form where the exponent is not necessarily an integer is also available:
theorem gen_binomial_complex: fixes z :: complex assumes "norm z < 1" shows "(λn. (a gchoose n) * z^n) sums (1 + z) powr a"https://isabelle.in.tum.de/library/HOL/HOL-Analysis/Generalised_Binomial_Theorem.html
-
The Partition Theorem
theorem Euler_partition_theorem: "card {p. p partitions n ∧ (∀i. p i ≤ 1)} = card {p. p partitions n ∧ (∀i. p i ≠ 0 ⟶ odd i)}" -
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"https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Cubic_Quartic.html
-
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_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://isabelle.in.tum.de/dist/library/HOL/HOL-Probability/Central_Limit_Theorem.html
-
Dirichlet’s Theorem
theorem Dirichlet: assumes "n > 1" and "coprime h n" shows "infinite {p. prime p ∧ [p = h] (mod n)}" -
Cayley-Hamilton Theorem
theorem Cayley_Hamilton: fixes A :: "'a :: comm_ring_1 ^ ('n :: finite) ^ 'n" shows "evalmat (charpoly A) A = 0" -
The Number of Platonic Solids
not formalised in Isabelle yet
-
Wilson’s Theorem
lemma wilson_theorem: assumes "prime p" shows "[fact (p - 1) = -1] (mod p)"https://isabelle.in.tum.de/dist/library/HOL/HOL-Number_Theory/Residues.html
-
The Number of Subsets of a Set
lemma card_Pow: "finite A ⟹ card (Pow A) = 2 ^ card A" -
π is Transcendental
theorem transcendental_pi: "¬algebraic pi" -
The Königsberg 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'" -
Product of Segments of Chords
theorem product_of_chord_segments: fixes S1 T1 S2 T2 X C :: "'a :: euclidean_space" assumes "between (S1, T1) X" "between (S2, T2) X" assumes "dist C S1 = r" "dist C T1 = r" assumes "dist C S2 = r" "dist C T2 = r" shows "dist S1 X * dist X T1 = dist S2 X * dist X T2" -
The Hermite-Lindemann Transcendence Theorem
theorem Hermite_Lindemann: fixes α β :: "'a ⇒ complex" assumes "finite I" assumes "⋀x. x ∈ I ⟹ algebraic (α x)" assumes "⋀x. x ∈ I ⟹ algebraic (β x)" assumes "inj_on α I" assumes "(∑x∈I. β x * exp (α x)) = 0" shows "∀x∈I. β x = 0" corollary Hermite_Lindemann_original: fixes n :: nat and α :: "nat ⇒ complex" assumes "inj_on α {..<n}" assumes "⋀i. i < n ⟹ algebraic (α i)" assumes "linearly_independent_over_int (α ` {..<n})" shows "algebraically_independent_over_rat n (λi. exp (α i))" -
Heron’s formula
theorem heron: fixes A B C :: "real ^ 2" defines "a ≡ dist B C" and "b ≡ dist A C" and "c ≡ dist A B" defines "s ≡ (a + b + c) / 2" shows "content (convex hull {A, B, C}) = sqrt (s * (s - a) * (s - b) * (s - c))"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Simplex_Content.html
-
Formula for the Number of Combinations
theorem n_subsets: "finite A ⟹ card {B. B ⊆ A ∧ card B = k} = (card A choose k)"https://isabelle.in.tum.de/dist/library/HOL/HOL/Binomial.html
-
The Laws of Large Numbers
theorem (in prob_space) strong_law_of_large_numbers_iid: fixes X :: "nat ⇒ 'a ⇒ real" assumes indep: "indep_vars (λ_. borel) X UNIV" assumes distr: "⋀i. distr M borel (X i) = distr M borel (X 0)" assumes L1: "integrable M (X 0)" shows "AE x in M. (λn. (∑i<n. X i x) / n) ⇢ expectation (X 0)" -
Bezout’s Theorem
lemma (in euclidean_ring_gcd) bezout_coefficients: "bezout_coefficients a b = (x, y) ⟹ x * a + y * b = gcd a b"https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Euclidean_Algorithm.html
-
Theorem of Ceva
not formalised in Isabelle yet
-
Fair Games Theorem
not formalised in Isabelle yet
-
Cantor’s Theorem
lemma Cantors_paradox: "∄f. f ` A = Pow A" -
L’Hôpital’s Rule
lemma lhopital: fixes f g f' g' :: "real ⇒ real" assumes "f ─x→ 0" and "g ─x→ 0" assumes "∀⇩F u in at x. g u ≠ 0" assumes "∀⇩F u in at x. g' u ≠ 0" assumes "∀⇩F u in at x. (f has_real_derivative f' u) (at u)" assumes "∀⇩F u in at x. (g has_real_derivative g' u) (at u)" assumes "filterlim (λx. f' x / g' x) F (at x)" shows "filterlim (λx. f x / g x) F (at x)" -
Isosceles Triangle Theorem
lemma isosceles_triangle: assumes "dist a c = dist b c" shows "angle b a c = angle a b c" -
Sum of a Geometric Series
lemma geometric_sums: "norm c < 1 ⟹ (λn. c^n) sums (1 / (1 - c))" lemma suminf_geometric: "norm c < 1 ⟹ (∑n. c ^ n) = 1 / (1 - c)" -
e is Transcendental
corollary e_transcendental_real: "¬ algebraic (exp 1 :: real)" -
Sum of an Arithmetic Series
lemma double_arith_series: fixes a d :: "'a :: comm_semiring_1" shows "2 * (∑i=0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)" -
Greatest Common Divisor Algorithm
The greatest common divisor is defined in the
semiring_gcdtypeclass. Instances are provided for all the basic types, such as naturals, integers, and polynomials. The most important properties are:lemma gcd_dvd1: "gcd a b dvd a" and gcd_dvd2: "gcd a b dvd b" and gcd_greatest: "c dvd a ⟹ c dvd b ⟹ c dvd gcd a b"https://isabelle.in.tum.de/dist/library/HOL/HOL/GCD.html
For Euclidean rings (such as naturals, integers, and polynomials over a field) the following executable algorithm is also provided and proven equivalent to the above:
context normalization_euclidean_semiring begin qualified function gcd :: "'a ⇒ 'a ⇒ 'a" where "gcd a b = (if b = 0 then normalize a else gcd b (a mod b))" endhttps://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Euclidean_Algorithm.html
Similar algorithms are also provided for polynomials in more general settings.
-
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)" -
Order of a Subgroup
proposition (in group) lagrange_finite: assumes "finite (carrier G)" and "subgroup H G" shows "card (rcosets H) * card H = order G"https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/Coset.html
-
Sylow’s Theorem
theorem sylow_thm: assumes "prime p" and "group G" and "order G = p ^ a * m" and "finite (carrier G)" obtains H where "subgroup H G" and "card H = p ^ a"https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/Sylow.html
-
Ascending or Descending Sequences
lemma Erdoes_Szekeres: fixes f :: "_ ⇒ 'a::linorder" shows "(∃S. S ⊆ {0..m * n} ∧ card S = m + 1 ∧ mono_on f (≤) S) ∨ (∃S. S ⊆ {0..m * n} ∧ card S = n + 1 ∧ mono_on f (≥) S)"https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Erdoes_Szekeres.html
-
The Principle of Mathematical Induction
theorem nat_induct: fixes n :: nat assumes "P 0" and "⋀n. P n ⟹ P (n + 1)" shows "P n" -
The Mean Value Theorem
theorem MVT: fixes a b :: real and f :: "real ⇒ real" assumes "a < b" and "∀x∈{a..b}. isCont f x" and "∀x∈{a<..<b}. f differentiable (at x)" shows "∃l z. z ∈ {a<..<b} ∧ (f has_real_derivative l) (at z) ∧ f b - f a = (b - a) * l" lemma MVT2: fixes a b :: real and f f' :: "real ⇒ real" assumes "a < b" and "∀x∈{a..b}. (f has_real_derivative f' x) (at x)" shows "∃z. z ∈ {a<..<b} ∧ f b - f a = (b - a) * f' z" -
Fourier Series
corollary Fourier_Fejer_Cesaro_summable_simple: assumes f: "continuous_on UNIV f" and periodic: "⋀x. f (x + 2*pi) = f x" shows "(λn. (∑m<n. ∑k≤2*m. Fourier_coefficient f k * trigonometric_set k x) / n) ⇢ f x" -
Sum of k-th powers
lemma sum_of_powers: fixes m n :: nat shows "(∑k=0..n. k ^ m) = (bernpoly (m + 1) (n + 1) - bernpoly (m + 1) 0) / (m + 1)" -
The Cauchy-Schwarz Inequality
theorem CauchySchwarzReal: fixes x::vector assumes "vlen x = vlen y" shows "¦x ⋅ y¦ ≤ ∥x∥ * ∥y∥"https://isa-afp.org/entries/Cauchy.shtml
An alternative version is available in the standard library:
lemma Cauchy_Schwarz_ineq2: "¦x ∙ (y :: real_inner)¦ ≤ norm x * norm y"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Inner_Product.html
-
The Intermediate Value Theorem
lemma IVT': fixes f :: "real ⇒ real" assumes "a ≤ b" and "y ∈ {f a..f b}" and "continuous_on {a..b} f" obtains x where "x ∈ {a..b}" and "f x = y"https://isabelle.in.tum.de/dist/library/HOL/HOL/Topological_Spaces.html
-
Fundamental Theorem of Arithmetic
The function
prime_factorizationis defined for any factorial semiring. It returns the factorization as a multiset that fulfils the following properties:lemma in_prime_factors_iff: "p ∈ set_mset (prime_factors x) ⟷ x ≠ 0 ∧ p dvd x ∧ prime p" lemma prod_mset_prime_factorization: assumes "x ≠ 0" shows "prod_mset (prime_factorization x) = normalize x" lemma prime_factorization_unique: assumes "x ≠ 0" "y ≠ 0" shows "prime_factorization x = prime_factorization y ⟷ normalize x = normalize y"The
normalizefunction is required because associated elements (like -3 and 3) have the same factorization; for natural numbers, it is the identity.https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Factorial_Ring.html
-
Divergence of the Prime Reciprocal Series
corollary prime_harmonic_series_diverges: "¬convergent (λn. ∑p←primes_upto n. 1 / p)"https://isa-afp.org/entries/Prime_Harmonic_Series.shtml
The more precise asymptotic estimate given by Mertens’ Second Theorem is also available:
theorem mertens_second_theorem: "(λx. (∑p | real p ≤ x ∧ prime p. 1 / p) - ln (ln x) - meissel_mertens) ∈ O(λx. 1 / ln x)" -
Dissection of Cubes (J.E. Littlewood’s “elegant” proof)
not formalised in Isabelle yet
-
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" -
Morley’s Theorem
not formalised in Isabelle yet
-
Divisibility by Three Rule
theorem three_divides_nat: "3 dvd n ⟷ 3 dvd sumdig n"https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/ThreeDivides.html
-
Lebesgue Measure and Integration
https://isa-afp.org/entries/Integration.shtml
A more recent and more extensive library of the Lebesgue Measure and Lebesgue integration (and also the Bochner integral and the Henstock–Kurzweil integral and the connections between all of these) is also in the standard distribution:
https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Lebesgue_Measure.html
https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Nonnegative_Lebesgue_Integration.html
https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Bochner_Integration.html
https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Henstock_Kurzweil_Integration.thy.html
-
Desargues’s Theorem
theorem desargues_3D: assumes "desargues_config_3D A B C A' B' C' P α β γ" shows "rk {α, β, γ} ≤ 2" -
Derangements Formula
theorem derangements_formula: assumes "n ≠ 0" and "finite S" and "card S = n" shows "card (derangements S) = round (fact n / exp 1)" -
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)(^)⇘R⇙k ⊙⇘P⇙ f = g ⊗⇘P⇙ q ⊕⇘P⇙ r ∧ (r = 𝟬⇘P⇙ | deg R r < deg R g)"https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/UnivPoly.html
Independently,
HOL-Computational_Algebraprovides notions of division and remainder in Euclidean rings (such as naturals, integers, polynomials):https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Euclidean_Algorithm.html
-
Stirling’s Formula
The following gives the full asymptotic expansion of the complex log-Gamma function, and, derived from that, the first term of the asymptotic expansion of the complex Gamma function:
theorem ln_Gamma_complex_asymptotics_explicit: fixes m :: nat and α :: real assumes "m > 0" and "α ∈ {0<..<pi}" obtains C :: real and R :: "complex ⇒ complex" where "∀s::complex. s ∉ ℝ⇩≤⇩0 ⟶ ln_Gamma s = (s - 1/2) * ln s - s + ln (2 * pi) / 2 + (∑k=1..<m. bernoulli (k+1) / (k * (k+1) * s ^ k)) - R s" and "∀s. s ≠ 0 ∧ ¦arg s¦ ≤ α ⟶ norm (R s) ≤ C / norm s ^ m" lemma Gamma_complex_asymp_equiv: fixes α :: real assumes α: "α ∈ {0<..<pi}" defines "F ≡ inf at_infinity (principal (complex_cone' α))" shows "Gamma ∼[F] (λs. sqrt (2 * pi) * (s / exp 1) powr s / s powr (1 / 2))"There are also these slightly simpler versions for the real Gamma function and the factorial:
theorem Gamma_asymp_equiv: "Gamma ∼ (λx. sqrt (2*pi/x) * (x / exp 1) powr x :: real)" theorem fact_asymp_equiv: "fact ∼ (λn. sqrt (2*pi*n) * (n / exp 1) ^ n :: real)" -
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¦" -
Pick’s Theorem
not formalised in Isabelle yet
-
The Birthday Problem
lemma birthday_paradox: assumes "card S = 23" "card T = 365" shows "2 * card {f ∈ S→⇩E S T. ¬ inj_on f S} ≥ card (S →⇩E T)"https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Birthday_Paradox.html
-
The Law of Cosines
lemma cosine_law_triangle: "dist b c ^ 2 = dist a b ^ 2 + dist a c ^ 2 - 2 * dist a b * dist a c * cos (angle b a c)" -
Ptolemy’s Theorem
theorem ptolemy: fixes A B C D center :: "real ^ 2" assumes "dist center A = radius" and "dist center B = radius" assumes "dist center C = radius" and "dist center D = radius" assumes ordering_of_points: "radiant_of (A - center) ≤ radiant_of (B - center)" "radiant_of (B - center) ≤ radiant_of (C - center)" "radiant_of (C - center) ≤ radiant_of (D - center)" shows "dist A C * dist B D = dist A B * dist C D + dist A D * dist B C" -
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)))"https://isabelle.in.tum.de/dist/library/HOL/HOL/Binomial.html
-
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)"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Determinants.html
-
Bertrand’s Postulate
theorem bertrand: "n > 1 ⟹ ∃p∈{n<..<2*n}. prime p" -
Buffon Needle Problem
definition needle :: "real ⇒ real ⇒ real ⇒ real set" where "needle l x φ = closed_segment (x - l / 2 * sin φ) (x + l / 2 * sin φ)" locale Buffon = fixes d l :: real assumes d: "d > 0" and l: "l > 0" begin definition Buffon :: "(real × real) measure" where "Buffon = uniform_measure lborel ({-d/2..d/2} × {-pi..pi})" theorem prob_short: assumes "l ≤ d" shows "𝒫((x,φ) in Buffon. needle l x φ ∩ {-d/2, d/2} ≠ {}) = 2 * l / (d * pi)" theorem prob_long: assumes "l ≥ d" shows "𝒫((x,φ) in Buffon. needle l x φ ∩ {-d/2, d/2} ≠ {}) = 2 / pi * ((l / d) - sqrt ((l / d)² - 1) + arccos (d / l))" end - Descartes Rule of Signs
theorem descartes_sign_rule: fixes p :: "real poly" assumes "p ≠ 0" shows "∃d. even d ∧ coeff_sign_changes p = count_pos_roots p + d" -
Atiyah-Singer Index Theorem
not formalised in Isabelle yet
-
Baker’s Theorem on Linear Forms in Logarithms
not formalised in Isabelle yet
-
Black-Scholes Formula
not formalised in Isabelle yet
-
Borsuk-Ulam Theorem
not formalised in Isabelle yet
-
Cauchy’s Integral Theorem
proposition Cauchy_theorem_homotopic_paths: assumes hom: "homotopic_paths s g h" and "open s" and f: "f holomorphic_on s" and vpg: "valid_path g" and vph: "valid_path h" shows "contour_integral g f = contour_integral h f" proposition Cauchy_theorem_homotopic_loops: assumes hom: "homotopic_loops s g h" and "open s" and f: "f holomorphic_on s" and vpg: "valid_path g" and vph: "valid_path h" shows "contour_integral g f = contour_integral h f"https://isabelle.in.tum.de/dist/library/HOL/HOL-Complex_Analysis/Cauchy_Integral_Theorem.html
-
Cauchy’s Residue Theorem
theorem Residue_theorem: fixes s pts :: "complex set" and f::"complex ⇒ complex" and g :: "real ⇒ complex" assumes "open s" "connected s" "finite pts" and "f holomorphic_on s-pts" and "valid_path g" and "pathfinish g = pathstart g" and "path_image g ⊆ s-pts" and "∀z. (z ∉ s) ⟶ winding_number g z = 0" shows "contour_integral g f = 2 * pi * 𝗂 * (∑p∈pts. winding_number g p * residue f p)"https://isabelle.in.tum.de/dist/library/HOL/HOL-Complex_Analysis/Residue_Theorem.html
-
Chen’s theorem
not formalised in Isabelle yet
-
Every vector space is free
lemma (in vector_space) basis_exists: obtains B where "B ⊆ V" "independent B" "V ⊆ span B" "card B = dim V"https://isabelle.in.tum.de/dist/library/HOL/HOL/Vector_Spaces.html
-
Classification of Finite Simple Groups
not formalised in Isabelle yet
-
Classification of semisimple Lie groups (Killing, Cartan, Dynkin)
not formalised in Isabelle yet
-
Sophie Germain’s theorem
not formalised in Isabelle yet
-
Gödel’s Completeness Theorem
-
Gödel’s Second Incompleteness Theorem
theorem Goedel_II: "¬ ({} ⊢ Neg (PfP «Fls»))" -
Green-Tao Theorem
not formalised in Isabelle yet
-
Feit-Thompson Theorem
not formalised in Isabelle yet
-
Fundamental Theorem of Galois Theory
not formalised in Isabelle yet
-
Heine–Borel Theorem
Heine–Borel is actually the definition of compactness in Isabelle/HOL in any topological space:
definition (in topological_space) compact :: "'a set ⇒ bool" where "compact S ⟷ (∀C. (∀c∈C. open c) ∧ S ⊆ ⋃C ⟶ (∃D⊆C. finite D ∧ S ⊆ ⋃D))"For types of the
heine_boreltype class, this is proven to be equivalent to the set being bounded and closed:lemma compact_eq_bounded_closed: fixes s :: "'a :: heine_borel set" shows "compact s ⟷ bounded s ∧ closed s"It is shown that all Euclidean spaces are Heine–Borel, i.e. that
euclidean_spaceis a subclass ofheine_borel.https://isabelle.in.tum.de/dist/library/HOL/Topological_Spaces.html
https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Elementary_Metric_Spaces.html https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Topology_Euclidean_Space.html -
Hessenberg’s Theorem = “Pappus → Desargues”
theorem hessenberg_thereom: assumes "is_pappus" shows "desargues_prop" -
Hilbert Basis Theorem
not formalised in Isabelle yet
-
Hilbert Nullstellensatz
theorem strong_Nullstellensatz: assumes "finite X" and "F ⊆ P[X]" shows "ℐ (𝒱 F) = √ideal (F::((_::{countable,linorder} ⇒⇩0 nat) ⇒⇩0 _::alg_closed_field) set)" -
Hilbert-Waring theorem
not formalised in Isabelle yet
-
Invariance of Dimension
corollary invariance_of_dimension: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes contf: "continuous_on S f" and "open S" and injf: "inj_on f S" and "S ≠ {}" shows "DIM('a) ≤ DIM('b)"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Further_Topology.html
-
IP=PSPACE
not formalised in Isabelle yet
-
Jordan Curve Theorem
corollary Jordan_inside_outside: fixes c :: "real ⇒ complex" assumes "simple_path c" "pathfinish c = pathstart c" shows "inside (path_image c) ≠ {} ∧ open (inside (path_image c)) ∧ connected (inside (path_image c)) ∧ outside (path_image c) ≠ {} ∧ open (outside (path_image c)) ∧ connected (outside (path_image c)) ∧ bounded (inside (path_image c)) ∧ ¬ bounded (outside (path_image c)) ∧ inside (path_image c) ∩ outside(path_image c) = {} ∧ inside (path_image c) ∪ outside(path_image c) = - path_image c ∧ frontier (inside (path_image c)) = path_image c ∧ frontier (outside (path_image c)) = path_image c"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Jordan_Curve.html
-
Kepler Conjecture
not formalised in Isabelle yet
-
Lie’s work relating Algebras and Groups
not formalised in Isabelle yet
-
Nash’s Theorem
not formalised in Isabelle yet
-
Perelman-Hamilton-Thurston theorem classifying compact 3-manifolds
not formalised in Isabelle yet
-
Poincaré Conjecture
not formalised in Isabelle yet
-
Riemann Mapping Theorem
theorem Riemann_mapping_theorem: "open S ∧ simply_connected S ⟷ S = {} ∨ S = UNIV ∨ (∃f g. f holomorphic_on S ∧ g holomorphic_on ball 0 1 ∧ (∀z ∈ S. f z ∈ ball 0 1 ∧ g(f z) = z) ∧ (∀z ∈ ball 0 1. <span id="1">g z ∈ S ∧ f(g z) = z))"<span>https://isabelle.in.tum.de/dist/library/HOL/HOL-Complex_Analysis/Riemann_Mapping.html
-
Sorting takes Θ(N log N) steps
datatype 'a sorter = Return "'a list" | Query 'a 'a "bool ⇒ 'a sorter" primrec count_queries :: "('a × 'a) set ⇒ 'a sorter ⇒ nat" where "count_queries _ (Return _) = 0" | "count_queries R (Query a b f) = 1 + count_queries R (f ((a, b) ∈ R))" definition count_wc_queries :: "('a × 'a) set set ⇒ 'a sorter ⇒ nat" where "count_wc_queries Rs sorter = (if Rs = {} then 0 else Max ((λR. count_queries R sorter) ` Rs))" primrec eval_sorter :: "('a × 'a) set ⇒ 'a sorter ⇒ 'a list" where "eval_sorter _ (Return ys) = ys" | "eval_sorter R (Query a b f) = eval_sorter R (f ((a,b) ∈ R))" definition is_sorting :: "('a × 'a) set ⇒ 'a list ⇒ 'a list ⇒ bool" where "is_sorting R xs ys ⟷ (mset xs = mset ys) ∧ sorted_wrt R ys" corollary count_queries_bigomega: fixes sorter :: "nat ⇒ nat sorter" assumes sorter: "⋀n R. linorder_on {..<n} R ⟹ is_sorting R [0..<n] (eval_sorter R (sorter n))" defines "Rs ≡ λn. {R. linorder_on {..<n} R}" shows "(λn. count_wc_queries (Rs n) (sorter n)) ∈ Ω(λn. n * ln n)"https://www.isa-afp.org/entries/Comparison_Sort_Lower_Bound.html
-
Stokes’ Theorem
not formalised in Isabelle yet
-
Stone–Weierstraß Theorem
theorem (in function_ring_on) Stone_Weierstrass: assumes f: "continuous_on S f" shows "∃F∈UNIV → R. uniform_limit S F f sequentially" proposition Stone_Weierstrass_uniform_limit: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes S: "compact S" and f: "continuous_on S f" obtains g where "uniform_limit S g f sequentially" and "⋀n. polynomial_function (g n)"https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Weierstrass_Theorems.html
-
Thales’ Theorem
theorem thales: fixes A B C :: "'a :: real_inner" assumes "dist B (midpoint A C) = dist A C / 2" shows "orthogonal (A - B) (C - B)" -
Yoneda lemma
https://www.isa-afp.org/entries/Category.html
-
ζ(-1) = -1 / 12
theorem zeta_even_nat: "zeta (2 * of_nat n) = of_real ((-1) ^ (n+1) * bernoulli (2*n) * (2*pi)^(2*n) / (2 * fact (2*n)))" corollary zeta_neg1: "zeta (-1) = - 1 / 12"