Lean maths in Orsay

Stream: general

[Patrick Massot]

Hopefully, everybody potentially interested already knows, but I'd like to make sure nobody is surprisingly around, or surprisingly interested in pure math. There will be a small Lean mathematically inclined users meeting in Orsay (near Paris) on August 27th-29th. The main idea was to capture people who will be in Dagstuhl on the preceding week but are usually on other continents. There will be Chris, Johan, Johannes, Kevin, Mario, Rob, Scott, and me. Hopefully we'll have fun with advanced math and Lean.

[Johan Commelin]

Are Chris and Kevin also from another continent?

[Kenny Lau]

they'll soon be

[Patrick Massot]

Johan, I guess you never went to the UK, right? I spent six months in York when I was undergrad, and I was called an "overseas student". I was "from the continent". And this was almost 15 years before Brexit.

[Patrick Massot]

More seriously, that part of the message was meant as an excuse for the somehow inconvenient dates. Of course I'm super happy to also have people would could come to Orsay at any time.

[Kevin Buzzard]

It is absolutely true that in this country we describe holidays in e.g. Spain as "holidays in Europe". That has been true for at least 30 years. We have an island mentality here.