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)