• Graph Theory |Nov 8, 2024 | Olivia Röhrig

    Mantel's Theorem via the AM-GM Inequality

    We cover a proof of Mantel's Theorem that the maximum number of edges in a triangle-free graph is bounded by \(n^2/4\) using the inequality of the arithmetic and geometric mean.
  • Graph Theory |Oct 15, 2024 | Christoph Spiegel Christoph Spiegel

    Mantel's Theorem via Cauchy's inequality

    We cover a proof of Mantel's Theorem that the maximum number of edges in a triangle-free graph is bounded by \(n^2/4\) using the Cauchy-Schwarz inequality and the handshaking lemma.
  • Graph Theory |Oct 11, 2024 | Christoph Spiegel Christoph Spiegel

    The Handshaking Lemma

    We cover a proof of the handshaking lemma, or more specifically the degree sum formula, that establishes that the sum of the degrees of all vertices in a finite graph is twice the number of edges.
  • Fundamentals |May 10, 2024 | Yves Jäckle Yves Jäckle

    A closer look at type theory

    We'll take a closer look at type theory and type checking, and how they allow us to express and check the correctness of mathematics. We'll discuss types from a theoretical perspective, sketching type-checking in the process, and then illustrate how to encode mathematics in this framework.
  • Number Theory |Mar 15, 2024 | Christoph Spiegel Christoph Spiegel

    Infinitude of Primes - Fürstenberg's proof

    We cover Fürstenberg's proof of the infinitude of primes that establishes a contradiction from the assumption that there are only finitely many primes from a unique topology in the integers.
  • Number Theory |Mar 8, 2024 | Christoph Spiegel Christoph Spiegel

    Infinitude of Primes - Folklore proof

    We cover the folklore proof of the infinitude of primes that establishes that for any prime \(p\) the prime divisors of the Mersenne number \(2^p - 1\) are bigger than \(p\) using Lagrange's theorem.
  • Number Theory |Mar 1, 2024 | Christoph Spiegel Christoph Spiegel

    Infinitude of Primes - Goldbach's Proof

    We cover Goldbach's proof of the infinitude of primes, showing that the Fermat numbers are pairwise distinct and prime, so that there must be infinitely many primes.
  • Fundamentals |Feb 23, 2024 | Christoph Spiegel Christoph Spiegel

    Getting used to types

    We have a look at the dependent type theory underlying Lean, exploring why we write n : ℕ and not n ∈ ℕ and discovering types stacked on types stacked on types stacked on types...
  • Number Theory |Feb 16, 2024 | Christoph Spiegel Christoph Spiegel

    Infinitude of Primes - Euclid's Proof

    We cover Euclid's proof of the infinitude of primes, leading the assumption that there is only a finite number of primes \(p_1, \ldots, p_r\) to a contradiction by showing that none of them divide \(p_1 \cdots p_r + 1\).
  • Number Theory |Feb 9, 2024 | Christoph Spiegel Christoph Spiegel

    Infinitude of Primes – The Statement

    We start by highlighting where to find basic definitions and properties of primality in mathlib, then introduces three versions of the infinitude of primes statement and establishes their equivalence.
  • Fundamentals |Feb 2, 2024 | Christoph Spiegel Christoph Spiegel

    Getting set up and started with Lean

    This post covers some general basics, such as managing and building Lean 4 projects, using the mathlib library, setting up VS Code for Lean, and copying this project's code repository.