## Stream: general

### Topic: Coq memes

#### Simon Hudon (Oct 20 2019 at 03:14):

This might look familiar to people here?

#### Mario Carneiro (Oct 20 2019 at 03:18):

where are the mathematicians?

#### Simon Hudon (Oct 20 2019 at 03:21):

Maybe you can post that one

#### 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

#### Mario Carneiro (Oct 20 2019 at 03:26):

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

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

#### 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

#### 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

#### 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

#### Mario Carneiro (Oct 20 2019 at 08:44):

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

#### 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?

#### Mario Carneiro (Oct 20 2019 at 09:49):

is "piecewise linear" really a standard acronym?

Oh YES

#### Patrick Massot (Oct 20 2019 at 09:50):

Here it gives almost 10 millions hits.

#### Patrick Massot (Oct 20 2019 at 09:50):

And this acronym existed before computers.

#### Mario Carneiro (Oct 20 2019 at 09:50):

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

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

#### Mario Carneiro (Oct 20 2019 at 09:56):

everything is equivalent under a sufficiently vague notion of equivalence

true

#### Simon Hudon (Oct 20 2019 at 15:30):

or rather λ x y, true

#### 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?

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

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

#### Kevin Buzzard (Oct 30 2019 at 22:41):

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

#### 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!

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

#### 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


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

#### Kevin Buzzard (Oct 31 2019 at 00:47):

Yeah, this is why I persevere.

#### Kevin Buzzard (Oct 31 2019 at 00:47):

I can see some fun ahead.

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

#### Kevin Buzzard (Oct 31 2019 at 00:50):

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

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

#### 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

#### Mario Carneiro (Oct 31 2019 at 00:52):

to look at what was done and figure out what happened

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

#### 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

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

#### Kevin Buzzard (Oct 31 2019 at 00:54):

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

#### Kevin Buzzard (Oct 31 2019 at 00:54):

I really like dots and boxes.

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

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

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

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

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

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

#### 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