The math performance, even for VERY hard problems, is already getting extremely good and progress is still high year-on-year.
What OpenAI (and everyone else, less publicly) seem to be doing, is to integrate these kinds of abilities into multi-modal models.
https://deepmind.google/discover/blog/ai-solves-imo-problems...
The real AI math advancement will be a computer which is as smart as a pigeon and innately understands what a number is, which means it is able to solve simple counting problems without training. AlphaGeometry or Strawberry aren't even close to that, and I suspect none of us will live to see such a sophisticated AI.
As impressive as it is, it makes LLMs look like they are just a fancy UI. Like, you can tell the computer to press the upvote button in English using your voice instead of using your mouse.
It's the same with AlphaProof. The LLM is just taking a problem specification in natural language and then acting as the UI of the theorem prover.
The moment you talk about using LLMs to solve decidable problems, people whip you with the idea that you should let the LLM generate python code. Aka, the LLM is just a fancy UI for specifying python programs in English.
Cool, but also somewhat hollow. It's no different than having a translator from one language to another.