Meeting (virtual and informal) for Lean and science

Stream: Natural sciences

[Joseph Tooby-Smith]

I would like to gauge interest in having an informal virtual meeting on the interface of Lean and science (broadly defined).

The main goal of the meeting would be to get to know others working in this area, and the sorts of things being worked on in this domain. The secondary goal would be to share ideas and feedback etc.

If more than four people say they are interested, I will set up a poll for a potential date and time.

[Tyler Josephson ⚛️]

Interested! I will send 4+ students from my group.

But - starting this summer we’ll also be leading a course to introduce newcomers to Lean, “Lean for Scientists and Engineers.” No official announcement yet, but that’ll be something coming up.

[Kim Morrison]

@Tyler Josephson ⚛️, it would be great if you could make a PR to https://leanprover-community.github.io/teaching/courses.html with details about the course when it is ready!

[Joseph Tooby-Smith]

/poll If people are still interested in such an informal meeting, here are some suggested time (feel free to suggest others)
2024-07-12T13:00:00+00:00
2024-07-15T14:00:00+00:00
2024-07-18T15:00:00+00:00
2024-07-26T16:00:00+00:00

[Joseph Tooby-Smith]

(Not sure how to adjust formatting of above message.)

[Thomas Murrills]

Note: there's an open PR on the zulip repo which will fix this! (Last activity was 4 months ago, though.)

In the meantime, maybe a separate message containing an ordinary numbered list with the times (and each poll option referring to a number) would be a workaround?

[Joseph Tooby-Smith]

Thanks @Thomas Murrills .

Here is a list of possible times:

1. 2024-07-12T09:00:00-04:00
2. 2024-07-15T10:00:00-04:00
3. 2024-07-18T11:00:00-04:00
4. 2024-07-26T12:00:00-04:00
5. 2024-07-15T13:00:00-04:00
6. 2024-07-22T14:00:00-04:00

[Joseph Tooby-Smith]

/poll What time would work?
1
2
3
4

[Joseph Tooby-Smith]

Given there seems to be no clear 'winner', I've added two more options. If there is still no clear 'winner' by Thursday, let's default to the most popular option which is furthest away from now.

[Joseph Tooby-Smith]

Given the above: Let's meet at 2024-07-26T12:00:00-04:00 , on a zoom link I will prepare closer to the time and post here. Anyone else should feel welcome to join.

[Joseph Tooby-Smith]

Here is a zoom link for the above, happening this Friday: Join Zoom Meeting

https://cornell.zoom.us/j/98897918171?pwd=cFVS1qF5bENehgca0oiomxDnRVgmeN.1

Meeting ID: 988 9791 8171

Passcode: 062305

[Joseph Tooby-Smith]

(starts in about 10 min)

[Tyler Josephson ⚛️]

How was the meeting? Sorry to miss it, was traveling with family. Hope to catch the next one!

[Joseph Tooby-Smith]

Hope your travel went good @Tyler Josephson ⚛️.

It went well! Lots of interesting discussions and it was great to meet everyone!

There was a consensus that we should do it again sometime. Someone suggested to me that using e.g. http://when2meet.com might make it easier to schedule things like this. But I'm open to other ideas.

[Joseph Tooby-Smith]

Anybody up for another such meeting sometime soon?

[Britt Anderson]

I would be very interested in joining. I am in a cognitive neuroscience division in psychology and part of a centre for theoretical neuroscience, and am very interested in the idea of writing code in a language that has the potential to offer the sort of guarantees Lean can offer. I just don't know if it is practical for me, but I would love to hear the discussions. I think my zulip tag/email may be an obfuscated one. For any direct communication just email: britt@uwaterloo.ca (Britt Anderson)

[mars0i]

I can't advocate for having a meeting, but if there is a meeting, I would love to sit in on it if I can. Not sure I'd have much to contribute.

[Joseph Tooby-Smith]

Ok, seems to be enough interest. So to pick a good time, please could people wanting to attend fill out:

https://www.when2meet.com/?27546423-YGhSH

