Lean Together 2019

Stream: general

[Rob Lewis]

Hi everyone! @Johannes Hölzl and I are organizing a Lean workshop in Amsterdam, Jan 7-11 2019. https://lean-forward.github.io/lean-together/2019/ The meeting will also be a "kickoff" for Jasmin Blanchette's new project, Lean Forward: https://lean-forward.github.io/

[Rob Lewis]

Please put the dates in your calendars. We'd love to see lots of you there.

[Kevin Buzzard]

So lean-forward is doing number theory in Lean, but there are no number theorists involved? This is just like the ERC grant which Cambridge holds -- they want to do maths but there are no mathematicians? Is this some big grant which was recently funded? CS grant funding agencies are funding computer scientists again and again to do mathematics, but mathematics funding agencies do not seem to be (other than Sloan and Hales I guess). I should probably apply for some money. I wonder what the maths funding agencies would think? They might have real trouble getting referees :-/

What does "Our vehicle will be Lean, a disruptive proof assistant developed at..." mean? Is it any more disruptive than any other proof assistant?

[Patrick Massot]

Do you mean http://www.few.vu.nl/~sdn249/publications.html is not number theory?

[Rob Lewis]

Sander Dahmen is very closely involved with the project: http://www.few.vu.nl/~sdn249/

[Rob Lewis]

I think he considers himself a number theorist! He certainly approved the text in the grant proposal before it was submitted, at the very least.

[Rob Lewis]

As for the "disruptive" language, you'd have to ask Jasmin exactly what he meant.

[Patrick Massot]

He probably meant he wanted the money

[Patrick Massot]

That looks very much like grant proposal language to me.

[Rob Lewis]

That would be my guess. :)

[Kevin Buzzard]

Do you mean http://www.few.vu.nl/~sdn249/publications.html is not number theory?

Oh that's definitely number theory! It is also completely impossible to do in Lean :-/ This needs all of the Wiles/TW machinery -- is the proposal to do that in Lean? ;-)

[Kevin Buzzard]

Indeed Sander Dahmen is actually employed by a mathematics department! i retract my assertion that there are no mathematicians involved :-)

[Patrick Massot]

Russell quipped that "the method of 'postulating' what we want has many advantages; they are the same as the advantages of theft over honest toil." However, for most mathematicians, this fundamentalism is unappealing and unrealistic. Modern research on Diophantine equations often depends on the modularity of elliptic curves, which constitutes the final step in the proof of Fermat's last theorem and relies on an overwhelming amount of theory. Full formalization being unrealistic, we will embrace flexible levels of formality.

[Patrick Massot]

from the website

[Johan Commelin]

Also, Freek Wiedijk understands how mathematicians think and what they want. For example he is a CS guy that doesn't care about being constructive!

[Amin Bandali]

@Rob Lewis Will there be video recordings of Lean Together?

[Rob Lewis]

@Amin Bandali We're nowhere close to planning those kinds of details yet. We can certainly look into it closer to the event, though.

[Amin Bandali]

@Rob Lewis Thanks, that'd be much appreciated.

[Rob Lewis]

Bumping this thread up to the top! We've added a bit more information to the Lean Together website. https://lean-forward.github.io/lean-together/2019/index.html

If you're free the week of January 7-11 and want to make the trip to Amsterdam, we'd love to see you there.

[Rob Lewis]

I don't know how to coordinate video recordings of the talks. But I plan to figure it out before January 7.

[Patrick Massot]

The hotel explanations on https://lean-forward.github.io/lean-together/2019/index.html are a bit vague, so we may end up very scattered if everyone tries to find a hotel independently. It would be friendlier if we coordinate a bit. Are there already people here who studied the question and decided something?

[Rob Lewis]

It's a bit vague because I don't know anything about hotels in Amsterdam and just copied from Jasmin's last workshop website. :slight_smile: If I remember right, some people at that workshop stayed at the Amsterdam Forest Hotel and didn't complain. It's close to the university, farther from the more exciting parts of town.

