Zulip Chat Archive

Stream: Lean Together 2021

Topic: porting mathlib to Lean 4

Rob Lewis (Jan 05 2021 at 09:30):

On yesterday's schedule we had a time slot to discuss porting mathlib to Lean 4. We very happily yielded this time to Leo and Sebastian's Lean 4 presentation -- to discuss porting, we need as much information as we can get about the target of the port!

Rob Lewis (Jan 05 2021 at 09:31):

Our social time immediately crashed Wonder, so we reconvened on Zoom, and there was an impromptu porting discussion there.

Rob Lewis (Jan 05 2021 at 09:32):

This wasn't a guided discussion and certainly no plans or decisions were made, so don't feel that you missed out on anything juicy if you weren't there :)

Rob Lewis (Jan 05 2021 at 09:33):

We won't have time to reschedule a porting discussion during this workshop, but we'll come back to the idea after people have had some time to play around with the brand new Lean 4 release. Stay tuned.

Last updated: Dec 20 2023 at 11:08 UTC