perhaps proof assistants should support multiple formalisms (think MLTT, ZFC, etc), letting you work in whichever is convenient at the moment by compiling your proofs between them as necessary
0

If you have a fediverse account, you can quote this note from your own instance. Search https://donotsta.re/objects/a7904b9f-7c89-40e9-a96b-cbee15ebc7e4 on your instance and quote it. (Note that quoting is not supported in Mastodon.)