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)