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
Abstract:
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.