porting mathlib to Lean 4

Stream: Lean Together 2021

[Rob Lewis]

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]

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

[Rob Lewis]

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]

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.