Formalizing 100 theorems in Coq

This is an appendix to Freek Wiedijk's webpage webpage on the "top 100" mathematical theorems, to keep track of the statements of the 79 theorems that are formalised in Coq.

Drop me or Freek an email or make a pull request if you have updates. Preferably edit this file, from which this page has been generated.

Options:





1. The Irrationality of the Square Root of 2

many versions (in coq-community/qarith-stern-brocot):

One of many proofs

Theorem sqrt2_not_rational : forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower

2. Fundamental Theorem of Algebra

Herman Geuvers et al. (in coq-community/corn):

Lemma FTA : forall f : CCX, nonConst _ f -> {z : CC | f ! z [=] [0]}.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

3. The Denumerability of the Rational Numbers

Milad Niqui (in coq-community/qarith-stern-brocot):

Definition same_cardinality (A:Type) (B:Type) :=
  { f : A -> B & { g : B -> A |
    forall b,(compose _ _ _ f g) b = (identity B) b /\
    forall a,(compose _ _ _ g f) a = (identity A) a } }.

Definition is_denumerable A := same_cardinality A nat.

Theorem Q_is_denumerable: is_denumerable Q.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Daniel Schepler (in coq-community/topology):

Inductive CountableT (X:Type) : Prop :=
  | intro_nat_injection: forall f:X->nat, injective f -> CountableT X.

Lemma Q_countable: CountableT Q.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower

4. Pythagorean Theorem

Frédérique Guilhot (in coq-community/HighSchoolGeometry):

