Comment by voxl

??? Look at any conference that publishes mechanized results? You'll see plenty of Isabelle, ACL2, Rocq, Agda. You exist in the pop science bubble. If Lean has done anything it's advertised itself well. It did a good job of that as far back as the Liquid Tensor Experiment, and it's pissed many people off in the community with it's marketing antics.