Manuel Eberl

Patrick Lederer

Arch. Formal Proofs, 2026

Swap Distance.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2026

Linear orders as rankings.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2026

2025

Dedekind Sums.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

Complex Lattices, Elliptic Functions, and the Modular Group.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

The Partition Function and the Pentagonal Number Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

Path Equivalence and Automation for Integration Contours.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

Verifying an Efficient Algorithm for Computing Bernoulli Numbers.

[BibT_eX]

[DOI]

Peter Lammich

Proceedings of the 16th International Conference on Interactive Theorem Proving, 2025

2024

Formalising Half of a Graduate Textbook on Number Theory (Formal Proof Development).

[BibT_eX]

[DOI]

Dataset, June, 2024

Parallel Shear Sort.

[BibT_eX]

[DOI]

Peter Lammich

Arch. Formal Proofs, 2024

Theta Functions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

The Rogers-Ramanujan Identities.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

Combinatorial q-Analogues.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

The Sum-of-Squares Function and Jacobi's Two-Square Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

The Boustrophedon Transform, the Entringer Numbers, and Related Sequences.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

The Karatsuba Square Root Algorithm.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

Concrete bounds for Chebyshev's prime counting functions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

A simple proof that π is irrational.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

Kummer's congruence.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

Continued Fractions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

Formalising Half of a Graduate Textbook on Number Theory (Short Paper).

[BibT_eX]

[DOI]

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2023

Elimination of Repeated Factors Algorithm.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2023

Executable Randomized Algorithms.

[BibT_eX]

[DOI]

Emin Karayel

Arch. Formal Proofs, 2023

Perfect Fields.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2023

Lambert Series.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2023

The Polylogarithm Function.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2023

The Cardinality of the Continuum.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2023

Two theorems about the geometry of the critical points of a complex polynomial.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2023

Chebyshev Polynomials.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2023

Strategyproofness and Proportionality in Party-Approval Multiwinner Elections.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence, 2023

2022

The Hales-Jewett Theorem.

[BibT_eX]

[DOI]

Ujkan Sulejmani

Arch. Formal Proofs, 2022

Pólya's Proof of the Weighted Arithmetic-Geometric Mean Inequality.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2022

The Sophomore's Dream.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2022

A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2022

The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2022

2021

Asymptotic Reasoning in a Proof Assistant (Asymptotische Beweisführung in einem Beweisassistenten)

[BibT_eX]

[DOI]

PhD thesis, 2021

Finitely Generated Abelian Groups.

[BibT_eX]

[DOI]

Joseph Thommes

Arch. Formal Proofs, 2021

Van der Waerden's Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Factorization of Polynomials with Algebraic Coefficients.

[BibT_eX]

[DOI]

René Thiemann

Arch. Formal Proofs, 2021

The Hermite-Lindemann-Weierstraß Transcendence Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Formal Puiseux Series.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

The Laws of Large Numbers.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

2020

Skip Lists.

[BibT_eX]

[DOI]

Max W. Haslbeck

Arch. Formal Proofs, 2020

Power Sum Polynomials.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

The Lambert W Function on the Reals.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

Gaussian Integers.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

Furstenberg's topology and his proof of the infinitude of primes.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

Mersenne primes and the Lucas-Lehmer test.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

Verified Textbook Algorithms - A Biased Survey.

[BibT_eX]

[DOI]

Maximilian P. L. Haslbeck

Proceedings of the Automated Technology for Verification and Analysis, 2020

2019

Probabilistic Primality Testing.

[BibT_eX]

[DOI]

Daniel Stüwe

Arch. Formal Proofs, 2019

Gauss Sums and the Pólya-Vinogradov Inequality.

[BibT_eX]

[DOI]

Rodrigo Raya

Arch. Formal Proofs, 2019

The Irrationality of ζ(3).

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2019

Selected Problems from the International Mathematical Olympiad 2019.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2019

Elementary Facts About the Distribution of Primes.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2019

The Inversions of a List.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2019

Nine Chapters of Analytic Number Theory in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Verified Real Asymptotics in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, 2019

Verifying Randomised Social Choice.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

Verified solving and asymptotics of linear recurrences.

[BibT_eX]

[DOI]

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving.

[BibT_eX]

[DOI]

J. ACM, 2018

Treaps.

[BibT_eX]

[DOI]

Max W. Haslbeck

Arch. Formal Proofs, 2018

The Prime Number Theorem.

[BibT_eX]

[DOI]

Lawrence C. Paulson

Arch. Formal Proofs, 2018

Randomised Binary Search Trees.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

The Transcendence of π.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

Symmetric Polynomials.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

Pell's Equation.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

The Error Function.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

Verified Analysis of Random Binary Tree Structures.

[BibT_eX]

[DOI]

Max W. Haslbeck

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

Proving Divide and Conquer Complexities in Isabelle/HOL.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

Monad normalisation.

[BibT_eX]

[DOI]

Joshua Schneider

Andreas Lochbihler

Arch. Formal Proofs, 2017

Dirichlet L-Functions and Dirichlet's Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

The Median-of-Medians Selection Algorithm.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

The Mason-Stother's Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Linear Recurrences.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

The Hurwitz and Riemann ζ Functions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Dirichlet Series.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Minkowski's Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Buffon's Needle Problem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Expected Shape of Random Binary Search Trees.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

The number of comparisons in QuickSort.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Lower bound on comparison-based sorting algorithms.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

The Euler-MacLaurin Formula.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

The Transcendence of e.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Bernoulli Numbers.

[BibT_eX]

[DOI]

Lukas Bulwahn

Arch. Formal Proofs, 2017

Bertrand's postulate.

[BibT_eX]

[DOI]

Julian Biendarra

Arch. Formal Proofs, 2017

2016

Fisher-Yates shuffle.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Stirling's formula.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Catalan Numbers.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Randomised Social Choice Theory.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

The Incompatibility of SD-Efficiency and SD-Strategy-Proofness.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

2015

Liouville numbers.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

Basic Geometric Properties of Triangles.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

The Divergence of the Prime Harmonic Series.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

Descartes' Rule of Signs.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

Landau Symbols.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

The Akra-Bazzi theorem and the Master theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

A Verified Compiler for Probability Density Functions.

[BibT_eX]

[DOI]

Johannes Hölzl

Proceedings of the Programming Languages and Systems, 2015

A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014

Sturm's Theorem.

[BibT_eX]

[DOI]