Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `There are infinitely many primes`

groundedproofs/Lax242665Proofs/InfinitelyManyPrimes.lean · lax-242665

What this proof establishes

no assumptions

thm✓Lax242665.InfinitelyManyPrimes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

  • page 2 of this submission's paper

Description

Euclid's argument: the smallest prime factor pp of n!+1n! + 1 cannot be at most nn, because then pp would divide n!n! and hence divide 11.