5 ms·

I hear you but point me to one novel formalization right now that is not Lean. It’s really becoming a refacto standard. Which is lovely but terrible for pedegog

• voxl 12d ago
  ??? 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.