Formalizing 100 theorems in Coq

This is an appendix to Freek Wiedijk's webpage on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq. Drop me or Freek an email or make a pull request if you have updates.

1. The Irrationality of the Square Root of 2

many versions (e.g. one in contribs/QArithSternBrocot/sqrt2):


Theorem sqrt2_not_rational : forall p q, q <> 0 -> p * p <> q * q * 2.

2. Fundamental Theorem of Algebra

Herman Geuvers et al. (in C-CoRN/fta/FTA):


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

3. The Denumerability of the Rational Numbers

Milad Niqui (in contribs/QArithSternBrocot/Q_denumerable):


Theorem Q_is_denumerable: same_cardinality Q nat.

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

Daniel Schepler (in contribs/ZornsLemma/CountableTypes):

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

Lemma Q_countable: CountableT Q.

4. Pythagorean Theorem

Frédérique Guilhot (contribs/HighSchoolGeometry/euclidien_classiques):


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.

Gabriel Braun (GeoCoq in Chapter 15):

A synthetic proof in the context of Tarski's axioms.
Lemma pythagoras :
 forall O E E' A B C AC BC AB AC2 BC2 AB2,
  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.

5. Prime Number Theorem

No known statement.

6. Godel’s Incompleteness Theorem

Russell O'Connor (in contribs/Goedel/goedel1, see description on r6.ca and proof archive: Goedel20050512.tar.gz):


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

Russell O'Connor (in contribs/Goedel/goedel2):
Russell O'Connor proved the theorem under the assumption of the last two Hilbert-Bernays-Loeb derivability conditions.
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.

7. Law of Quadratic Reciprocity

Nathanaël Courant (proof on github):


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

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

No known statement.

9. The Area of a Circle

No known statement.

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

Laurent Théry (in mathcomp/solvable/cyclic.v):


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

11. The Infinitude of Primes

Russell O'Connor (in cocorico, compatible with coq 7.3):

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

12. The Independence of the Parallel Postulate

No known statement.

13. Polyhedron Formula

Jean-François Dufourd (in contribs/EulerFormula/Euler3):

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

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

Jean-Marie Madiot (in Coqtail/Reals/Rzeta2):


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

15. Fundamental Theorem of Integral Calculus

Luís Cruz-Filipe (in C-CoRN/ftc/FTC):


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

The Coq development team (in standard library, Reals/RiemannInt):

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.

16. Insolvability of General Higher Degree Equations

No known statement.

17. DeMoivre’s Theorem

Coqtail team (in Coqtail/Complex/Cexp):

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.

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

Valentin Blot (see Valentin's website or directly the .tar.gz of the proof):


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)}}.

19. Four Squares Theorem

Guillaume Allais, Jean-Marie Madiot (in Coqtail/Arith/Lagrange_four_square):

"{a | P}" means "there exists a such that P" but in a constructive setting. Indeed, from the proof, we can extract a program computing a, b, c, d from n.
Theorem lagrange_4_square_theorem : forall n, 0 <= n ->
  { a : _ & { b: _ & { c : _ & { d |
    n = a * a + b * b + c * c + d * d } } } }.

20. All Primes Equal the Sum of Two Squares

Laurent Théry (in contribs/SumOfTwoSquare/TwoSquares):


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

Theorem two_squares_sum:
 forall n,
 0 <= n ->
 (forall p, prime p -> Zis_mod p 3 4 ->  Zeven (Zdiv_exp p n)) ->
  sum_of_two_squares n.

21. Green’s Theorem

No known statement.

22. The Non-Denumerability of the Continuum

Pierre-Marie Pédrot (in Coqtail/Reals/Logic/Runcountable):


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}.

C-CoRN team (in C-CoRN/reals/RealCount):

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

23. Formula for Pythagorean Triples

David Delahaye (in contribs/Fermat4/Pythagorean):


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

24. The Undecidability of the Continuum Hypothesis

No known statement.

25. Schroeder-Bernstein Theorem

Hugo Herbelin (in contribs/Schroeder/Schroeder):


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

Daniel Schepler (in contribs/ZornsLemma/CSB):

Section CSB.
Variable X Y:Type.
Variable f:X->Y.
Variable g:Y->X.
Hypothesis f_inj: injective f.
Hypothesis g_inj: injective g.

