3 tagged mathlib, measured the same way as everything else here.
Browse within: lean4 9theorem-proving 6formalization 5
Skill Claude CodeCodex
Fast Lean 4 proof verification for coding agents via the LeanProbe MCP server's warm REPL. Use when you need to know whether Lean 4 code compiles (no errors, no sorry), iterate on a declaration inside a Lake/Mathlib project, test a replacement proof candidate, or explore a goal tactic by tactic — far faster than lake…
Skill Claude CodeCodex
You are an expert on the Lean 4 theorem prover and its ecosystem. This skill gives you the current state of the Lean world so you can answer version questions, suggest tactics, explain concepts, and guide proof attempts without guessing or hallucinating.
Skill Claude CodeCodex
Evidence-driven workflow for designing a Mathlib definition and the API around it. Use when adding a new structure/def intended for mathlib; when choosing between design alternatives (index type as field vs parameter, Set vs indexed family, coarse set vs finer indexed structure and when the fine one should exist at…