Yes and no. If you want to port large low-level proof objects in all their gory detail, then this has been done already. But if you want to port the more concise higher-level proof scripts you run in all the same issues as with regular transpilers.

Compare it to porting machine code for one instruction set to another instruction set. This is usually doable in a straightforward manner (maybe with a mild performance penalty). But transpiling idiomatic Java to idiomatic Haskell is nigh impossible.

Luckily, the differences between Lean 3 and Lean 4 are not as large as between Java and Haskell. But still, they have different idioms, different syntax, different features. And this has to be taken care of.

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