Zulip Chat Archive

Stream: general

Topic: FMM 2021

Mario Carneiro (Jul 30 2021 at 02:26):

Just a heads up for folks who want to catch it live: CICM 2021 is going on this week, and the FMM (formal methods for mathematics) workshop on Friday and Saturday contains several talks from Lean folks (agenda):

2021-07-30T13:30:00+02:00: Mario Carneiro - Porting Mathlib (invited talk) (abstract)
2021-07-30T17:00:00+02:00: Muhammad Harun Ali Khan - Formalizing Fibonacci Squares (abstract)
2021-07-30T18:00:00+02:00: Alexander Bentkamp and Jeremy Avigad - Verified Optimization (work in progress) (abstract)
2021-07-31T15:00:00+02:00: Sebastien Gouezel - Formalizing the Gromov-Hausdorff space (abstract)
2021-07-31T15:30:00+02:00: Anthony Bordg and Nicolo Cavalleri - Elements of Differential Geometry in Lean: A Report for Mathematicians (abstract)
2021-07-31T14:00:00+02:00: Kensho Tsurusaki and Akiko Aizawa - Assimilating the structure of formal and informal proof (abstract)
2021-07-31T15:00:00+02:00: Jeremy Avigad - The design of mathematical language (invited talk)
2021-07-31T16:30:00+02:00: Yury Kudryashov - Formalizing rotation number and its properties in Lean (abstract)
2021-07-31T17:30:00+02:00: Eric Wieser - Scalar actions in Lean's mathlib (abstract)
2021-07-31T18:00:00+02:00: Alexander Best - Automatically Generalizing Theorems Using Typeclasses (abstract)

Thomas Browning (Jul 30 2021 at 03:42):

Will the talks be recorded?

Thomas Browning (Jul 30 2021 at 03:43):

some of those times are a bit early for me on the west coast

Yury G. Kudryashov (Jul 30 2021 at 04:50):

Thanks for a schedule with timezone information! Do you know which software should we use to attend? I failed to find this information on easychair.

Thomas Browning (Jul 30 2021 at 05:37):

I had the same question. I registered but wasn't able to find information on how to attend the live talks.

Kevin Buzzard (Jul 30 2021 at 06:12):

Thanks so much for the timetable Mario! I'd been looking for it recently but it wasn't on the website

Sebastien Gouezel (Jul 30 2021 at 07:08):

I received an email with the following information:

Topic: FMM 2021 - Workshop on Formal Mathematics for Mathematicians
Join Zoom Meeting

https://zoom.us/j/93567544812?pwd=ZnBETlYxL01SMUx3L3NLUFd6RVFXQT09
Meeting ID: 935 6754 4812
Passcode: 2021

Maybe not supposed to be public (I guess I received the email because I registered), but Zulip is not really public so I guess it's fine to post it here.

Eric Wieser (Jul 30 2021 at 07:50):

Registration for CICM is free, so if you register you probably need to feel no guilt in clicking that link

Eric Wieser (Jul 30 2021 at 07:51):

@Thomas Browning, there seems to be a google drive with some recordings, but I don't know if the workshops will do the same

Patrick Massot (Jul 30 2021 at 09:19):

How is it possible that we never heard of this Kensho Tsurusaki and Akiko Aizawa thing? Does anyone know whether anything they did is public?

Johan Commelin (Jul 30 2021 at 09:26):

Wow, that looks quite interesting indeed

Patrick Massot (Jul 30 2021 at 09:27):

It's very hard to tell without seeing a demo, but I find it incredible that they never registered here.

Patrick Massot (Jul 30 2021 at 09:27):

I would say it's not a very good omen.

Mario Carneiro (Jul 30 2021 at 09:29):

I remember seeing another lean project from a japanese team that was using some way out of date lean and was provided via zip file on the authors' web site. I think the japanese mostly have their own internet and don't drop by this one so often

Patrick Massot (Jul 30 2021 at 09:36):

