I am assuming you mean it's a bigger concern in Lean than other languages because of what people are attempting to do with it (formalize all of math)? Because the language itself, somewhat by design and somewhat by nature, seems to be more future proof than any other language I've ever used.

So if this project was completed in Lean 3, for sake of example, how compatible would it be with Lean 4 today?