I doubt that he was intending a burn here. He's not talking about user interface issues or the like.

He's most probably, I would assume, talking about the well-known issue that formalisation tools require knowledge that a standard mathematician doesn't possess, such as the names of all the Lean tactics, how to locate the right theorem to use in mathlib (the Lean library), the necessity to write mathematics in a very formal language which is based on dependent type theory rather than based on sets (which is what most mathematicians are used to), etc.

Moreover, formalised mathematics does not work with natural language (and perhaps can't), and it will not accept informal or intuitive arguments. There are a lot of very fiddly things that have to be attended to. One can't assume that the reader is a skilled mathematicians who can easily fill in trivial details, as when writing a maths paper for expert readers.

But the Lean people are acutely aware of all of this. In my opinion he's not so much offering them much needed criticism so much as acknowledging one of the known barriers to mathematicians from outside the formalisation community getting into formalisation.

This is a major point of the article, that real, serious mathematicians have broken through that barrier recently, and it's not the first time. So things have improved enough to show that it is possible for seriously committed mathematicians to do this, even famous ones!

It's honest constructive criticism. Lean is very hard to use. It's even hard to install and run.

Elan makes it actually quite easy. It's among the better package managers out there, comparable to cargo.

There's a single bash script to install both the runtime and the package manager on a variety of platforms, and the integrated build system and native module bundler is both powerful and isomorphic, so all you need to learn is Lean. Without any prior knowledge of Lean I was able to patch existing build scripts to support platform specific C extensions in less than half an hour.