Theorem Pythagore :
  forall A B C : PO,
  orthogonal (vec A B) (vec A C) <->
  Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C) :>R.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Gabriel Braun (in https://github.com/GeoCoq/GeoCoq/blob/master/Tarski_dev/Ch15_lengths.v):

A synthetic proof in the context of Tarski's axioms.

Lemma pythagoras :
  forall
    (Tn : Tarski_neutral_dimensionless)
    (TnEQD : Tarski_neutral_dimensionless_with_decidable_point_equality Tn),
  Tarski_2D TnEQD ->
  Tarski_euclidean TnEQD ->
  forall
    O E E' A B C AC BC AB AC2 BC2
     AB2 : Tpoint,
  O <> E ->
  Per A C B ->
  Length O E E' A B AB ->
  Length O E E' A C AC ->
  Length O E E' B C BC ->
  Prod O E E' AC AC AC2 ->
  Prod O E E' BC BC BC2 ->
  Prod O E E' AB AB AB2 ->
  Sum O E E' AC2 BC2 AB2.

Reproducibility: last checked December 2022 with Coq 8.16

Constructive: hypotheses partially classical

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

5. Prime Number Theorem

Formalized in: HOL Light, Isabelle, Metamath

6. Gödel’s Incompleteness Theorem

Russell O'Connor (in coq-community/hydra-battles):

The second theorem assumes the last two Hilbert-Bernays-Loeb derivability conditions.

(* in goedel1.v *)
Theorem Goedel'sIncompleteness1st :
  wConsistent T ->
  exists f : Formula,
    ~ SysPrf T f /\
    ~ SysPrf T (notH f) /\ (forall v : nat, ~ In v (freeVarFormula LNN f)).

(* in goedel2.v *)
Hypothesis HBL2 : forall f, SysPrf T (impH (box f) (box (box f))).

Hypothesis HBL3 : forall f g, SysPrf T (impH (box (impH f g)) (impH (box f) (box g))).

Theorem SecondIncompletness :
  SysPrf T Con -> Inconsistent LNT T.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, nqthm

7. Law of Quadratic Reciprocity

Nathanaëlle Courant (in https://github.com/Ekdohibs/coq-proofs/blob/master/Reciprocity/Reciprocity.v#L1560):

Theorem Quadratic_reciprocity :
  (legendre p q) * (legendre q p) = (-1) ^ (((p - 1) / 2) * ((q - 1) / 2)).

Reproducibility: last checked December 2022 with Coq 8.16

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, nqthm

8. The Impossibility of Trisecting the Angle and Doubling the Cube

Formalized in: HOL Light, Isabelle

9. The Area of a Circle

Formalized in: HOL Light, Isabelle, Lean, Metamath, ProofPower

10. Euler’s Generalization of Fermat’s Little Theorem

Laurent Théry (in mathcomp):

Theorem Euler_exp_totient a n : coprime a n -> a ^ totient n = 1 %[mod n].

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar

11. The Infinitude of Primes

Russell O'Connor (in cocorico):

This statement was formerly in cocorico, compatible with Coq 7.3

Theorem ManyPrimes : ~(EX l:(list Prime) | (p:Prime)(In p l)).

Reproducibility: old proof compatible with Coq 7.3

Constructive: yes

Axioms used: (none)

Georges Gonthier (in https://x80.org/rhino-coq/):

There are other proofs of this theorem but you can browse this one in your browser with JsCoq.

Lemma prime_above m : {p | m < p & prime p}.

Reproducibility: last checked December 2022 with Coq 8.16

Constructive: yes

Axioms used: (none)

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

12. The Independence of the Parallel Postulate

Formalized in: HOL Light, Isabelle

13. Polyhedron Formula

Jean-François Dufourd (in coq-contribs/euler-formula):

(* nc : number of connected components
   nv : number of vertices
   ne : number of edges
   nf : number of faces
   nd : number of darts
   plf m : m is a planar formation
   inv_qhmap : see Euler1.v *)

Theorem Euler_Poincare_criterion: forall m:fmap,
  inv_qhmap m -> (plf m <-> (nv m + ne m + nf m - nd m) / 2 = nc m).

Reproducibility: as of December 2022, build success with Coq 8.13.2, failure with 8.14.1 (using git tag v8.11.0)

Constructive: to be determined

Axioms used:

Formalized in: Coq (constructive), HOL Light, Mizar

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

Jean-Marie Madiot (in coq-community/coqtail-math):

Theorem zeta2_pi_2_6 : Rser_cv (fun n => 1 / (n + 1) ^ 2) (PI ^ 2 / 6).

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

15. Fundamental Theorem of Integral Calculus

Luís Cruz-Filipe (in coq-community/corn):

Theorem FTC1 : Derivative J pJ G F.
Theorem FTC2 : {c : IR | Feq J (G{-}G0) [-C-]c}.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

The Coq development team (in coq's standard library):

Lemma FTC_Riemann :
  forall (f:C1_fun) (a b:R) (pr:Riemann_integrable (derive f (diff0 f)) a b),
  RiemannInt pr = f b - f a.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

16. Insolvability of General Higher Degree Equations

Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub (in mathcomp):

Lemma example_not_solvable_by_radicals :
  ~ solvable_by_radical_poly ('X^5 - 4 *: 'X + 2 : {poly rat}).

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq, Lean

17. DeMoivre’s Theorem

Coqtail team (in coq-community/coqtail-math):

De Moivre's formula is easily deduced from Euler's formula thanks to e^(n*z)=(e^z)^n.

Lemma Cexp_trigo_compat : forall a, Cexp (0 +i a) = cos a +i sin a.
Lemma Cexp_mult : forall a n, Cexp (INC n * a) = (Cexp a) ^ n.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

18. Liouville’s Theorem and the Construction of Trancendental Numbers

Valentin Blot (in coq-community/corn):

Theorem Liouville_theorem2 :
  {n : nat | {C : IR | Zero [<] C | forall (x : Q),
       (C[*]inj_Q IR (1#Qden x)%Q[^]n) [<=] AbsIR (inj_Q _ x [-] a)}}.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar

19. Four Squares Theorem

Guillaume Allais, Jean-Marie Madiot (in coq-community/coqtail-math):

Coq extraction produces a program that indeed computes a, b, c, d

Theorem lagrange_4_square_theorem : forall n, 0 <= n ->
  { a : _ & { b: _ & { c : _ & { d |
    n = a * a + b * b + c * c + d * d } } } }.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS

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

Laurent Théry (in coq-contribs/sum-of-two-square):

Definition sum_of_two_squares :=
  fun p => exists a , exists b , p = a * a + b * b.

Theorem two_squares_exists:
  forall p, prime p -> p = 2 \/ Zis_mod p 1 4 -> sum_of_two_squares p.

Reproducibility: as of December 2022, build success with Coq 8.10.2, failure with 8.11.2 (using git tag v8.10.0)

Constructive: yes

Axioms used: (none)

Laurent Théry (in https://github.com/thery/twoSquare/blob/master/fermat2.v):

proof using gaussian integers and mathcomp

Lemma sum2sprime p :
  odd p -> prime p -> p \is a sum_of_two_square = (p %% 4 == 1).

Reproducibility: last checked December 2022 with Coq 8.16

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

21. Green’s Theorem

Formalized in: Isabelle

22. The Non-Denumerability of the Continuum

Pierre-Marie Pédrot (in coq-community/coqtail-math):

Theorem R_uncountable : forall (f : nat -> R),
  {l : R | forall n, l <> f n}.

Theorem R_uncountable_strong : forall (f : nat -> R) (x y : R),
  x < y -> {l : R | forall n, l <> f n & x <= l <= y}.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

C-CoRN team (in coq-community/corn):

Theorem reals_not_countable :
  forall (f : nat -> IR), {x :IR | forall n : nat, x [#] (f n)}.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

23. Formula for Pythagorean Triples

David Delahaye (in coq-contribs/fermat4):

Lemma pytha_thm3 : forall a b c : Z,
  is_pytha a b c -> Zodd a ->
  exists p : Z, exists q : Z, exists m : Z,
    a = m * (q * q - p * p) /\ b = 2 * m * (p * q) /\
    c = m * (p * p + q * q) /\ m >= 0 /\
    p >= 0 /\ q > 0 /\ p <= q /\ (rel_prime p q) /\
    (distinct_parity p q).

Reproducibility: as of December 2022, build success with Coq 8.11.2, failure with 8.12.2 (using git tag v8.10.0)

Constructive: no

Axioms used:

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

24. The Undecidability of the Continuum Hypothesis

Formalized in: Isabelle, Lean

25. Schroeder-Bernstein Theorem

Hugo Herbelin (in coq-contribs/schroeder):

Theorem Schroeder : A <=_card B -> B <=_card A -> A =_card B.

Reproducibility: as of December 2022, build success with Coq 8.16 (using git tag v8.11.0)

Constructive: no

Axioms used:

Daniel Schepler (in coq-community/topology):

Theorem CSB (X Y : Type) (f : X -> Y) (g : Y -> X) :
  injective f ->
  injective g ->
  exists h : X -> Y, bijective h.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

26. Leibniz’s Series for Pi

Guillaume Allais (in coq's standard library):

Lemma PI_2_aux : {z : R | 7 / 8 <= z <= 7 / 4 /\ - cos z = 0}.
Definition PI := 2 * proj1_sig PI_2_aux.

Definition PI_tg n := / INR (2 * n + 1).
Lemma exists_PI : {l:R | Un_cv (fun N => sum_f_R0 (tg_alt PI_tg) N) l}.
Definition Alt_PI : R := 4 * (let (a,_) := exist_PI in a).

Theorem Alt_PI_eq : Alt_PI = PI.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Luís Cruz-Filipe (in coq-community/corn):

Lemma ArcTan_one : ArcTan One[=]Pi[/]FourNZ.

Lemma arctan_series : forall c : IR,
  forall (Hs :
    fun_series_convergent_IR
      (olor ([--]One) One)
      (fun i =>
        (([--]One)[^]i[/]nring (S (2*i))
        [//] nringS_ap_zero _ (2*i)){**}Fid IR{^}(2*i+1)))
    Hc,
       FSeries_Sum Hs c Hc[=]ArcTan c.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS

27. Sum of the Angles of a Triangle

Frédérique Guilhot (in coq-community/HighSchoolGeometry):

Theorem somme_triangle :
  forall A B C : PO,
  A <> B :>PO ->
  A <> C :>PO ->
  B <> C :>PO ->
  plus (cons_AV (vec A B) (vec A C))
    (plus (cons_AV (vec B C) (vec B A)) (cons_AV (vec C A) (vec C B))) =
  image_angle pi :>AV.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Boutry, Gries, Narboux (in https://github.com/GeoCoq/GeoCoq/blob/master/Meta_theory/Parallel_postulates/parallel_postulates.v):

It is shown that the sum of angles is two rights is equivalent to other versions of the parallel postulate

Theorem equivalent_postulates_assuming_greenberg_s_axiom :
  greenberg_s_axiom ->
  all_equiv
    (alternate_interior_angles_postulate::
     alternative_playfair_s_postulate::
     alternative_proclus_postulate::
     alternative_strong_parallel_postulate::
     consecutive_interior_angles_postulate::
     euclid_5::
     euclid_s_parallel_postulate::
     existential_playfair_s_postulate::
     existential_thales_postulate::
     inverse_projection_postulate::
     midpoint_converse_postulate::
     perpendicular_transversal_postulate::
     postulate_of_transitivity_of_parallelism::
     playfair_s_postulate::
     posidonius_postulate::
     universal_posidonius_postulate::
     postulate_of_existence_of_a_right_lambert_quadrilateral::
     postulate_of_existence_of_a_right_saccheri_quadrilateral::
     postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights::
     postulate_of_existence_of_similar_triangles::
     postulate_of_parallelism_of_perpendicular_transversals::
     postulate_of_right_lambert_quadrilaterals::
     postulate_of_right_saccheri_quadrilaterals::
     postulate_of_transitivity_of_parallelism::
     proclus_postulate::
     strong_parallel_postulate::
     tarski_s_parallel_postulate::
     thales_postulate::
     thales_converse_postulate::
     triangle_circumscription_principle::
     triangle_postulate::
     nil).

Reproducibility: last checked December 2022 with Coq 8.16

Constructive: yes

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

28. Pascal’s Hexagon Theorem

Magaud and Narboux (in coq-contribs/projective-geometry):

Definition is_hexamy A B C D E F :=
  (A<>B / A<>C / A<>D / A<>E / A<>F /
  B<>C / B<>D / B<>E / B<>F /
  C<>D / C<>E / C<>F /
  D<>E / D<>F /
  E<>F) /
  let a:= inter (line B C) (line E F) in
  let b:= inter (line C D) (line F A) in
  let c:= inter (line A B) (line D E) in
  Col a b c.

Lemma hexamy_prop: pappus_strong -> forall A B C D E F,
  (line C D) <> (line A F) ->
  (line B C) <> (line E F) ->
  (line A B) <> (line D E) ->
  
  (line A C) <> (line E F) ->
  (line B F) <> (line C D) ->
  is_hexamy A B C D E F -> is_hexamy B A C D E F.

Reproducibility: as of December 2022, build success with Coq 8.13.2, failure with 8.14.1 (using git tag v8.10.0)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Mizar

29. Feuerbach’s Theorem

Benjamin Grégoire, Loïc Pottier, and Laurent Théry (in Coq's test suite):

Lemma Feuerbach:  forall A B C A1 B1 C1 O A2 B2 C2 O2:point,
  forall r r2:R,
  X A = 0 -> Y A =  0 -> X B = 1 -> Y B =  0->
  middle A B C1 -> middle B C A1 -> middle C A B1 ->
  distance2 O A1 = distance2 O B1 ->
  distance2 O A1 = distance2 O C1 ->
  collinear A B C2 -> orthogonal A B O2 C2 ->
  collinear B C A2 -> orthogonal B C O2 A2 ->
  collinear A C B2 -> orthogonal A C O2 B2 ->
  distance2 O2 A2 = distance2 O2 B2 ->
  distance2 O2 A2 = distance2 O2 C2 ->
  r^2%Z = distance2 O A1 ->
  r2^2%Z = distance2 O2 A2 ->
  distance2 O O2 = (r + r2)^2%Z
  \/ distance2 O O2 = (r - r2)^2%Z
  \/ collinear A B C.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq (constructive), HOL Light

30. The Ballot Problem

Jean-Marie Madiot (in coq-community/coq-100-theorems):

Theorem bertrand_ballot p q :
  let l := filter (fun votes => count_votes votes "A" =? p) (picks (p + q) ["A"; "B"]) in
  p >= q ->
  (p + q) * List.length (filter (throughout (wins "A" "B")) l) =
  (p - q) * List.length (filter (wins "A" "B") l).

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

31. Ramsey’s Theorem

Frédéric Blanqui (in color):

Theorem ramsey A (W : set A) n (P : Pinf W) B : forall (C : Pf B)
  (f : Pcard P (S n) -> elts C), Proper (Pcard_equiv ==> elts_eq) f ->
  exists c (Q : Pinf P), forall X : Pcard Q (S n), f (Pcard_subset Q X) = c.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower, nqthm

32. The Four Color Problem

Georges Gonthier, Benjamin Werner (in coq-community/fourcolor):

Theorem four_color m : simple_map m -> colorable_with 4 m.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq

33. Fermat’s Last Theorem

Formalized in: (none)

34. Divergence of the Harmonic Series

Coqtail (in coq-community/coqtail-math):

Lemma harmonic_series_equiv : (sum_f_R0 (fun n ⇒ / (S n))) ~ (fun n ⇒ ln (S (S n))).

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

35. Taylor’s Theorem

Luís Cruz-Filipe (in coq-community/corn):

Theorem Taylor : forall e, Zero [<] e -> forall Hb',
  {c : IR | Compact (Min_leEq_Max a b) c |
    forall Hc, AbsIR (F b Hb'[-]Part _ _ Taylor_aux[-]deriv_Sn c Hc[*] (b[-]a)) [<=] e}.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

36. Brouwer Fixed Point Theorem

Formalized in: HOL Light, Isabelle, Mizar

37. The Solution of a Cubic

Frédéric Chardard (in coq-community/coq-100-theorems):

Definition Cardan_Tartaglia_formula:=fun (a1:C) (a2:C) (a3:C) (n:nat) =>
  let s:=-a1/3 in
  let p:=a2+2*s*a1+3*Cpow s 2 in
  let q:=a3+a2*s+a1*Cpow s 2+Cpow s 3 in
  let Delta:=(Cpow (q/2) 2)+(Cpow (p/3) 3) in
  let alpha : C :=if(Ceq_dec p 0) then (RtoC 0) else (cubicroot (-(q/2)+Csqrt Delta)) in
  let beta:=if(Ceq_dec p 0) then -cubicroot q else -(p/3)/alpha in
  s+(alpha*Cpow CJ n+beta*Cpow CJ (n+n)).

Theorem Cardan_Tartaglia : forall a1 a2 a3 :C,
  let u1:=(Cardan_Tartaglia_formula a1 a2 a3 0) in
  let u2:=(Cardan_Tartaglia_formula a1 a2 a3 1) in
  let u3:=(Cardan_Tartaglia_formula a1 a2 a3 2) in
  forall u:C, (u-u1)*(u-u2)*(u-u3)=Cpow u 3+a1*Cpow u 2+a2*u+a3.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

38. Arithmetic Mean/Geometric Mean

Jean-Marie Madiot (in coq-community/coq-100-theorems):

using forward-backward induction

Theorem geometric_arithmetic_mean (a : nat -> R) (n : nat) :
  n <> O ->
  (forall i, (i < n)%nat -> 0 <= a i) ->
  prod n a <= (sum n a / INR n) ^ n
  /\
  (prod n a = (sum n a / INR n) ^ n -> forall i, (i < n)%nat -> a i = a O).

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: ACL2, Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

39. Solutions to Pell’s Equation

Formalized in: HOL Light, Isabelle, Lean, Metamath, Mizar

40. Minkowski’s Fundamental Theorem

Formalized in: HOL Light, Isabelle, ProofPower

41. Puiseux’s Theorem

Daniel de Rauglaudre (in https://github.com/roglo/puiseuxth/blob/master/coq/Puiseux.v):

Theorem puiseux_series_algeb_closed : ∀ (α : Type) (R : ring α) (K : field R),
  algeb_closed_field K
  → ∀ pol : polynomial (puiseux_series α),
    degree (ps_zerop K) pol ≥ 1
    → ∃ s : puiseux_series α, (ps_pol_apply pol s = 0)%ps.

Reproducibility: as of December 2022, build success with Coq 8.16

Constructive: no

Axioms used:

Formalized in: Coq, Isabelle

42. Sum of the Reciprocals of the Triangular Numbers

Coqtail (in coq-community/coqtail-math):

Lemma sum_reciprocal_triangular : Rser_cv (fun n => / triangle (S n)) 2.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

43. The Isoperimetric Theorem

Formalized in: (none)

44. The Binomial Theorem

The Coq development team (in coq's standard library):

For the non-constructive type R

Lemma binomial :
  forall (x y:R) (n:nat),
    (x + y) ^ n = sum_f_R0 (fun i:nat => C n i * x ^ i * y ^ (n - i)) n.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Laurent Thery & Jose C. Almeida (in coq-contribs/rsa):

For the type nat

Theorem exp_Pascal :
  forall a b n : nat,
  power (a + b) n =
  sum_nm n 0 (fun k : nat => binomial n k * (power a (n - k) * power b k)).

Reproducibility: last checked December 2022 with Coq 8.16

Constructive: yes

Axioms used: (none)

Jean-Marie Madiot (in coq-community/coqtail-math):

For any commutative ring X.

Definition newton_sum n a b : X :=
  CRsum (fun k => (Nbinomial n k) ** (a ^ k) * (b ^ (n - k))) n.

Theorem Newton : forall n a b, (a + b) ^ n == newton_sum n a b.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), ProofPower

45. The Partition Theorem

Formalized in: HOL Light, Isabelle, Lean, Metamath, Mizar

46. The Solution of the General Quartic Equation

Frédéric Chardard (in coq-community/coq-100-theorems):

For the non-constructive type R

Theorem Ferrari_formula: forall (a:C) (b:C) (c:C) (d:C),
  let s:=-a/4 in
  let p:= b+3*s*a+6*Cpow s 2 in
  let q:= c+2*b*s+3*a*Cpow s 2+4*Cpow s 3 in
  let r:= d+c*s+b*Cpow s 2+a*Cpow s 3+Cpow s 4 in
  let lambda:=Cardan_Tartaglia_formula (-p/2) (-r) (r*p/2-/8*Cpow q 2) 0 in
  let A:=Csqrt(2*lambda-p) in
  let cond:=(Ceq_dec (2*lambda) p) in
  let B:=if cond then (RtoC 0) else (-q/(2*A)) in
  let z1:=if cond then Csqrt (binom_solution p r 0)
                  else binom_solution A (B+lambda) 0 in
  let z2:=if cond then -Csqrt (binom_solution p r 0)
                  else binom_solution A (B+lambda) 1 in
  let z3:=if cond then Csqrt (binom_solution p r 1)
                  else binom_solution (-A) (-B+lambda) 0 in
  let z4:=if cond then -Csqrt (binom_solution p r 1)
                  else binom_solution (-A) (-B+lambda) 1 in
  let u1:=z1+s in
  let u2:=z2+s in
  let u3:=z3+s in
  let u4:=z4+s in
  forall u:C, (u-u1)*(u-u2)*(u-u3)*(u-u4)=Cpow u 4+a*Cpow u 3+b*Cpow u 2+c*u+d.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Metamath, Mizar

47. The Central Limit Theorem

Formalized in: Isabelle

48. Dirichlet’s Theorem

Formalized in: HOL Light, Isabelle, Metamath

49. The Cayley-Hamilton Theorem

Sidi Ould Biha (in mathcomp):

Theorem Cayley_Hamilton (R : comRingType) n' (A : 'M[R]_n'.+1) :
  horner_mx A (char_poly A) = 0.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath

50. The Number of Platonic Solids

Formalized in: HOL Light

51. Wilson’s Theorem

unknown (Inria, Microsoft) (in mathcomp):

(c) Copyright 2006-2016 Microsoft Corporation and Inria. Distributed under the terms of CeCILL-B.

Theorem Wilson : forall p, p > 1 -> prime p = (p %| ((p.-1)`!).+1).

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Laurent Théry (in coq-contribs/sum-of-two-square):

LGPL licence

Theorem wilson: forall p, prime p ->  Zis_mod (Zfact (p - 1)) (- 1) p.

Reproducibility: see #20

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, nqthm

52. The Number of Subsets of a Set

unknown (Inria, Microsoft) (in mathcomp):

Lemma card_powerset (T : finType) (A : {set T}) : #|powerset A| = 2 ^ #|A|.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Pierre Letouzey (in coq-contribs/fsets):

Lemma powerset_cardinal:
  forall s, MM.cardinal (powerset s) = two_power (M.cardinal s).

Reproducibility: as of December 2022, build success with Coq 8.10.2, failure with 8.11.2 (using git tag v8.10.0)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

53. Pi is Trancendental

Sophie Bernard and Laurence Rideau (in https://github.com/Sobernard/Lindemann/blob/master/LindemannTheorem.v):

The concept algebraicOver is from the Mathematical Components library, and the definition of PI is from the Coq standard library.

Notation "x 'is_algebraic'" := (algebraicOver QtoC x) (at level 55).
Theorem Pi_trans_by_LB : ~ (RtoC Rtrigo1.PI is_algebraic).

Formalized in: Coq, Isabelle

54. Konigsberg Bridges Problem

Jean-Marie Madiot (in coq-community/coq-100-theorems):

Theorem konigsberg_bridges :
  let E := [(0, 1); (0, 2); (0, 3); (1, 2); (1, 2); (2, 3); (2, 3)] in
  forall p, path p -> eulerian E p -> False.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

55. Product of Segments of Chords

Benjamin Grégoire, Loïc Pottier, and Laurent Théry (in Coq's test suite):

Lemma chords: forall O A B C D M:point,
  equaldistance O A O B ->
  equaldistance O A O C ->
  equaldistance O A O D ->
  collinear A B M -> collinear C D M ->
  scalarproduct A M B = scalarproduct C M D
  \/ parallel A B C D.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

56. The Hermite-Lindemann Transcendence Theorem

Sophie Bernard (in https://github.com/Sobernard/Lindemann/blob/master/LindemannTheorem.v):

The concept algebraicOver is from the Mathematical Components library.

Notation "x 'is_algebraic'" := (algebraicOver QtoC x) (at level 55).

Theorem HermiteLindemann (x : complexR) :
  x != 0 -> x is_algebraic -> ~ ((Cexp x) is_algebraic).

Formalized in: Coq, Isabelle

57. Heron’s Formula

Julien Narboux (in coq-contribs/area-method):

Definition Py A B C := A**B * A**B + B**C * B**C - A**C * A**C.

Lemma herron_qin : forall A B C,
  S A B C * S A B C = 1 / (2*2*2*2) * (Py A B A * Py A C A - Py B A C * Py B A C).

Reproducibility: as of December 2022, build success with Coq 8.13.2 and 8.14.1, failure with 8.15.2 and 8.16.0 (using git tag v8.10.0)

Constructive: no

Axioms used:

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar

58. Formula for the Number of Combinations

Pierre Letouzey (in coq-contribs/fsets):

Lemma powerset_k_cardinal : forall s k,
  MM.cardinal (powerset_k s k) = binomial (M.cardinal s) k.

Reproducibility: see #52

Constructive: yes

Axioms used: (none)

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

59. The Laws of Large Numbers

Avraham Shinnar, Barry Trager (in https://github.com/IBM/FormalML/blob/b9a36a612c01d6f7e05ae7f68a057d3a4728761d/coq/QLearn/slln.v#L7287):

Lemma Ash_6_2_5
  {Ts:Type} {dom: SigmaAlgebra Ts} {Prts: ProbSpace dom}.
  (X : nat -> Ts -> R) (mu : R)
  {rv : forall n, RandomVariable dom borel_sa (X n)}
  {isfe : forall n, IsFiniteExpectation Prts (X n)} :
  (forall n, FiniteExpectation Prts (X n) = mu) ->
  iid_rv_collection Prts borel_sa X ->
  almost Prts (fun omega => is_lim_seq (fun n => ((rvsum X n) omega)/(INR (S n))) mu).

Reproducibility: as of December 2022, build success with Coq 8.12 (use the provided .opam file with an additional coq <= 8.12.1 constraint)

Constructive: no

Axioms used:

Formalized in: Coq, Isabelle, Lean

60. Bezout’s Theorem

The Coq development team (in coq's standard library):

Inductive Zdivide (a b:Z) : Prop :=
  Zdivide_intro : forall q:Z, b = q * a -> Zdivide a b.

Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.

Inductive Zis_gcd (a b d:Z) : Prop :=
  Zis_gcd_intro :
  (d | a) ->
  (d | b) ->
  (forall x:Z, (x | a) -> (x | b) -> (x | d)) ->
    Zis_gcd a b d.

Inductive Bezout (a b d:Z) : Prop :=
  Bezout_intro : forall u v:Z, u * a + v * b = d -> Bezout a b d.

Lemma Zis_gcd_bezout : forall a b d:Z, Zis_gcd a b d -> Bezout a b d.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), ProofPower

61. Theorem of Ceva

Julien Narboux (in coq-contribs/area-method):

Theorem Ceva :
  forall A B C D E F G P : Point,
  inter_ll D B C A P ->
  inter_ll E A C B P ->
  inter_ll F A B C P ->
  F <> B ->
  D <> C ->
  E <> A ->
  parallel A F F B ->
  parallel B D D C ->
  parallel C E E A ->
  (A ** F / F ** B) * (B ** D / D ** C) * (C ** E / E ** A) = 1.

Reproducibility: see #57

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Metamath, Mizar

62. Fair Games Theorem

Avraham Shinnar, Barry Trager (in https://github.com/IBM/FormalML/blob/b9a36a612c01d6f7e05ae7f68a057d3a4728761d/coq/ProbTheory/MartingaleStopped.v#L1404-L1504):

Documentation with comments

Context
  {Ts:Type}
  {σ: SigmaAlgebra Ts}
  (prts: ProbSpace σ)
  
  (F : nat -> SigmaAlgebra Ts)
  {filt:IsFiltration F}
  {sub:IsSubAlgebras σ F}
      
  (τ:Ts -> option nat)
  {is_stop:IsStoppingTime τ F}
  
  (Y : nat -> Ts -> R)
  {rv:forall n, RandomVariable σ borel_sa (Y n)}
  {isfe:forall n, IsFiniteExpectation prts (Y n)}
  {adapt:IsAdapted borel_sa Y F}
  
  (conditions:
    (exists (N:nat),
        almost prts (fun ω => match τ ω with
                           | Some k => (k <= N)%nat
                           | None => False
                           end))
            
    \/
      (almost prts (fun ω => τ ω <> None)
       /\ exists (K:R),
          (forall n, almost prts (fun ω => Rabs (Y n ω) < K)))
    \/
      (Rbar_IsFiniteExpectation
         prts
         (fun ω => match τ ω with
                | Some n => INR n
                | None => p_infty
                end)
       /\ exists (K:R),
        forall n, almost prts (fun ω => Rabs (Y (S n) ω - Y n ω) <= K))
  ).
    
Theorem optional_stopping_time
        {mart:IsMartingale prts eq Y F} :
  FiniteExpectation prts (process_under Y τ) = FiniteExpectation prts (Y 0%nat).

Theorem optional_stopping_time_sub
        {mart:IsMartingale prts Rle Y F} :
  FiniteExpectation prts (process_under Y τ) >= FiniteExpectation prts (Y 0%nat).

Theorem optional_stopping_time_super
        {mart:IsMartingale prts Rge Y F} :
  FiniteExpectation prts (process_under Y τ) <= FiniteExpectation prts (Y 0%nat).

Reproducibility: see #59

Constructive: no

Axioms used:

Formalized in: Coq, Lean

63. Cantor’s Theorem

Gilles Kahn, Gerard Huet (in coq's standard library):

Naive Set Theory in Coq

Theorem Strict_Rel_is_Strict_Included :
  same_relation (Ensemble U) (Strict_Included U)
    (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))).

Reproducibility: Good (CI)

Constructive: no (extensionality)

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), ProofPower

64. L’Hopital’s Rule

Sylvain Dailler (in coq-community/coqtail-math):

Many other versions in the file, for example depending on whether the limits are finite or not.

Variables f g : R → R.
Variables a b L : R.
Hypothesis Hab : a < b.
Hypotheses (Df : ∀ x, open_interval a b x → derivable_pt f x)
           (Dg : ∀ x, open_interval a b x → derivable_pt g x).
Hypotheses (Cf : ∀ x, a ≤ x ≤ b → continuity_pt f x)
           (Cg : ∀ x, a ≤ x ≤ b → continuity_pt g x).
Hypothesis (Zf : limit1_in f (open_interval a b) 0 a).
Hypothesis (Zg : limit1_in g (open_interval a b) 0 a).

Hypothesis (g_not_0 : ∀ x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) ≠ 0 ∧ g x ≠ 0)
Hypothesis (Hlimder : ∀ eps, eps > 0 →
  ∃ alp,
    alp > 0 ∧
    (∀ x (Hopen : open_interval a b x), R_dist x a < alp →
      R_dist (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)) L < eps)).

Theorem Hopital_g0_Lfin_right : limit1_in (fun x ⇒ f x / g x) (open_interval a b) L a.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

65. Isosceles Triangle Theorem

Frédérique Guilhot (in coq-community/HighSchoolGeometry):

Lemma isocele_angles_base :
  isocele A B C -> cons_AV (vec B C) (vec B A) = cons_AV (vec C A) (vec C B).

Reproducibility: Good (CI)

Constructive: no

Axioms used:

GeoCoq team (in https://github.com/GeoCoq/GeoCoq/blob/master/Highschool/triangles.v):

Lemma isosceles_conga :
  forall Tn : Tarski_neutral_dimensionless,
  Tarski_neutral_dimensionless_with_decidable_point_equality Tn ->
  forall A B C : Tpoint,
  A <> C ->
  A <> B ->
  isosceles A B C -> CongA C A B A C B.

Reproducibility: last checked December 2022 with Coq 8.16

Constructive: hypotheses partially classical

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

66. Sum of a Geometric Series

Luís Cruz-Filipe (in coq-community/corn):

Lemma fun_power_series_conv_IR :
  fun_series_convergent_IR
  (olor ([--][1]) [1])
  (fun (i:nat) => Fid IR{^}i).

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

67. e is Transcendental

Sophie Bernard and Laurence Rideau (in https://github.com/Sobernard/Lindemann/blob/master/LindemannTheorem.v):

The concept algebraicOver is from the Mathematical Components library, and the definition of exp is from the Coq standard library.

Notation "x 'is_algebraic'" := (algebraicOver QtoC x) (at level 55).

Theorem e_trans_by_LB : ~ (RtoC (Rtrigo_def.exp 1) is_algebraic).

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath

68. Sum of an arithmetic series

many versions (in coq-community/coq-100-theorems):

Theorem arith_sum a b n : 2 * sum (fun i => a + i * b) n = S n * (2 * a + n * b).

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

69. Greatest Common Divisor Algorithm

The Coq development team (in coq's standard library):

The following statement handle binary integers; other types are handled in the same file.

Fixpoint Pgcdn (n: nat) (a b : positive) : positive :=
  match n with
  | O => 1
  | S n =>
    match a,b with
    | xH, _ => 1
    | _, xH => 1
    | xO a, xO b => xO (Pgcdn n a b)
    | a, xO b => Pgcdn n a b
    | xO a, b => Pgcdn n a b
    | xI a', xI b' =>
      match Pcompare a' b' Eq with
      | Eq => a
      | Lt => Pgcdn  n (b'-a') a
      | Gt => Pgcdn n (a'-b') b
      end
    end
  end.

Definition Zgcd (a b : Z) : Z :=
  match a,b with
  | Z0, _ => Zabs b
  | _, Z0 => Zabs a
  | Zpos a, Zpos b => Zpos (Pgcd a b)
  | Zpos a, Zneg b => Zpos (Pgcd a b)
  | Zneg a, Zpos b => Zpos (Pgcd a b)
  | Zneg a, Zneg b => Zpos (Pgcd a b)
  end.

Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Zgcd a b).

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), ProofPower

70. The Perfect Number Theorem

Raül Espejo Boix (in https://github.com/The-busy-man/Perfect-Number-s-Theorem/blob/main/perf_numT.v):

uses mathcomp

Theorem EulerT p: perfect p -> 2%|p -> p > 0 ->
  exists n, (p = (2^n-1)*2^n.-1)/\(prime (2^n - 1)).

Reproducibility: as of December 2022, build success with Coq 8.16

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar

71. Order of a Subgroup

unknown (Laurent Théry?) (in mathcomp):

Theorem Lagrange (gT : finGroupType) (G H : {group gT}) :
  H \subset G -> (#|H| * #|G : H|)%N = #|G|

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

72. Sylow’s Theorem

Laurent Théry (in mathcomp):

Theorem Sylow's_theorem (p : nat) (gT : finGroupType) (G : {group gT}) :
  [/\ forall P, [max P | p.-subgroup(G) P] = p.-Sylow(G) P,
      [transitive G, on 'Syl_p(G) | 'JG],
      forall P, p.-Sylow(G) P -> #|'Syl_p(G)| = #|G : 'N_G(P)|
   &  prime p -> #|'Syl_p(G)| %% p = 1%N].

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS

73. Ascending or Descending Sequences

Florent Hivert (in https://github.com/hivert/Coq-Combi/blob/master/theories/Erdos_Szekeres/Erdos_Szekeres.v):

Variable T : ordType. (* a totally ordered type *)
  (* <= is denoted (leqX T) *)
  (* >  is denoted (gtnX T) *)

Theorem Erdos_Szekeres (m n : nat) (s : seq T) :
  (size s) > (m * n) ->
  (exists t, subseq t s /\ sorted (leqX T) t /\ size t > m) \/
  (exists t, subseq t s /\ sorted (gtnX T) t /\ size t > n).

Reproducibility: CI for Coq 8.15, build success with Coq 8.16 after minor adaptations

Constructive: yes

Axioms used: (none)

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

74. The Principle of Mathematical Induction

Coq's type theory (in coq's standard library):

The induction priciple is automatically provided by Coq when defining unary natural numbers.

Inductive nat : Set :=  O : nat | S : nat -> nat.

nat_ind :
  forall P : nat -> Prop,
  P 0 ->
  (forall n : nat, P n -> P (S n)) ->
  forall n : nat, P n

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

The Coq development team (in coq's standard library):

Peano's induction principle is manually proved for binary natural integers.

peano_rect : forall (P : N -> Type),
  P 0 ->
  (forall n : N, P n -> P (succ n)) ->
  forall (n : N), P n

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

75. The Mean Value Theorem

Luís Cruz-Filipe (in coq-community/corn):

Theorem Law_of_the_Mean : forall a b, I a -> I b -> forall e, Zero [<] e ->
  {x : IR | Compact (Min_leEq_Max a b) x | forall Ha Hb Hx,
   AbsIR (F b Hb[-]F a Ha[-]F' x Hx[*] (b[-]a)) [<=] e}.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

76. Fourier Series

Formalized in: HOL Light, Isabelle, Lean, Metamath

77. Sum of kth powers

Frédéric Chardard (in coq-community/coq-100-theorems):

Lemma sum_kthpowers : forall r:nat, forall n:nat,
  (0<r)%nat->
  sum_f_R0 (fun k => ((INR k)^r)%R) n
  =((bernoulli_polynomial (S r) (INR n+1))-(bernoulli_polynomial (S r) 0))/(INR r+1).

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath

78. The Cauchy-Schwarz Inequality

Daniel de Rauglaudre (in https://github.com/roglo/cauchy_schwarz/blob/master/Cauchy_Schwarz.v):

Notation "'Σ' ( i = b , e ) , g" := (summation b e (λ i, (g)%R)).
Notation "u .[ i ]" := (List.nth (pred i) u 0%R).

Theorem Cauchy_Schwarz_inequality : ∀ (u v : list R) n,
  ((Σ (k = 1, n), (u.[k] * v.[k]))² ≤
   Σ (k = 1, n), (u.[k]²) * Σ (k = 1, n), (v.[k]²))%R.

Reproducibility: as of December 2022, build success with Coq 8.16

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

79. The Intermediate Value Theorem

The Coq development team (in coq's standard library):

non constructive version in Coq's standard library

Lemma IVT_cor :
  forall (f:R -> R) (x y:R),
    continuity f ->
    x <= y -> f x * f y <= 0 ->
    { z:R | x <= z <= y /\ f z = 0 }.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

80. The Fundamental Theorem of Arithmetic

unknown (Inria, Microsoft) (in mathcomp):

Lemma divisors_correct : forall n, n > 0 ->
  [/\ uniq (divisors n), sorted leq (divisors n)
    & forall d, (d \in divisors n) = (d %| n)].

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower

81. Divergence of the Prime Reciprocal Series

Formalized in: HOL Light, Isabelle, Lean, Metamath, ProofPower

82. Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof)

Formalized in: Lean

83. The Friendship Theorem

Alex Loiko (in https://github.com/aleloi/coq-friendship-theorem):

Theorem Friendship
  (T: finType) (T_nonempty: [set: T] != set0)
  (F : rel T) (Fsym: symmetric F) (Firr: irreflexive F) :
  (forall (u v: T), u != v -> #|[set w | F u w & F v w]| == 1) ->
  {u : T | forall v : T, u != v -> F u v}.

Reproducibility: as of December 2022, build success with Coq 8.16

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar

84. Morley’s Theorem

Frédérique Guilhot (in coq-community/HighSchoolGeometry):

Theorem Morley:
  forall (a b c : R) (A B C P Q T : PO),
  0 < a ->
  0 < b ->
  0 < c ->
  (a + b) + c = pisurtrois ->
  A <> B ->
  A <> C ->
  B <> C ->
  B <> P ->
  B <> Q ->
  A <> T ->
  C <> T ->
  image_angle b = cons_AV (vec B C) (vec B P) ->
  image_angle b = cons_AV (vec B P) (vec B Q) ->
  image_angle b = cons_AV (vec B Q) (vec B A) ->
  image_angle c = cons_AV (vec C P) (vec C B) ->
  image_angle c = cons_AV (vec C T) (vec C P) ->
  image_angle a = cons_AV (vec A B) (vec A Q) ->
  image_angle a = cons_AV (vec A Q) (vec A T) ->
  image_angle a = cons_AV (vec A T) (vec A C) -> equilateral P Q T.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Mizar

85. Divisibility by 3 Rule

many versions (in coq-community/coq-100-theorems):

Theorem div3 : forall n d,
  (number n d) mod 3 = (sumdigits n d) mod 3.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

86. Lebesgue Measure and Integration

Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero, Houda Mouhcine (in https://lipn.univ-paris13.fr/coq-num-analysis/tree/Tonelli.1.0/Lebesgue/):

This formalization covers the integration of nonnegative measurable functions (including the Beppo Levi theorem, Fatou's Lemma and the Tonelli theorem), the Bochner integral for functions taking their values in a Banach space (including the dominated convergence theorem), and the Lebesgue measure on the real numbers.

In the snippets below, _p stands for nonnegative and SF/sf for simple function.

Articles: on LInt_p, on Bochner integral.

(* From LInt_p.v *)
Definition LInt_p : (E -> Rbar) -> Rbar :=
  fun f => Rbar_lub (fun z : Rbar =>
    exists (g : E -> R), exists (Hg : SF gen g),
      non_neg g /\ (forall x, Rbar_le (g x) (f x)) /\
      LInt_SFp mu g Hg = z).

(* From BInt_Bif.v *)
Definition BInt {f : X -> E} (bf : Bif μ f) :=
  lim_seq (fun n => BInt_sf μ (seq bf n)).

(* From measure_R.v *)
Definition Lebesgue_measure : measure cal_L :=
  mk_measure cal_L lambda_star
    lambda_star_False lambda_star_ge_0 Lebesgue_sigma_additivity.

Reproducibility: as of December 2022, build success with Coq 8.16

Constructive: no

Axioms used:

Reynald Affeldt and Cyril Cohen (in mathcomp):

Mathcomp analysis has a formalization of Lebesgue measure and Lebesgue integration. Some definitions below.

(* in lebesgue_measure.v *)
Definition lebesgue_measure : {measure set gssets -> \bar R} :=
  Hahn_ext (@slength_measure R).

(* in lebesgue_integral.v *)
Definition nnintegral D (f : T -> \bar R) :=
  ereal_sup [set sintegral mu D g | g in
    [set g : nnsfun T R | forall x, D x -> (g x)%:E <= f x]].

Definition integral D (f : T -> \bar R) :=
  nnintegral D (f ^\+) - nnintegral D (f ^\-).

Reproducibility: Good (CI)

Constructive: yes

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

87. Desargues’s Theorem

Frédérique Guilhot (in coq-community/HighSchoolGeometry):

Theorem Desargues :
  forall A B C A1 B1 C1 S : PO,
  C <> C1 -> B <> B1 -> C <> S -> B <> S -> C1 <> S ->
  B1 <> S -> A1 <> B1 -> A1 <> C1 -> B <> C -> B1 <> C1 ->
  triangle A A1 B ->
  triangle A A1 C ->
  alignes A A1 S ->
  alignes B B1 S ->
  alignes C C1 S ->
  paralleles (droite A B) (droite A1 B1) ->
  paralleles (droite A C) (droite A1 C1) ->
  paralleles (droite B C) (droite B1 C1).

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Julien Narboux (in coq-contribs/area-method):

Proved with the area_method tactic.

Theorem Desargues :
  forall A B C X A' B' C' : Point, A' <>C' -> A' <> B' ->
  on_line A' X A ->
  on_inter_line_parallel B' A' X B A B ->
  on_inter_line_parallel C' A' X C A C ->
  parallel B C B' C'.

Reproducibility: see #57

Constructive: no

Axioms used:

Gabriel Braun (in https://geocoq.github.io/GeoCoq/html/GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg.html):

Hessenberg's proof following the book of Tarski.

Lemma l13_15 : forall A B C A' B' C' O ,
  ~Col A B C ->
  Par_strict A B A' B' ->
  Par_strict A C A' C' ->
  Col O A A' ->
  Col O B B' ->
  Col O C C' ->
  Par B C B' C'.

Lemma l13_18 : forall A B C A' B' C' O,
  ~Col A B C /\ Par_strict A B A' B' /\  Par_strict A C A' C' ->
  (Par_strict B C B' C' /\ Col O A A' /\ Col O B B' -> Col O C C') /\
  ((Par_strict B C B' C' /\ Par A A' B B') ->
  (Par C C' A A' /\ Par C C' B B'))  /\
  (Par A A' B B' /\ Par A A' C C' -> Par B C B' C').

(* Common Section hypotheses:
  (Tn : Tarski_neutral_dimensionless)
  (TnEQD : Tarski_neutral_dimensionless_with_decidable_point_equality Tn)
  Tarski_euclidean TnEQD *)

Reproducibility: last checked December 2022 with Coq 8.16

Constructive: hypotheses partially classical

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Metamath, Mizar

88. Derangements Formula

Fabian Wolff (in https://github.com/FabianWolff/coq-derangements-formula):

Theorem drm_formula: forall n, n > 0 ->
  round ((INR (fact n)) * (exp (-1))) = Some (Z.of_nat (length (drm_construct n))).

Reproducibility: as of December 2022, build success with Coq 8.16

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

89. The Factor and Remainder Theorems

unknown ((c) Microsoft Corporation and Inria) (in mathcomp):

CoInductive edivp_spec m d : nat * {poly F} * {poly F} -> Type :=
  EdivpSpec n q r of
  m = q * d + r & (d != 0) ==> (size r < size d) : edivp_spec m d (n, q, r).

Lemma edivpP m d : edivp_spec m d (edivp m d).

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

90. Stirling’s Formula

Coqtail team (in coq-community/coqtail-math):

Lemma Stirling_equiv :
  Rseq_fact ~ (fun n => sqrt (2 × PI) × (INR n) ^ n × exp (- (INR n)) × sqrt (INR n)).

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath

91. The Triangle Inequality

The Coq Development Team (in https://github.com/coq/coq/blob/trunk/theories/Reals/Rgeom.v):

Lemma triangle :
  forall x0 y0 x1 y1 x2 y2:R,
    dist_euc x0 y0 x1 y1 <= dist_euc x0 y0 x2 y2 + dist_euc x2 y2 x1 y1.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: ACL2, Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower

92. Pick’s Theorem

Formalized in: HOL Light

93. The Birthday Problem

Jean-Marie Madiot (in coq-community/coq-100-theorems):

This formalization uses lists of natural numbers to model sets

Theorem birthday_paradox :
  let l := picks 23 (enumerate 365) in
  2 * length (filter collision l) > length l.

Theorem birthday_paradox_min :
  let l := picks 22 (enumerate 365) in
  2 * length (filter collision l) < length l.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

94. The Law of Cosines

Frédérique Guilhot (in coq-community/HighSchoolGeometry):

Theorem Al_Kashi :
  forall (A B C : PO) (a : R),
  A <> B ->
  A <> C ->
  image_angle a = cons_AV (vec A B) (vec A C) ->
  Rsqr (distance B C) =
  Rsqr (distance A B) + Rsqr (distance A C) -
  2 * distance A B * distance A C * cos a.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS

95. Ptolemy’s Theorem

Tuan-Minh Pham (in coq-community/HighSchoolGeometry):

Theorem Ptolemee:
  forall (A B C D : PO),
  orient A B C -> orient A B D ->
  orient C D A -> orient C D B ->
  sont_cocycliques A B C D ->
  (distance A B  * distance C D) + (distance B C * distance D A) =
  distance A C  * distance B D.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

96. Principle of Inclusion/Exclusion

Jean-Marie Madiot (in coq-community/coq-100-theorems):

Theorem inclusion_exclusion (X : Set) (enum_X : list X) (l : list (set X)) :
  cardinal (list_union l) =
  sum
    (map (fun l' => cardinal (list_intersection l') *
                 alternating_sign (1 + length l'))
         (filter nonempty (sublists l))).

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower

97. Cramer’s Rule

Georges Gonthier et al. (in mathcomp):

Lemma mul_mx_adj : forall n (A : 'M[R]_n), A *m \adj A = (\det A)%:M.

Lemma trmx_adj : forall n (A : 'M[R]_n), (\adj A)^T = \adj A^T.

Lemma mul_adj_mx : forall n (A : 'M[R]_n), \adj A *m A = (\det A)%:M.

Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

98. Bertrand’s Postulate

Laurent Théry (in coq-community/bertrand):

Theorem Bertrand : forall n : nat, 2 <= n -> exists p : nat, prime p /\ n < p /\ p < 2 * n.

Reproducibility: Good (CI)

Constructive: no

Axioms used:

Formalized in: Coq, HOL Light, Isabelle, Lean, Metamath, Mizar

99. Buffon Needle Problem

Formalized in: Isabelle, ProofPower

100. Descartes Rule of Signs

Formalized in: HOL Light, Isabelle, ProofPower