I think they end up similar. Although Lean 3 is much more geared towards writing proofs with the addition of mathlib [0] which aims to be a library of formalize

I think they end up similar. Although Lean 3 is much more geared towards writing proofs with the addition of mathlib [0] which aims to be a library of formalized mathematics. [0] https://github.com/leanprover-community/mathlib https://github.com/leanprover-community/mathlib