Zulip Chat Archive

Stream: maths

Topic: prime 617 challenge


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rob Lewis (Jul 26 2018 at 17:45):

Why are you trying to use decidable_prime_1?

view this post on Zulip Rob Lewis (Jul 26 2018 at 17:46):

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

view this post on Zulip Mario Carneiro (Jul 26 2018 at 17:49):

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

view this post on Zulip Kevin Buzzard (Jul 26 2018 at 18:02):

I want a proof!

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jul 26 2018 at 18:09):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 26 2018 at 18:27):

There's a proper proof.

view this post on Zulip Mario Carneiro (Jul 26 2018 at 18:27):

I'm on it...

view this post on Zulip Kevin Buzzard (Jul 26 2018 at 18:31):

/me thinks that #eval should be renamed #evil

view this post on Zulip Rob Lewis (Jul 26 2018 at 18:41):

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

view this post on Zulip Rob Lewis (Jul 26 2018 at 18:41):

I end up missing obvious things in both places!

view this post on Zulip Mario Carneiro (Jul 28 2018 at 03:52):

Challenge accepted

example : nat.prime 617 := by norm_num

view this post on Zulip 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
-/

view this post on Zulip Johan Commelin (Jul 28 2018 at 06:33):

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

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 07:37):

Maybe you should have tried 57

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 07:38):

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

view this post on Zulip 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.

view this post on Zulip 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