While Euclid's classic proof that there are infinitely many primes is
easy to understand intuitively, I found the following proof simpler to
formalize for an automated proof verifier. (Specifically, this proof
avoids the product of a hypothetical finite set of all primes, which I
found cumbersome to work with.)
Here is the proof:
For any natural number n, the smallest divisor (greater than 1) of n!+1
As simple as it is, I was unable to find a published reference for this
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.