John Harrison.
Dedicated to Mike Gordon on the occasion of his 60th birthday.
Journal of Automated Reasoning, vol. 43, pp. 243-261, 2009.
Abstract:
We describe the computer formalization of a complex-analytic proof of the Prime
Number Theorem (PNT), a classic result from number theory characterizing the
asymptotic density of the primes. The formalization, conducted using the HOL
Light theorem prover, proceeds from the most basic axioms for mathematics yet
builds from that foundation to develop the necessary analytic machinery
including Cauchy's integral formula, so that we are able to formalize a direct,
modern and elegant proof instead of the more involved `elementary'
Erdös-Selberg argument. As well as setting the work in context and
describing the highlights of the formalization, we analyze the relationship
between the formal proof and its informal counterpart and so attempt to derive
some general lessons about the formalization of mathematics.
Bibtex entry:
@ARTICLE{harrison-pnt,
author = "John Harrison",
title = "Formalizing an analytic proof of the {P}rime
{N}umber {T}heorem (Dedicated to {M}ike {G}ordon on
the occasion of his 60th birthday)",
journal = "Journal of Automated Reasoning",
year = 2009,
volume = 43,
pages = "243--261"}