Top100MathematicalTheoremsInCoq

#language en ||Rank ||Theorem ||Statement ||Formalisation available from || ||<style="text-align: center;" |2>1 ||<style="text-align: center;" |2>The Irrationality of the Square Root of 2 ||{{{Theorem sqrt2_not_rational : forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.}}} ||UserContributions/Nijmegen/QArithSternBrocot/sqrt2.v || ||{{{ exists n, exists p, n ^2 = 2* p^2 /\ n <> 0}}} ||SquareRootTwo || ||2 ||Fundamental Theorem of Algebra ||{{{Lemma FTA : forall f : CCX, nonConst _ f -> {z : CC | f ! z [=] Zero}.}}} <
> {{{Lemma FTA_a_la_Henk : forall f : CCX, {x : CC | {y : CC | AbsCC (f ! x[-]f ! y) [>]Zero}} -> {z : CC | f ! z [=] Zero}.}}} ||UserContributions/Nijmegen/CoRN/fta/FTA.v || ||3 ||The Denumerability of the Rational Numbers ||{{{Theorem Q_is_denumerable: is_denumerable Q.}}} <
> ''where''<
> {{{Definition is_denumerable A := same_cardinality A nat.}}} <
>{{{Definition same_cardinality (A 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}}.}}} ||UserContributions/Nijmegen/QArithSternBrocot/Q_denumerable.v || ||4 ||Pythagorean Theorem || {{{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.}}} ||UserContributions/Sophia-Antipolis/geometry || ||6 ||Gödel's Incompleteness Theorem ||{{{ forall T : System, Included Formula NN T -> RepresentsInSelf T -> DecidableSet Formula T -> }}} {{{ }}} {{{{ f : Formula | (Sentence f) /\ ({SysPrf T f} + {SysPrf T (notH f)} -> Inconsistent LNN T)} }}} ||UserContributions/Berkeley/Godel || ||11 ||The Infinitude of Primes ||{{{(EX l:(list Prime) | (p:Prime)(In p l))}}} ||NotFinitePrimes || ||13 ||Polyhedron Formula || ? || UserContributions/Strasbourg/... || ||15 ||Fundamental Theorem of Integral Calculus ||{{{Lemma FTC1 : forall (J : interval) (F : PartFunct IR) (contF : Continuous J F)}}} {{{ }}} {{{(x0 : IR) (Hx0 : J x0) (pJ : proper J), Derivative J pJ (([-S-]contF) x0 Hx0) F}}} {{{ }}} {{{Lemma FTC2 : forall (J : interval) (F : PartFunct IR) (contF : Continuous J F)}}} {{{ }}} {{{(x0 : IR) (Hx0 : J x0) (pJ : proper J) (G0 : PartFunct IR), Derivative J pJ G0 F ->}}} {{{ }}} {{{ {c : IR | Feq J (([-S-]contF) x0 Hx0{-}G0) [-C-]c} }}} {{{ }}} {{{Lemma Barrow : forall (J : interval) (F : PartFunct IR), Continuous J F ->}}} {{{ }}} {{{forall (pJ : proper J) (G0 : PartFunct IR) (derG0 : Derivative J pJ G0 F) (a b : IR)}}} {{{ }}} {{{(H : Continuous_I (Min_leEq_Max a b) F) (Ha : J a) (Hb : J b),}}} {{{ }}} {{{let Ha' := Derivative_imp_inc J pJ G0 F derG0 a Ha in}}} {{{ }}} {{{let Hb' := Derivative_imp_inc J pJ G0 F derG0 b Hb in}}} {{{ }}} {{{Integral H[=]G0 b Hb'[-]G0 a Ha'}}} ||UserContributions/Nijmegen/CoRN || ||17 ||De Moivre's Theorem ||??? ||UserContributions/Sophia-Antipolis/ || ||18 ||Liouville's Theorem and the Construction of Transcendental Numbers|| ??? || UserContributions/Nijmegen/CoRN || ||20 ||All Primes Equal the Sum of Two Squares ||{{{forall n, 0 <= n -> (forall p, prime p -> Zis_mod p 3 4 -> Zeven (Zdiv_exp p n)) -> sum_of_two_square n}}} ||UserContributions/Sophia-Antipolis/SumOfTwoSquare || ||23 ||Formula for Pythagorean Triples ||{{{Lemma pytha_thm1 : forall a b c : Z, (is_pytha a b c) -> (pytha_set a b c).}}} {{{Lemma pytha_thm2 : forall a b c : Z, (pytha_set a b c) -> (is_pytha a b c).}}} ||http://coq.inria.fr/contribs/Fermat4.html (File Pythagorean.v) by ''http://cedric.cnam.fr/~delahaye/'' and ''http://www-lipn.univ-paris13.fr/~mayero/'' || ||25 ||Schroeder--Bernstein Theorem ||{{{forall A B:Ensemble U, A <=_card B -> B <=_card A -> A =card B.}}} ||UserContributions/Rocq/SCHROEDER || ||26 ||Leibnitz's Series for Pi ||??? ||UserContributions/Nijmegen/CoRN || ||27 ||Sum of the Angles of a Triangle ||??? ||UserContributions/Sophia-Antipolis/ || ||32 ||The Four Color Problem ||??? ||GeorgesGonthier http://research.microsoft.com/~gonthier/ || ||35 ||Taylor's Theorem ||{{{Lemma Taylor}}} {{{ }}} {{{: forall (I : interval) (pI : proper I) (F : PartFunct IR) (n : nat)}}} {{{ }}} {{{(f : forall i : nat, i < S n -> PartFunct IR)}}} {{{ }}} {{{(derF : forall (i : nat) (Hi : i < S n),}}} {{{ }}} {{{Derivative_n i I pI F (f i Hi)) (F' : PartFunct IR),}}} {{{ }}} {{{Derivative_n (S n) I pI F F' ->}}} {{{ }}} {{{forall (a b : IR) (Ha : I a),}}} {{{ }}} {{{I b ->}}} {{{ }}} {{{forall e : IR,}}} {{{ }}} {{{Zero[<]e ->}}} {{{ }}} {{{forall Hb' : Dom F b,}}} {{{ }}} {{{ {c : IR | Compact (Min_leEq_Max a b) c |}}} {{{ }}} {{{forall}}} {{{ }}} {{{Hc : Dom}}} {{{ }}} {{{(F'{}[-C-](One[/]nring (fac n)[//]nring_fac_ap_zero IR n){} }}} {{{ }}} {{{([-C-]b{-}FId){^}n) c,}}} {{{ }}} {{{AbsIR}}} {{{ }}} {{{(F b Hb'[-]}}} {{{ }}} {{{Taylor_Seq I pI F n f derF a Ha b}}} {{{ }}} {{{(Taylor_aux I pI F n f derF a b Ha)[-]}}} {{{ }}} {{{(F'{}[-C-](One[/]nring (fac n)[//]nring_fac_ap_zero IR n){} }}} {{{ }}} {{{([-C-]b{-}FId){^}n) c Hc*)[<=]e} }}} ||UserContributions/Nijmegen/CoRN || ||44 ||Binomial Theorem ||{{{(a + b) ^ n = \sum(i < n.+1) (bin n i * (a ^ (n - i) * b ^ i))}}} ||http://coqfinitgroup.gforge.inria.fr/binomial.html#exp_pascal || ||49 ||Cayley-Hamilton Theorem ||Every square matrix is a root of its characteristic polynomial : {{{forall A, (Zpoly (char_poly A)).[A] = 0}}} ||Math Components Project : http://coqfinitgroup.gforge.inria.fr/charpoly.html#Cayley_Hamilton || ||<style="text-align: center;" |2>51 ||<style="text-align: center;" |2>Wilson's Theorem ||{{{forall p, prime p -> Zis_mod (Zfact (p - 1)) (- 1) p}}} ||UserContributions/Sophia-Antipolis/ || ||{{{forall p, 1 < p -> (prime p <-> p %| (fact (p.-1)).+1)}}} ||http://coqfinitgroup.gforge.inria.fr/binomial.html#wilson || ||52 ||The Number of Subsets of a Set ||??? ||??? || ||55 ||Product of Segments of Chords ||{{{forall A B C D M O:point, samedistance O A O B -> samedistance O A O C -> samedistance O A O D ->}}}<
> {{{collinear A B M -> collinear C D M -> }}}<
> {{{ (distance M A)(distance M B)=(distance M C)(distance M D) / parallel A B C D. }}} ||to appear next... || ||<style="text-align: center;" |2>60 ||<style="text-align: center;" |2>Bezout's Theorem ||??? ||StandardLibrary/Coq.ZArith.Znumtheory || ||{{{forall m n, m > 0 -> {a | a < m & m %| gcdn m n + a * n} }}} <
> {{{forall m n, n > 0 -> {a | a < n & n %| gcdn m n + a * m} }}} ||http://coqfinitgroup.gforge.inria.fr/div.html#bezoutl || ||61 ||Theorem of Ceva ||??? ||UserContributions/Sophia-Antipolis/ || ||65 ||Isosceles Triangle Theorem ||??? ||UserContributions/Sophia-Antipolis/ || ||66 ||Sum of a Geometric Series ||{{{Lemma power_series_conv}}} {{{ }}} {{{: forall c : IR, AbsIR c[<]One -> convergent (power_series c)}}}<
> {{{Lemma power_series_sum}}} {{{ }}} {{{: forall c : IR,}}} {{{ }}} {{{AbsIR c[<]One ->}}} {{{ }}} {{{forall (H : Dom (f_rcpcl' IR) (One[-]c))}}} {{{ }}} {{{(Hc0 : convergent (power_series c)),}}} {{{ }}} {{{series_sum (power_series c) Hc0=}}} ||UserContributions/Nijmegen/CoRN || ||69 ||Greatest Common Divisor Algorithm ||??? ||StandardLibrary/Coq.ZArith.Znumtheory || ||71 ||Order of a Subgroup ||{{{forall (gT : finGroupType) (G H : {group gT}), H :<=: G -> (#|H| * #|G : H|)%N = #|G|}}} ||http://coqfinitgroup.gforge.inria.fr/groups.html#LaGrange || ||||<style="text-align: center;"> || || || ||72 ||Sylow Theorem ||{{{Lemma Sylow_exists: forall (p : nat) (gT : finGroupType) (G : {group gT}), {P : {group gT} | p.-Sylow(G) P} }}} <
> {{{Lemma Sylow_subj: forall (p : nat) (gT : finGroupType) (G P Q : {group gT}),}}} <
> {{{ p.-Sylow(G) P -> Q :<=: G -> p.-group Q -> exists2 x : gT, x \in G & Q :<=: P :^ x }}}<
> {{{Lemma card_Syl_dvd : forall (p : nat) (gT : finGroupType) (G : {group gT}), #|'Syl_p(G)| %| #|G| }}}<
> {{{Lemma card_Syl_mod : forall (p : nat) (gT : finGroupType) (G : {group gT}), prime p -> #|'Syl_p(G)| %% p = 1}}} ||http://coqfinitgroup.gforge.inria.fr/sylow.html || ||74 ||The Principle of Mathematical Induction ||{{{forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) ->}}} {{{ forall n : nat, P n}}} ||StandardLibrary || ||75 ||The Mean Value Theorem ||{{{Lemma Law_of_the_Mean : forall (I : interval) (pI : proper I) (F F' : PartFunct IR),}}} {{{ }}} {{{Derivative I pI F F' ->}}} {{{ }}} {{{forall a b : IR,}}} {{{ }}} {{{I a ->}}} {{{ }}} {{{I b ->}}} {{{ }}} {{{forall e : IR,}}} {{{ }}} {{{Zero[<]e ->}}} {{{ }}} {{{ {x : IR | Compact (Min_leEq_Max a b) x |}}} {{{ }}} {{{forall (Ha : Dom F a) (Hb : Dom F b) (Hx : Dom F' x),}}} {{{ }}} {{{AbsIR (F b Hb[-]F a Ha[-]F' x Hx*)[<=]e} }}} {{{ }}} {{{Lemma Law_of_the_Mean_ineq : forall (I : interval) (pI : proper I) (F F' : PartFunct IR),}}} {{{ }}} {{{Derivative I pI F F' ->}}} {{{ }}} {{{forall a b : IR,}}} {{{ }}} {{{I a ->}}} {{{ }}} {{{I b ->}}} {{{ }}} {{{forall c : IR,}}} {{{ }}} {{{(forall x : IR,}}} {{{ }}} {{{Compact (Min_leEq_Max a b) x ->}}} {{{ }}} {{{forall Hx : Dom F' x, AbsIR (F' x Hx)[<=]c) ->}}} {{{ }}} {{{forall (Ha : Dom F a) (Hb : Dom F b),}}} {{{ }}} {{{F b Hb[-]F a Ha[<=]c[*]AbsIR (b[-]a)}}} ||UserContributions/Nijmegen/CoRN || ||79 ||The Intermediate Value Theorem ||{{{Lemma Civt_op}}} {{{ }}} {{{: forall f : CSetoid_un_op IR,}}} {{{ }}} {{{contin f ->}}} {{{ }}} {{{(forall a b : IR, a[<]b -> {c : IR | a[<=]c /\ c[<=]b | f c[#]Zero}) ->}}} {{{ }}} {{{forall a b : IR,}}} {{{ }}} {{{a[<]b ->}}} {{{ }}} {{{f a[<=]Zero ->}}} {{{ }}} {{{Zero[<=]f b -> {z : IR | a[<=]z /\ z[<=]b /\ f z[=]Zero} }}} ||UserContributions/Nijmegen/CoRN || ||80 ||The Fundamental Theorem of Arithmetic ||??? ||UserContributions/Eindhoven/POCKLINGTON || ||87 ||Desargues's Theorem ||??? ||UserContributions/Sophia-Antipolis/geometry || ||89 ||The Factor and Remainder Theorems ||??? ||StandardLibrary || ||94 ||The Law of Cosines ||??? ||UserContributions/Sophia-Antipolis/ || ||97 ||Cramer's rule ||{{{forall (R : comRingType) (n : nat) (A : matrix R n n), A *m \adj A = \Z (\det A)}}} ||Math Components Project : http://coqfinitgroup.gforge.inria.fr/matrix.html#mulmx_adjr || ||98 ||Bertrand’s Postulate ||{{{forall n : nat, 2 <= n -> exists p : nat, prime p /\ n < p /\ p < 2 * n}}} ||UserContributions/Sophia-Antipolis/Bertrand ||

---

• The theorems regarding angles or triangles are proved in one of the two UserContributions/Sophia-Antipolis/geometry or UserContributions/Sophia-Antipolis/Angles (please specify if you know which contrib package contains them).

• The Ranks are taken from the original list of Top100MathematicalTheorems.

• See Also http://www.cs.ru.nl/~freek/100/