Gowers ATP Project

Stream: general

[Johan Commelin]

I guess most people on this zulip will be interested in reading this: https://gowers.wordpress.com/2022/04/28/announcing-an-automatic-theorem-proving-project/

[Riccardo Brasca]

" That last formalization [LTE] was carried out in Lean by the exciting group that is led by Kevin Buzzard. " :unamused: You should hire a social media manager

[Ruben Van de Velde]

Clearly Kevin doesn't need one :sweat_smile:

[Mauricio Collares]

The social media manager in me thinks livestreaming the last few hours of the project (working on the last few sorries, that is) would be very trendy :smiley: Andy Kelley did livestreams for the Zig self-hosting project where he'd just fix bugs for hours at a time and they were surprisingly entertaining.

[Arthur Paulino]

I took a quick look at their texts trying to find cues about the tooling they're planning to use and I couldn't find any :surprise:

[Yaël Dillies]

Finally! Bhavik told me three months ago that Tim would announce it two weeks later.

[Jireh Loreaux]

Mauricio Collares said:

The social media manager in me thinks livestreaming the last few hours of the project (working on the last few sorries, that is) would be very trendy

There we go, it's a revenue stream for mathlib to fund more build bots! We just need to set up a Twitch stream and get people to host it every few days! :laughter_tears:

[Patrick Massot]

Riccardo Brasca said:

" That last formalization [LTE] was carried out in Lean by the exciting group that is led by Kevin Buzzard. " :unamused: You should hire a social media manager

I think this isn't funny at all.

[Riccardo Brasca]

I didn't want to say it is funny, and I think it is a real problem. Let me stress that I know that Kevin never claimed to be the project's leader, it isn't his fault by any means.

[Patrick Massot]

Actually was answering the reactions to your message, not your message.

[Jireh Loreaux]

Just to be clear, since I am one of those reactions, I'm not laughing at the lack of credit where credit is due to Johan. I completely agree that's a serious issue, and one that has already been addressed in the comments on Tim's post (and now in the post itself).

I'm laughing because, no matter how much Kevin may emphasize that he is not somehow the leader of the Lean community, that message never seems to register with people outside the community. Somehow people still think "any Lean project whatsoever = that thing Kevin is leading." I'm laughing at the apparent futility of trying to communicate this idea. (And obviously, Kevin has led and participated in some important Lean projects as well, which I guess adds fuel to this particular fire.)

[Filippo A. E. Nuccio]

(deleted)

[Rob Lewis]

It was corrected in the text to something that's still not accurate:

That last formalization was carried out in Lean by a team led by Johan Commelin, which is part of the more general and exciting Lean group spearheaded by Kevin Buzzard.

[Eric Wieser]

Maybe it should read "lean group that everyone keeps mistaking Kevin Buzzard for leading"

[Arthur Paulino]

Maybe it's better to be explicit and tell them how the community would like it to be said. I sense an urge from the author to bring up Kevin's name there somehow

[Kevin Buzzard]

Hello. I absolutely agree with Patrick that this is not good. I really don't know what to do about it.

[Jireh Loreaux]

Perhaps the thing to do is for you to comment directly on Tim's post. That should send him the message, and then anyone else who reads your comment may also get the idea?

[Anatole Dedecker]

Also it may be worth setting a clear separation between the Lean team and the mathlib team, thus making sure Leo gets the credit he deserves (I recall Quanta mentioned him as « a computer scientist at MC Research »)

[Patrick Stevens]

Towards a concrete suggestion for Tim that's brief but close to the original text, I guess maybe this might do the trick?

That last formalization was carried out in Lean by a team led by Johan Commelin and Patrick Massot; and you may also have heard of Lean in the context of Kevin Buzzard's exciting Xena project to popularise formalization among undergraduates.

(Sorry if I've misattributed anything here - I follow what's going on, but not assiduously.)

[Patrick Stevens]

(While I am perpetually in awe at the speed and correctness with which Leo and friends manage to pump out a truly innovative language, that aspect doesn't really seem to fit in the context of the rest of Tim's paragraph.)

[Anatole Dedecker]

