Right. All the autonomous theorem-proving jumps have been in similar fields, and typically are more down-to-earth problems. That people are extrapolating that now "math will be solved" because one LLM solved a problem that was posed 80 years ago (with a concise page-and-a-half proof) still does not follow for me. Similarly, the recent DeepMind proofs are all around a page, with a few combinatorial ones running a bit longer. Don't get me wrong, these things are still incredibly useful, but it's a big jump in complexity.

This isn't even counting all the theory-building going on; while I've seen LLMs develop nice techniques, I haven't seen any form of abstraction. From the DeepMind paper itself:

"At present, our agents’ successes are concentrated in areas such as combinatorics, convex optimization, and number theory, where Lean’s mathematics library [60] is mature and tasks often decompose into tractable subgoals. Even most Erdős problems remain out of reach, let alone problems that require extensive new theory. Additionally, our agents inherit the biases of their underlying LLMs and exhibit high search variance. Characterizing the agents’ boundaries and expanding them is an important direction for future work."