Comment by 0815test

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.