Main result
For every natural number m >= 3, the extraction
formula returns the least prime greater than m.
- Contribution type
- New construction; Lean formalization
- Contribution
- Explicit finite extraction formula for the least prime above
m, with the final correctness theorem verified in Lean. - Mechanism
- factorial congruences, gcd filtering, valuation selection
- Lean theorem
ExtractingFirstPrime.extractedPrime_is_smallest_prime_gt- Lean and mathlib
- Lean 4.30.0-rc2, mathlib v4.30.0-rc2
- Build command
lake build