-
Upper bound on Ramsey numbers, Part III
We cover the third part of the proof that the \(k\)-th Ramsey number is bounded above by \(2^{2k-3}\), establishing the bound from the results of the two previous posts. -
Upper bound on Ramsey numbers, Part II
We cover the second part of the proof that the \(k\)-th Ramsey number is bounded above by \(2^{2k-3}\), establishing the central statement. -
Upper bound on Ramsey numbers, Part I
We cover the first part of the proof that the \(k\)-th Ramsey number is bounded above by \(2^{2k-3}\), establishing the necessary definitions and prerequisite lemmata. -
Inductive types and proof by induction
This post introduces inductive types and explains leans `induction` tactic. -
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
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
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
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
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
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
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
Getting used to types
We have a look at the dependent type theory underlying Lean, exploring why we writen : ℕand notn ∈ ℕand discovering types stacked on types stacked on types stacked on types... -
Number Theory
|Feb 16, 2024
|
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
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
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.