> If you know proposition X is true, it’s easier to figure out why.

This misses the point entirely. If you know proposition X is true or false, you won’t bother spending years trying to prove or disprove it, developing deep understanding and potentially even developing entire new fields of math in the process. (See FLT.)

That’s why it’s so destructive to the discovery process to have an LLM just generate a proof or counterexample without the side effect of generating useful explanatory or generative structures that we can build on.

That said, there are examples like Ramanujan where someone did an info dump of unexplained theorems that people try to mine useful structures from, but that’s not at all the mainstream of mathematical progress.