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, please so I can add them here.

## 1. Square Root of 2 is Irrational

```theorem sqrt_prime_irrational:
"prime p ⟹ sqrt (real p) ∉ ℚ"
```

## 2. Fundamental Theorem of Algebra

```lemma fundamental_theorem_of_algebra:
assumes nc: "¬ constant (poly p)"
shows "∃z::complex. poly p z = 0"
```

## 3. Denumerability of the Rational Numbers

```instance rat :: countable
proof
show "∃to_nat::rat ⇒ nat. inj to_nat"
```

## 4. Pythagorean Theorem

```lemma pythagoras_verbose:
"((A1::real) - 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)"

lemma pythagoras:
defines ort:"orthogonal ≡ (λ(A::point) B. fst A * fst B + snd A * snd B = 0)"
and vc:"vector ≡ (λ(A::point) B. (fst A  - fst B, snd A - snd B))"
and vcn:"vecsqnorm ≡ (λA::point. fst A ^ 2 + snd A ^2)"
assumes o: "orthogonal (vector A B) (vector C B)"
shows "vecsqnorm(vector C A) = vecsqnorm(vector B  A) + vecsqnorm(vector C B)"
```

## 5. Prime Number Theorem

```lemma PrimeNumberTheorem: "(λx. pi x * ln (real x) / (real x)) ----> 1"
```

## 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⌉)"
```

https://isa-afp.org/entries/Incompleteness.shtml

## 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::int)^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"
```

https://isa-afp.org/entries/Impossible_Geometry.shtml

## 9. The Area of a Circle

```lemma circle_area:
assumes "R ≥ 0"
shows "emeasure lborel {z::real×real. norm z ≤ R} = R^2 * pi"
```

https://github.com/3of8/circlearea/blob/master/Circle_Area.thy

## 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: "~ finite {p::nat. prime p}"
```

## 12. The Independence of the Parallel Postulate

https://isa-afp.org/entries/Tarskis_Geometry.shtml

## 14. Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + ….

```theorem basel_problem: "(λn. 1 / (n + 1)²) sums (pi^2 / 6)"
```

## 15. Fundamental Theorem of Integral Calculus

```lemma fundamental_theorem_of_calculus:
assumes "a ≤ b"
assumes f': "∀x. a ≤ x ∧ x ≤ b ⟶ DERIV f x :> f'(x)"
shows "Integral (a, b) f' (f(b) - f(a))"
```

## 17. DeMoivre’s Theorem

```lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"

lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
```

## 18. Liouville’s Theorem and the Construction of Transcendental Numbers

```corollary transcendental_liouville_constant:
"¬algebraic (standard_liouville (λ_. 1) 10)"
```

https://isa-afp.org/entries/Liouville_Numbers.shtml

## 19. Lagrange’s Four-Square Theorem

```theorem four_squares:
"(n::int) ≥ 0 ⟹ ∃ a b c d. a^2 + b^2 + c^2 + d^2 = n"
```

https://isa-afp.org/entries/FourSquares.shtml

## 20. All Primes (1 mod 4) Equal the Sum of Two Squares

```lemma qf1_prime_exists:
"zprime (4*m+1) ⟹ ∃ x y. x^2 + y^2 = 4*m+1"
```

## 21. Green’s theorem

```lemma GreenThm_typeI_typeII_divisible_region:
assumes valid_typeI_div: "valid_typeI_division s twoChain_typeI" and
valid_typeII_div: "valid_typeII_division s twoChain_typeII" and
f_analytically_valid: "∀twoC ∈ twoChain_typeI. analytically_valid (cubeImage twoC) (%x. (F x) ∙ i) j"
"∀twoC ∈ twoChain_typeII. analytically_valid (cubeImage twoC) (%x. (F x) ∙ j) i" and
only_vertical_division:
"only_vertical_division one_chain_typeI twoChain_typeI"
"boundary_chain one_chain_typeI" and
only_horizontal_division:
"only_horizontal_division one_chain_typeII twoChain_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"
```

## 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"
```

https://isa-afp.org/entries/Fermat4.shtml

## 25. Schroeder-Bernstein Theorem

```lemma schroeder_bernstein:
"[| f ∈ inj(X,Y);  g ∈ inj(Y,X) |] ==> ∃h. h ∈ bij(X,Y)"
```

## 26. Leibnitz’s Series for Pi

```theorem pi_series:
"pi / 4 = (∑ k. (-1)^k * 1 / real (k*2+1))"
```

## 27. 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"
```

https://isa-afp.org/entries/Triangle.shtml

## 30. 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)"
```

## 31. Ramsey’s Theorem

```lemma ramsey: "
∀(s::nat) (r::nat) (YY::'a set) (f::'a set => nat).
infinite YY
∧ (∀X. X <= YY ∧ finite X ∧ card X = r ⟶ f X < s)
⟶ (∃Y' t'.
Y' <= YY
∧ infinite Y'
∧ t' < s
∧ (∃X. X <= Y' ∧ finite X ∧ card X = r ⟶ f X = t'))"
```

https://isa-afp.org/entries/Ramsey-Infinite.shtml

## 34. Divergence of the Harmonic Series

```theorem DivergenceOfHarmonicSeries:
shows "¬summable (λn. 1/real (Suc n))"
```

## 35. Taylor’s Theorem

```lemma taylor:
assumes INIT: "n>0" "diff 0 = f"
and DERIV: "(∀ m t. m < n & a ≤ t & t ≤ b ⟶ DERIV (diff m) t :> (diff (Suc m) t))"
and INTERV: "a ≤ c " "c ≤ b" "a ≤ x" "x ≤ b" "x ≠ c"
shows "∃ t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
f x = (∑m<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 :: "'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"
```

