I think formal systems like Lean are still extremely interesting. And I would imagine that, if these machines get good at standard "informal" proofs, that the overhead of formalization would be a lot less painful for them than humans (it is pretty tedious these days but even for humans the friction is decreasing).

Verified proofs allow you to collaborate with much less trust (for humans or machines), at least in the phase where you are trying to figure out what is true. They don't guarantee that a proof is insightful for "why" a result is true, but that is much easier to put together once you have a valid proof.