Interactive Lean 4 + Mathlib formalization from a Claude Code conversation
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.
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