In theory yes, but there are two main things that makes it harder : - some technical details have changed. They don't affect the axiomatic aspects of Lean, but

In theory yes, but there are two main things that makes it harder : - some technical details have changed. They don't affect the axiomatic aspects of Lean, but they force us to redefine some things in a cleaner way. - we don't only want to port the theorem. We want to port them to a human-readable proof that can be easily maintained