tl;dr: An author with no math background spent a month and roughly $40k worth of tokens orchestrating multiple Claude and ChatGPT agents to produce a Lean-formalized proof of Conway's 50-year-old refinement conjecture on omnific integers. The workflow relied on separate "PM," math, red-team, and Lean agents, with frequent restarts, adversarial audits, and grounding via Lean formalization to prevent LLM hallucination and jargon drift. The proof passed mechanical checks but hasn't been independently verified by mathematicians yet.