Sturm's Theorem. - Manuel Eberl (Arch. Formal Proofs, 2014)

A Verified Compiler for Probability Density Functions. - Manuel Eberl; Johannes Hölzl; Tobias Nipkow (Arch. Formal Proofs, 2014)

A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL. - Manuel Eberl (CPP, 2015)

The Akra-Bazzi theorem and the Master theorem. - Manuel Eberl (Arch. Formal Proofs, 2015)

Landau Symbols. - Manuel Eberl (Arch. Formal Proofs, 2015)

Descartes' Rule of Signs. - Manuel Eberl (Arch. Formal Proofs, 2015)

The Divergence of the Prime Harmonic Series. - Manuel Eberl (Arch. Formal Proofs, 2015)

Basic Geometric Properties of Triangles. - Manuel Eberl (Arch. Formal Proofs, 2015)

Liouville numbers. - Manuel Eberl (Arch. Formal Proofs, 2015)

The Incompatibility of SD-Efficiency and SD-Strategy-Proofness. - Manuel Eberl (Arch. Formal Proofs, 2016)

Randomised Social Choice Theory. - Manuel Eberl (Arch. Formal Proofs, 2016)

Catalan Numbers. - Manuel Eberl (Arch. Formal Proofs, 2016)

Stirling's formula. - Manuel Eberl (Arch. Formal Proofs, 2016)

Fisher-Yates shuffle. - Manuel Eberl (Arch. Formal Proofs, 2016)

Bertrand's postulate. - Julian Biendarra; Manuel Eberl (Arch. Formal Proofs, 2017)

Bernoulli Numbers. - Lukas Bulwahn; Manuel Eberl (Arch. Formal Proofs, 2017)

The Transcendence of e. - Manuel Eberl (Arch. Formal Proofs, 2017)

The Euler-MacLaurin Formula. - Manuel Eberl (Arch. Formal Proofs, 2017)

Lower bound on comparison-based sorting algorithms. - Manuel Eberl (Arch. Formal Proofs, 2017)

The number of comparisons in QuickSort. - Manuel Eberl (Arch. Formal Proofs, 2017)

Expected Shape of Random Binary Search Trees. - Manuel Eberl (Arch. Formal Proofs, 2017)

Buffon's Needle Problem. - Manuel Eberl (Arch. Formal Proofs, 2017)

Minkowski's Theorem. - Manuel Eberl (Arch. Formal Proofs, 2017)

Dirichlet Series. - Manuel Eberl (Arch. Formal Proofs, 2017)

The Hurwitz and Riemann ζ Functions. - Manuel Eberl (Arch. Formal Proofs, 2017)

Linear Recurrences. - Manuel Eberl (Arch. Formal Proofs, 2017)

The Mason-Stother's Theorem. - Manuel Eberl (Arch. Formal Proofs, 2017)

The Median-of-Medians Selection Algorithm. - Manuel Eberl (Arch. Formal Proofs, 2017)

Dirichlet L-Functions and Dirichlet's Theorem. - Manuel Eberl (Arch. Formal Proofs, 2017)

Monad normalisation. - Joshua Schneider 001; Manuel Eberl; Andreas Lochbihler (Arch. Formal Proofs, 2017)

Proving Divide and Conquer Complexities in Isabelle/HOL. - Manuel Eberl (J. Autom. Reason., 2017)

The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency. - Felix Brandt 001; Manuel Eberl; Christian Saile; Christian Stricker 001 (Arch. Formal Proofs, 2018)

The Error Function. - Manuel Eberl (Arch. Formal Proofs, 2018)

Pell's Equation. - Manuel Eberl (Arch. Formal Proofs, 2018)

Symmetric Polynomials. - Manuel Eberl (Arch. Formal Proofs, 2018)

The Transcendence of π. - Manuel Eberl (Arch. Formal Proofs, 2018)

Randomised Binary Search Trees. - Manuel Eberl (Arch. Formal Proofs, 2018)

The Prime Number Theorem. - Manuel Eberl; Lawrence C. Paulson (Arch. Formal Proofs, 2018)

Treaps. - Max W. Haslbeck; Manuel Eberl; Tobias Nipkow (Arch. Formal Proofs, 2018)

Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving. - Florian Brandl; Felix Brandt 001; Manuel Eberl; Christian Geist (J. ACM, 2018)

Verified solving and asymptotics of linear recurrences. - Manuel Eberl (CPP, 2019)

Verifying Randomised Social Choice. - Manuel Eberl (FroCos, 2019)

Verified Real Asymptotics in Isabelle/HOL. - Manuel Eberl (ISSAC, 2019)

Nine Chapters of Analytic Number Theory in Isabelle/HOL. - Manuel Eberl (ITP, 2019)

The Inversions of a List. - Manuel Eberl (Arch. Formal Proofs, 2019)

Elementary Facts About the Distribution of Primes. - Manuel Eberl (Arch. Formal Proofs, 2019)

Selected Problems from the International Mathematical Olympiad 2019. - Manuel Eberl (Arch. Formal Proofs, 2019)

The Irrationality of ζ(3). - Manuel Eberl (Arch. Formal Proofs, 2019)

Gauss Sums and the Pólya-Vinogradov Inequality. - Rodrigo Raya; Manuel Eberl (Arch. Formal Proofs, 2019)