I'm also surprised to be surprised by Session 21 (Towards Formal Mathematics Activities at International Research Institutes). Are there people here who got invited? As far as I know we have quite a head start in this activity.

Eric Wieser (Jul 30 2021 at 09:38):

Note that Sebastien Gouezel's zoom link is only for the FMM track, not the NatFoM track that Kensho Tsurusaki and Akiko Aizawa are on

Eric Wieser (Jul 30 2021 at 09:43):

Patrick Massot said:

It's very hard to tell without seeing a demo

If they had a demo, I think it would be at https://github.com/Alab-NII (following breadcrumbs from https://www-al.nii.ac.jp/members/) - it's not.

Mario Carneiro (Jul 30 2021 at 09:44):

added session 21 to the agenda, as well as room names since two of the talks are in the NatFoM room instead of FMM

Alex J. Best (Jul 30 2021 at 10:53):

Patrick Massot said:

I'm also surprised to be surprised by Session 21 (Towards Formal Mathematics Activities at International Research Institutes). Are there people here who got invited? As far as I know we have quite a head start in this activity.

This was suggested as an informal thing at the business meeting yesterday, and was added to the schedule so that more people would become aware.
The brief summary of the proposal (which I think was by Koepke) is that well-respected mathematicians (i.e. Peter :grinning:) were taking note of formalization, and so its high time to apply to a bunch of research institutes (a list of some 10 or so examples were given) for semesters / programs aimed at more mathematical people (the HoTT year was mentioned as the last time anything like this really happened).
I think the business meeting was recorded if you want to take a look.

Eric Rodriguez (Jul 30 2021 at 11:05):

Eric Wieser said:

Thomas Browning, there seems to be a google drive with some recordings, but I don't know if the workshops will do the same

where is this google drive? I just registered but can't find it (nor the Zoom link, tbh, but Sebastien's link will do)

Patrick Massot (Jul 30 2021 at 12:11):

At least it should be noted that we successfully applied to summer schools in MSRI and ICERM, and almost managed IHES but failed.

Alex J. Best (Jul 30 2021 at 12:13):

I think you should go to the discussion and note that, its definitely intended as an open discussion. I didn't see too many other lean/mathlib people at the business meeting so I don't know if anyone who knows about those successes would be there.

Johan Commelin (Jul 30 2021 at 12:13):

Also the Lorentz meeting in Leiden

Mario Carneiro (Jul 30 2021 at 12:36):

Here are my slides: Porting_Mathlib.pdf

Eric Wieser (Jul 30 2021 at 12:37):

I think EasyChair has some place (edit: for presenters) to upload slides so that they appear on the program, but I haven't tried it

Mario Carneiro (Jul 30 2021 at 12:38):

cc: @Jasmin Blanchette

Eric Wieser (Jul 30 2021 at 12:39):

The button is here, accessible via the page we submitted the preprints to: image.png

Mario Carneiro (Jul 30 2021 at 12:41):

ah, got it

Mario Carneiro (Jul 30 2021 at 12:46):

@Gihan Marasingha re: lstlistings, see https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.md

Mario Carneiro (Jul 30 2021 at 12:48):

ah, reading your question again, I see you asked about a lean 4 version of this. No, I'm just using the lean 3 highlighter. I don't think any of the highlighters have been adjusted for lean 4 yet, except possibly the lean 4 vscode/emacs extensions?

Gabriel Ebner (Jul 30 2021 at 12:54):

There's also the lean 4 neovim extension which has an updated highlighter. But that's it I think.

Mario Carneiro (Jul 30 2021 at 12:57):

maybe we should try to get lean 3/4 hybrid highlighters upstreamed for use in github and zulip

Sebastian Ullrich (Jul 30 2021 at 12:58):

That would be great, the Lean 3 binder highlighting really screws up reading Lean 4 code on GitHub

Yaël Dillies (Jul 30 2021 at 12:59):

Are we also soon changing the .lean extension to .lean3?

