[ImprobableTruth]

The context of that "mastermind PR campaign" comment is a video watched now more than 70,000 times in which it's claimed that Coq is just not as good as Lean because it doesn't have quotient types, even though you can get them if you're willing to make the same trade-off that Lean does (broken SR). Calling Lean's framing a 'mastermind PR campaign' is of course still quite snippy, but I don't think it's totally unfair seeing as how it led to those comments.

>There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on.

I think it just takes time to fully move on. And while it's not the fault of the Lean community, when something like the recent quantamagazine article on formalizing mathematics essentially only mentions Coq to call it old and busted in comparison to Lean, that's only going to cause people to hold onto their resentments for longer.