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.

If the theorem is not part of the Isabelle distribution, the entry will usually contain a link to the repository that does. The list does not automatically track the most recent version of each theorem. If you find one that that is out of date and would like me to update it, let me know.

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

theorem rat_denum: "∃f :: nat ⇒ rat. surj f"

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"

http://www.andrew.cmu.edu/user/avigad/isabelle/NumberTheory/PrimeNumberTheorem.html

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

corollary circle_area: "r ≥ 0 ⟹ content (ball c r :: (real ^ 2) set) = r ^ 2 * pi"

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"

https://bitbucket.org/MohammadAbdulaziz/isabellegeometry/src/ec1dba0753fd4b9a327fee26d15c9743968f63c0/green.thy

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

39. Solutions to Pell's Equation

theorem pell_solutions:
  fixes D :: nat
  assumes "k. D = k2"
  obtains "x0" "y0" :: nat
  where   "(x::int) (y::int).
             x2 - D * y2 = 1 
            (n::nat. nat ¦x¦ + sqrt D * nat ¦y¦ = (x0 + sqrt D * y0) ^ n)"

corollary pell_solutions_infinite:
  fixes D :: nat
  assumes "k. D = k2"
  shows   "infinite {(x :: int, y :: int). x2 - D * y2 = 1}"

https://www.isa-afp.org/entries/Pell.html

40. Minkowski's Fundamental Theorem

theorem minkowski:
  fixes B :: "(real ^ 'n) set"
  assumes "convex B" and symmetric: "uminus ` B ⊆ B"
  assumes meas_B [measurable]: "B ∈ sets lebesgue"
  assumes measure_B: "emeasure lebesgue B > 2 ^ CARD('n)"
  obtains x where "x ∈ B" and "x ≠ 0" and "⋀i. x $ i ∈ ℤ"

https://www.isa-afp.org/entries/Minkowskis_Theorem.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)"

https://github.com/avigad/isabelle/blob/master/Analysis/Central_Limit_Theorem.thy#L69

48. Dirichlet's Theorem

theorem Dirichlet:
  assumes "coprime h n"
  shows   "infinite {p. prime p ∧ [p = h] (mod n)}"

https://devel.isa-afp.org/entries/Dirichlet_L.html

49. Cayley-Hamilton Theorem

theorem Cayley_Hamilton:
  fixes A :: "'acomm_ring_1^'nfinite^'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

57. 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))"

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

67. e is Transcendental

corollary e_transcendental_real: "¬ algebraic (exp 1 :: real)"

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

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:
  "(kn::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 "¦xy¦  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. ∑pprimes_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. vV  uV  vu  ! n. adjacent v n  adjacent u n" and "finite V"
  shows "v. nV. nv  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)(^)Rk P f = g P q P r 
        (r = 𝟬P | deg R r < deg R g)"

90. Stirling's Formula

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

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

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:
    "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"

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

98. Bertrand's Postulate

theorem bertrand: "n > 1 ⟹ ∃p∈{n<..<2*n}. prime p"

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

99. Buffon Needle Problem

theorem buffon_short:
assumes "l ≤ d"
shows   "emeasure (buffon l d) {True} = 2 * l / (d * pi)"

theorem buffon_long:
assumes "l ≥ d"
shows   "emeasure (buffon l d) {True} = 2 / pi * ((l / d) - sqrt ((l / d)⇧2 - 1) + arccos (d / l))"

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

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