## Stream: maths

### Topic: prime 617 challenge

#### Kevin Buzzard (Jul 26 2018 at 17:21):

import data.nat.prime

open nat

example : prime 617 := sorry


I tried dec_trivial with local attribute [instance] decidable_prime_1 but it times out on my machine. There is a lemma that says p is prime iff no factors <= sqrt(p) -- can one somehow persuade Lean to use this?

#### Kevin Buzzard (Jul 26 2018 at 17:29):

The reason this is even a thing is that a question on the number theory example sheet that students are working on asks them to use quadratic reciprocity to evaluate whether something is a square mod 617. They managed to solve the question assuming quadratic reciprocity and that 617 was prime :-) The smaller numbers we can handle

#### Rob Lewis (Jul 26 2018 at 17:44):

It looks like decidable_prime already does this: https://github.com/leanprover/mathlib/blob/master/data/nat/prime.lean#L90

#### Rob Lewis (Jul 26 2018 at 17:45):

Why are you trying to use decidable_prime_1?

#### Rob Lewis (Jul 26 2018 at 17:46):

#eval if nat.prime 617 then tt else ff is instant without adding the local instance.

#### Mario Carneiro (Jul 26 2018 at 17:49):

You can also use #eval to_bool (nat.prime 617) for the same purpose

I want a proof!

#### Kevin Buzzard (Jul 26 2018 at 18:02):

import data.nat.prime

open nat

theorem sqrt617 : sqrt 617 = 24 :=
begin
symmetry,
rw eq_sqrt,
split,
exact dec_trivial,
exact dec_trivial
end

theorem prime617iff : prime 617 ↔ ∀ m, 2 ≤ m → m ≤ 24 → ¬ (m ∣ 617) :=
begin
rw prime_def_le_sqrt,
rw sqrt617,
apply and_iff_right,
exact dec_trivial
end

theorem prime617 : prime 617 :=
begin
rw prime617iff,
show ∀ (m : ℕ), 2 ≤ m → m ≤ 24 → ¬m ∣ 617,
exact dec_trivial -- times out :-(
end


Is it possible to work out how close I got?

#### Kevin Buzzard (Jul 26 2018 at 18:09):

Hmm, I think I only make it up to 6 :-/

#### Kevin Buzzard (Jul 26 2018 at 18:15):

Ok I have a strat. I can prove 617 = 154 * 4 + 1 using norm_num and then use some lemmas about division to reduce non-divisibility of 617 by 4 to non-divisibility of 1 by 4, which I can prove with dec_trivial. I then repeat up to 24. I write a python script which generates the code I want.

#### Kevin Buzzard (Jul 26 2018 at 18:27):

import tactic.norm_num
import data.nat.prime

open nat

theorem sqrt617 : sqrt 617 = 24 :=
begin
symmetry,
rw eq_sqrt,
norm_num,
end

theorem prime617iff : prime 617 ↔ ∀ m, 2 ≤ m → m ≤ 24 → ¬ (m ∣ 617) :=
begin
rw prime_def_le_sqrt,
rw sqrt617,
apply and_iff_right,
exact dec_trivial
end

theorem prime617 : prime 617 :=
begin
rw prime617iff,
show ∀ (m : ℕ), 2 ≤ m → m ≤ 24 → ¬m ∣ 617,
intros m hm1 hm2,
cases m,cases hm1,
cases m,cases hm1,cases hm1_a, -- m = 1
cases m,show ¬ (2 ∣ 617), have h : 617 = 1 + 308 * 2 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m,show ¬ (3 ∣ 617), have h : 617 = 2 + 205 * 3 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (4 ∣ 617), have h : 617 = 1 + 154 * 4 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (5 ∣ 617), have h : 617 = 2 + 123 * 5 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (6 ∣ 617), have h : 617 = 5 + 102 * 6 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (7 ∣ 617), have h : 617 = 1 + 88 * 7 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (8 ∣ 617), have h : 617 = 1 + 77 * 8 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (9 ∣ 617), have h : 617 = 5 + 68 * 9 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (10 ∣ 617), have h : 617 = 7 + 61 * 10 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (11 ∣ 617), have h : 617 = 1 + 56 * 11 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (12 ∣ 617), have h : 617 = 5 + 51 * 12 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (13 ∣ 617), have h : 617 = 6 + 47 * 13 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (14 ∣ 617), have h : 617 = 1 + 44 * 14 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (15 ∣ 617), have h : 617 = 2 + 41 * 15 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (16 ∣ 617), have h : 617 = 9 + 38 * 16 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (17 ∣ 617), have h : 617 = 5 + 36 * 17 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (18 ∣ 617), have h : 617 = 5 + 34 * 18 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (19 ∣ 617), have h : 617 = 9 + 32 * 19 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (20 ∣ 617), have h : 617 = 17 + 30 * 20 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (21 ∣ 617), have h : 617 = 8 + 29 * 21 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (22 ∣ 617), have h : 617 = 1 + 28 * 22 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (23 ∣ 617), have h : 617 = 19 + 26 * 23 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
cases m, show ¬ (24 ∣ 617), have h : 617 = 17 + 25 * 24 := by norm_num,rw h,intro h2,
have h3 := mod_eq_zero_of_dvd h2,rw add_mul_mod_self_right at h3,cases h3,
revert hm2,exact dec_trivial,
end


#### Kevin Buzzard (Jul 26 2018 at 18:27):

There's a proper proof.

I'm on it...

#### Kevin Buzzard (Jul 26 2018 at 18:31):

/me thinks that #eval should be renamed #evil

#### Rob Lewis (Jul 26 2018 at 18:41):

Ah, sorry, I shouldn't try to read this while listening to talks.

#### Rob Lewis (Jul 26 2018 at 18:41):

I end up missing obvious things in both places!

#### Mario Carneiro (Jul 28 2018 at 03:52):

Challenge accepted

example : nat.prime 617 := by norm_num


#### Kenny Lau (Jul 28 2018 at 05:27):

import tactic.norm_num data.nat.prime

theorem prime_617 : nat.prime 617 := by norm_num

/-
norm_num failed to simplify
state:
⊢ nat.prime 617
-/


#### Johan Commelin (Jul 28 2018 at 06:33):

A wonderful example of the theorem that examples aren't theorems.

#### Kevin Buzzard (Jul 28 2018 at 07:37):

Maybe you should have tried 57

#### Kevin Buzzard (Jul 28 2018 at 07:38):

Looks like I need to update my blog post :-)

#### Kevin Buzzard (Jul 28 2018 at 07:55):

import tactic.norm_num data.nat.prime

theorem prime_617 : nat.prime 617 := by norm_num

/-
norm_num failed to simplify
state:
⊢ nat.prime 617
-/


Kenny it works for me. Did you update your mathlib? This is code that Mario just wrote.

#### Kevin Buzzard (Jul 28 2018 at 07:57):

And thanks Mario! I think my students were going to have some trouble with the example sheet questions if they couldn't get as far as 617.

Last updated: May 10 2021 at 08:14 UTC