Lean workshops 2023

Stream: general

[Alexander Bentkamp]

My colleagues (@Jon Eugster, @Marcus Zibrowius, Immi Halupczok) and I are considering to organize a “Lean for the Curious Mathematician" workshop in Düsseldorf in the week 04.–08 September, 2023.

Now we’ve found out that @Rob Lewis and @Sander Dahmen are organizing a similar workshop in the Netherlands in July;
@Dagur Ásgeirsson and @Boris Kjær are organizing a masterclass in Lean formalization in Copenhagen in June;
and @Heather Macbeth and @María Inés de Frutos Fernández are organizing a workshop for women in Edinburgh.

So we are thinking about whether the market for Lean workshops in 2023 is saturated already. I'd like to avoid a situation where we are competing against each other, especially regarding potential speakers. I'd be grateful about any thoughts on this.

[Johan Commelin]

In general, see https://leanprover-community.github.io/events.html for a list of upcoming events.
@Rob Lewis @Sander Dahmen @Heather Macbeth @María Inés de Frutos Fernández it looks like your events are not yet listed.

[Johan Commelin]

The Copenhagen event is somewhat specialized, so I don't think that causes "competition".

[María Inés de Frutos Fernández]

We still don't know the dates of our workshop (we have received confirmation that it was approved, but we are waiting for more details). Should we list it with date TBA?

[Johan Commelin]

Yes, that sounds like a good idea

[Johan Commelin]

Does the format support that?

[Trebor Huang]

2023 sounds just so futuristic to me. I didn't realize it's in a few weeks!

[Kevin Buzzard]

Regarding LFTCM -- is this somehow going to become a "flagship event" organised by the community every two years, or is it more flexible? My understanding is that we had one in 2020 and 2022, and the 2024 meeting has already been booked.

[Alexander Bentkamp]

I also talked to @Jeremy Avigad about this. Apparently there is a LFTCM admin team, and Jeremy is one of them. I don't know who the others are.

I wasn't aware that it was supposed to be only every second year. In that case, we'll probably reconsider and only do a smaller workshop or none at all.

[Johan Commelin]

Well, I guess it could also be yearly... We just missed 2021...

[Jeremy Avigad]

We don't have anything as specific as an LFTCM admin team! I fielded Alex's query as a member of the general admin team, in our role as "the first point of contact for the community as a whole."

This raises the question as to how best to coordinate meetings. For now, the general feeling among the admin team and maintainers is that we don't need anything very formal yet. Someone who wants to hold a meeting is advised to check with the admin team first for information and advice, and then they are advised to announce the plans on a public Zulip stream for feedback. When plans are settled, the meeting should be listed on the events page.

Maybe, for planning purposes, it would be helpful to list tentative events on the events page, in a special category with the label "tentative" or "in planning"? That way, anyone planning to hold a meeting will be able to see what others are working on.

My personal opinion is that we shouldn't limit the LFTCM meetings. If the community can sustain a dozen a year, why not? We can distinguish them with location and year, e.g. "Lean for the Curious Mathematician, Providence 2022". It's really just a matter of having sufficient resources and having enough of an audience to make it worthwhile.

On the other hand, I can see that it might be nice to have regularly scheduled Lean Together meetings with a standard format and community guidelines. If we get to that stage, we should probably set up a meetings team. (Conferences in CS have "steering committees," whose main job is to twist arms to find organizers every year.)

[Jeremy Avigad]

With all that, I never addressed Alex's question. I don't know whether having two LFTCMs so close together (chronologically and geographically) makes sense, since it might mean that they are competing for participants. I wouldn't object to it, but it might make more sense to stagger them more. We still don't have a good sense of how many people an in-person meeting will draw.

[Patrick Massot]

I agree with the general comments Jeremy wrote. And also Leiden in July and Düsseldorf in September seems really close. However the Leiden thing is less specific. It will not be only about Lean.

[Patrick Massot]

In particular the Leiden thing will definitely not be called LFTCM something.

[Patrick Massot]

It seems to be called "Machine-Checked Mathematics". But maybe I was dreaming it will mix Coq and Lean based on the fact that Assia is an organizer.

[Patrick Massot]

https://www.lorentzcenter.nl/machine-checked-mathematics.html

[Patrick Massot]

It still feels like doing the Dusseldorf one a bit later would be better.

[Heather Macbeth]

Jeremy Avigad said:

My personal opinion is that we shouldn't limit the LFTCM meetings. If the community can sustain a dozen a year, why not? We can distinguish them with location and year, e.g. "Lean for the Curious Mathematician, Providence 2022". It's really just a matter of having sufficient resources and having enough of an audience to make it worthwhile.

I agree with this. The Sage community has "Sage Days" and they have now reached Sage Days 116.
https://wiki.sagemath.org/Workshops

[Patrick Massot]

Sage days are much lighter than LFTCM. Anyone can organize one to gather a couple of friends.

[Eric Rodriguez]

maybe we should encourage chill Lean events too :)

[Kevin Buzzard]

Wasn't that what my September workshop was?

[Kevin Buzzard]

On a less chill note, if someone is going to look through this thread and round eveything up into some table it might be worth mentioning that AIM have just agreed to fund a virtual Lean workshop in formalising algebraic geometry, June 24-28, 2024, organised by myself, Johan Commelin, Adam Topaz and Joel Riou. There will be some more formal announcement nearer the time (this is over 18 months away!)

[Marcus Zibrowius]

Patrick Massot said:

It still feels like doing the Dusseldorf one a bit later would be better.

Both our limited funding and human resources at Düsseldorf are tied to 2023, and September is the last month before teaching starts. So if we stick to a week long format, there's not much leeway. If we limit ourselves to a weekend event, we could move it to later in the year.

[Marcus Zibrowius]

I have zero experience in organizing Lean workshops, but I'm much less worried about finding participants than finding speakers & instructors for tutorial sessions.

[Marcus Zibrowius]

If we go in the direction of hands-on tutorials, then it would seem to me that 20-30 participants would already be a good number to work with, and surely it wouldn't be a problem to find that many participants across Germany?? I think we might even fill half the room with participants from Düsseldorf. But even for this number of participants, we would need some experienced (non-local) instructors.

[Marcus Zibrowius]

If we go more in the direction of presentations, then the number of participants will strongly correlate with the number of high profile speakers, and again, this is where I imagine the bottleneck.

[María Inés de Frutos Fernández]

Johan Commelin said:

Does the format support that?

Does any want know this? I don't know how the start_date and end_date fields in events.yaml are processed.

[Patrick Massot]

The format doesn't support that yet. I'll fix it. For future reference, those kind of questions are answered in https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/make_site.py. If you search for event in that file you'll get an answer.

[Kevin Buzzard]

Do you know @Clara Löh ? She is in Germany and has been using lean in her teaching

[Alexander Bentkamp]

I keep hearing about her, but we never met. She would definitely be a great speaker to have at the workshop.

[Clara Löh]

To add to the list (even though we are not as far with the organisation as we wanted to be ...): Philipp Rümmer, Denis-Charles Cisinski, and I are organising a workshop/summer school in Regensburg (Germany) 18--29 September 2023 on proof assistants and their use in mathematics and computer science. Thus, the scope will be wider on the theoretical and application side, and we will cover several proof assistants (including Lean, of course).

[Clara Löh]

My impression is that many math students are interested in learning more about this technology (and way of thinking/working) and that there overall might not be enough options in Germany to do so.

[Clara Löh]

@Alexander Bentkamp of course, I would be happy to meet at some point :)

[Jeremy Avigad]

Sorry to be slow to catch up. I spent yesterday on airplanes to traveling to visit my in-laws in San Diego, and now I am on California time. The good news is that we seem to have escaped a brutal winter storm that is pounding the most of the US.

Since Marcus isn't worried about participants, I think we're all enthusiastic a meeting in Dusseldorf. @Alexander Bentkamp @Marcus Zibrowius, in a moment I'll start a private thread with Heather, Patrick, Johan, and me so that we can talk about organization.

