I'm not even so sure it's such a useless joke. I mean, it is, and I wouldn't want titles to be like "Academic publishers admit paywalls were a scam all along" (unless ALL major publishers actually admit it, which so far they didn't). But I clicked on "Math nerd explains how to spend 3 days proving 1+1=2" and when it turned out to be a Lean tutorial I thought "Oh, that's exactly what I wanted!". I don't know why, but "From Zero to QED: An informal introduction to formality with Lean 4" I didn't even notice. It's such a boring and verbose title with lame attempt at wordplay that, that my brain somehow filters it out.