Comparing proof assistants to chess engines for a talk

Stream: general

[Riccardo Brasca]

I am preparing a talk about proof assistants and I am thinking on making the following example as a more or less realistic dream about what proof assistants could be used for in the future, and why this is good for "standard" mathematics.

Computer are better at playing chess than essentially any human being since 20 years (or even more). Let's suppose that in 20 years computer will be better than humans in doing mathematics. Are we all going to be fired? I don't think so: people still enjoy playing chess very much and are not very interested that they can have a "chess god" in their phone. We can now use chess engines to discover, maybe by brute force, patterns that are essentially impossible to find for a human. But the players are still interested in understanding why these patterns exist, and are not satisfied by "white wins because it wins whatever black does".

This is very similar to what could happen with mathematics: even if a super Lean will find a proof of the Riemann hypothesis, we will still interested in understand it in human terms, but having a proof, even a very unnatural one, will surely help.

What do you think about this comparison? I am a very bad chess player, so I am a little worried that I am telling nonsense.

[Patrick Massot]

I was telling the same to a journalist a couple of hours ago, but this is an argument that is a bit dangerous: it's not clear people will continue paying us if this happen.

[Patrick Massot]

But it's not clear why they are paying us right now, so let's not worry too much.

[Patrick Massot]

Where will you talk about this?

[Riccardo Brasca]

On December 15th , in the Luxembourg Number Theory Day (I asked them if they'd prefer a talk about proof assistants or standard number theory and they voted for the former)

[Eric Rodriguez]

It's right now the world chess championship, and an interesting trend that I note is that players that don't understand chess as well prefer commentary with the assistance of engines, but higher-rated players tend to prefer without it, and would rather see concrete variations (series of moves) explaining why moves do/don't work. There's still a strong appreciation of "human" moves, though, as you say; weird suggestions by computers do often get called "computer moves" and dismissed (and this happens at all levels - maybe not so justifiably when I am analysing my own games!)

But I can sort of see the parallels even with existing work; for example, the McCune's theorem proof that was discussed some time ago (and Bhavik translated into Lean) I think most of us can agree is kind of unsatisfactory, and if it was an area of research that people were interested in, I think there would be further research and attempts for "natural" proofs. Meanwhile, the one proof that stands out in my head from the past few years (and to be fair, I'm still not involved in any specific research area, so it may be kind of a "pop-sci" answer) was Hao Huang's proof of the sensitivity conjecture, which, to be fair, is still a proof of a major result, but is mostly remembered because of its sheer elegancy. It seems unlikely a computer would find a proof like that, or even if it does present it in such an elegant way.

[Eric Rodriguez]

sorry for my ramble, but tl;dr yes I think it's an apt comparison

[Riccardo Brasca]

I understand that player are not very interested in moves found by computer that are, and probably will remain, impossible find for a human. But I guess that the general understanding of the game is improved thanks to chess engines (especially the endgame). My point is exactly that computer will never replace humans in doing mathematics, but even if they will be able to do "bad" proofs, this will help us in finding "good" proof.

[Riccardo Brasca]

The idea came by seeing a commentator not understanding why Carlsen was winning during game 6 of the championship (when is was very low on time before move 40) :laughing:

[Eric Rodriguez]

oh I thought you didn't know about chess! :b yes, I also wonder if there's a comparison to be made between the speed of humans/machines, although I don't think there is many speed maths competitions!

[Riccardo Brasca]

I am just very bad at it :D

[Kevin Buzzard]

Computers help humans to play chess now, this is clear. They only help some mathematicians to do mathematics (e.g. people computing tables of elliptic curves etc). There's a chance that all this formalisation stuff will later on help far more mathematicians to do mathematics.

[Scott Morrison]

(I recommend the (very) short story"The evolution of human science" by Ted Chiang, collected in his anthology "Stories of your life and others".)

[Bryan Gin-ge Chen]

It was actually published in Nature (and is available online!) under the title "Catching crumbs from the table".

[Filippo A. E. Nuccio]

Will the talk be in person or online (=can I see it?).

[Johan Commelin]

@Scott Morrison Thanks! That was a fun read!

[Riccardo Brasca]

Filippo A. E. Nuccio said:

Will the talk be in person or online (=can I see it?).

It will be in person, I don't think they are going to stream it...