Theorem CSB: exists h:X->Y, bijective h.

End CSB.

26. Leibniz’s Series for Pi

Guillaume Allais (in standard library, Reals/Ratan):


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.

Luís Cruz-Filipe (in C-CoRN/transc/MoreArcTan):

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.

27. Sum of the Angles of a Triangle

Frédérique Guilhot (in contribs/HighSchoolGeometry/angles_vecteurs):


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.

Boutry, Gries, Narboux (in GeoCoq/Meta_theory/Parallel_postulates/Euclid):

It is shown that the sum of angles is two rights is equivalent to other versions of the parallel postulate.
Theorem equivalent_parallel_postulates_assuming_greenberg_s_postulate :
  greenberg_s_postulate ->
  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::
     playfair_s_postulate::
     posidonius_postulate::
     posidonius_second_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_2_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).

28. Pascal’s Hexagon Theorem

Magaud and Narboux (in contribs/ProjectiveGeometry/plane/hexamys):


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.

29. Feuerbach’s Theorem

CertiGeo team, marelle project (in CertiGeo/feuerbach):


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 = distance2 O A1 ->
  r2^2 = distance2 O2 A2 ->
  distance2 O O2 = (r + r2)^2
  \/ distance2 O O2 = (r - r2)^2
  \/ collinear A B C.

30. The Ballot Problem

Jean-Marie Madiot (in file ballot.v):


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

31. Ramsey’s Theorem

The Coq development team (in standard library, Sets/Image and Sets/Infinite_sets):


Theorem Pigeonhole :
  forall (A:Ensemble U) (f:U -> V) (n:nat),
    cardinal U A n ->
    forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.

Lemma Pigeonhole_principle :
  forall (A:Ensemble U) (f:U -> V) (n:nat),
    cardinal _ A n ->
    forall n':nat,
      cardinal _ (Im A f) n' ->
      n' < n ->  exists x : _, (exists y : _, f x = f y /\ x <> y).

Theorem Pigeonhole_bis :
  forall (A:Ensemble U) (f:U -> V),
    ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.

Theorem Pigeonhole_ter :
  forall (A:Ensemble U) (f:U -> V) (n:nat),
    injective U V f -> Finite V (Im U V A f) -> Finite U A.

Jean-Marie Madiot (many versions by others) (pigeonhole.v):
constructive version (the proof from the standard library uses excluded middle)
Theorem pigeonhole :
  forall m n, m < n -> forall f, (forall i, f i < m) ->
    { i : nat & { j : nat | i < j < n /\ f i = f j } }.

Frédéric Blanqui (in CoLoR/Util/Set/Ramsey):

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.

32. The Four Color Problem

Georges Gonthier, Benjamin Werner (on github):


Theorem four_color : forall m : map R, simple_map m -> map_colorable 4 m.

33. Fermat’s Last Theorem

No known statement.

34. Divergence of the Harmonic Series

Coqtail (Coqtail/Reals/Rseries/Rseries_RiemannInt):


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

35. Taylor’s Theorem

Luís Cruz-Filipe (in C-CoRN/ftc/Taylor):


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}.

36. Brouwer Fixed Point Theorem

No known statement.

37. The Solution of a Cubic

Frédéric Chardard (in file 37.cardan3.v):


Theorem Cardan_Tartaglia : forall a1 a2 a3 :C,
    let s := -a1 / 3 in
    let p := a2 + 2 * s * a1 + 3 * pow s 2 in
    let q := a3 + a2 * s + a1 * pow s 2 + pow s 3 in
    (p <> 0 ->
     let Delta := pow (q / 2) 2 + pow (p / 3) 3 in
     let alpha := cubicroot (- (q / 2) + nroot 2 Delta) in
     let beta := - (p / 3) / alpha in
     let z1 := alpha + beta in
     let z2 := alpha * CJ + beta * pow CJ 2 in
     let z3 := alpha * pow CJ 2 + beta * CJ in
     forall u : C,
       (u - (s + z1)) * (u - (s + z2)) * (u - (s + z3))
       = pow u 3 + a1 * pow u 2 + a2 * u + a3)
    /\
    (p = 0 ->
     let z1 := - cubicroot q in
     let z2 := z1 * CJ in
     let z3 := z1 * pow CJ 2 in
     forall u : C,
       (u - (s + z1)) * (u - (s + z2)) * (u - (s + z3))
       = pow u 3 + a1 * pow u 2 + a2 * u + a3).

