Zulip Chat Archive

Stream: general

Topic: Coq memes


view this post on Zulip Simon Hudon (Oct 20 2019 at 03:14):

https://www.reddit.com/r/Coq/comments/djxaw0/the_people_you_meet_when_you_learn_coq/?utm_source=share&utm_medium=ios_app&utm_name=iossmf

This might look familiar to people here?

view this post on Zulip Mario Carneiro (Oct 20 2019 at 03:18):

where are the mathematicians?

view this post on Zulip Simon Hudon (Oct 20 2019 at 03:21):

Maybe you can post that one

view this post on Zulip Mario Carneiro (Oct 20 2019 at 03:23):

well, that might be an observation about the coq ecosystem. I don't think any of the lean mathematicians fit well in any of those camps, and seem to actively dislike several of the caricatures

view this post on Zulip Mario Carneiro (Oct 20 2019 at 03:26):

@Simon Hudon Do you think 2020 is the year of dependently typed haskell?

view this post on Zulip Simon Hudon (Oct 20 2019 at 04:54):

Actually, I haven't followed that saga. I don't know how far they will take dependent types and how the Lean / Coq wisdom of "don't make your functions dependently typed" will translate into Haskell.

view this post on Zulip Mario Carneiro (Oct 20 2019 at 05:02):

I think it's a "grass is greener" situation. Those that have dependent types don't want them, and those that don't have them want them

view this post on Zulip Mario Carneiro (Oct 20 2019 at 05:06):

I think what haskell is really missing compared to DTT languages is the ability to state and prove propositions

view this post on Zulip Kevin Buzzard (Oct 20 2019 at 07:39):

I have not embarked on a formal proof of FLT precisely because extensive questioning of serious mathematicians 1 year ago convinced me that it would be a worthless project

view this post on Zulip Mario Carneiro (Oct 20 2019 at 08:44):

The description of the "formal methods expert" certainly makes it sound like tilting at windmills

view this post on Zulip Patrick Massot (Oct 20 2019 at 09:30):

I've seen the PL acronym several times recently. I guess it's not used with its standard meaning of "piecewise linear". Is it programming language?

view this post on Zulip Mario Carneiro (Oct 20 2019 at 09:49):

is "piecewise linear" really a standard acronym?

view this post on Zulip Patrick Massot (Oct 20 2019 at 09:49):

Oh YES

view this post on Zulip Patrick Massot (Oct 20 2019 at 09:49):

Google PL topology

view this post on Zulip Patrick Massot (Oct 20 2019 at 09:50):

Here it gives almost 10 millions hits.

view this post on Zulip Patrick Massot (Oct 20 2019 at 09:50):

And this acronym existed before computers.

view this post on Zulip Mario Carneiro (Oct 20 2019 at 09:50):

i see, it does seem to be used in that area

view this post on Zulip Scott Morrison (Oct 20 2019 at 09:53):

I don't remember how many times I've asked "err... are we doing this PL or smooth?" (and usually getting a shrug as response...)

view this post on Zulip Mario Carneiro (Oct 20 2019 at 09:56):

everything is equivalent under a sufficiently vague notion of equivalence

view this post on Zulip Simon Hudon (Oct 20 2019 at 15:30):

true

view this post on Zulip Simon Hudon (Oct 20 2019 at 15:30):

or rather λ x y, true

view this post on Zulip Joonas Pihlaja (Oct 30 2019 at 22:29):

Sorry to barge in, but could you expand on the argument that leads to the conclusion that formalising FLT is a worthless project?

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 22:39):

I asked a whole bunch of serious number theorists how much they would care if a team of computer scientists announced tomorrow that they had fully formalised a proof of Fermat's Last Theorem, and the sup of the responses I got was "epsilon". They mostly said things like "I am far more interested in new stuff".

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 22:40):

Hence it is useless in terms of trying to advertise this sort of software to research mathematicians.

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 22:41):

You see, we checked it over 20 years ago, so you don't need to.

view this post on Zulip Luca Seemungal (Oct 30 2019 at 22:53):

I think that an issue is the fact that if you've discovered a new proof, it would take far less time to write it up as a pdf than in lean (unless you're sufficiently well trained in lean). And people still trust PDFs (at least I do) - especially if they're written in latex!

view this post on Zulip Joonas Pihlaja (Oct 30 2019 at 23:15):

I see. Thank you for your candid answer.

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 23:48):

I think that an issue is the fact that if you've discovered a new proof, it would take far less time to write it up as a pdf than in lean (unless you're sufficiently well trained in lean). And people still trust PDFs (at least I do) - especially if they're written in latex!

