mathlib / lean3 / lean4 status?

Stream: lean4

[Kevin Lacker]

Hi folks, it's been a little while since I worked on Lean stuff, and I was wondering what the status is on the Lean 3 / Lean 4 split. Is there any consensus for whether mathlib is going to migrate to Lean 4?

[Anne Baanen]

Indeed, there is now a lot of work going on to port mathlib to Lean 4, starting by translating Lean 3 syntax to Lean 4 and porting the existing mathlib tactics to the new system. I'm not very active in porting at the moment, hopefully the #mathlib4 stream gives a better idea on where we're at right now.

[Bryan Gin-ge Chen]

Here's a fairly recent blog post summarizing the current state of things: https://leanprover-community.github.io/blog/posts/intro-to-mathport/

[Kevin Lacker]

cool, sounds like some progress is being made.