# Past Formalisation Projects

## Algebra

- Symmetric Polynomials
- The Mason–Stothers Theorem
- Descartes' Rule of Signs
- Sturm's Theorem
- In the Isabelle distribution: factorial rings, Euclidean rings

## Analysis

- 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 dimension of
*n*-dimensional balls and simplices

## Probability

- 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

- 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

## Analytic Number Theory

## Prime Numbers

- 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

- 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 Recurrences
- Monad normalisation

(joint work with Joshua Schneider and Andreas Lochbihler)