Eric Wieser (Jul 30 2021 at 12:59):

The binder highlighting was reverted from vscode ( :sad: ), github is just very slow to update

Mario Carneiro (Jul 30 2021 at 12:59):

was that the same binder highlighting reverted from vscode?

Sebastian Ullrich (Jul 30 2021 at 13:00):

Though GH actually allows for some advanced language sniffing beyond the markdown identifier afair

Gabriel Ebner (Jul 30 2021 at 13:00):

Yes, it was reverted a few weeks ago. Unfortunately github is extremely slow to update the highlighters.

Eric Wieser (Jul 30 2021 at 13:00):

Yes. IMO the real fix here is to have an entirely separate github highlighter for lean 4 and give it => as a heuristic for distinguishing between lean4 and 3

Yaël Dillies (Jul 30 2021 at 13:00):

Uh, that's very hacky

Mario Carneiro (Jul 30 2021 at 13:00):

the lack of extension difference is a common issue for me

Yaël Dillies (Jul 30 2021 at 13:01):

Are we getting a nice \mapsto to use instead of =>, btw?

Mario Carneiro (Jul 30 2021 at 13:01):

if that is implemented, it will probably only be in mathlib

Yaël Dillies (Jul 30 2021 at 13:01):

That's fine for me :)

Sebastian Ullrich (Jul 30 2021 at 13:01):

Re. Lean 4 LaTeX highlighting, there are slightly updated versions at https://leanprover.github.io/lean4/doc/syntax_highlight_in_latex.html

Mario Carneiro (Jul 30 2021 at 13:01):

although I guess I shouldn't speak for the core team

Gihan Marasingha (Jul 30 2021 at 13:07):

On highlighting in vscode / Lean 3: it's a very uncommon issue, but you declare, say

inductive empty'

then subsequent code is not correctly highlighted.

Jeremy Avigad (Jul 30 2021 at 14:00):

I am sorry to see that my talk is scheduled at the same time as the ones by Sebastien G. and then Anthony Bordg and Nicolo Cavalleri. I am tempted to skip my talk and watch theirs...

Jasmin Blanchette (Jul 30 2021 at 14:00):

You can blame me for the scheduling (on the FMM side)...

Mario Carneiro (Jul 30 2021 at 14:03):

@Jasmin Blanchette Are the talk recordings going to end up on youtube et al? I would like my talk to be public, and that would solve Jeremy's double booking issue as well

Jasmin Blanchette (Jul 30 2021 at 14:09):

I don't know. The CICM organizers would surely know. You could ask madalina.erascu@e-uvt.ro .

Jasmin Blanchette (Jul 30 2021 at 14:09):

I'll need to find out at some point for sure. ;)

Jasmin Blanchette (Jul 30 2021 at 14:11):

They're discussing right now about whether they'll put the recording on line.

Jasmin Blanchette (Jul 30 2021 at 14:11):

Jasmin Blanchette (Jul 30 2021 at 14:16):

Doesn't sound too good...

Yury G. Kudryashov (Jul 30 2021 at 14:18):

Who holds the copyright?

Jasmin Blanchette (Jul 30 2021 at 14:21):

Who knows.

Jasmin Blanchette (Jul 30 2021 at 14:21):

If you want to join the discussion, it's happening right now at FMM during the break.

Yury G. Kudryashov (Jul 30 2021 at 14:34):

No, I don't. Still preparing for my talk.

Sebastien Gouezel (Jul 30 2021 at 14:53):

Jeremy Avigad said:

I am sorry to see that my talk is scheduled at the same time as the ones by Sebastien G. and then Anthony Bordg and Nicolo Cavalleri. I am tempted to skip my talk and watch theirs...

I'd do the same (I mean, skip my talk to attend yours, not the other way around :-)

Gihan Marasingha (Jul 30 2021 at 15:09):

Please don't both of you skip your talks.

Gihan Marasingha (Jul 30 2021 at 16:48):

