What sort of maths are LLMs good at?

Timothy Gowers’ post tries to separate different kinds of mathematical work instead of asking whether LLMs are simply “good at math.” His core claim is that models already look strong on areas where they can generate many candidates, recognize useful patterns from past work, and get fast feedback on whether something works. They look much weaker on the part mathematicians most prize, namely proofs that introduce a genuinely new method that later feels inevitable and elegant. He also notes a structural asymmetry between finding examples or counterexamples and proving universal statements. The comments largely agreed with that framing and made it more concrete. The recurring line was that current AI math wins look like test-time scaling and guided search, not autonomous theory creation. People kept coming back to a simple recipe: let the model produce lots of plausible objects, then use an external checker like Lean, a SAT solver, or numerical tests to kill bad branches cheaply. That explains why coding contests, counterexample hunting, and formal proof completion are moving faster than open-ended theory building. Several mathematically informed comments argued this is not “just brute force” in the old GOFAI sense, because proof spaces are too large for naive search and the models are clearly steering toward promising regions. Still, even the more bullish takes landed on the same practical point. The model is valuable because it proposes plausible next steps in human mathematical language, while the real reliability comes from verifiers and decomposition into lemmas. Skepticism focused less on whether AI can produce publishable fragments and more on whether that adds up to the kind of conceptual invention people mean by mathematical insight. Recent Anthropic claims around the zeta-function lower bound were read through that lens. The interesting part was not “AGI did math,” but that a non-mathematician could drive a large multi-agent search process and get a result that specialists then had to interpret and verify. That led to a broader concern that AI may flood mathematics with candidate results faster than experts can check them. The strongest bottom line was narrow but solid: current systems are good at exploration in spaces where correctness can be checked cheaply, and much less convincing at creating the theories, definitions, and long proof architectures that tell mathematicians what is worth proving in the first place.

Treat current AI math systems as high-powered search tools that become useful when you can verify outputs mechanically with Lean, SAT solvers, or numerical checks. If your problem depends on new conceptual framing, long-range proof structure, or trust without external validation, assume humans and formal tooling still carry the load.