quadratic reciprocity graph

Stream: general

[Kevin Buzzard]

Chris just sent me a text file of all the theorems used in his proof of quadratic reciprocity

[Kevin Buzzard]

quadratic_reciprocity.txt

[Kevin Buzzard]

Maybe @Chris Hughes can explain what this file represents while I spend 5 minutes doing emacs hackery on it

[Kevin Buzzard]

but in 10 minutes' time we're going to have this in GePhi

[Kenny Lau]

who is gephi?

[Patrick Massot]

Chris I'd very interested to know why you duplicate this meta-effort. If you don't like what I wrote in https://github.com/leanprover-community/leancrawler you can improve it, or propose a brand new stuff.

[Patrick Massot]

https://gephi.org/

[Chris Hughes]

It's a list (name × list name). Each element of the list is a declaration used in the proof and the list of depth one dependencies.

[Patrick Massot]

The same graph visualization format my crawler natively writes

[Chris Hughes]

I duplicated it to learn how to write meta mainly

[Patrick Massot]

Your meta code may be better than mine, you could contribute it

[Patrick Massot]

Learning meta stuff was also one of my main motivations

[Kevin Buzzard]

I've got it working

[Chris Hughes]

It does slightly different things from yours

[Kevin Buzzard]

quadratic_reciprocity.csv

[Kevin Buzzard]

I've never used gephi before in my life but it's very intuitive. The hard work is done.

[Kevin Buzzard]

open GePhi, click on "open graph file", select that csv file

[Kevin Buzzard]

make sure "separator" is set to semicolon, "import as" is set to "Adjacency List" and "Charset" apparently should be UTF-16LE (blame chris for this)

[Kevin Buzzard]

then Window -> Graph and you have a graph of the proof of quadratic reciprocity in Lean

[Kevin Buzzard]

and 10 gigs less of free ram

[Kevin Buzzard]

In the "statistics" section you can do a bunch of tests and compute things, and those run fine, it's just the visualisation stuff that really hammers the CPU

[Kevin Buzzard]

Diameter is 24, which I guess means that that's the longest chain of dependencies (25 definitions I guess)

[Kevin Buzzard]

chaos.png

[Kevin Buzzard]

It's still trying to see the wood from the trees

[Patrick Massot]

Did you use the Force 2 layout?

[Patrick Massot]

You need to push the scale parameter

[Patrick Massot]

Most of the very high valence vertices seem to be the usual suspects (eq, eq.rec...)

[Patrick Massot]

has_mem and friends, has_zero...

[Kevin Buzzard]

oh -- force 2 uses all the threads!

[Kevin Buzzard]

Oh that's much better

[Chris Hughes]

QR.png

[Kevin Buzzard]

That's a proof of quadratic reciprocity!

[Chris Hughes]

You can spend hours fiddling with all the options on that.

[Kevin Buzzard]

qr2.png

[Kevin Buzzard]

yeah. Yours is nice and arty :-)

[Mario Carneiro]

lol I guess it doesn't lend itself well to word cloud format

[Kevin Buzzard]

QR3.png You can see the words a bit better if you zoom in

[Mario Carneiro]

I notice that all the biggest things are typeclass instances

[Kevin Buzzard]

Nice to see polynomial.integral_domain._proof_12 there.

[Mario Carneiro]

what am I looking at?

[Kevin Buzzard]

Node size is based on "betweenness centrality"

[Kevin Buzzard]

and font size is proportional to node size

[Mario Carneiro]

I'm afraid I can't guess what that means

[Bryan Gin-ge Chen]

There's apparently a whole wikipedia page on it.

[Kevin Buzzard]

degree.png size now proportional to degree of node

[Kevin Buzzard]

OK last one, with size proportional to out-degree -- completely different. QR4.png Thanks so much to @Patrick Massot for pointing me to GePhi. It's really easy to use. Patrick's scripts even create a graph in GePhi format -- Chris sent me a list of edges and I had to do some emacs hackery to turn it into an appropriate format.

[Bryan Gin-ge Chen]

I know very little about quadratic reciprocity and this proof, but for those who do, in your opinion, what should be the biggest nodes in terms of "mathematical importance", i.e. the "key steps"?

[Chris Hughes]

The key steps are polynomials of degree n over an integral domain have at most n roots, Lagrange's theorem in group theory, cyclicness of units of finite field, the fact that integers mod p are a field. After that it's more or less just annoying manipulations of products that have no relevance outside of this proof.

[Patrick Massot]

it's really easy to use

Unfortunately it's not quite true. It's really easy to have fun with, like you and I did. But the purpose of this software is to actually get information from the graph, either visually or in tables. And this is much harder.

