Comment by WhitneyLand

The most important thing is keeping up the momentum to formalize more proofs and continue to strengthen the libraries and foundational work.

If that momentum is strongest with Lean so be it. At the same time things become more machine verifiable, converting to a new system will also become easier. It can already be strongly assisted using a general agent like Claude Code.