# 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.
Best,
Angeliki

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"
http://www21.in.tum.de/~wenzelm/papers/romantic.pdf

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


http://isabelle.in.tum.de/dist/library/HOL/HOL-Proofs-Extraction/document.pdf


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.