It's nice to see so much meeting activity! I guess this thread will serve as a place for people to share their plans.

[Tyler Josephson ⚛️]

I’m thinking about launching a Lean for Curious Scientists and Engineers workshop here in Maryland / online. Nothing official yet. I’m thinking we’d cover a mix of topics around FPIL and TPIL, guiding students in writing a program that performs some basic scientific calculation (like SciLean) as well as a proof about the math / code. I’d want this fully in Lean 4; mathport progress would affect the extent of what we can prove - having single variable calculus and limits by then would be helpful.

[Kevin Buzzard]

Will you need to relate float to real?

[Tyler Josephson ⚛️]

Good question. How are those related in Lean? Can we just write proofs with reals and implement them numerically with floats?

I’m personally more interested in “the mathematics of the software corresponds to the theory” than in “let’s be sure that floating point arithmetic errors don’t accumulate and lead to qualitatively bad numerical results.” Though we do need the second to be really sure about the results, especially in certain contexts like stiff ODEs or ill-conditioned matrices, those are old problems; formalizing the high-level mathematics of software is a newer challenge, and more interesting to me.

[Kevin Buzzard]

Right now they are 100% unrelated in lean, I believe.

[Henrik Böving]

There has been quite some discussion on how to relate them in #lean4 before but iirc all the attempts to get this done in a quick fashion were fruitless. Furthermore the fact that we define docs4#Float in Lean 4 in a way that makes them close to impossible to argue about in non trivial scenarios on their own already, because the Float type is really only a quick facade for C level floats with close to no support on the proving side of things, won't make establishing this connection easier either :/, not even taking into account the connection to reals stuff yet.

We could in theory attempt to write meta programs that mechanically translate things on the reals to things on floats (of course not translating things from the reals that have a native float implementation such as say arithmetic and trigonometric functions) without a proof that they are equivalent (whatever equivalent might mean in this context) if that is of interest.

If anyone does have concrete ideas or pointers for how to get this done in a way that does actually have these ideas of some form of equivalence and automated translation I'd be very interested in that, the problem has stayed on my mind ever since the mentioned #lean4 discussions^^

[Tyler Josephson ⚛️]

I think there’s interest, beyond just me. For example, one way to do this is described here: https://arxiv.org/abs/1706.08605

“We have proved that our system is correct in an idealized mathematical context with infinite-precision real numbers. To actually execute the system we need to replace all real numbers in the program with floating-point numbers. Although doing so technically invalidates the specification and can introduce numerical instability in some cases, this class of errors is well understood (Higham, 2002), could be ruled out as well in principle (Harrison, 2006; Boldo et al., 2015; Ramananandro et al., 2016) and is conceptually distinct from the algorithmic and mathematical errors that our methodology is designed to eliminate.”

[Henrik Böving]

So the way this stuff is implemented is rather hacky IMHO. Basically they have a definition of a tensor and the mathematical primitives here: https://github.com/dselsam/certigrad/blob/master/src/certigrad/tensor.lean (they avoid doing all of the mathematics by stating all of this stuff as axioms, in principle I believe their approach could also work out when actually doing all of this mathematically)

And then they have a Lean 3 fork that adds executable code for their library functions: https://github.com/leanprover/lean/blob/dd0ade03fc7c90825d03429fd6823b112e86cc67/src/library/vm/vm_eigen.cpp#L443 through eigen.

This is more or less the same as if we told the Lean runtime that the real numbers are equivalent to floats and tagged all the primitive real functions with their native implementations, both achievable via the @extern attribute right now. If people want it to do this way (this is more or less the same as "write meta programs that automatically do the conversion" with the difference that the meta programs already exist in form of the Lean compiler) we can do that of course. But I have a feeling mathematicians might be opposed to the idea of essentially telling the runtime and compiler float = real.

[Henrik Böving]

I think one might in fact be able to derive False using this approach + native_decide.

[Mario Carneiro]

using floats and native_decide you are already dangerously close to being able to prove false just by using oleans across architectures that vary in the implementation of floats

