Develop and verify a mathematical proof in Lean, continue an incomplete Lean project, or audit whether it proves the original statement. Connect actual inputs to intermediate lemmas, assemble the target theorem, check its transitive axioms, and provide a reproducible handoff.
Install
npx skills add wanshuiyin/Auto-claude-code-research-in-sleep --skill lean-formalizenpx skills add wanshuiyin/Auto-claude-code-research-in-sleep --skill lean-formalize -a claude-code -gnpx skills add wanshuiyin/Auto-claude-code-research-in-sleep --skill lean-formalize -a codex -ggemini skills install https://github.com/wanshuiyin/Auto-claude-code-research-in-sleep.git --path skills/lean-formalizegh skill install wanshuiyin/Auto-claude-code-research-in-sleep lean-formalizegit clone --depth 1 https://github.com/wanshuiyin/Auto-claude-code-research-in-sleep /tmp/wanshuiyin__Auto-claude-code-research-in-sleep
mkdir -p ~/.claude/skills ~/.agents/skills
cp -R /tmp/wanshuiyin__Auto-claude-code-research-in-sleep/skills/lean-formalize ~/.claude/skills/lean-formalize # Claude Code
cp -R /tmp/wanshuiyin__Auto-claude-code-research-in-sleep/skills/lean-formalize ~/.agents/skills/lean-formalize # Codex, Cursor, Gemini CLI, Copilot, OpenCode