## 1. selberg-sieve

The aim of this project is to formally verify the fundamental theorem of the Selberg sieve and prove some of its direct consequences. It was ported from this repo.

## 2. Build Instructions

TODO

## 3. Goals

I try to state the most important results and goals in `MainResults.lean`

as I work on them.

We prove the following version of the Fundamental Theorem of the Selberg sieve as adapted from Heath-Brown.

### Fundamental Theorem

Let

Suppose we can write

Then

### Prime counting function

To test this result, we prove that

We hope to later use this result to prove

### Brun's Theorem

Let