8 tagged mathlib, measured the same way as everything else here.
Browse within: lean4 8theorem-proving 6formalization 5
Skill Claude CodeCodex
Turn Magma code into a formalized Lean theorem. Use whenever the user pastes or points at Magma source, asks what a Magma routine is really proving, asks to formalize a computation or a computationally-discovered pattern, or wants a Magma experiment turned into a general statement. Covers running the code on…
Skill Claude CodeCodex
Formalize a claim of ordinary mathematics as Lean 4 + Mathlib and drive the live compile loop to zero errors. Use whenever the user states a mathematical claim, conjecture, exercise or definition; asks to formalize, state, prove, check or Lean-ify something; corrects or refines a previous formalization; asks why a…
Skill Claude CodeCodex
Find and verify the name of a Mathlib lemma, theorem, definition, instance or tactic, and report its real elaborated type. Use whenever the user asks what a theorem is called, whether Mathlib has some fact, what the exact statement or hypotheses of a lemma are, or what the API of a type or namespace looks like; and…
Skill Claude CodeCodex
Screen informal↔Lean 4 statement pairs for faithfulness defects. Use whenever writing, editing, translating, or reviewing Lean 4 theorem or definition statements that are meant to formalize informal mathematics: after drafting a statement, before committing formalizations, when auditing a benchmark file, or when the…
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
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…