Exactly lol. Not sure why everyone is taking the contribution of lean in finding the error so seriously. I would be more impressed when some mathematician find

Exactly lol. Not sure why everyone is taking the contribution of lean in finding the error so seriously. I would be more impressed when some mathematician finds a more severe error in their proofs with the help of theorem provers (meaning a mistake in their own intuition).