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:
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
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
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)
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
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:
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
Formalized in: HOL Light, Isabelle, Metamath
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
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
Formalized in: HOL Light, Isabelle
Formalized in: HOL Light, Isabelle, Lean, Metamath, ProofPower
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
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)
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
Formalized in: HOL Light, Isabelle
(* 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
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
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)
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
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
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
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
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
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)
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
Formalized in: Isabelle
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:
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
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
Formalized in: Isabelle, Lean
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:
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
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:
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
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:
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
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
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
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
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
Theorem four_color m : simple_map m -> colorable_with 4 m.
Reproducibility: Good (CI)
Constructive: yes
Axioms used: (none)
Formalized in: Coq
Formalized in: (none)
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
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
Formalized in: HOL Light, Isabelle, Mizar
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
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
Formalized in: HOL Light, Isabelle, Lean, Metamath, Mizar
Formalized in: HOL Light, Isabelle, ProofPower
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
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
Formalized in: (none)
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:
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)
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
Formalized in: HOL Light, Isabelle, Lean, Metamath, Mizar
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
Formalized in: Isabelle
Formalized in: HOL Light, Isabelle, Metamath
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
Formalized in: HOL Light
(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)
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
Lemma card_powerset (T : finType) (A : {set T}) : #|powerset A| = 2 ^ #|A|.
Reproducibility: Good (CI)
Constructive: yes
Axioms used: (none)
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
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
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
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
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
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
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
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
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
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
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
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
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
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:
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
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
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
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
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
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
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
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
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
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)
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
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
Formalized in: HOL Light, Isabelle, Lean, Metamath
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
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
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
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
Formalized in: HOL Light, Isabelle, Lean, Metamath, ProofPower
Formalized in: Lean
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
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
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
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:
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
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:
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:
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
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
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
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
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
Formalized in: HOL Light
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
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
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
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
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
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
Formalized in: Isabelle, ProofPower
Formalized in: HOL Light, Isabelle, ProofPower