[Patrick Massot]

I'm not complaining, I really mean what I wrote: I'd prefer to stay in the same hotel as other participants, so let's coordinate.

[Simon Hudon]

Sometimes conferences have deals with specific hotels. That might kill two birds with one stone

[Kevin Buzzard]

I am pretty sure that my _department_ has various agreements with specific local hotels.

[Rob Lewis]

Sure -- if you decide on something I'm happy to update the website and point people in that direction. Our university has some kind of arrangement with some hotels, but I'm told they're expensive and the closer hotels aren't part of it.

[Rob Lewis]

Not sure if our little workshop has the sway to negotiate a group rate, heh.

[Patrick Massot]

It should be university level negociation, not workshop level

[Rob Lewis]

Yeah, ideally, but based on what I'm told about booking hotels through the university, someone's already messed that negotiation up.

[Rudi Grinberg]

just to confirm, is there an attendance fee?

[Rob Lewis]

No attendance fee. Coffee breaks are on us, but you're all paying for your own lunches. :smile:

[Simon Hudon]

You have a lot to learn about attracting grad students. No free food? Tsk tsk tsk

[Rob Lewis]

I thought it was more important to give our visitors the traditional Dutch experience: overpaying for individual slices of bread and cheese at the cafeteria. Typisch nederlands!

[Simon Cruanes]

Will there be videos of the talks, or a webpage collecting all the speakers' slides? For those who can't attend because they're too far away?

[Rob Lewis]

Slides, for sure. Videos/streaming will be available assuming I (or someone else) can figure out how to do it.

[Rob Lewis]

A reminder, now that the meeting in Freiburg is over: we'll meet again in Amsterdam, Jan 7-11. There are 46(!) registered participants so far. We'll have a number of talks, including from Sebastian about Lean 4 and Tom Hales about progress on the Formal Abstracts project. All are welcome to join, and if you'd like to give a talk yourself, please tell me reasonably soon.

[Rob Lewis]

https://lean-forward.github.io/lean-together/2019/index.html

[Rob Lewis]

Hi all, we've posted a very tentative schedule of talks: https://docs.google.com/spreadsheets/d/e/2PACX-1vTE9MXMytWN-IQm6xBvSsWCa4Rc0QMFrp2P81pfDr9zqS-kf0wTLhU5UGVbgVzMxGieeiBLzKtyDdiG/pubhtml#
Now is your chance to complain about the timing! If you were hoping to give a talk but never told me, you should tell me soon. And if you haven't sent me a title yet, you should do that before I start making them up for you.

[Rob Lewis]

