# Extracting the First Prime Greater than m

Lean formalization for the note `Extracting the First Prime Greater than m`.

The main theorem is `ExtractingFirstPrime.extractedPrime_is_smallest_prime_gt`, which verifies that the formula in the note returns the least prime greater than `m` for every natural number `m >= 3`.

Run the check with:

```sh
lake build
```