2024
Arch. Formal Proofs, 2024
The Boustrophedon Transform, the Entringer Numbers, and Related Sequences.
Arch. Formal Proofs, 2024
The Karatsuba Square Root Algorithm.
Arch. Formal Proofs, 2024
Concrete bounds for Chebyshev's prime counting functions.
Arch. Formal Proofs, 2024
A simple proof that π is irrational.
Arch. Formal Proofs, 2024
Arch. Formal Proofs, 2024
Arch. Formal Proofs, 2024
Formalising Half of a Graduate Textbook on Number Theory (Short Paper).
Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024
2023
Elimination of Repeated Factors Algorithm.
Arch. Formal Proofs, 2023
Executable Randomized Algorithms.
Arch. Formal Proofs, 2023
Arch. Formal Proofs, 2023
Arch. Formal Proofs, 2023
The Polylogarithm Function.
Arch. Formal Proofs, 2023
The Cardinality of the Continuum.
Arch. Formal Proofs, 2023
Two theorems about the geometry of the critical points of a complex polynomial.
Arch. Formal Proofs, 2023
Arch. Formal Proofs, 2023
Strategyproofness and Proportionality in Party-Approval Multiwinner Elections.
Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence, 2023
2022
The Hales-Jewett Theorem.
Arch. Formal Proofs, 2022
Pólya's Proof of the Weighted Arithmetic-Geometric Mean Inequality.
Arch. Formal Proofs, 2022
Arch. Formal Proofs, 2022
A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent.
Arch. Formal Proofs, 2022
The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections.
Arch. Formal Proofs, 2022
2021
Asymptotic Reasoning in a Proof Assistant (Asymptotische Beweisführung in einem Beweisassistenten)
PhD thesis, 2021
Finitely Generated Abelian Groups.
Arch. Formal Proofs, 2021
Van der Waerden's Theorem.
Arch. Formal Proofs, 2021
Factorization of Polynomials with Algebraic Coefficients.
Arch. Formal Proofs, 2021
The Hermite-Lindemann-Weierstraß Transcendence Theorem.
Arch. Formal Proofs, 2021
Arch. Formal Proofs, 2021
The Laws of Large Numbers.
Arch. Formal Proofs, 2021
2020
Verified Analysis of Random Binary Tree Structures.
J. Autom. Reason., 2020
Arch. Formal Proofs, 2020
Arch. Formal Proofs, 2020
The Lambert W Function on the Reals.
Arch. Formal Proofs, 2020
Arch. Formal Proofs, 2020
Furstenberg's topology and his proof of the infinitude of primes.
Arch. Formal Proofs, 2020
Mersenne primes and the Lucas-Lehmer test.
Arch. Formal Proofs, 2020
Verified Textbook Algorithms - A Biased Survey.
Proceedings of the Automated Technology for Verification and Analysis, 2020
2019
Probabilistic Primality Testing.
Arch. Formal Proofs, 2019
Gauss Sums and the Pólya-Vinogradov Inequality.
Arch. Formal Proofs, 2019
The Irrationality of ζ(3).
Arch. Formal Proofs, 2019
Selected Problems from the International Mathematical Olympiad 2019.
Arch. Formal Proofs, 2019
Elementary Facts About the Distribution of Primes.
Arch. Formal Proofs, 2019
The Inversions of a List.
Arch. Formal Proofs, 2019
Nine Chapters of Analytic Number Theory in Isabelle/HOL.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019
Verified Real Asymptotics in Isabelle/HOL.
Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, 2019
Verifying Randomised Social Choice.
Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019
Verified solving and asymptotics of linear recurrences.
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.
J. ACM, 2018
Arch. Formal Proofs, 2018
The Prime Number Theorem.
Arch. Formal Proofs, 2018
Randomised Binary Search Trees.
Arch. Formal Proofs, 2018
Arch. Formal Proofs, 2018
Arch. Formal Proofs, 2018
Arch. Formal Proofs, 2018
Arch. Formal Proofs, 2018
The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency.
Arch. Formal Proofs, 2018
2017
Proving Divide and Conquer Complexities in Isabelle/HOL.
J. Autom. Reason., 2017
Arch. Formal Proofs, 2017
Dirichlet L-Functions and Dirichlet's Theorem.
Arch. Formal Proofs, 2017
The Median-of-Medians Selection Algorithm.
Arch. Formal Proofs, 2017
The Mason-Stother's Theorem.
Arch. Formal Proofs, 2017
Arch. Formal Proofs, 2017
The Hurwitz and Riemann ζ Functions.
Arch. Formal Proofs, 2017
Arch. Formal Proofs, 2017
Arch. Formal Proofs, 2017
Arch. Formal Proofs, 2017
Expected Shape of Random Binary Search Trees.
Arch. Formal Proofs, 2017
The number of comparisons in QuickSort.
Arch. Formal Proofs, 2017
Lower bound on comparison-based sorting algorithms.
Arch. Formal Proofs, 2017
The Euler-MacLaurin Formula.
Arch. Formal Proofs, 2017
Arch. Formal Proofs, 2017
Arch. Formal Proofs, 2017
Arch. Formal Proofs, 2017
2016
Arch. Formal Proofs, 2016
Arch. Formal Proofs, 2016
Arch. Formal Proofs, 2016
Randomised Social Choice Theory.
Arch. Formal Proofs, 2016
The Incompatibility of SD-Efficiency and SD-Strategy-Proofness.
Arch. Formal Proofs, 2016
2015
Arch. Formal Proofs, 2015
Basic Geometric Properties of Triangles.
Arch. Formal Proofs, 2015
The Divergence of the Prime Harmonic Series.
Arch. Formal Proofs, 2015
Descartes' Rule of Signs.
Arch. Formal Proofs, 2015
Arch. Formal Proofs, 2015
The Akra-Bazzi theorem and the Master theorem.
Arch. Formal Proofs, 2015
A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015
2014
A Verified Compiler for Probability Density Functions.
Arch. Formal Proofs, 2014
Arch. Formal Proofs, 2014