(Notice that there are tabs at the top of that page. You can click on them to see all the titles and abstracts we've gotten so far.)

[Johan Commelin]

I am really looking forward to Lean Together! You've got a fantastic crowd of people coming together.

[Johan Commelin]

(Scroll down to the bottom if you want to read the question first :upside_down:) Here is one challenge that we might want to think about. There will be a bunch of mathematicians attending the conference that have no prior experience with ITPs as far as I know. (I know at least three participants come from the Dutch arithmetic geometry community.) The goal of this workshop, and of Lean Forward in general, is to work towards ITPs that are actually used by mathematicians; and that is exactly what my goal is (and Scott's, Patrick's, Kevin's goal as well). I know that mathematicians have not shown very much dedication towards ITPs, and this might be frustrating for some people from the CS side. To make these people stay we will have to address the following issue:
These people work with abelian schemes, Galois representations, F-isocrystals, Artin stacks, etc... these notions are not fancy for them, they are their basic Lego blocks. These concepts have been around for at least 30 years, more like 60. When they visit Johannes's talk on what's in mathlib, they will find that schemes and perfectoid spaces haven't made it into mathlib, even though Kevin (and Kenny, Patrick, me) have been working on them for around a year.
And then they will remember the talk from the day before, about Lean 4, and how that's around the corner. And they will hear some chat during the coffee breaks that porting to Lean 4 is going to be a bit of a nasty issue. And they will realise that none of their basic building blocks has ever made it into Coq, Isabelle, Mizar, or whatever.
So... long story short: how are we going to convince them (and me?) that all this formalisation effort is not ephemeral, and that ITPs should stabilise in the near future?

[Andrew Ashworth]

hmm, but I don't think they will stabilize in the near future

[Andrew Ashworth]

it is ephemeral, but each bit of code reduces the effort needed to write it again when the next best thing comes out

[Andrew Ashworth]

After all, a translation of a book is much easier to write than coming up with the original ideas to begin with...

[Johan Commelin]

We currently are only translating mathlish to Lean. And its taking forever...

[Johan Commelin]

We don't even have a working definition of perfectoid spaces yet. And that definition is completely useless without theorems about them. To prove interesting theorems requires at least 10x as much work as defining them. So there we are 3 mathematicians working on a definition for 1 year. My guess is that we are 10 years away from using "almost mathematics" to compare the "etale site" of a "perfectoid field" with its "tilt". That theorem would be immensely useful, but all those words need a lot of work to get them into Lean. We could crowd source this, but the crowd will only help if their work doesn't become obsolete before it is even finished.

[Andrew Ashworth]

Ahh, I would agree with Leo here - ITPs are probably not for you if all you are interested in is the mathematics

[Andrew Ashworth]

after all, it takes years to become an expert user like Mario or Johannes

[Andrew Ashworth]

you can't even convince programmers to formally verify their software :p so why should the working mathematician? even so, I appreciate that people are interested in ITPs, and these early adopters will surely influence future progress in the area

[Scott Morrison]

how are we going to convince them (and me?) that all this formalisation effort is not ephemeral, and that ITPs should stabilise in the near future?

Because now that Lean makes it possible for even mathematicians to write new tactics, we're seeing all sorts of new kinds of automation appearing, reducing the barrier of drudgery usually imposed by an ITP.

(And this automation runs quickly, and is being enthusiastically adopted in the mathematical library, and .... oh.)

[Johan Commelin]

(And this automation runs quickly, and is being enthusiastically adopted in the mathematical library, and .... oh.)

Well... we're working on the caching, right (-;

[Johan Commelin]

@Scott Morrison So your answer is... maybe Lean 3.4.x is just good enough for us. And otherwise we'll make one more transition to Lean 4, but then we should be fine?

[Scott Morrison]

No... There's another decade at least of throwing out old theorem provers in favour of new ones.

[Scott Morrison]

And maybe we never get there; it's not as if programmers have run out of enthusiasm for new programming languages, 64 years after FORTRAN.

[Scott Morrison]

But maybe we'll get something like TeX: good fundamentals, extensible enough you never need to throw it out, that the mathematicians can happily grow old with. :-)

[Scott Morrison]

I think we should be enthusiastic about throwing out theorem provers.

[Scott Morrison]

I think in some ways it's a bit sad that there are relatively few "converts" from Coq and Isabelle/HOL to the Lean world. Those worlds did a great job of building community, funding, infrastructure, jobs for people, etc, and so of course they have strong attachments. But it's too much to expect individuals to change. :-)

[Johan Commelin]

But how can we ever work with perfectoid spaces if we are constantly change theorem provers?

[Scott Morrison]

Just remember that when Mean comes along, even if you're at the time invested in Lean 7, to advise the youngsters to try it out instead. :-)

[Johan Commelin]

We'll spend all our time reproving Hilbert basis.

[Scott Morrison]

Depressing, isn't it.

[Andrew Ashworth]

I don't think it will be that big of a change, after all, it will still be based on dependent type theory

[Andrew Ashworth]

the tactics may change but the lemma and theorem statements, and how they are constructed from underlying building blocks, i.e., the theory design, that will be the same

[Johan Commelin]

We really need something as stable as TeX. And I don't see why we can't. We just need to convince Knuth to dedicate TAOCP 4.d to ITP's instead of whatever is on his list.

[Scott Morrison]

It will be a great opportunity to rewrite proofs in a more readable and maintainable form. :-)