38. Arithmetic Mean/Geometric Mean

Jean-Marie Madiot (in file mean.v, 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).

39. Solutions to Pell’s Equation

No known statement.

40. Minkowski’s Fundamental Theorem

No known statement.

41. Puiseux’s Theorem

Daniel de Rauglaudre (on gforge (use login anonsvn / anonsvn if needed)):


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.

42. Sum of the Reciprocals of the Triangular Numbers

Coqtail (in Coqtail/Reals/Triangular):


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

43. The Isoperimetric Theorem

No known statement.

44. The Binomial Theorem

The Coq development team (in standard library, Reals/Binomial):

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.

Laurent Thery & Jose C. Almeida (in contribs/RSA/Binomials):
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)).

Jean-Marie Madiot (in Coqtail/Hierarchy/Commutative_ring_binomial):
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.

45. The Partition Theorem

No known statement.

46. The Solution of the General Quartic Equation

No known statement.

47. The Central Limit Theorem

No known statement.

48. Dirichlet’s Theorem

No known statement.

49. The Cayley-Hamilton Theorem

Sidi Ould Biha (in mathcomp/algebra/mxpoly):


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

50. The Number of Platonic Solids

No known statement.

51. Wilson’s Theorem

unknown (Inria, Microsoft) (in mathcomp/ssreflect/binomial):

copyrighted:

(c) Copyright Microsoft Corporation and Inria. All rights reserved.
Theorem Wilson : forall p, p > 1 -> prime p = (p %| ((p.-1)`!).+1).

Laurent Théry (in contribs/SumOfTwoSquare/Wilson):
licence: LGPL
Theorem wilson: forall p, prime p ->  Zis_mod (Zfact (p - 1)) (- 1) p.

52. The Number of Subsets of a Set

unknown (Inria, Microsoft) (in mathcomp/ssreflect/finset):


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

Pierre Letouzey (in contribs/FSets/PowerSet):

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

53. Pi is Trancendental

Sophie Bernard and Laurence Rideau ():

The concept algebraicOver is available from the public release ssreflect-1.4, ratr is the type of rational numbers. The definition of PI is from the Coq standard library.
Theorem pi_transcendant : ~ (algebraicOver ratr (PI)%:C).

54. Konigsberg Bridges Problem

Jean-Marie Madiot (in file konigsberg_bridges.v):


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.

55. Product of Segments of Chords

Loïc Pottier, Benjamin Grégoire, Laurent Théry (in CertiGeo/chords):

The proof uses just two tactics. The first one transforms the goal into an algebraic statement and the second one generates and then checks a proof certificate.

More information here: http://hal.inria.fr/inria-00504719_v1/
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.

56. The Hermite-Lindemann Transcendence Theorem

Sophie Bernard (on github. See installation instructions):


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

57. Heron’s Formula

Julien Narboux (in AreaMethod/pythagoras_difference_lemmas):


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

58. Formula for the Number of Combinations

Pierre Letouzey (in contribs/FSets/PowerSet):


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

59. The Laws of Large Numbers

No known statement.

60. Bezout’s Theorem

The Coq development team (in standard library, ZArith/Znumtheory):


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.

61. Theorem of Ceva

Julien Narboux (in contribs/AreaMethod/examples_2):


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.

62. Fair Games Theorem

No known statement.

63. Cantor’s Theorem

Gilles Kahn, Gerard Huet (in standard library, Sets/Powerset.v):

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

64. L’Hopital’s Rule

Sylvain Dailler (Coqtail) (in Coqtail/Reals/Hopital):

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.

65. Isosceles Triangle Theorem

Frédérique Guilhot (in contribs/HighSchoolGeometry/isocele):


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

GeoCoq team (GeoCoq in triangle.v):


Lemma isosceles_conga :
  A<>C -> A <> B ->
  isosceles A B C ->
  Conga C A B A C B.

66. Sum of a Geometric Series

Luís Cruz-Filipe (in C-CoRN/ftc/MoreFunSeries):


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

67. e is Transcendental

Sophie Bernard and Laurence Rideau ():

The concept algebraicOver is available from the public release ssreflect-1.4, ratr is the type of rational numbers. The definition of exp is from the Coq standard library.
Theorem e_transcendant : ~ (algebraicOver ratr (exp 1)%:C).

68. Sum of an arithmetic series

many versions (e.g. file 68.sumarith.v):


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

69. Greatest Common Divisor Algorithm

The Coq development team (in standard library, ZArith/Znumtheory):

This is a binary version, as it is more efficient in coq.

(There are several other versions in this 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).

70. The Perfect Number Theorem

No known statement.

71. Order of a Subgroup

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


Theorem Lagrange G H : H \subset G -> (#|H| * #|G : H|)%N = #|G|.

72. Sylow’s Theorem

Laurent Théry (in mathcomp/solvable/sylow):


Theorem Sylow's_theorem :
  [/\ 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].

73. Ascending or Descending Sequences

Florent Hivert (on Github):


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

74. The Principle of Mathematical Induction

built-in (definition of natural numbers in Coq's standard library: Coq/Init/Datatypes):

This is automatically deduced by coq when defining the set of natural numbers. This lemma is inhabited by the following term:

fun P HO HS => fix f n : P n := match n with O => HO | S p => HS p (f p) end
Inductive nat : Set :=  O : nat | S : nat -> nat.

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

75. The Mean Value Theorem

Luís Cruz-Filipe (in C-CoRN/ftc/Rolle):


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}.

76. Fourier Series

No known statement.

77. Sum of kth powers

No known statement.

78. The Cauchy-Schwarz Inequality

Daniel de Rauglaudre (in roglo/cauchy_schwarz):


Notation "'Σ' ( i = b , e ) , g" := (summation b e (λ i, (g)%R)).
Notation "u .[ i ]" := (List.nth (pred i) u 0%R).
Cauchy_Schwarz_inequality
     : ∀ (u v : list R) (n : nat),
       (Σ (k = 1, n), (u.[k] * v.[k])²
        ≤ Σ (k = 1, n), ((u.[k])²) * Σ (k = 1, n), ((v.[k])²))%R

79. The Intermediate Value Theorem

The Coq development team (in Coq's standard library: Reals/Rsqrt_def):

(non constructive version)
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 }.

80. The Fundamental Theorem of Arithmetic

unknown (Inria, Microsoft) (ssreflect/prime):


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

81. Divergence of the Prime Reciprocal Series

No known statement.

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

No known statement.

83. The Friendship Theorem

No known statement.

84. Morley’s Theorem

Frédérique Guilhot (on Github: HighSchoolGeometry/exercice_morley):

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.

85. Divisibility by 3 Rule

many versions (local):


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

86. Lebesgue Measure and Integration

No known statement.

87. Desargues’s Theorem

Frédérique Guilhot (in contribs/HighSchoolGeometry/affine_classiques):


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

Julien Narboux (in contribs/AreaMethod/examples_2):
Proved with the area_method tactic.
http://dpt-info.u-strasbg.fr/~narboux/area_method.html
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'.

Gabriel Braun (GeoCoq/Ch13_6_Desargues_Hessenberg):

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').

88. Derangements Formula

No known statement.

89. The Factor and Remainder Theorems

unknown ((c) Microsoft Corporation and Inria) (math-comp/algebra/polydiv):


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

90. Stirling’s Formula

Coqtail team (Coqtail/Reals/RStirling):


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

91. The Triangle Inequality

The Coq Development Team (in standard library, Reals/Rgeom):


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.

92. Pick’s Theorem

No known statement.

93. The Birthday Problem

Jean-Marie Madiot (in file birthday.v):

Note: 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.

94. The Law of Cosines

Frédérique Guilhot (in contribs/HighSchoolGeometry/metrique_triangle):


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.

95. Ptolemy’s Theorem

Tuan Minh Pham (link to the publication on HAL):

forall (O A B C D : PO) (r: R),
convexQuad A B C D ? concyclic O r A B C D ?
AD ? BC + AB ? CD = AC ? BD.

96. Principle of Inclusion/Exclusion

Jean-Marie Madiot (in file inclusionexclusion.v):


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

97. Cramer’s Rule

Georges Gonthier et al. (coqfinitgroup/matrix):


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.

98. Bertrand’s Postulate

Laurent Théry (in contribs/Bertrand/Bertrand):


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

99. Buffon Needle Problem

No known statement.

100. Descartes Rule of Signs

No known statement.