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.