[Kevin Buzzard]

I think that Gauss knew all of the facts that Chris quoted when he formulated the law, but it took him years to find the proof. Perhaps because in some sense the proof isn't conceptual -- or at least the proofs Gauss found weren't. Now we can deduce it from more general reciprocity laws which do have conceptual proofs, but to formalise those proofs we need some basic algebraic number theory first (factorisation of ideals into prime ideals in the integers of a number field).

[Kenny Lau]

https://github.com/leanprover/mathlib/issues/40

[Patrick Massot]

screenshot_232944.png

[Kevin Buzzard]

We could do that in 10 minutes flat Kenny if you were interested

[Patrick Massot]

This is probably a more readable graph

[Kevin Buzzard]

However we wouldn't be able to prove anything about them, it would just be a PR stunt

[Kenny Lau]

do what in 10 minutes?

[Kevin Buzzard]

Is the middle dot eq?

[Patrick Massot]

It's limited to mathlib (not core), all declarations used in quadratic reciprocity (big dot in the center) but not recursors or other auto-generated stuff

[Kevin Buzzard]

Oh

[Kevin Buzzard]

Is the middle dot QR then?

[Patrick Massot]

Yes

[Patrick Massot]

qr.gephi

[Kevin Buzzard]

Define adeles in 10 minutes. Adeles of K are adeles of Q tensor K.

[Kenny Lau]

aha

[Kevin Buzzard]

Adeles of Q are just restricted product of p-adics

[Kevin Buzzard]

And the reals

[Kenny Lau]

and R

[Patrick Massot]

Blue is definition, orange is theorem, green is instance

[Kevin Buzzard]

Can you label some of the nodes?

[Patrick Massot]

Kevin, please download the gephi file. I claim it contains relevant stuff

[Patrick Massot]

Not noise

[Kevin Buzzard]

@Bryan Gin-ge Chen quadratic reciprocity does not follow easily from these standard facts that Chris quoted. The hard part is putting everything together in a subtle way. I wonder how long a computer would take to prove it just given the standard facts. I suspect a long time. As Chris said, you end up doing some delicate counting with some intermediate lemmas that you never use again for anything else

[Kevin Buzzard]

The conceptual proof uses the fact that if $p\equiv1$ mod 4, then $\mathbb{Q}(p^{1/2})\subseteq\mathbb{Q}(\zeta_p)$ where $\zeta_p=e^{2\pi i/p}$

[Kenny Lau]

and then doing a lot of non-trivial stuff

[Patrick Massot]

Even better: a version removing any declaration whose name contains "coe" or "cast" (which is noise from a mathematical point of view) qr.gephi

[Kevin Buzzard]

The factorization of a prime number $q$ in $\mathbb{Q}(p^{1/2})$ is governed by whether $p$ is a square mod $q$

[Patrick Massot]

screenshot_234141.png

[Kevin Buzzard]

but the factorization in $\mathbb{Q}(\zeta_p)$ is determined by the behaviour of $q$ mod $p$ and there's the link.

[Patrick Massot]

In this last version you can actually browse the graph and see what's there

[Kevin Buzzard]

This proof historically came much later though. It then goes on to become Artin reciprocity in the early 1900s, which then gets generalised to Langlands reciprocity, a statement sufficiently vague that nobody knows what it is.

[Kevin Buzzard]

But we know it when we see it.

[Kevin Buzzard]

We just can't state it precisely.

[Kevin Buzzard]

Patrick is it easy to say what the definitions and instances are?

[Kenny Lau]

one should ask

[Patrick Massot]

Do you want lists of definitions, or do you want to know which color is what?

[Kenny Lau]

is Chris's proof a proof?

[Kevin Buzzard]

Not of Langlands reciprocity, but probably of quadratic reciprocity.

[Kenny Lau]

should proofs give us some understanding about why it is true?

[Kevin Buzzard]

I was wondering what the names of the small list of things that weren't theorems were. I can look tomorrow. I'm just off to bed.

[Kevin Buzzard]

should proofs give us some understanding about why it is true?

That's so 1900s.

[Kevin Buzzard]

If it happens, it's a bonus. If it doesn't, rotten luck.

[Patrick Massot]

Kevin, in gephi, if you go to tab probably called "data lab" (guessing from my French speaking version), you can sort by type of node

[Kevin Buzzard]

It's like asking if food which is good for you should taste nice.

[Patrick Massot]

But of course I can also ask the python shell. Definitions are:

