Using Codex to attack math problemsFor mathematicians and TCS people who have never used an AI coding agent.