5 tagged formalization, measured the same way as everything else here.
Browse within: lean4 5mathlib 5theorem-proving 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…