Past Formalisation Projects
Algebra
- Formal Puiseux Series
- Gaussian Integers
- Power Sum Polynomials
- Symmetric Polynomials
- The Mason–Stothers Theorem
- Linear Recurrences
- Descartes' Rule of Signs
- Sturm's Theorem
- In the Isabelle distribution: factorial rings, Euclidean rings
Analysis
- The Lambert W Function on the Reals
- The Error Function
- The Euler–MacLaurin Formula
- In the Isabelle distribution: The Γ function, Generalised Binomial Theorem, summability tests, connection of formal power series and analytic functions
Asymptotics
- Stirling's formula
- Landau Symbols
- The Akra-Bazzi theorem and the Master theorem
- In the Isabelle distribution: The
real_asymp
method for proving asymptotic properties of real-valued functions
Geometry
- Minkowski's Theorem
- Basic Geometric Properties of Triangles
- In the Isabelle distribution: The volume of n-dimensional balls and simplices
Probability
- The Laws of Large Numbers
- Buffon's Needle Problem
- A Verified Compiler for Probability Density Functions
(joint work with Johannes Hölzl and Tobias Nipkow) - In the Isabelle distribution: Giry monad. Additionally, some contributions to Sébastien Gouëzel's entry on Ergodic Theory (namely the ergodicity of the shift map).
Combinatorics and General Number Theory
- Furstenberg's topology and his proof of the infinitude of primes
- Pell's Equation
- Bernoulli Numbers
(joint work with Lukas Bulwahn) - Catalan Numbers
- In the Isabelle distribution: Carmichael's function and primitive roots in residue rings
Transcendental Number Theory
- The Hermite–Lindemann–Weierstraß Transcendence Theorem
- The Transcendence of π
- The Transcendence of e
- Liouville numbers
Analytic Number Theory
- The Irrationality of ζ(3)
- Gauss Sums and the Pólya–Vinogradov Inequality
(joint work with Rodrigo Raya) - Dirichlet L-Functions and Dirichlet's Theorem
- Dirichlet Series
- The Hurwitz and Riemann ζ Functions
Prime Numbers
- Mersenne primes and the Lucas–Lehmer test
- Elementary Facts About the Distribution of Primes
- Probabilistic Primality Testing
(joint work with Daniel Stüwe) - The Prime Number Theorem
(joint work with Lawrence C. Paulson) - Bertrand's postulate
(joint work with Julian Biendarra) - The Divergence of the Prime Harmonic Series
Social Choice Theory
- The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
(joint work with Felix Brandt, Christian Saile, and Christian Stricker) - Randomised Social Choice Theory
- The Incompatibility of SD-Efficiency and SD-Strategy-Proofness
Algorithms and Data Structures
- Skip Lists
(joint work with Max W. Haslbeck) - The Inversions of a List
- Randomised Binary Search Trees
- Treaps
(joint work with Max W. Haslbeck and Tobias Nipkow) - The Median-of-Medians Selection Algorithm
- Expected Shape of Random Binary Search Trees
- Lower bound on comparison-based sorting algorithms
- The number of comparisons in QuickSort
- Fisher–Yates shuffle
Other
- Selected Problems from the International Mathematical Olympiad 2019
- Monad normalisation
(joint work with Joshua Schneider and Andreas Lochbihler)