I started teaching myself Haskell for fun about a year and a half ago, and ended up going down a rabbit hole of formal logic, set theory, mathematical foundations etc. which I did not expect at all; I'm currently spending some time looking at algebraic topology to give me a grounding to go into homotopy type theory.
For anyone else with an interests in this area, I'd strong urge you to look at some of the work from Kevin Buzzard (Imperial College), perhaps better known as an algebraic number theorist, who leads the Xena  Project, which started as an attempt to completely formalise all the problem sheets for one of the undergraduate maths modules at Imperial in Lean. There's also a GitHub repo  with a lot of work to build on.
Adam Chlipala (MIT) also teaches a course in formal program verification in Coq based on his book  which is a valuable resource.
Well, adding consistent axioms often allows proving more thing, but that in itself does not necessarily mean it's more useful, and certainly not that proofs are easier -- that, I believe, was the question. For example, adding the axiom 1/0 = 0 is consistent with ordinary arithmetics, and also allows you to prove more things (e.g. that 1/0 = 0), but is not necessarily useful and not necessarily helpful.
Note also that all well-known foundations, including HoTT are mutually relatively consistent, which amounts to being translatable into each other (so if you can derive a contradiction in one, then you can convert that into a contradiction in the other). However that is not so important in practice. Proof automation is most important for large scale reasoning. Indeed the Lean project was started with the explicit aim of bringing better proof automation to provers based on the Curry-Howard correspondence.
The main issue with Lean 4 is that there is currently no tactic state, but the designer Leo de Moura is currently hard at work at this, because they need tactics to start work on their IMO Grand Challenge https://imo-grand-challenge.github.io/ . Even when tactics are done, there will be no type class inference so the port of the maths library from Lean 3 to Lean 4 will probably not begin then. Type class inference is a complex issue and some of the chat on the zulip chat is about issues that users have been having in Lean 3 and how they might be fixed in Lean 4. But, in short, the basic principles are all the same. In short, I would thoroughly recommend this book.
Lean 4 has already gone public: https://github.com/leanprover/lean4/
Also, afaik it won't differ from Lean 3 to the degree where learning Lean 3 is useless.
Right now it actually takes far more time to write lean code than to prove things by hand. What is typically done in a single lecture in an intro Algebraic Number Theory course can take hours upon hours to implement. E.g. the Pell equation . You have to be extremely explicit about everything, and can't handwave the details you do in human proofs.
Right now the overhead of writing proofs in Lean is so large that you'd prove a theorem with pen and paper before attempting it in Lean. So far it is a useful tool for proof verification, but not for actually coming up with them.
As things stand, computer proofs are only better than humans for things that are highly combinatorial in nature. which due to performance concerns usually aren't written in languages running in VMs.
The documentation for it isn't so great but Lean is a fully dependently typed programming language with a good VM. It is optimized for interactive theorem proving which means the type checker is really fast. I think getting a good native compiler out of it is not far off.
It also has inbuilt support for quotient structures, which is a huge timesaver when dealing with Algebra. Might not be so important if you want to prove the correctness of programs.
But I think the main advantage is that Lean is it's own meta-programming language, so you don't need to switch to Ltac/OCaml to write tactics.
The main advantage Coq has is it's code extraction feature. There was talk about implementing code extraction to C++ in Lean, but I don't think it has been done yet.
An oversimplified summary would be that Coq was designed with programmers in mind, while Lean was designed with mathematicians.