Formalisation Projects

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

• Two theorems about the geometry of the critical points of a complex polynomial
• Chebyshev Polynomials
• Elimination of Repeated Factors Algorithm
  (joint work with Katharina Kreuzer)
• Perfect Fields
  (joint work with Katharina Kreuzer)
• 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

• Generalised Hypergeometric Series
• Continued Fractions
• Lambert Series
• The Sophomore's Dream
• A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent
• The Euler–MacLaurin Formula
• In the Isabelle distribution: summability tests

Complex Analysis

• Laurent Series Expansions on an Annulus
• The Detour Calculus: Rigorous Local Deformation of Integration Contours
• Path Equivalence and Automation for Integration Contours
• In the Isabelle distribution: Generalised Binomial Theorem, connection of formal power series and analytic functions, meromorphicity, the Weierstraß Factorisation Theorem

Special Functions

• The Incomplete Gamma Function
• The Polylogarithm Function
• The Lambert W Function on the Reals
• The Error Function
• In the Isabelle distribution: The Γ function

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

• Executable Randomized Algorithms
  (joint work with Emin Karayel)
• 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

• Archimedes' Cattle Problem
• The Sum-of-Squares Function and Jacobi's Two-Square Theorem
• The Boustrophedon Transform, the Entringer Numbers, and Related Sequences
• A simple proof that π is irrational
• Kummer's Congruence
• 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

• Rademacher's Series for the Partition Function
  (joint work with Lawrence C. Paulson)
• Perron's Formula
• Complex Lattices, Elliptic Functions, and the Modular Group
  (joint work with Anthony Bordg, Wenda Li, and Lawrence C. Paulson)
• The Partition Function and the Pentagonal Number Theorem
• Dedekind Sums
  (joint work with Anthony Bordg, Lawrence C. Paulson, and Wenda Li)
• Combinatorial q-Analogues
• The Rogers–Ramanujan Identities
• Theta Functions
• 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

• Concrete bounds for Chebyshev’s prime counting functions
• 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 Impossibility of Strategyproof Rank Aggregation
  (joint work with Patrick Lederer)
• 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

• Height Bounds for Height-Balanced Trees
• Bessel Functions of the First Kind
• Complete Elliptic Integrals and the Arithmetic–Geometric Mean
• The Exponential and Logarithmic Integral
• The Karatsuba Square Root Algorithm
• Parallel Shear Sort
  (joint work with Peter Lammich)
• 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

• Linear orders as rankings
• Swap Distance
• The Cardinality of the Continuum
• 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)