I believe you just have to give a name (doesn't need to be your real one) and when you are free - no need to make a password etc. I will put a pick a popular time on Friday or over the Weekend. Thanks!

[Joseph Tooby-Smith]

Ok, looking at when people are free, seems like there is a natural time to meet:

2024-11-19T19:00:00Z

So let us meet then!
I moved institution and no longer have access to a paid zoom account. Would someone who has one mind volunteering to make a zoom meeting for this?

[Britt Anderson]

Joseph Tooby-Smith said:

Would someone who has one mind volunteering to make a zoom meeting for this?

https://uwaterloo.zoom.us/j/98435874101?pwd=ntcsf5UWyiWbvGyEYrYHDftZbYtUZU.1

[Joseph Tooby-Smith]

Reminder: This starts in about 2 hours. Anyone with an interest in science + lean is welcome to join!

[Joseph Tooby-Smith]

Thanks to everyone who turned up to this. It was great to meet everyone!

Towards the end, the idea was put out there of starting a collaboration effort on some (yet to be determined) science-Lean related project(s), and to hold regularly scheduled meetings with this goal in mind.

The aim of the first such meeting would be to work out exactly what project(s) we would like to work on. If you are interested in getting involved in something like this (as I believe at least three of us are), here is a scheduling link for the first meeting (after which we can hopefully find a regular time):

https://www.when2meet.com/?27671949-FVuXd

[Joseph Tooby-Smith]

Ok, let us do: 2024-12-03T17:00:00Z

[Joseph Tooby-Smith]

Reminder that this is happening tomorrow. Would someone mind making a zoom link again?

[Britt Anderson]

Don't know how long I can stay, but I can always turn hosting duties over.

https://uwaterloo.zoom.us/j/4607061919?pwd=MGJFU3FwQ3ZCTjVPN0hKNE9ZR2ZOQT09&omn=91583563242

[Joseph Tooby-Smith]

Following on from the meeting yesterday. Two projects were identified as possible areas for collaboration. These are roughly described below:

Project 1 Units and dimensions: The aim would be to formalize units and dimensions into Lean in a way which is easy to use and generally applicable.

Project 2 Abstractions and scientific evidence in Lean : The aim would be to paint a clear picture about how we do science, and understand if and how scientific reasoning can be linked with Lean.

Anyone who was at the meeting yesterday, and believes I have grossly misrepresented one of the projects (which I may well have) let me know and I will edit.

If you would like to get involved in either of these projects, and feel you can make a contribution please indicate with the poll below. After which I will make private message threads.

[Joseph Tooby-Smith]

/poll Interest in projects
Project 1
Project 2

[Tyler Josephson ⚛️]

I'd just add re Project 2 that this would involve thinking about syntax and semantics in potentially new ways - that there may be many potential ways to try to bridge the "real world" (with measurements), our ideas about physics (which may be uncertain and/or informed by data), and the very high-confidence, yet highly abstract world of Lean and Mathlib.

[Eric Wieser]

I'd perhaps warn against private message threads here, since it makes it impossible to add more people later

[Alex Meiburg]

Just curious: would the units and dimensions likely be as torsors? I've thought a bit about a way to try to do this, it seems interesting but I'm not confident (or able to devote time to it atm)

[Tyler Josephson ⚛️]

We’ve been working on dimensions in Lean, and recently ported our Lean 3 version into Lean 4. We define dimension as a type and prove it’s an abelian group, along with Buckingham Pi. We haven’t figured out how to extend this to units yet.

https://github.com/ATOMSLab/LeanBET/blob/main/DimensionalAnalysis.lean

[Tyler Josephson ⚛️]

@Max Bobbin and @Colin Jones ⚛️ will be wrapping up a manuscript draft on this in the coming weeks.

[Eric Wieser]

I'm a little surprised to see that you converted to lean 4 by hand (and so got lean3-style names and syntax) rather than using mathport to get more idiomatic code

[Tyler Josephson ⚛️]

@Eric Wieser My student had trouble getting mathport to run on their computer, and since it was a short file and something rather one-off, he just did it by hand. Any pointers on how to make it idiomatic? We’d want to update it to have the right style.

[Eric Wieser]

As an example transformation,

class has_time (α : Type u) :=
[dec : DecidableEq α]
(time : α)

should become

class HasTime (α : Type u) where
  [dec : DecidableEq α]
  time : α

[Eric Wieser]

It's possible to run mathport in gitpod, which at least takes any particular student computer out of the mix