The law of quadratic reciprocity. The jewel in the crown of mathematics! Still not proved in Lean! [edit March 2019; QR is now in Lean, thanks to Chris Hughes, but let’s not let that spoil the story.]

Clara List and Sangwoo Jo were thinking about this today. They formalised the statement. There are two “supplements” to the law, describing when and are squares mod . For the case they used the dreaded version

which they obtained from a reliable source. Who even came up with that way of expressing what’s going on? Does it *ever* help? What’s wrong with just writing that it’s if or 7 mod 8, and otherwise? When I’ve lectured the basic number theory course at Imperial, it’s this latter statement that comes out in the wash.

So the `ring`

tactic came to the rescue:

```
import tactic.ring
lemma quad_res_two_case_three (n : ℕ) : n % 8 = 3 → (n ^ 2 - 1) / 8 % 2 = 1 :=
begin
intro H,
have H2 := nat.mod_add_div n 8,
rw H at H2,
rw ←H2,
suffices : ∀ t : ℕ, ((3 + 8 * t) ^ 2 - 1) / 8 % 2 = 1,
exact this (n/8),
intro t,
have H3 : (1 + 2 * (4*t^2 + 3*t)) % 2 = 1,
rw nat.add_mul_mod_self_left,exact dec_trivial,
suffices : ((3 + 8 * t) ^ 2 - 1) / 8 = (1 + 2 * (4 * t ^ 2 + 3 * t)),
rwa this,
suffices : ((3 + 8 * t) ^ 2 - 1) = 8 * (1 + 2 * (4 * t ^ 2 + 3 * t)),
rw this,
rw nat.mul_div_cancel_left _ (show 8 > 0, from dec_trivial),
ring
end
```

I had to write three more of these but I leave them as exercises (or you can find them in our UROP project repo here in the “M3P14” directory).

So what’s going on in this code? Well, we’d like to use the `ring`

tactic to make this easily, unfortunately it’s an assertion about naturals and it involves both subtraction and division, neither of which are defined to be what mathematicians think of them as, so we have to be careful. In particular we can’t just apply `ring`

and hope it will work.

Unsurprisingly, the first step is to write as , reducing the goal to

`((3 + 8 * t) ^ 2 - 1) / 8 % 2 = 1`

The next trick is to observe that `(1 + 2 * (4*t^2 + 3*t)) % 2 = 1`

because the thing we’re reducing mod 2 is 1 plus something even. This reduces us to proving

`((3 + 8 * t) ^ 2 - 1) / 8 = (1 + 2 * (4 * t ^ 2 + 3 * t))`

but `ring`

still won’t do this because we have an integer division here. However `nat.mul_div_cancel_left`

is that if `n>0`

then `n * m / n = m`

, meaning that it suffices to prove

`(3 + 8 * t) ^ 2 - 1 = 8 * (1 + 2 * (4 * t ^ 2 + 3 * t))`

and `ring`

is smart enough to know that the last subtraction is not a problem, and closes our goal.