@Rob Lewis , @Minchao Wu is there an idiot's guide to using the Mathematica - Lean link? (I mention this here due to the links with the optimization talk).

Mario Carneiro (Jul 30 2021 at 17:35):

I would guess that it has bitrot somewhat, it was written way back around the dawn of mathlib

Mario Carneiro (Jul 30 2021 at 17:39):

actually maybe not, it looks like leanprover-community-bot has been tending to https://github.com/robertylewis/mathematica

Kevin Buzzard (Jul 31 2021 at 09:11):

I thought the problem was that it didn't work with the most recent mathematica, not that it didn't work with the most recent lean

Patrick Massot (Jul 31 2021 at 09:58):

That was the status three years ago I think.

Gabriel Ebner (Jul 31 2021 at 10:45):

I'm pretty sure it still works with recent Lean. Rob showed me demo earlier this year, and it even showed mathematica plots using Lean widgets.

Mario Carneiro (Jul 31 2021 at 11:17):

For this morning's talks:

Topic: NatFoM 2021 - Workshop on Natural Formal Mathematics
Join Zoom Meeting
https://zoom.us/j/96006940486?pwd=SU8wWnpMZFJGR2hhZ0kzQUk1RGQyUT09
Meeting ID: 960 0694 0486
Passcode: 2021

Sebastien's link still works for FMM.

Eric Wieser (Jul 31 2021 at 12:06):

Patrick Massot said:

How is it possible that we never heard of this Kensho Tsurusaki and Akiko Aizawa thing? Does anyone know whether anything they did is public?

As a reminder, this is happening now at Mario's most recent link

Gihan Marasingha (Jul 31 2021 at 16:45):

@Rob Lewis: if you have the time, can you do a video demo of the Mathematica link?

Rob Lewis (Aug 02 2021 at 19:44):

@Gihan Marasingha Sorry for the very slow response. I don't have time right now, but I'll add it to my to-do list. I need to make minor revisions to the new journal version of the paper, so that's a good time to check the code is up to date and do a demo.

Rob Lewis (Aug 02 2021 at 19:45):

Everything was current last fall, and some things may have been touched since then. The CI bot updates aren't much of a promise though. Code compiling doesn't mean the link works fully since CI doesn't have a Mathematica install...

Oliver Nash (Aug 03 2021 at 16:13):

I missed a few of these talks. Are there recordings available anywhere yet?

Jasmin Blanchette (Aug 03 2021 at 16:18):

Not yet. I think the CICM organizers are still debating whether and how to make the videos available without violating EU privacy regulations.

Patrick Massot (Aug 03 2021 at 16:19):

How is it possible that this question is more complicated than for the dozens of conferences we attended online since the beginning of the Covid era?

Oliver Nash (Aug 03 2021 at 16:21):

Of course I have no idea, but my impression is that people are gradually taking privacy more seriously which I for one welcome.

Filippo A. E. Nuccio (Aug 03 2021 at 16:24):

@Jasmin Blanchette Do you think that it will be possible for you to post the link here once, and if, they'll be available? Thanks! :pray:

Jasmin Blanchette (Aug 03 2021 at 19:34):

It's a big if (i.e. I doubt the organizers will make this happen). But if so, I'll try to remember. You can also keep an eye on the CICM/FMM web sites. There are also the proceedings coming.

Mario Carneiro (Aug 03 2021 at 21:32):

I'm somewhat upset that they recorded us under these conditions. If I had known it would be a problem I would have recorded myself instead of leaving it to them

Filippo A. E. Nuccio (Aug 04 2021 at 11:22):

May be the organisers will let you have your video, which you can then put on youtube/wherever?

Yaël Dillies (Aug 04 2021 at 11:37):

Yeah but surely the privacy problem isn't about the speakers, but about those participants who had their videos on?

Eric Wieser (Aug 04 2021 at 11:58):

Is that even captured in the zoom recording? I thought it only captured the speaker and possibly those asking questions

Eric Wieser (Aug 04 2021 at 11:58):

And the latter could be fixed by removing the Q&A, which seems better than losing the talks in their entirety

Mario Carneiro (Aug 04 2021 at 12:07):

Filippo A. E. Nuccio said:

May be the organisers will let you have your video, which you can then put on youtube/wherever?

I've already asked; they are keeping the videos private even from speakers for now. I would really like to know why they can't just solicit waivers from everyone to get around any legal boogeyman. Participants are already required to accept to being recorded since it's baked into zoom's interface

Filippo A. E. Nuccio (Aug 04 2021 at 13:35):

I see, thanks! Let's hope they will end up freeing the videos.

Nicolò Cavalleri (Aug 06 2021 at 10:27):

For people who asked during my talk, here you can find my slides for my presentation and here there is a link to the preprint!

Nicolò Cavalleri (Aug 06 2021 at 10:45):

Btw among the talks I missed I would be super interested in watching Mario's one so if someone has access to even only that single talk I would be super happy if they could share it, if Mario is ok with that

Gihan Marasingha (Aug 07 2021 at 22:55):

Zoom has a statement about GDPR. This should be no problem. https://zoom.us/gdpr

Zoom’s products now feature an explicit consent mechanism for EU users. Existing or new users coming from IP address detected from EU when signing into the Zoom desktop or mobile application, or joining a meeting without being signed in, across any platform (Mac, Windows, Linux, iOS, Android, Web, ChromeOS) will be presented with a one-time privacy policy update. Consent to the updated Privacy Policy and Terms of Service are stored for compliance purposes. Audio notifications can be enabled for users who are joining a meeting that is being recorded, via the telephone. Visual recording indicators are also present.

Eric Wieser (Aug 17 2021 at 19:00):

The organizers relented and released the videos to the speakers, thankfully; uploading them is left as an exercise to the speaker.

Eric Wieser (Aug 17 2021 at 19:05):

Perhaps the YouTube account used for lftcm should hold a playlist of videos uploaded individually by speakers?

Johan Commelin (Aug 17 2021 at 19:06):

yeah, that's the leanprover community account... I guess it can host such a playlist

Mario Carneiro (Aug 17 2021 at 19:46):

I've got the mp4 for my talk, let me know how to get it to you

Eric Wieser (Aug 17 2021 at 20:21):

I was thinking of just uploading it to our own accounts and having a playlist that linked to those videos

Patrick Massot (Aug 17 2021 at 20:22):

I guess many speakers don't have a personal YouTube account.

Scott Morrison (Aug 17 2021 at 23:41):

I can upload them to the community account if you can get them to me. (Send a URL, share from Dropbox, share from google drive, whatever you like.)

Mario Carneiro (Aug 22 2021 at 06:11):

My talk is now up along with others on the leanprover community playlist: https://www.youtube.com/watch?v=fOO2fByx8tw&list=PLlF-CfQhukNlRnFgVMklVTZCvBUX2oaDC&index=1

Filippo A. E. Nuccio (Aug 26 2021 at 19:21):

@Sebastien Gouezel Is there any way to have access to the video of your talk at CICM21 about Gromov-Hausdorff, or you prefer not to make it public? Same question for @Anthony Bordg and @Nicolò Cavalleri .

Sebastien Gouezel (Aug 26 2021 at 20:41):

I don't know, sorry. They have probably sent me a link to download the video, but I must have erased it by error because I can't find it any more...

Nicolò Cavalleri (Aug 26 2021 at 22:28):

I will take care of this soon! I am sailing and I only have my phone so lately it has been hard to do this kind of things!

Scott Morrison (Aug 26 2021 at 23:57):

As Sebastien was in the same session as Nicolò, it's likely they will be in the same video. (They've be sending links to the entire session, leaving it to speakers to cut.) @Nicolò Cavalleri, if you forward me your link I'm happy to cut and upload both videos.