A formalized proof of Dirichlet's theorem on primes in arithmetic progression
DOI:
https://doi.org/10.6092/issn.1972-5787/1558Abstract
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. (2009). 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
License
Copyright (c) 2009 John Harrison
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy