Use when deciding whether a formalized proof should delegate to Mathlib, when refactoring standalone proofs into Mathlib wrappers, or when reviewing delegation refactors for correctness.
Instalação
Instalar com Codex ou Claude Copie este prompt, cole no Codex, Claude ou outro assistente e deixe que ele revise a página da skill e instale para você.
Use when deciding whether a formalized proof should delegate to Mathlib, when refactoring standalone proofs into Mathlib wrappers, or when reviewing delegation refactors for correctness.
allowed-tools
Read, Edit, Bash, Glob, Grep
Mathlib Delegation for FormalFrontier
This skill guides the decision and execution of refactoring formalized proofs from standalone implementations to thin Mathlib wrappers. Delegation produces shorter, more maintainable code — but requires care to avoid losing fidelity to the textbook.
When to Delegate
Delegate to Mathlib when:
Mathlib has the exact result (possibly under a different name or with more generality)
Your proof reimplements Mathlib internals (e.g., building AbsoluteValue from scratch when AbsoluteValue.trivial exists)
The proof is a special case of a Mathlib theorem (e.g., "Z_(p) is a DVR" follows from Mathlib's general Dedekind domain localization result)
Do NOT delegate when:
The textbook statement adds pedagogical value beyond what Mathlib provides (keep the formalized statement, delegate only the proof)
Mathlib's version has different hypotheses that change the mathematical meaning
The delegation would obscure the connection to the textbook presentation
Decision Checklist
Before starting a delegation refactor:
Find the Mathlib declaration: Use the mathlib-api-lookup skill
Verify signature compatibility: Check that Mathlib's hypotheses match or generalize yours
Check generality direction: Mathlib is often more general (works for any Dedekind domain, not just Z). This is fine — your item instantiates the general result
Confirm the result is the same: Not just "similar" — mathematically identical for the relevant case
Delegation Patterns
Pattern 1: Full Delegation (replace definition + proof)
When Mathlib has both the definition and the theorem, replace both.
Example: Example 1.3 — trivial absolute value (PR #125)
Before (custom 9-line definition):
noncomputable def trivialAbsoluteValue (k : Type*) [DecidableEq k] [Field k] :
AbsoluteValue k ℝ where
toFun x := if x = 0 then 0 else 1
map_mul' x y := by
by_cases hx : x = 0 <;> by_cases hy : y = 0 <;> simp [hx, hy, mul_comm]
nonneg' x := by split <;> norm_num
eq_zero' x := by constructor <;> intro h <;> simp_all [ite_eq_left_iff]
add_le' x y := by
by_cases hx : x = 0 <;> by_cases hy : y = 0 <;> simp [hx, hy]
by_cases hxy : x + y = 0 <;> simp [hxy]
Find the Mathlib declaration (see mathlib-api-lookup skill)
Write the delegated version alongside the original (don't delete yet)
Verify it compiles: lake build must pass with zero errors
Update the docstring to reference the Mathlib declaration:
/-- Example 1.14: The localization ℤ_(p) is a DVR.
This delegates to Mathlib's `IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain`,
which establishes the result for any Dedekind domain localized at a nonzero prime. -/
Clean up imports: Remove imports that were only needed by the old proof; add any new imports needed
Remove the old code once the new version compiles
Documentation Pattern
Every delegated item should have:
Module docstring (/-! ... -/): High-level description of the textbook item
Declaration docstring (/-- ... -/): One line stating the result, one line naming the Mathlib declaration being used
Inline comments only where the delegation is non-obvious (e.g., explaining why (K := K) is needed for instance resolution)
Example:
/-!
# Example 1.14: Localization at a prime ideal
The localization ℤ_(p) for a prime p is a discrete valuation ring (DVR).
This delegates to Mathlib's general result for Dedekind domain localizations.
-/
/-- ℤ localized at a nonzero prime ideal is a DVR.
Delegates to `IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain`. -/
theorem localization_at_prime_is_dvr ...
Common Pitfalls
1. Name Mismatches
Mathlib declarations often have different names than you'd expect. Use grep -r on .lake/packages/mathlib/ to find the exact name. Primed variants (foo') are common and have slightly different hypotheses.
2. Generality Differences
Mathlib may require more general type parameters. Use named arguments ((K := K)) to help instance resolution when the general version doesn't infer your specific types.
3. Missing Instances
After delegation, the proof may fail because an instance that was manually constructed in the old proof is now needed by Mathlib's automation. Use haveI to provide it:
haveI : Fact (Nat.Prime p) := ⟨hprime⟩
4. Import Changes
Delegation often changes which Mathlib modules are needed. After refactoring:
Remove imports that are no longer used
Add imports for the delegated declaration
Verify with lake build — import errors are immediate
5. Breaking Downstream Code
If other files reference lemmas or intermediate steps from the old proof, the delegation may break them. Check for dependents before deleting helper lemmas:
