[IngoBlechschmid]

Good questions!

Nowadays, there is indeed a movement towards interoperability between the various proof assistants, one of these bridge-building projects is called Dedukti: https://deducteam.github.io/ It's a challenging project because the different proof assistants which are currently in use differ in their foundational perspectives and their idioms. The question how to best formalize mathematics is still an open research problem, just as the question how to best develop programs, but we already have quite a good understanding of many important issues in this area.

Also, by now there are attempts to use AI for discovering proofs, see for instance https://leandojo.org/ or https://github.com/lean-dojo/LeanDojoChatGPT.