Formalizing 100 theorems in Coq

Statistics

• 0 here but not there:
• 8 there but not here: 32 34 42 55 57 60 84 89
• 51 remaining: 5 7 8 9 12 16 19 21 24 28 30 31 33 36 37 38 39 40 41 43 45 46 47 48 50 53 54 56 58 59 62 64 67 70 73 76 77 78 81 82 83 85 86 88 91 92 93 95 96 99 100

1. The Irrationality of the Square Root of 2 (ref hol mizar isabelle proofpower)

• many versions (contribs/Nijmegen/QArithSternBrocot/sqrt2.v):

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

+

2. Fundamental Theorem of Algebra (ref hol mizar isabelle proofpower)

• Herman Geuvers et al. (contribs/Nijmegen/CoRN/fta/FTA.v):

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

+

3. The Denumerability of the Rational Numbers (ref hol mizar isabelle proofpower)

• Milad Niqui (contribs/Nijmegen/QArithSternBrocot/Q_denumerable.v):

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

+

4. Pythagorean Theorem (ref hol mizar isabelle proofpower)

• Frédérique Guilhot (contribs/Sophia-Antipolis/HighSchoolGeometry/euclidien_classiques.v):

  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.

+

5. Prime Number Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

6. Godel’s Incompleteness Theorem (ref hol mizar isabelle proofpower)

• Russell O'Connor (contribs/Berkeley/Goedel/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)).

• Russell O'Connor (contribs/Berkeley/Goedel/goedel2.v):

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

+

7. Law of Quadratic Reciprocity (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

8. The Impossibility of Trisecting the Angle and Doubling the Cube (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

9. The Area of a Circle (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

10. Euler’s Generalization of Fermat’s Little Theorem (ref hol mizar isabelle proofpower)

• Laurent Théry (contribs/Saclay/Ssreflect/theories/cyclic.v):

  Theorem Euler : forall a n, coprime a n -> a ^ phi n  = 1 %[mod n].

+

11. The Infinitude of Primes (ref hol mizar isabelle proofpower)

• Russell O'Connor (http://coq.inria.fr/cocorico/NotFinitePrimes):

  (in coq 7.3)

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

+

12. The Independence of the Parallel Postulate (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

13. Polyhedron Formula (ref hol mizar isabelle proofpower)

• Jean-François Dufourd (contribs/Strasbourg/EulerFormula/Euler3.v):

  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 + …. (ref hol mizar isabelle proofpower)

• Jean-Marie Madiot (http://coqtail.sourceforge.net/main.php?page=3&doc=Reals.Rzeta2):

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

+

15. Fundamental Theorem of Integral Calculus (ref hol mizar isabelle proofpower)

• Luís Cruz-Filipe (contribs/Nijmegen/CoRN/ftc/FTC.v):

  See contribs/Nijmegen/CoRN for definitions

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

• The Coq development team (theories/Reals/RiemannInt.v):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

17. DeMoivre’s Theorem (ref hol mizar isabelle proofpower)

• Coqtail team (http://coqtail.sourceforge.net/main.php?page=3&doc=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 (ref hol mizar isabelle proofpower)

• Valentin Blot (http://perso.ens-lyon.fr/valentin.blot/?download=M1_sources.tar.gz):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

20. All Primes Equal the Sum of Two Squares (ref hol mizar isabelle proofpower)

• Laurent Théry (contribs/Sophia-Antipolis/SumOfTwoSquare/TwoSquares.v):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

22. The Non-Denumerability of the Continuum (ref hol mizar isabelle proofpower)

• Pierre-Marie Pédrot (http://coqtail.sourceforge.net/main.php?page=3&doc=Reals.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 (contribs/Nijmegen/CoRN/reals/RealCount.v):

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

+

23. Formula for Pythagorean Triples (ref hol mizar isabelle proofpower)

• David Delahaye (contribs/CNAM/Fermat4/Pythagorean.v):

  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 Coninuum Hypothesis (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

25. Schroeder-Bernstein Theorem (ref hol mizar isabelle proofpower)

• Hugo Herbelin (contribs/Rocq/Schroeder/Schroeder.v):

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

+

26. Leibnitz’s Series for Pi (ref hol mizar isabelle proofpower)

• The Coq development team (theories/Reals/Rtrigo.v, theories/Reals/AltSeries.v):

  The Leibniz'Series *is* the definition of pi in the standard library.
  
  Here are two statements showing the equivalence with the most common definition of pi being twice the smallest positive x for which cos(x)=0.
  
  However this is relying on the axiom sin(pi/2)=1, which is about to be removed.

  Definition tg_alt (Un:nat -> R) (i:nat) : R := (-1) ^ i * Un i.
  Definition PI_tg (n:nat) := / INR (2 * n + 1).
  Lemma exist_PI : { l:R | Un_cv (fun N:nat => sum_f_R0 (tg_alt PI_tg) N) l }.
  Definition PI : R := 4 * (let (a,_) := exist_PI in a).
  
  Lemma cos_PI2 : cos (PI / 2) = 0.
  Theorem cos_gt_0 : forall x:R, - (PI / 2) < x -> x < PI / 2 -> 0 < cos x.
  
  Axiom sin_PI2 : sin (PI / 2) = 1.

• Russell O'Connor (contribs/Nijmegen/CoRN/transc/MoreArcTan.v):

  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 (ref hol mizar isabelle proofpower)

• Frédérique Guilhot (contribs/Sophia-Antipolis/HighSchoolGeometry/angles_vecteurs.v):

  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.
  

+

28. Pascal’s Hexagon Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

29. Feuerbach’s Theorem (ref hol mizar isabelle proofpower)

• CertiGeo team, marelle project (http://www-sop.inria.fr/marelle/CertiGeo/feuerbach.html):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

31. Ramsey’s Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

32. The Four Color Problem (ref hol mizar isabelle proofpower)

The proof seems to have been proven (Coq, not in contribs, Georges Gonthier, see this page) but the statement is not here yet. Add a statement.

33. Fermat’s Last Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

34. Divergence of the Harmonic Series (ref hol mizar isabelle proofpower)

The proof seems to have been proven (Coq, contrib, Frédérique Guilhot, see this page) but the statement is not here yet. Add a statement.

35. Taylor’s Theorem (ref hol mizar isabelle proofpower)

• Luís Cruz-Filipe (contribs/Nijmegen/CoRN/ftc/Taylor.v):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

37. The Solution of a Cubic (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

38. Arithmetic Mean/Geometric Mean (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

39. Solutions to Pell’s Equation (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

40. Minkowski’s Fundamental Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

41. Puiseux’s Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

42. Sum of the Reciprocals of the Triangular Numbers (ref hol mizar isabelle proofpower)

The proof seems to have been proven (Coq, contrib, Frédérique Guilhot, see this page) but the statement is not here yet. Add a statement.

43. The Isoperimetric Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

44. The Binomial Theorem (ref hol mizar isabelle proofpower)

• The Coq development team (theories/Reals/Binomial.v):

  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 (contribs/Sophia-Antipolis/RSA/Binomials.v):

  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 (Coqtail/Hierarchy/Commutative_ring_binomial.v):

  For any commutative ring X.

  Theorem Nnewton : forall n a b, (a + b) ^ n == newton_sum n a b.
  
  Definition newton_sum n a b : X :=
      CRsum (fun k => (Nbinomial n k) ** (a ^ k) * (b ^ (n - k))) n.

+

45. The Partition Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

46. The Solution of the General Quartic Equation (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

47. The Central Limit Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

48. Dirichlet’s Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

49. The Cayley-Hamilton Thoerem (ref hol mizar isabelle proofpower)

• Sidi Ould Biha (contribs/Saclay/Ssreflect/theories/charpoly.v):

  Theorem Cayley_Hamilton : forall A, (Zpoly (char_poly A)).[A] = 0.

+

50. The Number of Platonic Solids (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

51. Wilson’s Theorem (ref hol mizar isabelle proofpower)

• unknown (Inria, Microsoft) (contribs/Saclay/Ssreflect/theories/binomial.v):

  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 (contribs/Sophia-Antipolis/SumOfTwoSquare/Wilson.v):

  licence: LGPL

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

+

52. The Number of Subsets of a Set (ref hol mizar isabelle proofpower)

• unknown (Inria, Microsoft) (contribs/Saclay/Ssreflect/theories/finfun.v):

  Variable eT : finType.
  Variable A : pred eT.
  Definition powerset := pffun_on false A predT.
  
  Lemma card_powerset : #|powerset| = 2 ^ #|A|.

• Pierre Letouzey, Jean-Christophe Filliâtre (unsure) (contribs/Orsay/FSets/PowerSet.v):

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

+

53. Pi is Trancendental (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

54. Konigsberg Bridges Problem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

55. Product of Segments of Chords (ref hol mizar isabelle proofpower)

The proof seems to have been proven (Coq, not in contribs, Loïc Pottier, see this page) but the statement is not here yet. Add a statement.

56. The Hermite-Lindemann Transcendence Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

57. Heron’s Formula (ref hol mizar isabelle proofpower)

The proof seems to have been proven (Coq, contrib, Frédérique Guilhot, see this page) but the statement is not here yet. Add a statement.

58. Formula for the Number of Combinations (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

59. The Laws of Large Numbers (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

60. Bezout’s Theorem (ref hol mizar isabelle proofpower)

The proof seems to have been proven (Coq, standard library, see this page) but the statement is not here yet. Add a statement.

61. Theorem of Ceva (ref hol mizar isabelle proofpower)

• Julien Narboux (contribs/Rocq/AreaMethod/examples_2.v):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

63. Cantor’s Theorem (ref hol mizar isabelle proofpower)

• Gilles Kahn, Gerard Huet (theories/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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

65. Isosceles Triangle Theorem (ref hol mizar isabelle proofpower)

• Frédérique Guilhot (contribs/Sophia-Antipolis/HighSchoolGeometry/isocele.v):

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

+

66. Sum of a Geometric Series (ref hol mizar isabelle proofpower)

• Luís Cruz-Filipe (contribs/Nijmegen/CoRN/ftc/MoreFunSeries.v):

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

+

67. e is Transcendental (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

68. Sum of an arithmetic series (ref hol mizar isabelle proofpower)

• many versions (local):

  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 (ref hol mizar isabelle proofpower)

• The Coq development team (theories/ZArith/Znumtheory.v):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

71. Order of a Subgroup (ref hol mizar isabelle proofpower)

• unknown (Laurent Théry?) (contribs/Saclay/Ssreflect/theories/groups.v):

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

+

72. Sylow’s Theorem (ref hol mizar isabelle proofpower)

• Laurent Théry (contribs/Saclay/Ssreflect/theories/sylow.v):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

74. The Principle of Mathematical Induction (ref hol mizar isabelle proofpower)

• built-in (theories/Init):

  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 (ref hol mizar isabelle proofpower)

• Luís Cruz-Filipe (contribs/Nijmegen/CoRN/ftc/Rolle.v):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

77. Sum of kth powers (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

78. The Cauchy-Schwarz Inequality (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

79. The Intermediate Value Theorem (ref hol mizar isabelle proofpower)

• The Coq development team (theories/Reals/Rsqrt_def.v):

  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 (ref hol mizar isabelle proofpower)

• unknown (Inria, Microsoft) (contribs/Saclay/Ssreflect/theories/prime.v):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

82. Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

83. The Friendship Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

84. Morley’s Theorem (ref hol mizar isabelle proofpower)

The proof seems to have been proven (Coq, contrib, Frédérique Guilhot, see this page) but the statement is not here yet. Add a statement.

85. Divisibility by 3 Rule (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

86. Lebesgue Measure and Integration (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

87. Desargues’s Theorem (ref hol mizar isabelle proofpower)

• Frédérique Guilhot (contribs/Sophia-Antipolis/HighSchoolGeometry/affine_classiques.v):

  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 (contribs/Rocq/AreaMethod/examples_2.v):

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

+

88. Derangements Formula (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

89. The Factor and Remainder Theorems (ref hol mizar isabelle proofpower)

The proof seems to have been proven (Coq, contrib, Laurent Théry, Loïc Pottier, see this page) but the statement is not here yet. Add a statement.

90. Stirling’s Formula (ref hol mizar isabelle proofpower)

• Coqtail team (http://coqtail.sourceforge.net/main.php?page=3&doc=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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

92. Pick’s Theorem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

93. The Birthday Problem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

94. The Law of Cosines (ref hol mizar isabelle proofpower)

• Frédérique Guilhot (contribs/Sophia-Antipolis/HighSchoolGeometry/metrique_triangle.v):

  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 (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

96. Principle of Inclusion/Exclusion (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

97. Cramer’s Rule (ref hol mizar isabelle proofpower)

• Georges Gonthier et al. (http://coqfinitgroup.gforge.inria.fr/matrix.html):

  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 (ref hol mizar isabelle proofpower)

• Laurent Théry (contribs/Sophia-Antipolis/Bertrand/Bertrand.v):

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

+

99. Buffon Needle Problem (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.

100. Descartes Rule of Signs (ref hol mizar isabelle proofpower)

Apparently the proof has not been formalized yet. Add a statement anyway.