Lean4 math library

Stream: mathlib4

[Rick Sánchez]

Is it safe to assume that that mathlib will be ported to lean4 eventually?

[Wojciech Nawrocki]

AFAIK yes, but the eventual port may or may not have something to do with mathlib4 which is written by hand. There are automated efforts including at least mathport and binport.

[Kevin Buzzard]

It's definitely safe to assume this. Microsoft are backing the initiative so it will get done somehow.