I think too much credit in the AI math discussion is being given to LLMs rather than to Lean, which an incredibly well designed language around which Mathlib coalesced as a side-effect of it's capability

I doubt of this progress could have been made without the specific combination of Lean + Mathlib. Automatic Theorem Provers are not a new idea, but we don't see these breakthroughs happening with any other stack