# What will happen to mathlib when we transition to Lean 4?

Today, there's an exciting large-scale effort to digitize mathematics in Lean's mathematics library mathlib.

I understand that a transition to Lean 4 is looming. I've heard that Lean has had issues with backwards compatibility in the past, but I don't know the details.

When is Lean 4 expected to become the most widely used version of Lean? Will mathlib suffer from this transition? If so, how?

The community hopes to eventually move fully to Lean4. There's some details about the history of earlier Lean versions here, but they're not too relevant as the first two versions were very experimental. Now, some members of the community and Microsoft are diligently working on mathport, which will hopefully provide a full syntax-ful translation of Lean3 code into idiomatic Lean4 code. The main test-case for this, at the moment, is mathlib itself, and we are pretty determined to make it work.