# Zulip Chat Archive

## Stream: general

### Topic: Decidable nat.prime

#### Patrick Johnson (Jan 26 2022 at 19:33):

I implemented a decidable instance for `nat.prime`

. Do we already have such instance that I'm not aware of? If not, should I open a PR?

#### Patrick Johnson (Jan 26 2022 at 19:38):

By decidable, I mean solvable using `dec_trivial`

, like this:

```
example : nat.prime 7 ∧ ¬nat.prime 8 := dec_trivial
```

#### Johan Commelin (Jan 26 2022 at 19:41):

I'm pretty sure it's there already. There's also a `norm_num`

extension for proving primality

#### Eric Rodriguez (Jan 26 2022 at 19:41):

there's actually two: docs#nat.decidable_prime and docs#nat.decidable_prime1

#### Mario Carneiro (Jan 26 2022 at 19:52):

The reason why `decidable_prime_1`

is not the default instance (and similar for other decidability instances like it) is because it is slower to perform computations like this than `norm_num`

style proofs. You will very quickly run into the problem that direct computation on `nat`

using this method works on unary numerals and so inevitably hits a wall at not-very-large numbers. `decidable_prime`

is a more useful instance because it computes in `#eval`

quickly (and in fact it is used in `norm_num`

internally)

#### Mario Carneiro (Jan 26 2022 at 19:53):

If you really want to do computation in the kernel you should use docs#num instead of `nat`

#### Mario Carneiro (Jan 26 2022 at 19:53):

There is in fact an instance for primality over num as well: docs#num.decidable_prime

#### Patrick Johnson (Jan 26 2022 at 19:58):

Oh, I didn't look at the docs for `nat.prime`

:face_palm:. I just tried `dec_trivial`

and since it failed, I thought we don't even have a decidability instance, so I wrote one. But it was a fun excercise anyway. My instance timeouts for numbers >100, so it's pretty much useless.

#### Patrick Johnson (Jan 26 2022 at 19:59):

TIL that `norm_num`

can also prove primality. That's interesting.

#### Kevin Buzzard (Jan 26 2022 at 22:54):

Here's how it happened: https://xenaproject.wordpress.com/2018/07/26/617-is-prime/

Last updated: Dec 20 2023 at 11:08 UTC