Coq memes

Stream: general

[Simon Hudon]

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?

[Mario Carneiro]

where are the mathematicians?

[Simon Hudon]

Maybe you can post that one

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Patrick Massot]

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?

[Mario Carneiro]

is "piecewise linear" really a standard acronym?

[Patrick Massot]

Oh YES

[Patrick Massot]

Google PL topology

[Patrick Massot]

Here it gives almost 10 millions hits.

[Patrick Massot]

And this acronym existed before computers.

[Mario Carneiro]

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

[Scott Morrison]

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

[Mario Carneiro]

everything is equivalent under a sufficiently vague notion of equivalence

[Simon Hudon]

true

[Simon Hudon]

or rather λ x y, true

[Joonas Pihlaja]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Luca Seemungal]

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!

[Joonas Pihlaja]

I see. Thank you for your candid answer.

[Kevin Buzzard]

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 :-/

[Luca Seemungal]

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

[Luca Seemungal]

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.

[Kevin Buzzard]

Yeah, this is why I persevere.

[Kevin Buzzard]

I can see some fun ahead.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

to look at what was done and figure out what happened

[Kevin Buzzard]

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"

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

I really like dots and boxes.

[Kevin Buzzard]

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"

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Scott Morrison]

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

[Luca Seemungal]

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.

[Luca Seemungal]

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.

[Tim Hosgood]

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)

[Martin Dvořák]

We need our own page. What would you call it? I suggest "Lean memes for formally-verified teens".