erdos-banger

Step-by-step workflow for proving an Erdos problem in Lean 4 using Claude Code/Codex (subscription-first). Invoke as /erdos-prove <problem-id>.

Complete guide to the Erdos CLI toolkit for mathematical research. Use when discussing Erdos problems, Lean formalization, literature search, or when the user asks about CLI commands, API costs, or environment configuration.