> Lean did that irritating thing which it sometimes does: it complained about the human presentation of an argument in the standard literature, and on closer inspection it turned out that the human argument left something to be desired.
Tongue-in-cheek irritation aside, this is actually awesome. I think Lean (and other theorem provers) are going to end up being important tools in math going forward.
Tongue-in-cheek irritation aside, this is actually awesome. I think Lean (and other theorem provers) are going to end up being important tools in math going forward.