Lean 3/4 confusion appears to be systemic in training data for Claude 4, Gemini 2.5, and quite likely other LLMs. This project has focused so far on category theory but many problems will occur in other domains as well. We have found the below prompts to be effective and time-saving for AI assistants working on Lean 4. See CLAUDE.md for tactics and links to tests and a protocol for using development plans to which AIs have contributed.