Sure. But even many high-caliber research mathematicians can’t do Putnam problems in a heartbeat. If we get to the point where an LLM can solve any homework problem that appears in a textbook, including graduate textbooks, that would already be something like a “lemma prover” if not a full-blown “theorem prover”.

Anyway, I think five years ago I was skeptical that ML would even get to the point of being able to solve competition problems, and I was proven wrong, so my priors have been updated.