[SmartestUnknown]

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