Zulip Chat Archive

Stream: general

Topic: quadratic reciprocity graph


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 15:40):

quadratic_reciprocity.txt

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 15:41):

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

view this post on Zulip Kenny Lau (Sep 16 2018 at 15:42):

who is gephi?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 16 2018 at 15:42):

https://gephi.org/

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 16 2018 at 15:43):

The same graph visualization format my crawler natively writes

view this post on Zulip Chris Hughes (Sep 16 2018 at 15:43):

I duplicated it to learn how to write meta mainly

view this post on Zulip Patrick Massot (Sep 16 2018 at 15:43):

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

view this post on Zulip Patrick Massot (Sep 16 2018 at 15:44):

Learning meta stuff was also one of my main motivations

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 15:44):

I've got it working

view this post on Zulip Chris Hughes (Sep 16 2018 at 15:45):

It does slightly different things from yours

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 15:45):

quadratic_reciprocity.csv

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 15:46):

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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 15:48):

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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 15:48):

and 10 gigs less of free ram

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 15:52):

chaos.png

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 15:53):

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

view this post on Zulip Patrick Massot (Sep 16 2018 at 15:55):

Did you use the Force 2 layout?

view this post on Zulip Patrick Massot (Sep 16 2018 at 15:56):

You need to push the scale parameter

view this post on Zulip Patrick Massot (Sep 16 2018 at 15:58):

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

view this post on Zulip Patrick Massot (Sep 16 2018 at 15:58):

has_mem and friends, has_zero...

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 16:07):

oh -- force 2 uses all the threads!

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 16:07):

Oh that's much better

view this post on Zulip Chris Hughes (Sep 16 2018 at 19:38):

QR.png

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 19:53):

That's a proof of quadratic reciprocity!

view this post on Zulip Chris Hughes (Sep 16 2018 at 19:55):

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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 20:27):

qr2.png

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 20:28):

yeah. Yours is nice and arty :-)

view this post on Zulip Mario Carneiro (Sep 16 2018 at 20:29):

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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 20:31):

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

view this post on Zulip Mario Carneiro (Sep 16 2018 at 20:32):

I notice that all the biggest things are typeclass instances

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 20:33):

Nice to see polynomial.integral_domain._proof_12 there.

view this post on Zulip Mario Carneiro (Sep 16 2018 at 20:33):

what am I looking at?

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 20:33):

Node size is based on "betweenness centrality"

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 20:34):

and font size is proportional to node size

view this post on Zulip Mario Carneiro (Sep 16 2018 at 20:34):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 16 2018 at 20:35):

There's apparently a whole wikipedia page on it.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 20:36):

degree.png size now proportional to degree of node

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:29):

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

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:30):

screenshot_232944.png

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:30):

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

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:31):

This is probably a more readable graph

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:31):

do what in 10 minutes?

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:31):

Is the middle dot eq?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:32):

Oh

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:32):

Is the middle dot QR then?

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:32):

Yes

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:33):

qr.gephi

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:33):

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

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:33):

aha

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:33):

Adeles of Q are just restricted product of p-adics

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:33):

And the reals

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:33):

and R

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:33):

Blue is definition, orange is theorem, green is instance

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:34):

Can you label some of the nodes?

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:35):

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

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:35):

Not noise

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:40):

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

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:41):

and then doing a lot of non-trivial stuff

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:41):

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

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:41):

screenshot_234141.png

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:42):

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

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:43):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:44):

But we know it when we see it.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:44):

We just can't state it precisely.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:44):

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

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:45):

one should ask

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:45):

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

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:45):

is Chris's proof a proof?

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:45):

Not of Langlands reciprocity, but probably of quadratic reciprocity.

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:46):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:46):

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

That's so 1900s.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:46):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:47):

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

view this post on Zulip 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']

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:49):

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']

view this post on Zulip Patrick Massot (Sep 16 2018 at 21:50):

and I should also go to bed

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:57):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:58):

What insight does that give us?

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:58):

I can confirm the part about third year undergraduate

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:59):

I was in the very course

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 21:59):

You went to Toby's lectures?

view this post on Zulip Kenny Lau (Sep 16 2018 at 21:59):

yes

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 22:01):

And the student was right :-)

view this post on Zulip 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 :-)

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 22:01):

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

view this post on Zulip Kenny Lau (Sep 16 2018 at 22:02):

the rectangle one

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Sep 17 2018 at 12:50):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Sep 17 2018 at 13:07):

I guess I could try some of these

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Sep 17 2018 at 13:32):

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

view this post on Zulip Reid Barton (Sep 17 2018 at 13:32):

Oh, I see.

view this post on Zulip Reid Barton (Sep 17 2018 at 13:32):

Hm...

view this post on Zulip Reid Barton (Sep 17 2018 at 13:33):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 17 2018 at 13:38):

Oh, I also missed part of the definition of S

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 17 2018 at 13:44):

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

view this post on Zulip Reid Barton (Sep 17 2018 at 13:45):

I guess maybe I can express not prime too, then

view this post on Zulip Reid Barton (Sep 17 2018 at 13:45):

Or being prime, rather

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 17 2018 at 14:04):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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