Formalizing an analytic proof of the Prime Number Theorem (extended abstract)

John Harrison.

Extended abstract of talk presented at the TTVSI Festschrift in honour of Mike Gordon's 60th birthday, 26th March 2008 at the Royal Society, London.
This is superseded by the corresponding full paper


We describe the formalization, using the HOL Light theorem prover, of an analytic proof of the Prime Number Theorem, from Newman's `Analytic Number Theory' textbook. In this short presentation we give few details; a full paper will appear in a special issue of the Journal of Automated Reasoning. But we consider in general terms the role of `machinery' in formalizing non-trivial mathematics, and give some statistics on the length of parts of the proof relative to the informal text.

DVI, PostScript or PDF