The Prime Proof
On this page you can find supplementing material to our paper: "CERES: An analysis of Fürstenberg's proof of the infinity of primes".
In this paper we use the system CERES to analyze Fürstenberg's topological proof of the infinity of primes. Showing that Euclid's original proof can be obtained as one of the analytic arguments from Fürstenberg's proof.
This analysis is based on the characteristic clause sets of the schematic proofformalization of Fürstenberg's topological proof. The characteristic clause sets of selected cases are given below. Note that, these are redundancyfree in terms of tautology elimination and subsumption.
One aspect in which the application of CERES on this example differs from the other examples is in the method of refutation of the characteristic clause sets. We have failed, after a systematic application of the theorem provers Prover9 and Otter, to produce a refutation in a fully automatic manner. Therefore, we have refuted the sets using our interactive resolution theorem prover ATP. A technical report describing the refutation of the set for the three primes proof can be found here.
The formalization of Fürstenberg's proof is divided into the following parts:
 defs.hlk  basic definitions and axioms,
 c_union.hlk  proves that the union of two closed sets is again closed,
 inf_proof.hlk  proves that all open nonempty sets are infinite,
 prog_closed.hlk  proves that progressions are closed,
 main.hlk  schematic version of Fürstenberg's topological proof.
Note that, due to their sizes, some of the following files are compressed (gziped). We recommend you leave them compressed since uncompressing would yield files of tremendous sizes (more then 1 GB in some cases). Besides the system CERES and all our tools are also capable of working with gziped files directly.
These are some exemplary cases assuming only k + 1 primes exist.

instance of the above proof scheme assuming only one prime exists (k = 0):
$ hlk ceres o prime0.xml prime0.hlk theproof
$ ceres sk cs prime0.xml theproof prime0ce.xml
Supplemental files: prime0ce.pdf (characteristic clause set and axioms)

instance of the above proof scheme assuming only two primes exist (k = 1):
$ hlk ceres o prime1.xml prime1.hlk theproof
$ ceres sk cs prime1.xml theproof prime1ce.xml
Supplemental files: prime1ce.pdf (characteristic clause set and axioms)

instance of the above proof scheme assuming only three primes exist (k = 2):
$ hlk ceres o prime2.xml prime2.hlk theproof
$ ceres sk cs prime2.xml theproof prime2ce.xml
Supplemental files: prime2ce.pdf (characteristic clause set and axioms)

instance of the above proof scheme assuming only four primes exist (k = 3):
$ hlk ceres o prime3.xml prime3.hlk theproof
$ ceres sk cs prime3.xml theproof prime3ce.xml
Supplemental files: prime3ce.pdf (characteristic clause set and axioms)

instance of the above proof scheme assuming only thirteen primes exist (k = 12):
$ hlk ceres o prime12.xml prime12.hlk theproof
$ ceres sk cs prime12.xml theproof prime12ce.xml
Supplemental files: prime12ce.pdf (characteristic clause set and axioms)