This is exactly the problem. A maths undergraduate and they are already brainwashed :-/

view this post on Zulip Luca Seemungal (Oct 31 2019 at 00:01):

Somehow imo there are two kinds of mathematicians - ones where "proof comes first" and others where "ideas come first". You'll often see proof people get bogged down in annoying details that many people won't care about, and you'll often see ideas people wave their hands about and claim certain things to be true that may not be convincingly so.

I believe that lean has the potential to unify these two seemingly opposite mentalities. Ideally we would get Lean to the point where an ideas person could prove a theorem by "waving their hands within lean" and lean would have good enough tactics to complete the proof. Something like:

theorem riemman_hypothesis (whatever) :=
begin
*waves hands in lean and lean works out the uninteresting details*
end

view this post on Zulip Luca Seemungal (Oct 31 2019 at 00:21):

Although thinking about this, I am having doubts. Is this really the ideal? What if lean works out a lemma that is actually fairly interesting? Then because it was only used in aid of this one theorem, no human will look into it or investigate it. Is this mathematical progress? What is progress? Also, we want the computer to generate proofs that are human-like - proofs that resemble a human's thought process. Do we actually want this though? I can imagine this being a contentious issue in the future.

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:47):

Yeah, this is why I persevere.

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:47):

I can see some fun ahead.

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:49):

As I've said several times before, "Appel--Haken II: computers return" is when a computer belches out a one million line long piece of OCaml code claiming to be a proof of the Riemann Hypothesis, and it's completely non-human-readable but it typechecks.

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:50):

It's at that point you begin to wonder what the point of pure mathematicians is.

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:51):

I gave up dots and boxes when I realised that computers would be playing the 5x5 game (my favourite size) perfectly soon, I figured there was no more point playing.

view this post on Zulip Mario Carneiro (Oct 31 2019 at 00:52):

I think there is an interesting task to be done once you have that computer proof of RH

view this post on Zulip Mario Carneiro (Oct 31 2019 at 00:52):

to look at what was done and figure out what happened

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:52):

At one point I was probably the best 5x5 dots and boxes player on the planet but sometimes I would agonise for three or more hours over a middle-game move just thinking "I would like to force a win from here, but this is such hard work to analyse, at this stage it is clearly a job for a computer"

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:53):

and that was when I moved onto n x n dots and boxes, to stay one step ahead, and wrote https://arxiv.org/abs/1305.2156

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:54):

because computers were beating me at 5x5 but I could still prove the theorem in that paper and a computer couldn't have generated that proof.

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:54):

@Ellen Arlt is formalising that paper this year for her MSc project in Lean.

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:54):

I really like dots and boxes.

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:56):

And another really funny thing about that paper is that I have never met my co-author. We have played dots and boxes against each other online and at some point I realised that he had a brilliance which I lacked. And then he emailed me saying he was a schoolkid and could he do a school project with me on dots and boxes and I said "yeah alright"

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:57):

and I taught him the theory, which I'd learnt from Berlekamp, and and then he solved a hard problem and we wrote it up as a joint paper.

view this post on Zulip Kevin Buzzard (Oct 31 2019 at 00:57):

and now we have technical conversations about machine learning and dots and boxes occasionally. I should get him on this chat.

view this post on Zulip Scott Morrison (Oct 31 2019 at 06:20):

I wish I'd known to use dots-and-boxes as my "example combinatorial game", rather than domineering. :-)

view this post on Zulip Luca Seemungal (Oct 31 2019 at 08:40):

On the topic of a million line ocaml proof of the RH - I'm not sure if I would accept that. Clearly, I'm an undergraduate and so I wouldn't understand a written proof of it anyway, but there's some sense in which a _wrong_ proof with good, enlightening, ideas is better than a _right_ proof that doesn't bring anything new to the table. In my opinion, I would prefer no proof at all rather than such a million line proof.

view this post on Zulip Luca Seemungal (Oct 31 2019 at 08:41):

If such a million line proof arises, then I think that the job of the pure mathematician would be to figure out the good ideas that came into the proof.

view this post on Zulip Tim Hosgood (Oct 31 2019 at 14:07):

If such a million line proof arises, then I think that the job of the pure mathematician would be to figure out the good ideas that came into the proof.

this seems like a good description of what a pure mathematician might be good for in the future, but it also raises the old question of "if nobody really understands a whole proof, is it really a proof?". By nice compositionality stuff, we could maybe show that it's enough to understand little bits of the proof and how the little bits fit together, but I don't think it's impossible that a computer could produce a proof which was in no way compositional (i.e. it was just one long meandering thread that couldn't be split into nice little segments)


Last updated: May 15 2021 at 23:13 UTC