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. 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 (Avigad et al. p. 19).
In 2009, John Harrison employed HOL Light to formalize a proof employing complex analysis. 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 argument.”
Read more about this topic: Prime Number Theorem
Famous quotes containing the word computer:
“The archetype of all humans, their ideal image, is the computer, once it has liberated itself from its creator, man. The computer is the essence of the human being. In the computer, man reaches his completion.”
—Friedrich Dürrenmatt (1921–1990)