John Harrison.
Journal of Formalized Reasoning, vol. 2, number 1, pp. 63-83, 2009.
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 is twofold.
First we describe a simple and efficient proof of the theorem informally, which
is 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.
Bibtex entry:
@ARTICLE{harrison-dirichlet,
author = "John Harrison",
title = "A formalized proof of {D}irichlet's theorem on
primes in arithmetic progression",
journal = "Journal of Formalized Reasoning",
volume = 2,
number = 1,
year = 2009,
pages = "63--83"}