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

Proof of `Every prime other than 2 is odd`

groundedproofs/Lax242665Proofs/OddPrimes.lean · lax-242665

What this proof establishes

no assumptions

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

An even prime is divisible by 22, so 22 is 11 or the prime itself.