Master’s practical course, Master’s thesis, or IDP
There is an ongoing effort to formalise Tom Apostol’s classic textbook on Analytic Number Theory. Most of the core content has already been formalised, but there are some chapters that have been left out completely, e.g. Number Partitions.
The goal of the practical course work would be to formalise as much as possible of this material.
Prerequisites:
The book is written in a very accessible style and the above-mentioned chapters should not require any mathematical knowledge beyond normal undergraduate-level algebra and analysis. Experience with formalisation in Isabelle/HOL is, of course, mandatory.
Advisor:
Manuel Eberl, email {eberlm} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]