# Formalizing 100 theorems in Coq

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

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

Options:

### 1. The Irrationality of the Square Root of 2

One of many proofs

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 2. Fundamental Theorem of Algebra

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 3. The Denumerability of the Rational Numbers

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

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


Reproducibility: Good (CI)

Constructive: no

Axioms used:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• FunctionalExtensionality.functional_extensionality_dep
• classic
• other geometry axioms

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:

• Eqdep.Eq_rect_eq.eq_rect_eq

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

### 5. Prime Number Theorem

Formalized in: HOL Light, Isabelle, Metamath

### 6. Gödel’s Incompleteness Theorem

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

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

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

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

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 7. Law of Quadratic Reciprocity

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:

• proof_irrelevance
• constructive_definite_description
• classic

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

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

Formalized in: HOL Light, Isabelle

### 9. The Area of a Circle

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

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

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 11. The Infinitude of Primes

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

### 12. The Independence of the Parallel Postulate

Formalized in: HOL Light, Isabelle

### 13. Polyhedron Formula

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

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


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

Constructive: to be determined

Axioms used:

• Euler3.expf_clos_symm

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

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

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


Reproducibility: Good (CI)

Constructive: no

Axioms used:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic

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

### 15. Fundamental Theorem of Integral Calculus

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic

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

### 16. Insolvability of General Higher Degree Equations

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq, Lean

### 17. DeMoivre’s Theorem

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

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

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

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 19. Four Squares Theorem

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

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

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

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

### 21. Green’s Theorem

Formalized in: Isabelle

### 22. The Non-Denumerability of the Continuum

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 23. Formula for Pythagorean Triples

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:

• Coq's axioms for real numbers

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

### 24. The Undecidability of the Continuum Hypothesis

Formalized in: Isabelle, Lean

### 25. Schroeder-Bernstein Theorem

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:

• classic
• Extensionality_Ensembles

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:

• constructive_definite_description
• classic

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

### 26. Leibniz’s Series for Pi

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic

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

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 27. Sum of the Angles of a Triangle

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic
• many geometry axioms

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_triangle_whose_angles_sum_to_two_rights::
postulate_of_existence_of_similar_triangles::
postulate_of_parallelism_of_perpendicular_transversals::
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:

• Eqdep.Eq_rect_eq.eq_rect_eq

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

### 28. Pascal’s Hexagon Theorem

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:

• many projective geometry axioms
• including decidability of incidence

Formalized in: Coq, HOL Light, Mizar

### 29. Feuerbach’s Theorem

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:

• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

Formalized in: Coq (constructive), HOL Light

### 30. The Ballot Problem

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 31. Ramsey’s Theorem

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:

• CoLoR.Util.Logic.DepChoice.dep_choice
• ClassicalEpsilon.constructive_indefinite_description
• Description.constructive_definite_description
• classic

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

### 32. The Four Color Problem

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

Formalized in: Coq

### 33. Fermat’s Last Theorem

Formalized in: (none)

### 34. Divergence of the Harmonic Series

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


Reproducibility: Good (CI)

Constructive: no

Axioms used:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic

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

### 35. Taylor’s Theorem

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 36. Brouwer Fixed Point Theorem

Formalized in: HOL Light, Isabelle, Mizar

### 37. The Solution of a Cubic

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic

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

### 38. Arithmetic Mean/Geometric Mean

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

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

### 39. Solutions to Pell’s Equation

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

### 40. Minkowski’s Fundamental Theorem

Formalized in: HOL Light, Isabelle, ProofPower

### 41. Puiseux’s Theorem

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:

• Puiseux_series.LPO (equivalent to sig_forall_dec)

Formalized in: Coq, Isabelle

### 42. Sum of the Reciprocals of the Triangular Numbers

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


Reproducibility: Good (CI)

Constructive: no

Axioms used:

• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

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

### 43. The Isoperimetric Theorem

Formalized in: (none)

### 44. The Binomial Theorem

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:

• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

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

### 45. The Partition Theorem

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

### 46. The Solution of the General Quartic Equation

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic

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

### 47. The Central Limit Theorem

Formalized in: Isabelle

### 48. Dirichlet’s Theorem

Formalized in: HOL Light, Isabelle, Metamath

### 49. The Cayley-Hamilton Theorem

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 50. The Number of Platonic Solids

Formalized in: HOL Light

### 51. Wilson’s Theorem

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

### 52. The Number of Subsets of a Set

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

### 53. Pi is Trancendental

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

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


Formalized in: Coq, Isabelle

### 54. Konigsberg Bridges Problem

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 55. Product of Segments of Chords

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:

• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

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

### 56. The Hermite-Lindemann Transcendence Theorem

