Post #4249910

See also a question asked today on Math Overflow, “Are we stuck with Lean?”. The proposed alternative, Metamath, isn’t type-theoretic and thus skips the entire dialogue between type theory and proof assistants.