There are indeed several different proof systems. "Formalizing 100 Theorems" tracks the progress of the "top" ones compared to a set of well-known proofs:
The top ones (sorted from most to least complete) are HOL Light, Isabelle, Metamath, Coq, Mizar, and Lean. Lean actually has the fewest proofs of those systems, though of course there are advantages to Lean as well.
I think some duplication is inevitable because there are fundamental disagreements on "what is important".
One problem with most of them as a "store of proof knowledge" is that most of these proof systems don't (normally) store the proof in terms of axioms, definitions, and previously-proven theorems. Instead, they store a program (as a sequence of tactic statements) that, if run, is intended to help the prover rediscover the proof... assuming that tactics never change (even though they do). As a result, older proofs in some of these systems can no longer be verified as being correct. This is one thing that attracts me to Metamath; Metamath stores literally every step, with all mathematical knowledge (including all axioms and definitions) in the database, so proofs stay proven. It also makes verification super-fast, e.g., 28K theorems can be verified in less than 1 second.
Others believe other traits are important, so they end up with different systems.
As far as translations between systems, I'm very interested in what happens with Metamath Zero. That work might, in the end, enable mutual translations between various systems. We'll see!
(Disclaimer: I'm addicted to Lean. My view is biased.)
Note that Lean is not so high on that list, but also note that serious theorem proving in Lean is less than 5 years old, whereas the other systems are (several) decades old.
There are at least two entries on the list that have only been formalized in Lean, and not in any other system. We are catching up pretty quickly.
It's clear that this list has an important status. But in my opinion, building a library of undergrad maths, which is what what TFA is mainly about, is a lot more important. We are tracking our progress over at https://leanprover-community.github.io/undergrad.html
I am not aware of such an organized effort in other systems. Without such a fleshed-out undergrad library, we'll never get to systematic formalization of (post)grad mathematics.
http://www.cs.ru.nl/%7Efreek/100/
The top ones (sorted from most to least complete) are HOL Light, Isabelle, Metamath, Coq, Mizar, and Lean. Lean actually has the fewest proofs of those systems, though of course there are advantages to Lean as well.
I think some duplication is inevitable because there are fundamental disagreements on "what is important".
One problem with most of them as a "store of proof knowledge" is that most of these proof systems don't (normally) store the proof in terms of axioms, definitions, and previously-proven theorems. Instead, they store a program (as a sequence of tactic statements) that, if run, is intended to help the prover rediscover the proof... assuming that tactics never change (even though they do). As a result, older proofs in some of these systems can no longer be verified as being correct. This is one thing that attracts me to Metamath; Metamath stores literally every step, with all mathematical knowledge (including all axioms and definitions) in the database, so proofs stay proven. It also makes verification super-fast, e.g., 28K theorems can be verified in less than 1 second.
Others believe other traits are important, so they end up with different systems.
As far as translations between systems, I'm very interested in what happens with Metamath Zero. That work might, in the end, enable mutual translations between various systems. We'll see!