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 corresponding to one peer-reviewed publication each, 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.     «

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...     »

Diese Dissertation beschreibt meine Arbeit in der Formalisierung von Mathematik mit dem Beweisassistenten Isabelle/HOL, insbesondere von Mathematik im Zusammenhang mit asymptotischen Konzepten wie Grenzwerten und Funktionswachstum. Diese Arbeit beinhaltet sowohl die Formalisierung grundlegenden mathematischen Materials für die Isabelle/HOL-Standardbibliothek als auch die Etablierung neuer Werkzeuge zur Beweisautomatisierung. Beides wurde seitdem erfolgreich in vielen Anwendungen eingesetzt, sowohl Formalisierungen in der reinen Mathematik (wie Analysis und Zahlentheorie) als auch in der Informatik (z. B. Algorithmenanalyse). Konkret besteht diese Arbeit aus vier Teilen im Bereich „asymptotische Beweisführung in Isabelle/HOL“ mit jeweils einer zugehörigen Veröffentlichung: Der erste Teil ist ein Werkzeug zur Beweisautomatisierung, das Techniken aus der Computeralgebra verwendet, um Grenzwerte und andere asymptotische Eigenschaften für eine große Klasse von reellen Funktionen zu berechen und zu beweisen (ähnlich wie Systeme wie Maple oder Mathematica). Der zweite Teil beschreibt den formalen Beweis eines kochrezeptartigen Theorems von Akra und Bazzi, das eine Verallgemeinerung des bekannten Master-Theorems für „divide-and-conquer“-Rekurrenzen darstellt. Dieses Theorem ist ein grundlegender Bestandteil der Analyse von „divide-and-conquer“-Algorithmen in der Informatik. Die Formalisierung beinhaltet außerdem Werkzeuge, die die Anwendung des Theorems auf konkrete Algorithmen angenehmer gestalten. Der dritte Teil ist die Formalisierung der Theorie der linearen Rekurrenzen und rationalen Erzeugendenfunktionen – insbesondere wie geschlossene Lösungen und asymptotische Abschätzungen für sie gewonnen werden können. Diese finden Anwendungen in der Kombinatorik und der Analyse von Algorithmen und Datenstrukturen. Zusätzlich werden ein verifizierter ausführbarer Löser sowie eine Zertifizierer für asymptotische Abschätzungen entwickelt. Als letzter Punkt wird, um die Nutzbarkeit der zuvor dargelegten Bibliothek und Maschinerie zu zeigen, die Formalisierung des Großteils von Apostols Lehrbuch über analytische Zahlentheorie geschildert. Dies beinhaltet formale Beweise für den Primzahlsatz, den Satz von Dirichlet, und viele andere Resultate über die Verteilung der Primzahlen und das asymptotische Verhalten zahlentheoretischer Funktionen.     «

Diese Dissertation beschreibt meine Arbeit in der Formalisierung von Mathematik mit dem Beweisassistenten Isabelle/HOL, insbesondere von Mathematik im Zusammenhang mit asymptotischen Konzepten wie Grenzwerten und Funktionswachstum. Diese Arbeit beinhaltet sowohl die Formalisierung grundlegenden mathematischen Materials für die Isabelle/HOL-Standardbibliothek als auch die Etablierung neuer Werkzeuge zur Beweisautomatisierung. Beides wurde seitdem erfolgreich in vielen Anwendungen eingesetzt, sowo...     »