Comment by thejokeisonme

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).