[Scott Morrison]

Yeah, I've decided to just be naively optimistic that Lean 3 to Lean 4 will be a doable migration.

[Johan Commelin]

Right, but why do you think mathematicians should get involved, if you also want to change their tooling every 2 years?

[Scott Morrison]

I mean, in the long run, what's this bullshit about begin ... end blocks and this strange Haskell like syntax for writing mathematics? I want to work with an interactive theorem prover inside a \begin{proof} ... \end{proof} block, in natural language.

[Scott Morrison]

Until we get there, we'll keep throwing out ITPs.

[Andrew Ashworth]

I mean, they don't have to change their tooling... you are welcome to fix a Coq release version, or HOL, as you like

[Andrew Ashworth]

and indeed, that is what industrial users do

[Johan Commelin]

Right so we want to write an ITP in COBOL :grinning:

[Scott Morrison]

Once we get there, you can upgrade under the hood as long as your upgrade can still read all the old (natural language) proofs, or at least go over to a blackboard with the previous version and hash it out. :-)

[Johan Commelin]

@Andrew Ashworth But maths is such a big interconnected web that we need the entire world-wide community to fix the same version.

[Johan Commelin]

Otherwise I can't make use of my collaborators library.

[Scott Morrison]

It's just a long project. Wishing that everyone could fix on a version is no good if that version is as hopeless as Lean is today.

[Johan Commelin]

Catch 22

[Scott Morrison]

(And I mean that in the most positive way possible: Lean is awesome compared to the alternatives, in my view.)

[Patrick Massot]

When they visit Johannes's talk on what's in mathlib, they will find that schemes and perfectoid spaces haven't made it into mathlib, even though Kevin (and Kenny, Patrick, me) have been working on them for around a year.

I think it's a bit misleading to say we've been working on perfectoids for around a year. One year ago I was about to install Lean (Github says I managed to install Lean on November 25th, it's almost my Lean birthday!) and you were pretty far away if I remember correctly. Since then we (Kevin, you and me) have been using Lean only part-time, and the perfectoid project began on June 2nd. More importantly, as I told you in Freiburg, we need to read again and again the second message in the perfectoid thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/Perfectoid.20spaces/near/127308229 We asked "what should we do?" to one of the (two or three?) people who worked from the beginning to the end on the single huge pure math formalization project ever. And then we completely ignored the answer, and didn't write a detailed roadmap. I think there is hope for more efficient future projects.

[Rob Lewis]

Indeed, I have no desire to try to tell a crowd of mathematicians that "all this formalisation effort is not ephemeral, and that ITPs should stabilise in the near future." Neither of these statements are true, at least from a mathematical perspective. But that doesn't mean that there's no value in working on these projects right now, and it shouldn't stop people from doing that work if they understand the situation.

The audience here won't be a random selection of people. They'll all have been convinced to attend a workshop specifically about formal mathematics. If they learn the current state of things and get scared off, it doesn't bother me so much -- we won't have to deal with them complaining about why nothing works. :) The point is to catch the people who are interested enough to deal with all the shortcomings, and get them to help fix some of those shortcomings.

With that said, there's probably a better ordering of talks that puts some more optimistic ones earlier on. The schedule is guaranteed to shift around before January and I'll keep this in mind!

[Simon Cruanes]

Maybe proofs written in a hierarchical style (with intermediate steps spelled out with have φ₁; have φ₂; …) would help make them robust and portable across versions? One could rely on ATPs to re-prove the low-level steps when changing versions…

[Rob Lewis]

We now have 60 people registered for Lean Together. That's, like, twice as many as we were expecting. Exciting!

