## Stream: general

#### Kevin Buzzard (Sep 16 2018 at 15:39):

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

#### Kevin Buzzard (Sep 16 2018 at 15:40):

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

#### Kevin Buzzard (Sep 16 2018 at 15:41):

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

who is gephi?

#### Patrick Massot (Sep 16 2018 at 15:42):

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 (Sep 16 2018 at 15:42):

https://gephi.org/

#### Chris Hughes (Sep 16 2018 at 15:43):

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 (Sep 16 2018 at 15:43):

The same graph visualization format my crawler natively writes

#### Chris Hughes (Sep 16 2018 at 15:43):

I duplicated it to learn how to write meta mainly

#### Patrick Massot (Sep 16 2018 at 15:43):

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

#### Patrick Massot (Sep 16 2018 at 15:44):

Learning meta stuff was also one of my main motivations

#### Kevin Buzzard (Sep 16 2018 at 15:44):

I've got it working

#### Chris Hughes (Sep 16 2018 at 15:45):

It does slightly different things from yours

#### Kevin Buzzard (Sep 16 2018 at 15:45):

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

#### Kevin Buzzard (Sep 16 2018 at 15:46):

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

#### Kevin Buzzard (Sep 16 2018 at 15:46):

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 (Sep 16 2018 at 15:48):

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

#### Kevin Buzzard (Sep 16 2018 at 15:48):

and 10 gigs less of free ram

#### Kevin Buzzard (Sep 16 2018 at 15:50):

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 (Sep 16 2018 at 15:51):

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

chaos.png

#### Kevin Buzzard (Sep 16 2018 at 15:53):

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

#### Patrick Massot (Sep 16 2018 at 15:55):

Did you use the Force 2 layout?

#### Patrick Massot (Sep 16 2018 at 15:56):

You need to push the scale parameter

#### Patrick Massot (Sep 16 2018 at 15:58):

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

#### Patrick Massot (Sep 16 2018 at 15:58):

has_mem and friends, has_zero...

#### Kevin Buzzard (Sep 16 2018 at 16:07):

oh -- force 2 uses all the threads!

#### Kevin Buzzard (Sep 16 2018 at 16:07):

Oh that's much better

QR.png

#### Kevin Buzzard (Sep 16 2018 at 19:53):

That's a proof of quadratic reciprocity!

#### Chris Hughes (Sep 16 2018 at 19:55):

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

qr2.png

#### Kevin Buzzard (Sep 16 2018 at 20:28):

yeah. Yours is nice and arty :-)

#### Mario Carneiro (Sep 16 2018 at 20:29):

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

#### Kevin Buzzard (Sep 16 2018 at 20:31):

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

#### Mario Carneiro (Sep 16 2018 at 20:32):

I notice that all the biggest things are typeclass instances

#### Kevin Buzzard (Sep 16 2018 at 20:33):

Nice to see polynomial.integral_domain._proof_12 there.

#### Mario Carneiro (Sep 16 2018 at 20:33):

what am I looking at?

#### Kevin Buzzard (Sep 16 2018 at 20:33):

Node size is based on "betweenness centrality"

#### Kevin Buzzard (Sep 16 2018 at 20:34):

and font size is proportional to node size

#### Mario Carneiro (Sep 16 2018 at 20:34):

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

#### Kevin Buzzard (Sep 16 2018 at 20:36):

degree.png size now proportional to degree of node

#### Kevin Buzzard (Sep 16 2018 at 20:38):

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 (Sep 16 2018 at 20:44):

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 (Sep 16 2018 at 20:55):

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 (Sep 16 2018 at 20:59):

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 (Sep 16 2018 at 21:29):

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 (Sep 16 2018 at 21:29):

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

#### Patrick Massot (Sep 16 2018 at 21:30):

screenshot_232944.png

#### Kevin Buzzard (Sep 16 2018 at 21:30):

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

#### Patrick Massot (Sep 16 2018 at 21:31):

This is probably a more readable graph

#### Kevin Buzzard (Sep 16 2018 at 21:31):

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

#### Kenny Lau (Sep 16 2018 at 21:31):

do what in 10 minutes?

#### Kevin Buzzard (Sep 16 2018 at 21:31):

Is the middle dot eq?

#### Patrick Massot (Sep 16 2018 at 21:31):

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

Oh

#### Kevin Buzzard (Sep 16 2018 at 21:32):

Is the middle dot QR then?

Yes

qr.gephi

aha

And the reals

and R

#### Patrick Massot (Sep 16 2018 at 21:33):

Blue is definition, orange is theorem, green is instance

#### Kevin Buzzard (Sep 16 2018 at 21:34):

Can you label some of the nodes?

Not noise

#### Kevin Buzzard (Sep 16 2018 at 21:37):

@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 (Sep 16 2018 at 21:40):

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 (Sep 16 2018 at 21:41):

and then doing a lot of non-trivial stuff

#### Patrick Massot (Sep 16 2018 at 21:41):

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 (Sep 16 2018 at 21:41):

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 (Sep 16 2018 at 21:41):

screenshot_234141.png

#### Kevin Buzzard (Sep 16 2018 at 21:42):

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

#### Patrick Massot (Sep 16 2018 at 21:43):

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

#### Kevin Buzzard (Sep 16 2018 at 21:43):

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 (Sep 16 2018 at 21:44):

But we know it when we see it.

#### Kevin Buzzard (Sep 16 2018 at 21:44):

We just can't state it precisely.

#### Kevin Buzzard (Sep 16 2018 at 21:44):

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

#### Patrick Massot (Sep 16 2018 at 21:45):

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

#### Kenny Lau (Sep 16 2018 at 21:45):

is Chris's proof a proof?

#### Kevin Buzzard (Sep 16 2018 at 21:45):

Not of Langlands reciprocity, but probably of quadratic reciprocity.

#### Kenny Lau (Sep 16 2018 at 21:46):

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

#### Kevin Buzzard (Sep 16 2018 at 21:46):

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 (Sep 16 2018 at 21:46):

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

That's so 1900s.

#### Kevin Buzzard (Sep 16 2018 at 21:46):

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

#### Patrick Massot (Sep 16 2018 at 21:46):

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 (Sep 16 2018 at 21:47):

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

#### Patrick Massot (Sep 16 2018 at 21:48):

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 (Sep 16 2018 at 21:49):

instances:

['zmodp.comm_ring',
'list.perm.setoid',
'zmod.has_neg',
'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 (Sep 16 2018 at 21:50):

and I should also go to bed

#### Kenny Lau (Sep 16 2018 at 21:57):

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

#### Kevin Buzzard (Sep 16 2018 at 21:58):

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 (Sep 16 2018 at 21:58):

What insight does that give us?

#### Kenny Lau (Sep 16 2018 at 21:59):

I was in the very course

#### Kevin Buzzard (Sep 16 2018 at 21:59):

You went to Toby's lectures?

yes

#### Kevin Buzzard (Sep 16 2018 at 22:01):

And the student was right :-)

#### Kevin Buzzard (Sep 16 2018 at 22:01):

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 (Sep 16 2018 at 22:01):

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

#### Kenny Lau (Sep 16 2018 at 22:02):

the rectangle one

#### Kevin Buzzard (Sep 17 2018 at 08:26):

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 (Sep 17 2018 at 08:34):

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 (Sep 17 2018 at 08:36):

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

Yes, we are!

#### Reid Barton (Sep 17 2018 at 12:22):

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 (Sep 17 2018 at 12:23):

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

#### Kevin Buzzard (Sep 17 2018 at 12:50):

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).

#### Reid Barton (Sep 17 2018 at 12:56):

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 (Sep 17 2018 at 13:05):

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

#### Kevin Buzzard (Sep 17 2018 at 13:05):

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

#### Reid Barton (Sep 17 2018 at 13:07):

I guess I could try some of these

#### Reid Barton (Sep 17 2018 at 13:26):

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 (Sep 17 2018 at 13:27):

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 (Sep 17 2018 at 13:30):

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 (Sep 17 2018 at 13:31):

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

#### Reid Barton (Sep 17 2018 at 13:32):

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

Oh, I see.

Hm...

#### Reid Barton (Sep 17 2018 at 13:33):

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

#### Reid Barton (Sep 17 2018 at 13:36):

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

#### Reid Barton (Sep 17 2018 at 13:38):

Oh, I also missed part of the definition of S

#### Reid Barton (Sep 17 2018 at 13:39):

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 (Sep 17 2018 at 13:40):

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 (Sep 17 2018 at 13:44):

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

#### Reid Barton (Sep 17 2018 at 13:45):

I guess maybe I can express not prime too, then

#### Reid Barton (Sep 17 2018 at 13:45):

Or being prime, rather

#### Reid Barton (Sep 17 2018 at 13:53):

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 (Sep 17 2018 at 13:57):

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 (Sep 17 2018 at 14:04):

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

#### Reid Barton (Sep 17 2018 at 23:21):

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 (Sep 17 2018 at 23:22):

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

#### Reid Barton (Sep 17 2018 at 23:23):

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

Last updated: May 09 2021 at 19:11 UTC