# Zulip Chat Archive

## Stream: new members

### Topic: ith prime

#### Lucas Allen (Dec 30 2020 at 06:51):

Hello, I'd like to define the notion of the "ith prime," So far I have

```
import data.nat.prime
open nat
def primes_greater_than_n (n : ℕ) : set ℕ := {p : ℕ | n < p ∧ prime p}
def prime.ith : ℕ → ℕ
| 0 := 1
| (i+1) := set.min (primes_greater_than_n (prime.ith i)) --min isn't right, want the smallest element of a set of ℕ
```

However `min`

isn't what I'm looking for, I need a function that returns the minimum element in a set of `ℕ`

, is there something like this in mathlib? Also, is this a good way to formalize "ith prime"? At the moment I'm content with a definition which only works in proofs, but I think it'd be cool if it could be used to compute the ith prime as well. Thanks.

#### Kenny Lau (Dec 30 2020 at 06:56):

`nat.find`

#### Alex J. Best (Dec 30 2020 at 06:57):

```
import data.nat.prime
open nat
def ith_prime : ℕ → ℕ
| 0 := 2
| (i + 1) := nat.find (exists_infinite_primes $ ith_prime i + 1)
#eval ith_prime 4
```

#### Lucas Allen (Dec 30 2020 at 07:13):

Cool Thanks.

#### Lucas Allen (Dec 30 2020 at 07:15):

Oh you can compute the primes as well. :)

#### Kevin Buzzard (Dec 30 2020 at 08:11):

Lean's kernel isn't checking those computations though. How will this work in Lean 4 by the way?

#### Mario Carneiro (Dec 30 2020 at 08:22):

what do you mean?

#### Mario Carneiro (Dec 30 2020 at 08:22):

I don't think it will be significantly different in lean 4

#### Mario Carneiro (Dec 30 2020 at 08:23):

I think there might be a `vm_compute`

kind of construct in lean 4 if you feel like trusting `#eval`

to be a proof

#### Kevin Buzzard (Dec 30 2020 at 08:26):

I mean "now you're supposed to compile it, will there will be be a VM?"

#### Kevin Buzzard (Dec 30 2020 at 08:28):

Will #eval exist? Not that I ever use it...

#### Bryan Gin-ge Chen (Dec 30 2020 at 08:42):

So this is another example where `#eval`

can show something but `dec_trivial`

can't prove it:

```
import data.nat.prime
open nat
def ith_prime : ℕ → ℕ
| 0 := 2
| (i + 1) := nat.find (exists_infinite_primes $ ith_prime i + 1)
#eval ith_prime 4
example : ith_prime 4 = 11 := dec_trivial -- nope
```

I'm still surprised by this not working, but maybe I should know better.

Let me check my understanding. Mario suggested using `whnf`

to try to figure out what gets stuck in a previous thread:

```
set_option pp.proofs true
run_cmd tactic.whnf `(by simp [ith_prime]; apply_instance : decidable (ith_prime 4 = 11)) >>= tactic.trace
/- something nasty starting with
nat.decidable_eq
(nat.find
(eq.rec (ith_prime._main._proof_1 3)
(funext
(λ (n : ℕ), ...
-/
```

Is the issue here similar to the one in that thread, where using well-founded recursion leads to something that doesn't reduce? Is there any reasonable way to define `ith_prime`

so that it plays well with `dec_trivial`

?

#### Kevin Buzzard (Dec 30 2020 at 08:48):

Who cares what the primes actually are? The only theorem you need about them is that there's at least two of them (or occasionally that there are infinitely many)

#### Mario Carneiro (Dec 30 2020 at 08:49):

I think lean 4 still has `#eval`

. It will automatically use the VM for functions in the same file and compiled code for functions defined in other files

#### Mario Carneiro (Dec 30 2020 at 08:50):

The `vm_compute`

thing will be more interesting to you, I think, because it basically replaces `dec_trivial`

with "proof by `#eval`

"

#### Mario Carneiro (Dec 30 2020 at 08:56):

```
import data.nat.prime
open nat
def find_prime : ℕ → ℕ → ℕ
| 0 n := 0
| (i+1) n :=
by haveI := decidable_prime_1 n; exact
if prime n then n else find_prime i (n+1)
def ith_prime : ℕ → ℕ
| 0 := 2
| (i + 1) := let n := ith_prime i in find_prime n (n+1)
example : ith_prime 4 = 11 := dec_trivial
```

You need bertrand's postulate to prove the correctness of this function though

#### Mario Carneiro (Dec 30 2020 at 08:58):

but you can prove without much difficulty that it is correct if it returns a nonzero number

#### Kevin Buzzard (Dec 30 2020 at 09:57):

Wasn't there a partially finished version of Bertrand's postulate in a branch somewhere? I could see if I could drum up some interest on the discord?

#### Johan Commelin (Dec 30 2020 at 09:58):

I think Patrick Stevens was working on this

#### Johan Commelin (Dec 30 2020 at 09:58):

There are some PRs even

#### Mario Carneiro (Dec 30 2020 at 10:10):

incidentally, bertrand's postulate is also in the strike zone for the set.mm import: it only talks about nat and prime and it's been proven in metamath already. So I guess we've got it already via the set.mm -> lean bridge

#### Kevin Buzzard (Dec 30 2020 at 12:33):

Oleans or it didn't happen

#### Kevin Buzzard (Dec 30 2020 at 12:33):

Any version of lean/mathlib fine

#### Kevin Buzzard (Dec 30 2020 at 12:34):

Any community master version

#### Kevin Buzzard (Dec 30 2020 at 12:35):

Get a tick on the leaderboard/graveyard!

Last updated: May 11 2021 at 22:14 UTC