Editing Prime number theorem (section)

== Computer verifications ==
In 2005, Avigad ''et al.'' employed the [[Isabelle theorem prover]] to devise a computer-verified variant of the Erdős–Selberg proof of the PNT.<ref name=Avigad>{{cite journal|first1=Jeremy | last1=Avigad |first2=Kevin |last2=Donnelly |first3=David | last3=Gray |first4=Paul | last4=Raff | title=A formally verified proof of the prime number theorem|year=2008 | mr=2371488 | journal=[[ACM Transactions on Computational Logic]] | volume=9 | issue=1 | pages=2 | doi=10.1145/1297658.1297660 | arxiv=cs/0509025| s2cid=7720253 }}</ref> This was the first machine-verified proof of the PNT. Avigad chose to formalize the Erdős–Selberg proof rather than an analytic one because while Isabelle's library at the time could implement the notions of limit, derivative, and [[transcendental function]], it had almost no theory of integration to speak of.<ref name=Avigad/>{{rp|19}}

In 2009, [[John Harrison (mathematician)|John Harrison]] employed [[HOL Light]] to formalize a proof employing [[complex analysis]].<ref>
{{cite journal
 |title=Formalizing an analytic proof of the Prime Number Theorem
 |last=Harrison
 |first=John
 |url=http://www.cl.cam.ac.uk/~jrh13/papers/mikefest.html
 |journal=[[Journal of Automated Reasoning]]
 |mr=2544285
 |year = 2009 |volume = 43 |pages = 243–261 | issue=3
 |doi=10.1007/s10817-009-9145-6|citeseerx=10.1.1.646.9725
 |s2cid=8032103
}}</ref> By developing the necessary analytic machinery, including the [[Cauchy integral formula]], Harrison was able to formalize "a direct, modern and elegant proof instead of the more involved 'elementary' Erdős–Selberg<!-- Erdös not Erdős in quote, but Wikipedia editorially corrects it --> argument".