Asymptotic Reasoning in a Proof Assistant
by Manuel Eberl
PhD thesis at the Technical University of Munich (2021)
Abstract:
This dissertation describes my work in the formalisation of mathematics with the proof assistant Isabelle/HOL, particularly mathematics related to asymptotic concepts such as limits and function growth. This work consists of both the formalisation of fundamental mathematical material for the Isabelle/HOL standard library and the creation of new proof automation tools. Both of these have since been used successfully in many formalisation applications both in pure mathematics (such as analysis and number theory) and computer science (i.e. algorithm analysis).
Specifically, this thesis presents four major contributions, each corresponding to one peer-reviewed publication under the umbrella of ‘asymptotic reasoning in Isabelle/HOL’: The first of these introduces a proof automation tool that employs techniques from computer algebra to compute and prove limits and other asymptotic properties for a large class of real-valued functions (much like systems such as Maple or Mathematica). This tool has been instrumental in all my subsequent formalisation work, and no comparable instrumentation exists in other proof assistants.
Second, a formal proof of a ‘cookbook method’ theorem due to Akra and Bazzi, which is a sweeping generalisation of the well-known Master Theorem of divide-and-conquer recurrences. In computer science, this theorem is a staple of the analysis of divide-and-conquer algorithms. The formalisation also provides tooling to facilitate the application of the theorem to specific algorithms.
Third, a formalisation of the theory of linear recurrences and rational generating functions – in particular how to obtain closed-form solutions and asymptotic estimates of linear recurrences. These have applications in combinatorics and in the analysis of algorithms and data structures. In addition to the theorems, a verified executable solver for linear recurrences and a certifier for their asymptotics are also provided. Finally, in order to demonstrate the usability of the aforementioned library and machinery, the last publication then describes its application to the formalisation of the vast majority of Apostol’s classic textbook on analytic number theory, including the Prime Number Theorem, Dirichlet’s Theorem, and many more results on the distribution of prime numbers and the asymptotic behaviour of number-theoretic functions.
BibTeX:
@phdthesis{eberl21,
author = "Eberl, Manuel",
title = "Asymptotic Reasoning in a Proof Assistant",
type = "Dissertation",
year = 2021,
school = "Technical University of Munich",
url = "http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20210121-1554821-1-2"
}