The concept algebraicOver is from the Mathematical Components library.

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

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


Formalized in: Coq, Isabelle

### 57. Heron’s Formula

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:

• classic
• many geometry axioms

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

### 58. Formula for the Number of Combinations

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


Reproducibility: see #52

Constructive: yes

Axioms used: (none)

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

### 59. The Laws of Large Numbers

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• relational_choice
• propositional_extensionality
• proof_irrelevance
• functional_extensionality_dep
• eq_rect_eq
• dependent_unique_choice
• constructive_indefinite_description
• constructive_definite_description
• classic
• JMeq_eq
• Extensionality_Ensembles

Formalized in: Coq, Isabelle, Lean

### 60. Bezout’s Theorem

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

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

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

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

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 61. Theorem of Ceva

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:

• classic
• many geometry axioms

Formalized in: Coq, HOL Light, Metamath, Mizar

### 62. Fair Games Theorem

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

(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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• relational_choice
• propositional_extensionality
• proof_irrelevance
• functional_extensionality_dep
• Eq_rect_eq.eq_rect_eq
• dependent_unique_choice
• constructive_indefinite_description
• constructive_definite_description
• classic
• JMeq_eq
• Ensembles.Extensionality_Ensembles

Formalized in: Coq, Lean

### 63. Cantor’s Theorem

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:

• Extensionality_Ensembles

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

### 64. L’Hopital’s Rule

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic

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

### 65. Isosceles Triangle Theorem

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic
• many geometry axioms

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:

• Eqdep.Eq_rect_eq.eq_rect_eq

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

### 66. Sum of a Geometric Series

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 67. e is Transcendental

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

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

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


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

### 68. Sum of an arithmetic series

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 69. Greatest Common Divisor Algorithm

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

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

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

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 70. The Perfect Number Theorem

uses mathcomp

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


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

Constructive: yes

Axioms used: (none)

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

### 71. Order of a Subgroup

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 72. Sylow’s Theorem

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 73. Ascending or Descending Sequences

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

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


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

Constructive: yes

Axioms used: (none)

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

### 74. The Principle of Mathematical Induction

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

### 75. The Mean Value Theorem

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 76. Fourier Series

Formalized in: HOL Light, Isabelle, Lean, Metamath

### 77. Sum of kth powers

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic

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

### 78. The Cauchy-Schwarz Inequality

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:

• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

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

### 79. The Intermediate Value Theorem

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

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

### 80. The Fundamental Theorem of Arithmetic

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 81. Divergence of the Prime Reciprocal Series

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

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

Formalized in: Lean

### 83. The Friendship Theorem

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


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

Constructive: yes

Axioms used: (none)

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

### 84. Morley’s Theorem

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic
• many geometry axioms

Formalized in: Coq, HOL Light, Mizar

### 85. Divisibility by 3 Rule

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 86. Lebesgue Measure and Integration

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


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

Constructive: no

Axioms used:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• relational_choice
• propositional_extensionality
• dependent_unique_choice
• Description.constructive_definite_description

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:

• propositional_extensionality
• functional_extensionality_dep
• constructive_indefinite_description

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

### 87. Desargues’s Theorem

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:

• ClassicalDedekindReals.sig_forall_dec
• FunctionalExtensionality.functional_extensionality_dep
• classic
• other geometry axioms

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:

• classic
• many geometry axioms

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:

• Eqdep.Eq_rect_eq.eq_rect_eq

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

### 88. Derangements Formula

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


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

Constructive: no

Axioms used:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

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

### 89. The Factor and Remainder Theorems

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

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 90. Stirling’s Formula

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic

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

### 91. The Triangle Inequality

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep

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

### 92. Pick’s Theorem

Formalized in: HOL Light

### 93. The Birthday Problem

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.

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 94. The Law of Cosines

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• FunctionalExtensionality.functional_extensionality_dep
• classic
• other geometry axioms

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

### 95. Ptolemy’s Theorem

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:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• FunctionalExtensionality.functional_extensionality_dep
• classic
• other geometry axioms

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

### 96. Principle of Inclusion/Exclusion

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 97. Cramer’s Rule

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

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


Reproducibility: Good (CI)

Constructive: yes

Axioms used: (none)

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

### 98. Bertrand’s Postulate

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

Reproducibility: Good (CI)

Constructive: no

Axioms used:

• ClassicalDedekindReals.sig_not_dec
• ClassicalDedekindReals.sig_forall_dec
• functional_extensionality_dep
• classic

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

### 99. Buffon Needle Problem

Formalized in: Isabelle, ProofPower

### 100. Descartes Rule of Signs

Formalized in: HOL Light, Isabelle, ProofPower