Abstract : There is a constant stream of claims about the ability of AI tools to "do math," often interpreted as the ability to provide natural language proofs to well-specified questions. The methods by which such proofs are produced are often opaque, because the systems used to produce them allow for multiple layers where human intervention can enter, so that the autonomous nature of solutions is not clear. I will illustrate the issues with a question in symplectic topology which was part of the first batch of problems released by First Proof, and compare the human solution with the attempts obtained by testing publicly available AI systems, the submissions of internal groups at OpenAI and Deepmind, as well as an experimental prototype built on Claude Code for which we can see all the steps (and the costs) on the way towards an attempted solution.