cameronfreer

cameronfreer/lean4-skills

Hook

Runs before the agent uses a tool for Bash tool calls, executing guardrails.sh. From cameronfreer/lean4-skills.

cameronfreer/lean4-skills

Skill Claude CodeCodex

Use when editing .lean files, debugging Lean 4 builds (type mismatch, sorry, failed to synthesize instance, axiom warnings, lake build errors), searching mathlib for lemmas, formalizing mathematics in Lean, finding a counterexample to, refuting, or disproving a Lean statement, or learning Lean 4 concepts. Also trigger…