# 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)