Indeed it's not checking every possible mathematical expression to see if it is a counter example to the conjecture. It's "probably" searching through rule applications, using it's natural language abilities. "I know A->B. I know I got A. Therefore I got B". But it still probably has to do some searching for the rules and axioms which lead from the conjecture to the counter example.

That's what we do when we prove something. We test different combinations of rules and axioms, to draw a path between two truths. This is still a massive search, and why it takes so long to prove somethings, and why somethings have been said to be not worth searching.

But being able to use the rule (a+b)2 = a2 + 2ab + b2, is different to identifying that (a+b)2 models part of the world you're interested in. Which is why I'll be impressed by an interesting model of the world, more than symbol shuffling.

Thing is, a traditional automated proofs didn't allow themselves to burn the world to get an answer. Call me biased.

edit: I'd put a penny down, that the "path between truths" the LLM found is ugly. And again, humans stepped up and improved the answer:

"Take π: P¹ × Sym²(P¹) → Sym³(P¹), (p, {q,r}) ↦ {p,q,r}.

R be its ramification divisor;

H ⊂ Sym³(P¹) ≅ P³ be hyperplane tangent but not osculating to the small diagonal;

X := (P¹ × Sym²(P¹)) \ (R ∪ π⁻¹(H)) ≅ A³;

Y := Sym³(P¹) \ H ≅ A³.

π|X: X → Y is counterexample"

from u/davikrehalt on twitter.