Comment by nxobject

As Coq (now Rcoq) found to their chagrin... I'm convinced half of the reason Lean has surpassed Coq in mindshare in formal mathematics was because it's impossible to not chuckle at the name sometimes.