Please take a look at the papers about Lean (https://leanprover-community.github.io/papers.html https://leanprover-community.github.io/papers.html) and explain

Please take a look at the papers about Lean (https://leanprover-community.github.io/papers.html https://leanprover-community.github.io/papers.html) and explain to me how that "reinvents everything". There are several new and non-trivial things going on in this language! Look at the papers about hygienic macros, or functional-but-in-place, or any of the others.