tl;dr: Following OpenAI's announcement of ten major math/CS results solved by LLMs, Timothy Gowers observes that most headline successes involve finding (counter)examples rather than proving theorems, and explores why. He argues this likely isn't because LLMs favor existential statements, but because their strengths—broad knowledge and rapid brute-force search—suit certain example-finding strategies (off-the-shelf checks, just-do-it constructions, probabilistic/generic arguments). Humans may retain an edge on problems requiring a "nose" for pruning deep search trees toward surprising, conceptual proofs—though Gowers expects LLMs to close this gap soon.