Wiedijk’s 100 Theorems

Content created by Fredrik Bakke, Louis Wasserman, Egbert Rijke and malarbol.

Created on 2024-10-17.
Last modified on 2025-11-10.

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

25. Schröder–Bernstein theorem

Author: Elif Uskuplu

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

Author: Fredrik Bakke

open import foundation.cantor-schroder-bernstein-decidable-embeddings using
  ( Cantor-Schröder-Bernstein-WLPO)

42. Sum of the Reciprocals of the Triangular Numbers

Author: Louis Wasserman

open import elementary-number-theory.triangular-numbers using
  ( sum-reciprocal-triangular-number-ℕ)

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)

66. Sum of a Geometric Series

Author: Louis Wasserman

open import real-numbers.geometric-sequences-real-numbers using
  ( compute-sum-standard-geometric-fin-sequence-ℝ ;
    compute-sum-standard-geometric-series-ℝ)

68. Sum of an arithmetic series

Author: malarbol

open import elementary-number-theory.triangular-numbers using
  ( compute-triangular-number-ℕ)
open import ring-theory.arithmetic-series-semirings using
  ( compute-sum-add-mul-nat-Semiring)

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-neighborhood-ℝ)

Author: Louis Wasserman

open import real-numbers.absolute-value-real-numbers using
  ( triangle-inequality-abs-ℝ)
open import real-numbers.distance-real-numbers using
  ( triangle-inequality-dist-ℝ)

See also

  • The spiritual successor to Formalizing 100 Theorems is 1000+ theorems [1000+].

References

[1000+]
1000plus. 1000+ theorems. URL: https://1000-plus.github.io/.
[Wie]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.

Recent changes