Probabilistic Primality Testing. - Daniel Stüwe; Manuel Eberl (Arch. Formal Proofs, 2019)

Verified Textbook Algorithms - A Biased Survey. - Tobias Nipkow; Manuel Eberl; Maximilian P. L. Haslbeck (ATVA, 2020)

Mersenne primes and the Lucas-Lehmer test. - Manuel Eberl (Arch. Formal Proofs, 2020)

Furstenberg's topology and his proof of the infinitude of primes. - Manuel Eberl (Arch. Formal Proofs, 2020)

Gaussian Integers. - Manuel Eberl (Arch. Formal Proofs, 2020)

The Lambert W Function on the Reals. - Manuel Eberl (Arch. Formal Proofs, 2020)

Power Sum Polynomials. - Manuel Eberl (Arch. Formal Proofs, 2020)

Skip Lists. - Max W. Haslbeck; Manuel Eberl (Arch. Formal Proofs, 2020)

Verified Analysis of Random Binary Tree Structures. - Manuel Eberl; Max W. Haslbeck; Tobias Nipkow (J. Autom. Reason., 2020)

The Laws of Large Numbers. - Manuel Eberl (Arch. Formal Proofs, 2021)

Formal Puiseux Series. - Manuel Eberl (Arch. Formal Proofs, 2021)

The Hermite-Lindemann-Weierstraß Transcendence Theorem. - Manuel Eberl (Arch. Formal Proofs, 2021)

Factorization of Polynomials with Algebraic Coefficients. - Manuel Eberl; René Thiemann (Arch. Formal Proofs, 2021)

Van der Waerden's Theorem. - Katharina Kreuzer; Manuel Eberl (Arch. Formal Proofs, 2021)

Finitely Generated Abelian Groups. - Joseph Thommes; Manuel Eberl (Arch. Formal Proofs, 2021)

Asymptotic Reasoning in a Proof Assistant (Asymptotische Beweisführung in einem Beweisassistenten) - Manuel Eberl (2021)

The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections. - Théo Delemazure; Tom Demeulemeester; Manuel Eberl; Jonas Israel; Patrick Lederer (Arch. Formal Proofs, 2022)

A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent. - Manuel Eberl (Arch. Formal Proofs, 2022)

The Sophomore's Dream. - Manuel Eberl (Arch. Formal Proofs, 2022)

Pólya's Proof of the Weighted Arithmetic-Geometric Mean Inequality. - Manuel Eberl (Arch. Formal Proofs, 2022)

The Hales-Jewett Theorem. - Ujkan Sulejmani; Manuel Eberl; Katharina Kreuzer (Arch. Formal Proofs, 2022)

Strategyproofness and Proportionality in Party-Approval Multiwinner Elections. - Théo Delemazure; Tom Demeulemeester; Manuel Eberl; Jonas Israel; Patrick Lederer (AAAI, 2023)

Chebyshev Polynomials. - Manuel Eberl (Arch. Formal Proofs, 2023)

Two theorems about the geometry of the critical points of a complex polynomial. - Manuel Eberl (Arch. Formal Proofs, 2023)

The Cardinality of the Continuum. - Manuel Eberl (Arch. Formal Proofs, 2023)

The Polylogarithm Function. - Manuel Eberl (Arch. Formal Proofs, 2023)

Lambert Series. - Manuel Eberl (Arch. Formal Proofs, 2023)

Perfect Fields. - Manuel Eberl; Katharina Kreuzer (Arch. Formal Proofs, 2023)

Executable Randomized Algorithms. - Emin Karayel; Manuel Eberl (Arch. Formal Proofs, 2023)

Elimination of Repeated Factors Algorithm. - Katharina Kreuzer; Manuel Eberl (Arch. Formal Proofs, 2023)

Formalising Half of a Graduate Textbook on Number Theory (Short Paper). - Manuel Eberl; Anthony Bordg; Lawrence C. Paulson; Wenda Li 001 (ITP, 2024)

Continued Fractions. - Manuel Eberl (Arch. Formal Proofs, 2024)

Kummer's congruence. - Manuel Eberl (Arch. Formal Proofs, 2024)

A simple proof that π is irrational. - Manuel Eberl (Arch. Formal Proofs, 2024)

Concrete bounds for Chebyshev's prime counting functions. - Manuel Eberl (Arch. Formal Proofs, 2024)

The Karatsuba Square Root Algorithm. - Manuel Eberl (Arch. Formal Proofs, 2024)

The Boustrophedon Transform, the Entringer Numbers, and Related Sequences. - Manuel Eberl (Arch. Formal Proofs, 2024)

The Sum-of-Squares Function and Jacobi's Two-Square Theorem. - Manuel Eberl (Arch. Formal Proofs, 2024)

Combinatorial q-Analogues. - Manuel Eberl (Arch. Formal Proofs, 2024)

The Rogers-Ramanujan Identities. - Manuel Eberl (Arch. Formal Proofs, 2024)

Theta Functions. - Manuel Eberl (Arch. Formal Proofs, 2024)

Parallel Shear Sort. - Manuel Eberl; Peter Lammich (Arch. Formal Proofs, 2024)

Formalising Half of a Graduate Textbook on Number Theory (Formal Proof Development). - Manuel Eberl; Anthony Bordg; Lawrence C. Paulson; Wenda Li 001 (Zenodo, 2024)