[krapht]

"Lean doesn't even use one of the most obvious things that make interactive proof systems far more usable - a declarative mode instead of the usual tactics-based scripts."

Citation needed. I can make a perfectly reasonable Isar-style declarative proof in Lean. Just because most users of Lean choose not to do this doesn't mean it can't be done. I should mention that users are more willing to write imperative proof code instead of declarative in Lean is because 1) the interactive debugger is responsive and easy to use, and 2) writing a nicely structured declarative proof is more work than an imperative proof.

[ratmice]

Indeed, most of the book https://leanprover.github.io/logic_and_proof/ is entirely term mode proofs, with tactics largely absent.