Interactive Lean 4 + Mathlib formalization from a Claude Code conversation
7 files for Claude Code: lean-interact, formalize-from-magma, formalize, install and 3 more — 4,212 tokens loaded in every session.
CLAUDE.md A 4,212 tok .claude/settings.json C — .claude/skills/formalize-from-magma/SKILL.md A 109 tok .claude/skills/formalize/SKILL.md A 168 tok .claude/skills/install/SKILL.md C 221 tok .claude/skills/lean-session/SKILL.md A 154 tok .claude/skills/mathlib-lookup/SKILL.md A 170 tok These files are nasqret/lean-interact's own configuration — they tell Claude Code how to work on this repository, so they are not mods to install elsewhere. Copy one as a starting point and replace the parts that are about this project.