素数定理的一个形式化验证证明
人工智能
2007-05-23 v3 计算机科学中的逻辑
符号计算
摘要
素数定理由哈达维和德拉维埃-维尔-普西森独立于 1896 年提出，断言质数的密度在正整数中渐近等于 1 / ln x。而他们的证明严重依赖复分析的方法，而 1948 年 Selberg 和 Erdös 提供了初等证明。我们描述了使用 Isabelle 证明助理获得的 Selberg 证明的形式化验证版本。
引用
@article{arxiv.cs/0509025,
title = {A formally verified proof of the prime number theorem},
author = {Jeremy Avigad and Kevin Donnelly and David Gray and Paul Raff},
journal= {arXiv preprint arXiv:cs/0509025},
year = {2007}
}
备注
23 pages