Yeah, it's so funny seeing all these people discover Lean as if it invented mechanizing mathematics. Even Coq wasn't the first (might have been the first with dependent types though).