Yeah in that situation they’re really talking about the community, I was thinking about other cases

[Junyan Xu]

maybe we also want to add some details to https://leanprover-community.github.io/meet.html

[Johan Commelin]

Just for the record: if we want to attach two names to the Lean side of LTE, that would be me and @Adam Topaz.

[Johan Commelin]

Just for more record: Kevin posted a comment on Tim's blog: https://gowers.wordpress.com/2022/04/28/announcing-an-automatic-theorem-proving-project/#comment-476405

[Kevin Buzzard]

I agree with Johan's assessment of the main drivers behind LTE.

Patrick is right to call this sort of thing out and as some of us know, it's not the first time that this sort of thing has happened. I'm very happy to try and correct errors which appear online.

[Kevin Buzzard]

Re the separation of lean and mathlib: this is something else which the "general math public" also do not get for the most part. In fact in the past things were even worse: when I moved into this area I started a blog called the Xena Project which is a slightly nebulous concept driven by the idea that we should be getting young mathematicians to use theorem provers (something I still believe very deeply). By about 2019 it seemed that most casual observers in the maths community couldn't tell the difference between Xena, Lean and mathlib and it was at around this point that Patrick told me that more of an effort was needed on my part to start distinguishing between them. Apparently the current state of play is that now people in the maths community can't tell the difference between Kevin Buzzard, Lean and mathlib which is in some sense even worse. Perhaps it's time for some kind of Xena blog post attempting to put this thing to bed once and for all.

[Filippo A. E. Nuccio]

Everything concerning the Lean=Kevin or the LTE=Kevin problems has been perfectly addressed and I have nothing to add, I just want to say a word about the mathlib=Lean issue. I think our community has some true responsibility here, not only "the press": going here I am on the webpage of the "Lean Community"; and the title is "Lean and its Mathematical LIbrary", already presenting them as a whole. Moreover, clicking on GitHub on the left panel, the link redirects to the mathlib repository, not to the one containing the Lean code. Finally, further below, there is a "Library overview" (clearly pointing to mathlib) but presenting is as the only library that matters in Lean. I think that it is completely normal that nobody sees a difference between Lean and mathlib: I am not claiming this is right, but if we want this to change (and probably we should more honestly ask ourselves whether this is the case), something must be done from our side.

[Eric Wieser]

It clouds the matter further that mathlib uses a community fork of Lean, which is now developed only by people who aren't Leo

[Henrik Böving]

I believe some of this change should come automatically once Lean 4 becomes the mainly used version, we already have some regular programming going on and I'd hope it will only increase from now on so one would expect more and more non mathlib (in fact even non mathematical) Lean libraries to pop up.

[Yaël Dillies]

The document too needs updating.

[Kevin Buzzard]

You're right. I need to email Tim about an unrelated matter; I'll mention it.

[Johan Commelin]

I guess most people on this zulip will be interested in reading this: https://gowers.wordpress.com/2022/04/28/announcing-an-automatic-theorem-proving-project/

[Eric Taucher]

Kevin Buzzard said:

I'd be far more interested in hearing from the AI/ML people about how feasible Tim's project is.

In reading the manifesto one thought that was constant in my mind was,
Is anyone aware of CHR and/or using CHR for theorem proving?

.> Constraint Handling Rules (CHR) is a committed-choice rule-based language embedded in Prolog. It is designed for writing constraint solvers.

So the way I am thinking is that CHR would be a meta language used to construct several constraint solvers and those could be used for certain areas of math. For getting the solvers to communicate, I only have guesses at present.

As for defining cheating I was expecting to see something asking for a pedigree.

Anyway, those are some thoughts I had and hopefully this will break the ice so that others might toss up their thoughts.

[Eric Taucher]

FYI
I am not an expert in CHR but keep it in my toolbox for problem solving if ever there be a need.
Found this paper which might let others see why some of us like CHR. It gives a nice run down of ways in which CHR has/is being used with references.

Constraint Handling Rules - What Else? (pdf)
Thom Fruhwirth
University of Ulm, Germany

[Patrick Massot]

Let me make sure that @Daniel Selsam saw this thread.