Re: [isabelle] enumerating primes?
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
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 archive was generated by a fusion of
Pipermail (Mailman edition) and