From what I understand, it’s more like requiring each programmer to write implementations of arrays, dictionaries, date/time handling code, float parsing and printing, etc.

Once the language designers had figured out the hardware was now capable enough to make libraries useful, it only took one programmer to do that tedious work. After that all other programmers could reuse that work.

This will be similar: once a large body of definitions and proofs has been built, mathematicians will be able to reuse higher-level constructs to build proofs for their theorems.

It likely also will be similar in that there will be multiple approaches to this with one (or a few; it could be that one system works best/will have the largest set of definitions for one branch of mathematics, while another ‘wins’ in another) ending up victorious.

Exactly. There are multiple ongoing projects to formalize existing math, there seems to be some convergence on Lean4 at the moment, but the best analogy is probably programming languages, where there's a constant battle between the old guards with huge staying power and newer entrants with just too many good ideas to ignore. Except that here a lot of the attractiveness of a language will come from how much math has been formalized in that language, which gives a huge advantage to the early leaders. So there might be a bit more emphasis on 'superset-languages' like Kotlin or TypeScript here, that can make use of the libraries from existing languages.

I think porting automation will eventually solve this problem. It's really easy to write "amazingly good test-suites" for this stuff. So a computer will do the porting and you essentially "only need to read mehod signatures" to make sure the port is correct. (In which case it is completely correct with all edge cases included). This is still some work but much more manageable than e.g. porting JS to Python...

This isn't about Terry Tao specifically, but proof assistants can help you manage a proof when it's gotten too big or complex to manage in your head without making mistakes.

There was this project to use Lean to prove a theorem of Peter Scholze's (Scholze is a well-respected professor and a famous mathemtician). Apparently, it was so big and complex that he could barely keep it in his head, so after writing the proof, he and Kevin Buzzard formalized it with Lean.

https://www.quantamagazine.org/lean-computer-program-confirm...

Then, 6 months later, he was interviewed, where he talks about using Lean for proving his theorem:

https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...

And the experiment was finished in 2022. Announcement: https://leanprover-community.github.io/blog/posts/lte-final/