The mathlib library is over 600K lines of code, all written in Lean 3. Lean 4 promises great extensibility, faster tactics, powerful and convenient macro programming – and no backward compatibility. As we have no desire to part with such a rich source of advanced formal mathematics, we are planning to port all of it to Lean 4. This might be the largest source-porting effort done in a theorem prover, so we're taking things slowly and investing heavily in high quality automated porting tool development. In this talk I will discuss our plans for how to translate all this source code to Lean 4 while preserving the quality standards and synthesizing the styles and tactics developed in mathlib with the new Lean 4 style.