A formalized proof of Dirichlet's theorem on primes in arithmetic progression

Authors

  • John Harrison Intel Corporation

DOI:

https://doi.org/10.6092/issn.1972-5787/1558

Abstract

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.

Downloads

Published

2010-01-07

How to Cite

Harrison, J. (2010). A formalized proof of Dirichlet’s theorem on primes in arithmetic progression. Journal of Formalized Reasoning, 2(1), 63–83. https://doi.org/10.6092/issn.1972-5787/1558

Issue

Section

Articles