['finset.univ',
 'fintype.fintype_prod_right',
 'nat.modeq',
 'multiset',
 'nat.prime',
 'zmodp',
 'fintype.fintype_prod_left',
 'zmod',
 'fintype.card',
 'zmodp.legendre_sym',
 'fintype.of_equiv',
 'multiset.card',
 'multiset.map',
 'set_fintype',
 'order_of',
 'nat.decidable_prime_1']

[Patrick Massot]

instances:

['zmodp.comm_ring',
 'list.perm.setoid',
 'zmod.has_neg',
 'zmod.add_comm_semigroup',
 'zmod.has_zero',
 'zmodp.decidable_eq',
 'fintype.decidable_exists_fintype',
 'zmodp.discrete_field',
 'zmod.has_one',
 'zmodp.fintype',
 'fin.fintype',
 'fintype.decidable_forall_fintype',
 'decidable_gpowers',
 'zmod.comm_ring',
 'fintype.subsingleton',
 'prod.fintype',
 'nat.decidable',
 'zmod.fintype']

[Patrick Massot]

and I should also go to bed

[Kenny Lau]

there's something wrong with me if Patrick consistently goes to bed earlier than me

[Kevin Buzzard]

I am not sure that Gauss's proofs of quadratic reciprocity gave us any understanding of why the theorem is true. The arguments are sufficiently elementary to be easily checkable by a third year undergraduate but at the end of the day it's a big motivationless computation of eg the number of dots in a rectangle counted in a weird way

[Kevin Buzzard]

What insight does that give us?

[Kenny Lau]

I can confirm the part about third year undergraduate

[Kenny Lau]

I was in the very course

[Kevin Buzzard]

You went to Toby's lectures?

[Kenny Lau]

yes

[Kevin Buzzard]

And the student was right :-)

[Kevin Buzzard]

I got some of the summer students to formalise his example sheet questions and after a few hours one of them came up to me and told me that the first part of the first question was false :-)

[Kevin Buzzard]

Which proof did he give? The Hardy and Wright one?

[Kenny Lau]

the rectangle one

[Kevin Buzzard]

there's something wrong with me if Patrick consistently goes to bed earlier than me

It's called "you are not a parent and don't have a job" -- I'm not sure that this qualifies as something wrong with you, it just means you're young.

[Kevin Buzzard]

But back to the point I've been thinking more about quadratic reciprocity. What insight does that stupid rectangle proof give you? It's of the form "divide the rectangle up into about 6 regions, prove some boring lemmas about the number of points in each region, add everything up, deduce quadratic reciprocity". I am not at all sure that it gives you any insight into why the theorem is true at all. Chris gave an excellent summary of the proof -- "invoke some standard lemmas and then do a completely unmotivated computation about an apparently unrelated rectangle, and it happens to drop out". Kenny -- you probably followed Toby's proof -- can you then give me a succinct one-line summary as to why an odd prime p is a square mod 13 if and only if 13 is a square mod p? That assertion on the face of it looks like the ramblings of a madman -- those statements clearly have nothing to do with each other. The proof is entirely non-constructive as well (of course -- actually computing the square root of 13 mod p is computationally hard if p is huge, whereas computing a square root of p mod 13 is trivial). Is the rectangle proof really a proof? I read it and read it, and I still have no idea "why" the theorem is true.

Looking at it now, that proof of quadratic reciprocity looks pretty much the same as the four colour theorem proof to me -- that proof goes something like: divide the problem up into around 2000 graphs, prove a lemma about each graph, put everything together. And yet people regard quadratic reciprocity as a brilliant thing and the 4 colour proof as something which gives no insight. Are we just being blinded by the fact that 6 is less than 2000?

[Johan Commelin]

Are we just being blinded by the fact that 6 is less than 2000?

Yes, we are!

[Reid Barton]

Wasn't there some "one-sentence" proof which showed an equation (maybe writing a prime 1 mod 4 as the sum of two squares?) has a solution by exhibiting an involution on some set of tuples of integers whose fixed points were solutions to the equations, and then exhibiting a second involution on the same set which obviously had a unique fixed point (or maybe an odd number of them)

[Chris Hughes]

Yes. Here it is in lean https://github.com/dorhinj/leanstuff/blob/master/fermat_sum_two_squares.lean

[Kevin Buzzard]

This is Zagier's "one line proof" that a prime which is 1 mod 4 is the sum of two squares. Since then a slightly simpler involution argument has been found: see https://www.sciencedirect.com/science/article/pii/S0012365X15004355 (possibly behind a firewall).

[Kevin Buzzard]

Zagier's proof is here: https://www.jstor.org/stable/2323918?origin=crossref&seq=1#metadata_info_tab_contents

[Reid Barton]

