I only have an undergrad in math, so very little understanding, but I'd be pretty surprised if it couldn't do forall just as well. Like, say it found this counterexample which relies on axial stretching or whatever approach. Then it already knows how that made the proof work, and can use it to try to prove NS has smooth solutions modulo this particular kind of defect (so it could make some statement about cohomology, or some additional constraining equation). Or if that doesn't work, then it can find a counterexample, which we've established it's good at. Then repeat until you've characterized what does work. The various defects, along with being defect free, become definitions. Now you have a theory.

>Then it already knows how that made the proof work..

I think you cannot assume so, because pattern matching is not reasoning.