[Rob Lewis]

For those who were asking about recordings a while back: the talks will be streamed and recorded by people from the VU A/V department. Much better than me pointing a webcam at the front of the room.

[Johan Commelin]

@Rob Lewis @Johannes Hölzl I guess all speakers will be using slides for their talk; at least I will. But is there also a blackboard in the lecture room?

[Johan Commelin]

I might want to do some improvised sketches using chalk...

[Rob Lewis]

I think there's a whiteboard. Definitely either a whiteboard or a blackboard, but I can't remember which.

[Patrick Massot]

Did you prepare a large supply of whiteboard pens?

[Rob Lewis]

Of course, there's a large supply in the department office next to my office.

[Kevin Buzzard]

I definitely want to do some improvised sketches using whiteboard pens. I am not even sure I will have any pdf slides, but I will want to use Lean with my laptop.

[Andrew Ashworth]

Do lecture rooms still come with chalkboards? I haven't seen one since the 90s.

[Patrick Massot]

Sure!

[Patrick Massot]

But probably only in maths departments...

[Andrew Ashworth]

I did read that there was a huge uproar when some Japanese manufacturer of chalk went out of business. https://gizmodo.com/why-mathematicians-are-hoarding-this-special-type-of-ja-1711008881

[Mario Carneiro]

hagoromo, I'm sure

[Mario Carneiro]

only time I've ever seen brand loyalty for chalk

[Andrew Ashworth]

I had no idea people actually liked chalkboards better than whiteboards until I read that article

[Johan Commelin]

@Kevin Buzzard I remember there was lots of confusion in Orsay about when someone qualifies as a mathematician. Maybe we finally have some sort of binary test :lol:

[Kevin Buzzard]

I miss blackboards

[Kevin Buzzard]

I still use whiteboards, especially when lecturing to 3rd or 4th years

[Gabriel Ebner]

Hello! I'm currently on the bus from Schiphol to Amstelveen and I'm staying at the Amsterdam Forest Hotel in case anybody wants to meet up.

[Patrick Massot]

I'll stay there too, but my train should arrive in Amsterdam on Sunday at 20:44, so I guess I'll see people only on Monday morning

[Sebastian Ullrich]

I should arrive at the hotel at around the same time

[Patrick Massot]

But I guess you'll have dinner before arriving, right?

[Sebastian Ullrich]

Haven't planned that far yet...

[Kevin Buzzard]

Can someone post some instructions on how to get from "Vrije Universiteit Amsterdam, De Boelelaan 1105" (which google maps can find) to "Main building, room Agora 1 (floor 3)" (which I can't get it to find)? Or a direct google maps link to the main building or whatever? PS I will be arriving late on Sunday and am not staying at Forest (too slow; I only bought tickets etc after my course had finished).

[Rob Lewis]

De Boelelaan 1105 is the main building. Don't be confused if Google Maps calls it the Hoofdgebouw. There are signs inside that will direct you to the Agora rooms.

[Johan Commelin]

@Kevin Buzzard Are you travelling together with Kenny? He speaks Dutch...

[Rob Lewis]

There's also a map on the website that identifies the main building. The Agora rooms are roughly right above where it says 1105, I think.

[Rob Lewis]

Note for the Americans coming, European "floor 3" is really the 4th floor. :slight_smile:

[Kevin Buzzard]

Great, thanks. No, I'm not travelling with Kenny, I think Kenny and Chris sorted their flights out ages ago; I only just bought mine a few days ago.

[Patrick Massot]

I have a better plan for finding the room. Is there anyone staying at the forest hotel who knows how to go to the lecture room, and how long it takes? If yes then I'd this person to tell me at what time we should meet for breakfast.

[Rob Lewis]

I just made a new stream for the workshop so we can avoid spamming people who aren't coming. #Lean Together 2019

[Patrick Massot]

Don't they deserve to be spammed?