Yes this is the one I was thinking of. Nice!
I wonder how many of these verifications could be done automatically with a tool like Z3. Obviously it wouldn't be able to do the steps which use the fact that p is prime, but those cases could be handled manually and then fed in as additional hypotheses.

[Kevin Buzzard]

I would be very interested in hearing people's opinion on to what extent this is possible.

[Kevin Buzzard]

Any mathematics which is undergraduate level -- I am interested in what state of the art proof verification software can do.

[Reid Barton]

I guess I could try some of these

[Reid Barton]

Here's what I did so far. I didn't put in the assumption that p is prime obviously, I just stated it must be at least 5 in case that was important.

(declare-const p Int)
(assert (> p 4))

(declare-datatypes () ((Triple (mk (x Int) (y Int) (z Int)))))

(define-fun S ((t Triple)) Bool
  (= (+ (* (x t) (x t)) (* 4 (y t) (z t))) p))
(define-fun f1 ((t Triple)) Triple
  (mk (x t) (z t) (y t)))
(define-fun f2 ((t Triple)) Triple
  (ite (< (+ (x t) (z t)) (y t))
       (mk (+ (x t) (* 2 (z t))) (z t) (- (y t) (x t) (z t)))
       (ite (< (* 2 (y t)) (x t))
        (mk (- (x t) (* 2 (y t))) (+ (- (x t) (y t)) (z t)) (y t))
        (mk (- (* 2 (y t)) (x t)) (y t) (+ (- (x t) (y t)) (z t))))))

(declare-const t Triple)
(assert (S t))

(push)
(assert (not (S (f1 t))))
(check-sat)             ; unsat
(pop)

(push)
(assert (not (= t (f1 (f1 t)))))    ; unsat
(check-sat)
(pop)

(push)
(assert (not (S (f2 t))))       ; unsat
(check-sat)
(pop)

(push)
(assert (not (= t (f2 (f2 t)))))
(check-sat)             ; sat

(declare-const t1 Triple)
(assert (= t1 (f2 t)))
(declare-const t2 Triple)
(assert (= t2 (f2 t1)))

(check-sat)             ; sat
(get-model)             ; p = 9, t = (3,1,0), t1 = (1,2,1), t2 = (3,2,0)
(pop)

[Reid Barton]

I learned that to prove f2 is an involution on S I need some further condition--looking at Chris's proof it's these checks that x, y, z have to be positive.

[Reid Barton]

Now I replaced the last section by

(push)
(assert (not (= t (f2 (f2 t)))))
(assert (> (x t) 0))
(assert (> (y t) 0))
(assert (> (z t) 0))
(check-sat)                             ; unsat
(pop)

so x y z positive is enough to prove it.

[Chris Hughes]

You only need that p is not square for x y z positive. Can you weaken the condition to that?

[Reid Barton]

I didn't even say that p is prime or what it is mod 4 yet

[Reid Barton]

Oh, I see.

[Reid Barton]

Hm...

[Reid Barton]

I'm not sure if I can encode "p is not square" in a helpful way

[Reid Barton]

I tried (assert (forall ((n Int)) (not (= p (* n n))))), but now Z3 seems to be running forever on the fourth check

[Reid Barton]

Oh, I also missed part of the definition of S

[Reid Barton]

okay, now it can actually do the fourth part with (assert (forall ((n Int)) (not (= p (* n n))))) and with the nonnegativity included in the definition of S

[Reid Barton]

For f2 having a unique fixed point, it can prove (if I ask it to) that for a fixed point, we must have x = y

[Reid Barton]

Here's the whole thing https://gist.github.com/rwbarton/440ef225da3c243c1c03028d5d32f87b

[Reid Barton]

I guess maybe I can express not prime too, then

[Reid Barton]

Or being prime, rather

[Reid Barton]

Updated: https://gist.github.com/rwbarton/440ef225da3c243c1c03028d5d32f87b
If I tell it p is prime, it can check the first four facts and it can still prove that a fixed point of f2 must satisfy x = y but it can't deduce that x = y = 1. I guess it doesn't hit on the idea of using distributivity

[Reid Barton]

I can't get (set-option :produce-proofs true) to do anything, not sure whether I am using it wrong or whether Z3 just doesn't want to produce proofs for the theory of integer arithmetic

[Reid Barton]

oh you have to ask it for the proof explicitly as well

[Reid Barton]

Kevin I would say that the partitions proof no longer has any steps which I would want out to Z3. At least not very large ones.

[Reid Barton]

I think I could explain it to someone at the board and there aren't really any mysterious computations happening.

[Reid Barton]

Whereas the Zagier proof has a couple ring computations to do plus various facts about linear inequalities to check