HLK ProofTool
TU Vienna logic.at Theory and Logic Group (E185-2)

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 proof-formalization of Fürstenberg's topological proof. The characteristic clause sets of selected cases are given below. Note that, these are redundancy-free 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:

You need to have all these files together with the concrete instantiation files (which you will find further below) in order to successfully run the HLK compiler on them.

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.