首页|Formalization of the Prime Number Theorem with a Remainder Term
Formalization of the Prime Number Theorem with a Remainder Term
扫码查看
点击上方二维码区域，可以放大扫码查看
原文链接
NETL
NSTL
Springer Nature
Abstract This paper describes the formalization of the prime number theorem with a remainder term in the Isabelle/HOL proof assistant. First, we formalized several lemmas in complex analysis that were not available in the library, such as the Borel–Carathéodory theorem and the factorization of an analytic function on a compact region. Then, we use these results to formalize a zero-free region of the Riemann zeta function with an explicitly computed constant and deduce the asymptotic growth order of ζ′(s)/ζ(s)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\zeta '(s) / \zeta (s)$$\end{document} near Re(s)=1\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textrm{Re}(s) = 1$$\end{document}. Finally, using a specific form of Perron’s formula, we prove the prime number theorem with the classical remainder term, expressed in terms of ψ(x)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\psi (x)$$\end{document}. We also formalized the result that the prime number theorem stated using ψ(x)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\psi (x)$$\end{document} can imply the version stated using π(x)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\pi (x)$$\end{document}. Thus, we can achieve the main result of this paper. Our work extensively utilizes the rich libraries of complex analysis and asymptotic analysis in Isabelle/HOL, including concepts such as the winding number, the residue theorem, and proof automation tools such as the tactic. This is why we chose Isabelle to formalize analytic number theory instead of using other interactive provers.
Shuhao Song、Bowen Yao
展开 >
Beijing University of Chemical Technology||Fudan University
NETL
NSTL
Springer Nature
