The entire article makes it sound like Lean is significant step in usability and power over other systems. That seems like an important thing and makes me interested to download it and play with it.
Microsoft Research seems to have done some exciting things with provers over the years - Z3 is another significant program. All under the direction of Leonardo de Moura, notably.
Power, perhaps. But I'm a bit skeptical about usability. 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. (Yes, you can kinda sorta fake the former with "structuring" tactics, except not really - declarative proofs are really their own kind of thing.) There even used to be systems that automatically rendered inputed definitions and declarative proofs in natural language (given that the basic terms and symbols were previously defined of course) which does enable even an average mathematician to easily figure out what the system is up to. You just can't do this properly if all you have is a list of "tactics" fiddling with the prover state.
"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.
