The law of quadratic reciprocity. The jewel in the crown of mathematics! Still not proved in Lean!

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

$\left(\frac{2}{p}\right)=(-1)^{\frac{p^2-1}{8}}$

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 $+1$ if $p\equiv 1$ or 7 mod 8, and $-1$ 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,
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 $n$ as $8t+3$, 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.