首页    期刊浏览 2024年11月07日 星期四
登录注册

文章基本信息

  • 标题:A formalized proof of Dirichlet's theorem on primes in arithmetic progression
  • 本地全文:下载
  • 作者:John Harrison
  • 期刊名称:Journal of Formalized Reasoning
  • 印刷版ISSN:1972-5787
  • 出版年度:2009
  • 卷号:2
  • 期号:1
  • 页码:63-83
  • DOI:10.6092/issn.1972-5787/1558
  • 语种:English
  • 出版社:Alma Mater Studiorum - University of Bologna
  • 摘要:We describe the formalization using the HOL Light theorem prover of Dirichlet's theorem on primes in arithmetic progression. The proof turned out to be more straightforward than expected, but this depended on a careful choice of an informal proof to use as a starting-point. The goal of this paper iis twofold. First we describe a simple and efficient proof of the theorem informally, which iis otherwise difficult to find in one self-contained place at an elementary level. We also describe its, largely routine, HOL Light formalization, a task that took only a few days.
国家哲学社会科学文献中心版权所有