617 is prime

More number theory today. Clara List and Sangwoo Jo were trying to do a question from the third year number theory example sheet; to work out whether 605 was a square modulo 617. They decided to assume the law of quadratic reciprocity (which we hopefully will have formalised by the end of the summer) and to go on from there. But the next problem is to prove that 617 is prime, so the law can be applied! People who know about the Jacobi symbol might think that this problem can be avoided, but the problem with using the Jacobi symbol is that if it evaluates to +1 then this does not guarantee that the top is a square modulo the bottom.

Now Lean was not designed to do calculations, and whilst it knows that primality is decidable it does not have an efficient algorithm to actually do the deciding (or at least, it did not seem to at the time of writing). In particular, the code

import data.nat.prime

open nat

example : prime 617 := dec_trivial

fails! It should compile in theory, but it times out in practice. Lean was not designed to do computations. Lean was designed to do things like verify the proof that there are infinitely many primes (which involves theoretically multiplying lots of primes together and adding one, without ever actually calculating the product).

I was sufficiently interested in this to dig further. Lean’s maths library does have the theorem that an integer is prime iff it has no factors with , and it can deduce with little trouble that to prove that 617 is prime, it suffices to show that it has no divisors with . However, proving, for example, that 3 does not divide 617, is a lot of work for Lean’s default algorithm, which I assume is doing something like subtracting 3 from 617 hundreds of times and storing the result in ever more complex proof terms or some such thing. The problem is that the natural number 617 is stored internally as succ (succ (succ (succ ... (succ zero))))))) ... ), which is very unwieldy to work with in practice. What to do?

Remember that the thing Lean is good at is theorems. For example it knows the following theorem:

add_mul_mod_self_right : ∀ (x y z : ℕ), (x + y * z) % z = x % z

[here % denotes the “remainder after division” operator] so if it somehow knew that 617 = 2 + 205 * 3 then it would be able to use this theorem to prove that 617 had remainder 2 when divided by 3, and checking non-divisibility by all positive integers in this way we can deduce that 617 is prime.

Now checking that 617 = 2 + 205 * 3 is something Lean can manage! It has a powerful norm_num tactic which works with numbers using a sensible binary format and where it can do calculations efficiently; it can then translate its arguments into a formal proof that the calculations are correct. So all we need to do now is to figure out how to write 617 as r + q * m for .

To do this I just wrote some python code whose output was the Lean code I wanted.

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
-- the rest of this code was written by python!
  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 

Now maybe the python code I wrote to generate that Lean code has bugs! Maybe if I change 617 to some other prime it wouldn’t work for some silly reason. But who cares! The Lean code that my python code generated compiled fine, in well under a second, and now we have a proof that 617 is prime.

This is exactly what tactics are. Lean tactics are on the whole written in Lean’s metaprogramming language, and are not checked by the kernel. Tactics might have bugs — they might not always do what it says they will do. However this does not affect our proofs. If my python code had failed to produce valid equations then the Lean code would simply not have compiled, and we would have learnt nothing. But my python code did work, and then the Lean code compiled and then it didn’t matter whether the python code was buggy or not. Similarly tactics can fail — either because the user applies them in a situation where they are not designed to succeed, or because the programmer made some error. However they can never prove something false, because after the tactic produces the code, the kernel checks it, and if the kernel says the code proves the theorem, then who cares where it came from.

This algorithm can manifestly be generalised and one might imagine writing such a tactic in Lean, using unsafe calculations to do the division and remainder, and then checking them in the kernel.

***

Note added 2 days later: Mario beefed up the norm_num tactic and now theorem prime_617 : nat.prime 617 := by norm_num works out of the box! Life is great!

Advertisement