Re: [isabelle] enumerating primes?

Dear Stefan,

many thanks for the papers!

In fact my intention is to formalise a different proof, my motivation is that the proof I am considering also provides some computational content- in particular it gives that assuming we have r many primes,
we can always construct some  prime P >p_r and we moreover have that
P \leq 4^r +1.

Thanks again for the papers though, it is very interesting material indeed.

On 2018-05-08 16:54, Stefan Berghofer wrote:

a (constructive) proof of the existence of infinitely many primes can
e.g. be found in the paper

  "A comparison of the mathematical proof languages Mizar and Isar"

by Markus Wenzel and Freek Wiedijk. You can find a formalization of
this proof in section 7 of the

together with an explanation of how a program can be extracted from this proof.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.