[kevinbuzzard]

I just confirmed with Azerbayev that the typo in the example from Munkres ("identify" not "identity") was indeed what was fed to the algorithm (and the algorithm got it right anyway). We found some other funny examples when asking Lean to write strange definitions of differentiation: it would sometimes just write the correct definition (in correct Lean) despite being asked to write something else, perhaps because it has seen the correct definition far too often? It's pretty weird to play with!