## 37. 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))"
```

## 38. Arithmetic Mean / Geometric Mean

```theorem CauchysMeanTheorem_Eq:
fixes z::"real list"
assumes "pos z"
shows "gmean z = mean z ⟷ het z = 0"
```

https://isa-afp.org/entries/Cauchy.shtml

## 44. The Binomial Theorem

```corollary binomial:
"(a+b::nat)^n = (∑k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))"
```

## 45. 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)}"
```

https://isa-afp.org/entries/Euler_Partition.shtml

## 46. 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"
```

## 47. 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_integrable: "⋀n. integrable M (X n)" 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)"
```

## 49. Cayley-Hamilton Theorem

```theorem Cayley_Hamilton:
fixes A :: "'a∷comm_ring_1^'n∷finite^'n"
shows "evalmat (charpoly A) A = 0"
```

https://isa-afp.org/entries/Cayley_Hamilton.shtml

## 51. Wilson’s Theorem

```theorem Wilson_Russ:
"zprime p ==> [zfact (p - 1) = -1] (mod p)"
```

## 52. The Number of Subsets of a Set

```lemma card_Pow:
"finite A ⟹ card (Pow A) = 2 ^ 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'"
```

https://isa-afp.org/entries/Koenigsberg_Friendship.shtml

## 55. 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"
```

https://www.isa-afp.org/entries/Chord_Segments.shtml

## 58. Formula for the Number of Combinations

```theorem n_subsets:
"finite A ⟹ card {B. B ⊆ A ∧ card B = k} = (card A choose k)"
```

## 60. Bezout’s Theorem

```lemma bezout:
"∃(d::nat) x y. d dvd a ∧ d dvd b ∧ (a * x - b * y = d ∨ b * x - a * y = d)"
```

## 63. Cantor’s Theorem

```lemma cantor1:
"¬ (∃f:: 'a ⇒ 'a set. ∀S. ∃x. f x = S)"
```

## 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)"
```

## 65. Isosceles Triangle Theorem

```lemma isosceles_triangle:
assumes "dist a c = dist b c"
shows   "angle b a c = angle a b c"
```

https://isa-afp.org/entries/Triangle.shtml

## 66. Sum of a Geometric Series

```lemma geometric_sums:
"norm c < 1 ⟹ (λn. c^n) sums (1 / (1 - c))"

lemma suminf_geometric:
"norm c < 1 ⟹ suminf (λn. c^n) = 1 / (1 - c)"
```

## 68. Sum of an Arithmetic Series

```lemma arith_series_int:
"2 * (∑i∈{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"
```

## 69. Greatest Common Divisor Algorithm

```lemma 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::nat)^(n+1) - 1)"
```

https://isa-afp.org/entries/Perfect-Number-Thm.shtml

## 71. Order of a Subgroup

```theorem (in group) lagrange:
"⟦finite(carrier G); subgroup H G⟧
⟹ card(rcosets 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"
```

## 73. Ascending or Descending Sequences

```lemma Erdoes_Szekeres:
fixes f :: "_ ⇒ 'a::linorder"
shows "(∃S. S ⊆ {0..m * n} ∧ card S = m + 1 ∧ mono_on f (op ≤) S) ∨
(∃S. S ⊆ {0..m * n} ∧ card S = n + 1 ∧ mono_on f (op ≥) S)"
```

## 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:
assumes lt:  "a < b"
and con: "∀x. a ≤ x & x ≤ b --> isCont f x"
and dif: "∀x. a < x & x < b --> f differentiable (at x)"
shows "∃l z::real. a < z & z < b & DERIV f z :> l &
(f(b) - f(a) = (b-a) * l)"

lemma MVT2:
"[| a < b; ∀x. a ≤ x & x ≤ b --> DERIV f x :> f'(x) |]
==> ∃z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))"
```

## 77. Sum of kth powers

```lemma sum_of_powers:
"(∑k≤n::nat. (real k) ^ m) = (bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0) / (m + 1)"
```

## 78. 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

## 79. The Intermediate Value Theorem

```lemma IVT:
fixes f :: "'a :: linear_continuum_topology ⇒ 'b :: linorder_topology"
shows "f a ≤ y ⟹ y ≤ f b ⟹ a ≤ b ⟹
(∀x. a ≤ x ∧ x ≤ b ⟶ isCont f x) ⟹
∃x. a ≤ x ∧ x ≤ b ∧ f x = y"
```

## 80. Fundamental Theorem of Arithmetic

```theorem unique_prime_factorization:
"∀n. Suc 0 < n --> (∃!l. primel l ∧ nondec l ∧ prod l = n)"
```

## 81. 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

## 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"
```

https://isa-afp.org/entries/Koenigsberg_Friendship.shtml

## 85. Divisibility by Three Rule

```theorem three_divides_nat:
shows "(3 dvd n) = (3 dvd sumdig n)"
```

## 86. Lebesgue Measure and Integration

https://isa-afp.org/entries/Integration.shtml

## 88. Derangements Formula

```theorem derangements_formula:
assumes "n ≠ 0" "finite S" "card S = n"
shows "card (derangements S) = round (fact n / exp 1)"
```

https://isa-afp.org/entries/Derangements.shtml

## 89. 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)"
```

## 91. 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¦"
```

## 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)"
```

## 94. 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)"
```

https://isa-afp.org/entries/Triangle.shtml

## 95. 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:
shows "dist A C * dist B D = dist A B * dist C D + dist A D * dist B C"

```

https://www.isa-afp.org/entries/Ptolemys_Theorem.shtml

## 96. 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)))"
```

## 97. 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)"
```

## 100. 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"
```

https://isa-afp.org/entries/Descartes_Sign_Rule.shtml