Freek Wiedijk’s 100 Theorems

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-10-17.
Last modified on 2024-10-29.

This file records formalized results from Freek Wiedijk’s Formalizing 100 Theorems. [Wie]

module literature.100-theorems where

The list

3. The Denumerability of the Rational Numbers

Author: Fredrik Bakke

open import elementary-number-theory.rational-numbers using
  ( is-countable-ℚ)

11. The Infinitude of Primes

Author: Egbert Rijke

open import elementary-number-theory.infinitude-of-primes using
  ( infinitude-of-primes-ℕ)

22. The Non-Denumerability of the Continuum

This is not yet formalized.

25. Schröder–Bernstein Theorem

Author: Elif Uskuplu

Note: The formalization of the Cantor-Schröder-Bernstein theorem in agda-unimath is a generalization of the statement to all types, i.e., it is not restricted to sets. This generalization is originally due to Martin-Escardó, hence we refer to the generalization as the Cantor-Schröder-Bernstein-Escardó theorem.

open import foundation.cantor-schroder-bernstein-escardo using
  ( Cantor-Schröder-Bernstein-Escardó)
open import foundation.cantor-schroder-bernstein-escardo using
  ( Cantor-Schröder-Bernstein)

44. The Binomial Theorem

Author: Egbert Rijke

open import commutative-algebra.binomial-theorem-commutative-rings using
  ( binomial-theorem-Commutative-Ring)
open import commutative-algebra.binomial-theorem-commutative-semirings using
  ( binomial-theorem-Commutative-Semiring)
open import ring-theory.binomial-theorem-rings using
  ( binomial-theorem-Ring)
open import ring-theory.binomial-theorem-semirings using
  ( binomial-theorem-Semiring)
open import elementary-number-theory.binomial-theorem-integers using
  ( binomial-theorem-ℤ)
open import elementary-number-theory.binomial-theorem-natural-numbers using
  ( binomial-theorem-ℕ)

52. The Number of Subsets of a Set

Author: Egbert Rijke

open import univalent-combinatorics.decidable-subtypes using
  ( number-of-elements-decidable-subtype-is-finite)

58. Formula for the number of combinations

Author: Egbert Rijke

open import univalent-combinatorics.binomial-types using
  ( has-cardinality-binomial-type)

60. Bezout’s Lemma

Author: Bryan Lu

Note that the 60th theorem in Freek’s list is listed as “Bezout’s Theorem”, while the linked theorems are formalizations of Bezout’s lemma, even though these are different statements.

open import elementary-number-theory.bezouts-lemma-integers using
  ( bezouts-lemma-ℤ)
open import elementary-number-theory.bezouts-lemma-natural-numbers using
  ( bezouts-lemma-ℕ)

63. Cantor’s Theorem

Author: Egbert Rijke

open import foundation.cantors-theorem using
  ( theorem-Cantor)

69. Greatest Common Divisor Algorithm

Author: Egbert Rijke

open import
  elementary-number-theory.greatest-common-divisor-natural-numbers using
  ( GCD-ℕ)

74. The Principle of Mathematical Induction

Author: Egbert Rijke

open import elementary-number-theory.natural-numbers using
  ( ind-ℕ)

80. The Fundamental Theorem of Arithmetic

Author: Victor Blanchi

open import elementary-number-theory.fundamental-theorem-of-arithmetic using
  ( fundamental-theorem-arithmetic-list-ℕ)

91. The Triangle Inequality

Author: malarbol

open import real-numbers.metric-space-of-real-numbers using
  ( is-triangular-premetric-leq-ℝ)

96. Principle of Inclusion/Exclusion

This is not yet formalized.

References

[Wie]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.
  • The spiritual successor to Formalizing 100 Theorems is 1000+ theorems, also due to Freek Wiedijk.

Recent changes