[Tyler Josephson ⚛️]

Henrik Böving said:

So the way this stuff is implemented is rather hacky IMHO. Basically they have a definition of a tensor and the mathematical primitives here: https://github.com/dselsam/certigrad/blob/master/src/certigrad/tensor.lean (they avoid doing all of the mathematics by stating all of this stuff as axioms, in principle I believe their approach could also work out when actually doing all of this mathematically)

Oh I agree. Indeed, this was 5-6 years ago; with mathlib, we can do the mathematics right. We can also execute in Lean 4 or in compiled C, rather than link to a library like they do. But as a proof of concept for software development, I appreciate this.

[Henrik Böving]

No this is not the part that I find hacky. The axioms is just stuff that we know how to resolve in Lean already, they just did it this way because they didn't want to do the job of mathlib essentially, that's perfectly fine of course. The hacky part about this (to me) is how they make the connection between the reals/tensors and the computable floating point numbers. It is basically declaring an equivalence between them and while that's possible in Lean 4 easily, we'd just write

@[extern "lean_float_add"]
def Real.add : Real -> Real -> Real := ...
-- the type declaration and integration gets a little bit trickier but still doable

it feels very hacky since it is breaking the contract that the extern implementation should be equivalent to the one in the system which can actually break the system if you poke it hard enough. And that's something we do definitely not want in a fleshed out implementation. And the open question for Lean 4 is mostly, how do we tie reals and floats together in a way so this does not happen, the mathematics around reals, how we can interact with extern code is solved problems.

And to my knowledge right now nobody has an idea how to teach this connection properly to Lean 4 :(

[Kevin Buzzard]

Fully expecting the answer no: are there functions lower, upper : Float -> Real with the property that "the real number modelled by f : Float" (whatever that means, if it means anything at all) is in the closed inteval [lower f, upper f] and for all the operations in (whatever operations computer scientists deem are the canonical operations on Float) there are corresponding compatible interval arithmetic theorems in Real, e.g. lower(f)+lower(g) <= lower (f+g) and upper(f+g) <= upper(f)+upper(g)?

[Kevin Buzzard]

I'm fully expecting edge cases to break even naive hopes like this (I don't know the first thing about floats)

[Mario Carneiro]

No, that one is not true even without float weirdness. There needs to be an interval extension of + in there somewhere, because you have provided no way for the bounds on a number to grow as you apply more operations

[Mario Carneiro]

The natural choice for lower and upper there are the rounding limits of the number, i.e. +- 1 ULP from the float's real value (in the finite case), but if you add two numbers with a 1 ULP bound you get a number with a 2 ULP bound

[Kevin Buzzard]

Right -- I'm allowing the bounds to grow -- I'm only asking for inequalities. So the more stuff you do to real numbers the less accuracy you have.

[Kevin Buzzard]

I'm suggesting that you can link floats to interval arithmetic, but I'm not suggesting that you can get back.

[Joseph Myers]

For examples of calculations of how ulp errors propagate in floating-point arithmetic, see e.g. the start of https://www.mpfr.org/algorithms.pdf (working with interval arithmetic is likely to be simpler in many cases, but also slower). Note that those calculations assume an unbounded exponent range; underflow and overflow add extra complications.

[Junyan Xu]

Maybe relevant:
Hales, A Revision of the Proof of the Kepler Conjecture mentions floating point and MPFI in p.9-10 (section 4.1-4.2).
A Verified ODE Solver and the Lorenz Attractor ("Light-weight data refinement")

both in Isabelle/HOL, unsurprisingly.

[Henrik Böving]

The second one refers to this: https://home.in.tum.de/~hoelzl/documents/hoelzl09realinequalities.pdf which does make use of interval arithmetics on floating point numbers.

[Henrik Böving]

"We overload the polymorphic constant real to interpret float values as real value" /o\ et tu!

[Junyan Xu]

The author is apparently on this Zulip but the last activity was in 2019 ...

[Mario Carneiro]

Yes, Johannes Hoelzl is one of the founders of mathlib, although he's gone radio silent since he went to Apple