It seems misleading to lump AlphaGeometry in with this: that system works by having an LLM generate hundreds of Lean programs and trying to find the one that works. Frankly the project is pointless and borderline dishonest: it is a hideously expensive way to solve useless Olympiad problems, but it won't work at all for actual mathematical research since we wouldn't have nearly enough training data. It does not represent even the slightest advancement at AI performing mathematics, it's pure gimmickry. I suspect the entire point of AlphaGeometry is to generate comments like yours, "AI is now an Olympian-level mathematician."

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.

Yeah sure, but AlphaProof is "cheating", because they are using an external system to do the hard work and the LLM is just there for translation and semantic information retrieval.

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.