teach
25Command
Teach the skill a new pattern or project convention.
32 13d ago A 11 tokens
original MIT
unformalise
26Command
Turn a Lean declaration into mathematics. Renders the statement and a paragraph-level proof sketch as Unicode in the terminal by default (Γ, ℂ, →, ≤ — readable in chat without any math renderer). Optionally outputs Verso markup (--verso), Markdown (--md), or appends the result to the project's verso-blueprint as a…
32 13d ago A 155 tokens
original MIT
Stop
27Hook
Runs when the agent finishes a response, executing beastmode_stop.sh. From CBirkbeck/mathlib-quality.
32 13d ago A
tokens not measured
original MIT
PreToolUse
28Hook
Runs before the agent uses a tool for Bash tool calls, executing pr_gate.sh. From CBirkbeck/mathlib-quality.
32 13d ago A
tokens not measured
copy · 67% MIT
Skill Claude CodeCodex
Mathlib code quality and style enforcement for Lean 4.
32 13d ago A 15 tokens
original MIT
Agent
You audit AND fix Lean 4 declarations. For each declaration in your batch, you MUST.
32 13d ago A 0 tokens
original MIT
Agent
You are a meticulous proof golfer that analyzes proofs line by line, searching for optimization opportunities using patterns from real mathlib PR reviews.
32 13d ago A 0 tokens
original MIT
Agent
You are a specialized agent for splitting large Lean 4 files into smaller, focused modules.
32 13d ago A 0 tokens
original MIT
Agent
You are a specialized agent for finding mathlib equivalents of custom definitions and lemmas.
32 13d ago A 0 tokens
original MIT
Agent
You are a specialized agent for golfing Lean 4 proofs to mathlib standards. Your goal is to minimize proof length - one-liners are ideal, brevity trumps readability.
32 13d ago A 0 tokens
original MIT
Agent
You are a specialized agent for decomposing long Lean 4 proofs to mathlib quality standards.
32 13d ago A 0 tokens
original MIT
voyager
36Skill Claude CodeCodex
Post a "what's new in Tau Ceti" update as the voyager bot on the Lean Zulip — detect named theorems and significant definitions newly added to the TauCeti library since the last update, verify they are genuinely new (not already in Mathlib) and genuinely significant (via a ChatGPT second opinion), and post them with…
32 13d ago B 111 tokens
original MIT
Instructions file CodexOpenCode
Instructions for CBirkbeck/AINTLIB, covering aintlib — rules for ai sessions, structure, if you are a producer (proving new theorems), if you are a cleaner (the fleet, on main) and if you are the bump worker (daily, on main).
5 4d ago A 2,270 tokens
original Apache-2.0
Instructions file
Instructions for CBirkbeck/AINTLIB, covering aintlib — rules for ai sessions, structure, if you are a producer (proving new theorems), if you are a cleaner (the fleet, on main) and if you are the bump worker (daily, on main).
5 4d ago A 2,269 tokens
copy · 97% Apache-2.0