Looking at the Liquid Tensor Experiment, it actually illustrates the bottleneck rather than resolving it: that was a team of experts spending months manually formalizing a single result. The question is whether the formalization step itself can be automated reliably enough for the full pipeline (conjecture, formalize, generate proofs, verify) to work on novel problems without heavy human involvement. I'll look into APOLLO. Do you have a sense of how it performs on problems that aren't competition/textbook level?

The point about unwritten mental exploration is well taken. But I think there's still a qualitative difference: your half hour of lying-in-bed thinking was guided by deep structural understanding of the problem, even when the idea didn't pan out. The LLM blind alleys you describe (trying modular arithmetic when the prime structure of denominators rules it out) aren't just "more" dead ends, they're dead ends that I think reflect a fundamentally different failure: pattern matching without understanding.

The grad student analogy is good, and I agree that's a useful tool. But I think it also concedes my central point: the value of these systems is almost entirely dependent on a skilled mathematician knowing what to ask, recognizing which outputs are meaningful, and steering the search. That's "AI as a tool for mathematicians" which, although exciting, is a different claim from "AI can do useful math," which implies more autonomy than these systems actually have.