The following is a list of all the published Isabelle/HOL formalisation projects that I (co-)authored. All of these are published either as articles in the Archive of Formal Proofs or, in some cases, the Isabelle/HOl standard library.
Algebra
- Factorization of Polynomials with Algebraic Coefficients
(joint work with René Thiemann) - Finitely Generated Abelian Groups
(joint work with Joseph Thommes) - Formal Puiseux Series
- Power Sum Polynomials
- Symmetric Polynomials
- The Mason–Stothers Theorem
- Descartes' Rule of Signs
- Sturm's Theorem
- In the Isabelle distribution: factorial rings, Euclidean rings
Analysis
- The Sophomore's Dream
- A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent
- 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)
Combinatorics and General Number Theory
- Gaussian Integers
- 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
- Furstenberg's topology and his proof of the infinitude of primes
- 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 Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections
(joint work with Théo Delemazure, Tom Demeulemeester, Jonas Israel, and Patrick Lederer) - 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
- The Hales–Jewett Theorem
(joint work with Ujkan Sulejmani and Katharina Kreuzer) - Pólya’s Proof of the Weighted Arithmetic–Geometric Mean Inequality
- Van der Waerden's Theorem
(joint work with Katharina Kreuzer) - Selected Problems from the International Mathematical Olympiad 2019
- Linear Recurrences
- Monad normalisation
(joint work with Joshua Schneider and Andreas Lochbihler)