[FOM] Re: formal verification of the prime number theorem

[Timothy Y. Chow]

"Jeremy Avigad" <avigad at cmu.edu> wrote:
> I am pleased to announce that with the help of Kevin Donnelly, David
> Gray, and Paul Raff, I have verified a proof of the prime number theorem
> using the Isabelle proof assistant.

Congratulations!  A landmark achievement.

Not to deprive you of the enjoyment of basking in your accomplishment for 
a while, but...what next?  How about Khinchin's "Three Pearls of Number 
Theory" in his book by that name?  Or Dirichlet's theorem on primes in 
arithmetic progressions?

Tim