> Metamath is based on set theory, and would therefore address some concerns one might have with the propositions-as-types philosophy used by Lean

Isn't the entire point mathematicians adopted Lean where they spurned Haskell is because of the batteries-included ZFC object language in the former? Metamath implements a set theory object language just the same, it's not based on it at all in this sense. You just changed one metalanguage for another.