with one click
with one click
[HINT] Download the complete skill directory including SKILL.md and all related files
| name | mathlib-quality |
| description | Mathlib code quality and style enforcement for Lean 4 |
| trigger | {"filePatterns":["*.lean"],"keywords":["mathlib","style","cleanup","golf","PR","submit","bump","upgrade","update","status","progress","bottleneck","stuck","frontier"]} |
This skill activates when:
.lean files intended for mathlib contribution/project-statusThis skill helps bring Lean 4 code up to mathlib standards by:
| Command | Description |
|---|---|
/develop | Planning only. Searches mathlib, designs API, drafts proof sketches from your sources, writes a detailed ticket board where every ticket contains the full Lean statement, a numbered proof sketch citing sources, the mathlib lemmas needed, and the generality decision. After approval, /develop stops — workers run via /extended-work. |
/extended-work | Execution only. Pick up one ticket from the /develop board and work it to completion or concrete approach error. Strict no-complaining, no-pivoting, no-divergence mode: forbidden phrases include "this is a multi-week effort", "this is too complex", "let me try a different approach without first proving the planned one fails". Stops only on DONE / PROOF-SKETCH FAILURE / MATHLIB GAP / SCOPE-DEFINITION ERROR / DEPENDENCY NOT MET — each with a required concrete report. |
/cleanup | Style audit + cleanup + golf (whole file or single declaration). 9-phase methodical workflow: doctor (baseline build) → prepare → audit punch-list → file-level fixes → per-declaration deep golf with diff gates → refactoring → final gates + cumulative checks → built-in /simplify pass → report. Absorbed: /check-style (Phase 2 audit), /check-mathlib (Phase 4 item 13 — five-method search + six strict rules + common-equivalents lookup), the inline mechanical pass of /generalise (Phase 4 item 18), and shouyi-style diff gates (Phase 4 + 6). Phase 6.5 hand-off to the built-in /simplify skill catches holistic issues the rule-driven pass missed. |
/cleanup-all | Run /cleanup on every file in the project, tracked file by file |
/decompose-proof | Break long proofs into helper lemmas |
/overview | Project declaration inventory for consolidation analysis |
/project-status | Mathematician's snapshot driven by un-formalising the Lean code — chat summary + live browser dashboard. Source of truth is the project's .lean files (not the ticket file). The agent reads every declaration's body and writes English annotations (math name, description, proof-state narrative for sorries, ingredients in scope, what-would-help) to .mathlib-quality/.status_annotations.json. Server merges that sidecar into the live dashboard at http://127.0.0.1:8765/ (clickable dependency tree built from in-body references, arrow-key nav, polls every 3 s, KaTeX math, Lean syntax highlighting). Body-hash caching keeps re-runs fast. Drill-down by decl name: /project-status fooBar_comp or /project-status MyProj.fooBar_comp. Tickets are a status overlay only. Tone is descriptive math reportage, not difficulty rhetoric. Flags: --no-browser, --skip-unformalise, --stop. |
/expert-review | Two-mode skill for external mathematical review. Mode 1: produce a self-contained REVIEW_BRIEF.md (no Lean, no file paths) — goals, plan, references, status, blockers, numbered questions — and stop, waiting for the reviewer's reply. Mode 2 (--reply): once the reviewer responds, map their answers onto our questions, propose ticket/work-order updates, apply only after user approval. Session history persists in .mathlib-quality/expert-review/<date>/. |
/generalise | Audit a lemma or definition for assumption weakening. Tries mechanical weakenings from a catalogue (typeclass parents, drop-unused, point-localise, strict→weak), then performs a literature search (WebSearch + ChatGPT MCP if available + mathlib's five-method search). Auto-applies small safe changes; presents big changes (public-API, restating, renames) as numbered options for user approval. |
/split-file | Split large files (>1500 lines) into focused modules |
/pre-submit | Pre-PR submission checklist |
/bump-mathlib | Bump mathlib version and fix resulting breakage |
/fix-pr-feedback | Fetch PR comments, implement fixes locally, wait for user approval before pushing, then watch CI to completion. 8-phase workflow with explicit comment-coverage check. |
/setup-rag | Set up RAG MCP server for PR feedback search |
/setup-chatgpt | Set up ChatGPT MCP server for mathematical second opinions |
/teach | Teach the skill a project-specific pattern or convention |
/contribute | Contribute local learnings back to the repo via PR |
/integrate-learnings | (Maintainers) Process community contributions into reference docs |
For enhanced suggestions based on 4,600+ real mathlib PR reviews, run /setup-rag to configure the RAG MCP server. This gives Claude Code access to searchable PR feedback examples for golfing and style.
For mathematical second opinions from ChatGPT during formalization work, run /setup-chatgpt. This creates an MCP server that lets Claude Code query ChatGPT via the Codex CLI for proof strategies, Mathlib API hints, or verification of mathematical claims. Requires the ChatGPT desktop app and a Plus/Pro subscription.
UpperCamelCase.lean (e.g., TopologicalSpace.lean)module keyword before importsby placement: Always at END of preceding line (not on its own line)· (not indented) for subgoalsfun x ↦ ... over λ x, ...<| over $ to avoid parentheseschange over show in proofsFill lines to ~100 characters. Do NOT break lines at 50-60 characters when there is room for more. Short lines waste vertical space and make proofs look longer than they need to be.
Rule: Pack as much as fits on each line, up to the 100-character limit. Only break when you must.
Lean's own pretty-printer (format.width, default 120 cols) follows the same principle — fill to
the target width, break at natural boundaries. Mathlib uses 100 chars. Match the compactness that
Lean's formatter would produce at width 100.
Formatting tools to use:
simp only lists: Use simp? and apply its "Try this:" suggestion — Lean formats it correctly#check @theorem_name as a width reference — if Lean packs the type
compactly, your declaration syntax should be equally compactexact/rw calls: Use exact?/rw? when available for correct formattingSignatures: Put multiple parameters on the same line. Only break to a new line when the next parameter would exceed 100 chars.
-- BAD: breaks lines too early, wastes vertical space
theorem pv_chain_identity
(S : Finset UpperHalfPlane)
(hS : ∀ p ∈ S, p ∈ 𝒟)
(hS_complete :
∀ p, p ∈ 𝒟 →
orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) :
∃ H₀ : ℝ, ... := by
-- GOOD: fills to ~100 chars, fewer lines
theorem pv_chain_identity (S : Finset UpperHalfPlane) (hS : ∀ p ∈ S, p ∈ 𝒟)
(hS_complete : ∀ p, p ∈ 𝒟 → orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) :
∃ H₀ : ℝ, ... := by
simp only lists: Pack lemma names to fill the line. Do not put one or two per line.
-- BAD: artificially narrow
simp only [ne_eq, mul_eq_zero,
OfNat.ofNat_ne_zero, not_false_eq_true,
ofReal_eq_zero, Real.pi_ne_zero,
I_ne_zero, or_self]
-- GOOD: fills to ~100 chars
simp only [ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, not_false_eq_true, ofReal_eq_zero,
Real.pi_ne_zero, I_ne_zero, or_self]
have statements and expressions: Keep on one line when possible.
-- BAD: unnecessary line breaks in expression
rw [show -(2 * ↑Real.pi * I *
((k : ℂ) / 12 - (orderAtCusp' f : ℂ))) =
2 * ↑Real.pi * I *
(-((k : ℂ) / 12 - (orderAtCusp' f : ℂ)))
from by ring] at h_eq
-- GOOD: pack the expression
rw [show -(2 * ↑Real.pi * I * ((k : ℂ) / 12 - (orderAtCusp' f : ℂ))) =
2 * ↑Real.pi * I * (-((k : ℂ) / 12 - (orderAtCusp' f : ℂ))) from by ring] at h_eq
Return type: Keep conclusion on the same line as : when it fits.
-- BAD: conclusion on separate line unnecessarily
theorem foo (h : P) :
Q := by
-- GOOD: fits on one line
theorem foo (h : P) : Q := by
by Placement (CRITICAL)-- CORRECT: by at end of preceding line
theorem foo : P := by
exact h
-- WRONG: by on its own line
theorem foo : P :=
by exact h
-- Use focusing dot · at column 0
theorem foo : P ∧ Q := by
constructor
· exact hp
· exact hq
Use where syntax for structure/class instances:
instance instOrderBot : OrderBot ℕ where
bot := 0
bot_le := Nat.zero_le
CRITICAL: Different naming conventions for defs vs lemmas/theorems!
| Declaration Type | Returns | Case Style | Example |
|---|---|---|---|
lemma/theorem | Prop | snake_case | continuous_of_bounded |
def | Data (ℂ, ℝ, Set, etc.) | lowerCamelCase | cauchyPrincipalValue |
structure/inductive | Type | UpperCamelCase | ModularForm |
| Structure fields | - | lowerCamelCase or snake_case | toFun, map_one' |
Key rule: Look at what the declaration returns:
snake_caselowerCamelCaseUpperCamelCaseExamples:
-- Lemmas/theorems (return Prop) → snake_case
theorem continuous_of_uniform : Continuous f := ...
lemma norm_le_of_mem_ball : ‖x‖ ≤ r := ...
-- Defs returning data → lowerCamelCase
def cauchyPrincipalValue (f : ℝ → ℂ) : ℂ := ...
def residueAtPole (f : ℂ → ℂ) (z₀ : ℂ) : ℂ := ...
def fundamentalDomain : Set ℂ := ...
-- Types → UpperCamelCase
structure ModularForm where ...
inductive BoundarySegment where ...
| Type | Variables |
|---|---|
| Universes | u, v, w |
| Generic types | α, β, γ |
| Propositions | a, b, c |
| Type elements | x, y, z |
| Assumptions | h, h₁, h₂ or hf, hg |
| Predicates | p, q, r |
| Lists/Sets | s, t |
| Naturals | m, n, k |
| Integers | i, j, k |
| Groups | G, H |
| Rings | R, S |
| Fields | K, 𝕜 |
| Vector spaces | E, F |
LE, Ne (not Le, NE)Factorization not Factorisation_aux suffix, must be privateIsNormal), no prefix for adjectivesAll lemma/definition names MUST follow mathlib conventions. When cleaning up a file:
Common naming issues to fix:
| Bad Name | Good Name | Rule |
|---|---|---|
myLemma | my_lemma | snake_case for lemmas |
Lemma1 | lemma_one or descriptive | no numbers, snake_case |
fooAux | foo_aux | snake_case with _aux suffix |
helper | main_theorem_aux | name should reference parent |
Factorisation | Factorization | American English |
continuous_Function | continuous_function | consistent snake_case |
| Symbol | Name in identifiers |
|---|---|
∨ | or |
∧ | and |
→ | imp or of (hypothesis) |
↔ | iff (often omitted) |
¬ | not |
∀ | forall or all |
∃ | exists |
= | eq (often omitted) |
≠ | ne |
∈ | mem |
∪ | union |
∩ | inter |
⋃ | iUnion (indexed) |
⋂ | iInter (indexed) |
\ | sdiff |
ᶜ | compl |
+ | add |
- | sub (binary) or neg (unary) |
* | mul |
^ | pow |
/ | div |
• | smul |
∣ | dvd |
≤ | le or ge (swapped) |
< | lt or gt (swapped) |
⊔ | sup |
⊓ | inf |
⨆ | iSup (indexed) |
⨅ | iInf (indexed) |
C_of_A_of_BFor theorem A → B → C, name it C_of_A_of_B (hypotheses in appearance order):
-- Good: hypotheses in order of appearance
add_pos_of_pos_of_pos -- conclusion: add_pos; hyps: pos, pos
continuous_of_uniform -- conclusion: continuous; hyp: uniform
norm_bound_of_compact -- conclusion: norm_bound; hyp: compact
-- Use abbreviations
pos, neg, nonpos, nonneg -- replace zero_lt, lt_zero, le_zero, zero_le
-- Bad names
lemma1, helper, aux -- non-descriptive
myCustomLemma -- wrong case
| Pattern | Naming |
|---|---|
| Extensionality | .ext (marked @[ext]), .ext_iff |
| Injectivity | f_injective (Function.Injective), f_inj (bidir, @[simp]) |
| Induction (Prop) | T.induction_on (value first), T.induction (constructors first) |
| Recursion (Type) | T.recOn (value first), T.rec (constructors first) |
Most predicates are prefixes: isClosed_Icc, isOpen_ball
Exceptions (suffixes, like atoms): _injective, _surjective, _bijective, _monotone, _antitone
/-! ## Section Name -/) throughout the file
_aux suffix (e.g., foo_aux, bar_step_aux)privateThe skill learns from every use and gets better over time. There are three layers:
Every command (/cleanup, /develop, /bump-mathlib, etc.) automatically records significant learnings to .mathlib-quality/learnings.jsonl in your project. This captures:
The MCP server loads local learnings at query time and boosts search results with project-specific patterns. This means suggestions improve as you use the tool more within a project.
Run /contribute to review your local learnings and create a PR on the mathlib-quality repo. This shares your discoveries with all users. Learnings are anonymized before contribution.
Use /teach to explicitly record project-specific patterns:
/teach "always use grind before omega for Fin goals in this project"
/teach "in this codebase, prefer explicit universe variables"
.mathlib-quality/learnings.jsonl (JSONL format, one entry per line)data/community_learnings/ (contributed via PRs)skills/mathlib-quality/learning/schema.md for the full JSON schemaUse /develop to plan and execute a mathematical development:
/develop creates a comprehensive plan with ticket board/cleanup tickets keep code at mathlib quality/overview to generate a full declaration inventory./cleanup on each file — one agent per declaration./decompose-proof on files with long proofs./pre-submit before creating PR.For quick single-proof golfing: Use /cleanup file.lean theorem_name.
/fix-pr-feedback/pre-submit before pushingStart here - comprehensive guide from PR analysis:
references/mathlib-quality-principles.md - Core quality principles (synthesized from 4,600+ PR reviews)For detailed guidance:
references/style-rules.md - Complete formatting rulesreferences/naming-conventions.md - Naming patterns (defs vs lemmas distinction)references/proof-patterns.md - Proof golf techniquesreferences/pr-feedback-examples.md - Real feedback examplesreferences/linter-checks.md - Automated linter rulesPattern-specific examples (load based on proof content):
examples/inline_have.md - Inline have blocks (77 PR examples)examples/term_mode.md - Convert to term mode (311 exact removals)examples/simp_golf.md - Simplify simp usage (311 simp removals)examples/automation.md - Use grind/fun_prop (1144 automation suggestions)examples/decompose_proof.md - Break long proofs into helper lemmasThis skill works alongside the lean4-theorem-proving skill:
lean_diagnostic_messages to check for errors after editslean_goal to verify proof state during golfinghave blocks - Inline have foo := bar unless used 2+ times
have h := lemma x → inline as lemma x where usedhave h : T := by ... → keep (has proof content) or extract as helpersimp without arguments - Use simp only [...] for non-terminal simp
simp (closing the goal) should NOT be squeezed unless performance is poorsorry - Remove all before submissionset_option trace.*fun_prop - Prefer fun_prop over continuity/measurabilityprivate with _aux suffixby on its own line - ALWAYS put by at end of preceding lineλ instead of fun - Use fun x ↦ ...When renaming/removing public declarations, use:
@[deprecated (since := "YYYY-MM-DD")]
alias old_name := new_name
-- With explanation
@[deprecated "Use foo_bar instead" (since := "YYYY-MM-DD")]
theorem old_theorem ...
Deprecations can be removed after 6 months.
Rule: No proof should exceed 50 lines. Target: main theorems <15 lines.
Long proofs indicate the mathematical structure hasn't been properly captured. Every proof decomposes naturally based on its mathematical content.
| Length | Action |
|---|---|
| <15 lines | Ideal |
| 15-30 lines | Consider decomposition |
| 30-50 lines | Must decompose |
| >50 lines | Critical - aggressive decomposition required |
This is a careful, systematic process. Do it right, not fast.
Scan the file and list ALL proofs >30 lines with their line numbers and counts.
Before touching any code, read the entire proof and answer:
cases, by_cases, rcases that split into independent branches?Before extracting ANY helper, search mathlib to see if it already exists:
lean_loogle "Continuous → Bounded" -- Type pattern search
lean_leansearch "continuous function on compact is bounded" -- Natural language
lean_local_search "continuousOn_compact" -- Local name search
Many "helper lemmas" are already in mathlib. Use them instead of writing new ones.
CRITICAL: Don't create single-use helpers. Before extracting, ask:
-- BAD: Single-use helper tied to specific context
private lemma residue_theorem_step1 (γ : PiecewiseC1Curve) (S0 : Finset ℂ)
(hγ_in_U : ∀ t ∈ Icc γ.a γ.b, γ.toFun t ∈ U) : ... := ...
-- GOOD: General lemma that could be useful elsewhere
lemma norm_sum_le_of_disjoint_balls {S : Finset ℂ} {ε : ℝ} (hε : 0 < ε)
(h_disjoint : ∀ s ∈ S, ∀ s' ∈ S, s ≠ s' → Disjoint (ball s ε) (ball s' ε)) :
‖∑ s ∈ S, f s‖ ≤ ∑ s ∈ S, ‖f s‖ := ...
If a proof has cases h with | inl => ... | inr => ... or by_cases:
-- Before: 80-line proof with two cases
theorem foo : P ∨ Q → R := by
intro h
cases h with
| inl hp => ... 40 lines ...
| inr hq => ... 40 lines ...
-- After: Two focused helpers + short main proof
private lemma foo_of_left (hp : P) : R := by ... 40 lines ...
private lemma foo_of_right (hq : Q) : R := by ... 40 lines ...
theorem foo : P ∨ Q → R := fun h => h.elim foo_of_left foo_of_right
Review ALL definitions in the file:
norm_bound_of_continuous, not theorem_aux1-- Good: describes what it proves
private lemma norm_bound_of_continuous_on_compact : ...
private lemma limit_of_dominated_convergence : ...
lemma disjoint_balls_of_separated : ... -- General, could be public
-- Bad: just references parent
private lemma big_theorem_aux1 : ...
private lemma step_2 : ...
| Generality | Visibility |
|---|---|
| Very general, useful elsewhere | lemma (public) - consider if mathlib has it |
| Specific to this file's topic | private lemma |
| Only used once, can't generalize | private lemma with _aux suffix |
Main theorems should read as clear outlines:
private lemma continuity_bound : ‖f x‖ ≤ C := by ...
private lemma dominated_pointwise : ‖f_n x‖ ≤ g x := by ...
theorem main_result : ... :=
limit_theorem (continuity_bound hf) (dominated_pointwise hg)
For each proof >30 lines:
lean_loogle, lean_leansearch)_aux1, _aux2)Rule: Use mathlib DIRECTLY. Do not create wrapper lemmas.
If mathlib has a lemma, USE IT DIRECTLY at call sites. Do NOT create a "convenience wrapper".
A wrapper lemma like this is FORBIDDEN:
-- FORBIDDEN: This just wraps mathlib lemmas
lemma my_finite_lemma [DiscreteTopology S] (hK : IsCompact K) : Set.Finite (S ∩ K) := by
haveI : DiscreteTopology (S ∩ K).Elem := DiscreteTopology.of_subset ‹_› Set.inter_subset_left
exact hK.finite this
Instead, use the mathlib lemmas DIRECTLY where needed:
-- CORRECT: Use mathlib directly at the call site
theorem main_result ... := by
...
haveI : DiscreteTopology (S ∩ K).Elem := DiscreteTopology.of_subset ‹_› Set.inter_subset_left
have h_finite := (hK.inter_left hS_closed).finite this
...
Before creating ANY lemma, ask:
Before creating ANY custom definition or hypothesis condition, search mathlib for an equivalent. When found, use the mathlib version as a type class or instance argument, not a custom Prop.
BAD: Custom condition as explicit hypothesis
-- Custom condition that duplicates mathlib
lemma foo (hS : ∀ s ∈ S, ∃ ε > 0, Metric.ball s ε ∩ S = {s}) : P := ...
GOOD: Mathlib type class as instance argument
-- Use mathlib's DiscreteTopology directly
lemma foo [DiscreteTopology S] : P := ...
| Custom Condition | Use Instead |
|---|---|
∀ s ∈ S, ∃ ε > 0, ball s ε ∩ S = {s} | [DiscreteTopology S] |
∀ s ∈ S, ∃ ε > 0, ∀ s' ∈ S, s' ≠ s → ε ≤ dist s s' | [DiscreteTopology S] |
∀ x, f x ≤ g x (for continuous f, g) | hle : f ≤ g with [Preorder] |
| Custom finiteness predicate | [Finite S] or Set.Finite S |
| Custom compactness predicate | [CompactSpace X] or IsCompact S |
When you need specific properties that your custom condition provided, use mathlib's lemmas:
-- From DiscreteTopology, recover ball isolation:
obtain ⟨ε, hε_pos, hε_ball⟩ := exists_ball_inter_eq_singleton_of_mem_discrete hs
-- From DiscreteTopology, derive positive distance:
-- s' ∉ ball s ε means ε ≤ dist s' s, hence 0 < ‖s' - s‖
have h_pos : 0 < ‖s' - s‖ := by
have h := exists_ball_inter_eq_singleton_of_mem_discrete hs
...
CRITICAL: Search MULTIPLE ways before concluding something isn't in mathlib.
For each custom definition, lemma, or condition:
https://huggingface.co/spaces/delta-lab-ai/Lean-Finder
Supports BOTH type signatures AND natural language queries. This is the most powerful search tool.
Type signature queries:
IsCompact s → DiscreteTopology s → s.Finite∀ x ∈ S, ∃ ε > 0, ball x ε ∩ S = {x}Natural language queries:
lean_loogle "DiscreteTopology → Set.Finite"
lean_loogle "IsCompact → DiscreteTopology → Finite"
lean_loogle "∀ x ∈ S, ∃ ε > 0, _"
lean_leansearch "discrete topology subset inherits discrete"
lean_leansearch "compact set with discrete topology is finite"
lean_leansearch "isolated points metric space"
# Search for key terms
grep -r "DiscreteTopology.of_subset" .lake/packages/mathlib/
grep -r "IsCompact.finite" .lake/packages/mathlib/
Mathlib/Topology/DiscreteSubset.lean, Topology/Compactness/*.leanMathlib/Topology/MetricSpace/*.leanMathlib/Analysis/Normed/*.leanMathlib/Topology/Constructions.leanOften the exact lemma you need is a building block. Search for:
.of_subset, .subset, .inter variants_left, _right variants_of_* implication variantsWhen cleaning up a file:
[TypeClass X] syntaxBefore (25 lines) - WRONG: Custom lemma duplicating mathlib:
lemma finite_of_discrete_inter_compact
(hS : ∀ s ∈ S, ∃ ε > 0, Metric.ball s ε ∩ S = {s})
(hS_closed : IsClosed S) (hK : IsCompact K) : Set.Finite (S ∩ K) := by
have h_discrete : DiscreteTopology (S ∩ K).Elem := by
rw [discreteTopology_subtype_iff']
intro x ⟨hx_S, hx_K⟩
obtain ⟨ε, hε_pos, hε_ball⟩ := hS x hx_S
-- ... 15 more lines manually proving discrete ...
exact (hK.inter_left hS_closed).finite h_discrete
After - CORRECT: DELETE the lemma, use mathlib directly at call sites:
-- The lemma finite_of_discrete_inter_compact is DELETED entirely.
-- At call sites, use mathlib directly:
theorem main_theorem ... := by
...
-- Need finiteness? Use mathlib's IsCompact.finite + DiscreteTopology.of_subset:
haveI : DiscreteTopology (S ∩ K).Elem := DiscreteTopology.of_subset ‹_› Set.inter_subset_left
have h_finite := (hK.inter_left hS_closed).finite this
...
Key mathlib lemmas to use DIRECTLY:
DiscreteTopology.of_subset: discrete topology inherits to subsetsIsCompact.finite: compact + discrete → finiteIs this lemma just combining mathlib lemmas?
├── YES (1-5 lines of mathlib calls) → DELETE IT, use mathlib directly
└── NO (genuinely new content) → Keep it, but search mathlib first
my_foo that just calls Mathlib.foofoo_bar that just calls foo then barGoal: Minimize proof length. One-liners are ideal. Brevity trumps readability.
For thorough optimization, use the deep golfer methodology:
data/pr_feedback/curated_examples.md)lean_multi_attempt on chunks with: grind, aesop, simp_all, fun_prop, omega, ringSee agents/deep-golfer-prompt.md for the full deep golfer methodology.
| Pattern | Savings | Priority |
|---|---|---|
by rfl → rfl | 1 line | ⭐⭐⭐⭐⭐ |
by exact h → h | 1 line | ⭐⭐⭐⭐⭐ |
fun x => f x → f | Tokens | ⭐⭐⭐⭐⭐ |
rw; exact → rwa | 50% | ⭐⭐⭐⭐⭐ |
Single-use have inline | 30-50% | ⭐⭐⭐⭐ |
Multi-step → grind | 60-80% | ⭐⭐⭐⭐⭐ |
.trans chains | 2-3 lines | ⭐⭐⭐⭐ |
fun_prop for Analysis Properties-- IMPORTANT: Unfold definitions first so fun_prop can see structure
example : Continuous F := by simp only [F]; fun_prop
example : Differentiable ℝ f := by simp only [f]; fun_prop
grind for Case Analysis-- Powerful automation for case analysis and Finset/card goals
example (hs : s.card = 1) : ∃ a, s = {a} := by grind
example : castSucc i ≠ 0 := by grind [castSucc_ne_zero_iff]
-- For distance/metric goals
example : dist a b < ε := by grind [Real.dist_eq]
-- For cardinality
example (h : n.primeFactors = ∅) : n ≤ 1 := by grind [Finset.card_eq_zero, primeFactors_eq_empty]
omega for Arithmetic Goals (PREFERRED)For impossible arithmetic/inequality goals (including Fin inequalities), prefer omega as the most direct tactic:
-- omega handles these directly
example (h : n < m) : n + 1 < m + 1 := by omega
example (i : Fin n) : i.val < n := by omega
example (h : a ≤ b) (h' : b < c) : a < c := by omega
ring / ring_nf - Polynomial arithmeticlinarith / nlinarith - Linear/nonlinear arithmeticomega - Integer/natural arithmetic (PREFERRED for arithmetic)aesop - Automated proof searchgrind - Powerful case analysis automationexact? / apply? - Find applicable lemmasMathlib's built-in linters catch these automatically - no need to fix manually:
When a file exceeds ~1500 lines, use /split-file to split it.
Step 1: Group by naming prefix Declarations about the same object share naming prefixes:
cauchyPrincipalValue* → CauchyPrincipalValue.leanresidue*, Residue* → Residue.leanintegral_* → Integration.leanStep 2: Choose structure based on size
For 1500-3000 lines:
Module/
├── Basic.lean -- Definitions + core lemmas
└── Theorems.lean -- Main results (imports Basic)
For >3000 lines:
Module/
├── Defs.lean -- Pure definitions
├── GroupA.lean -- Lemmas about object A
├── GroupB.lean -- Lemmas about object B
└── Main.lean -- Main theorems (imports all)
Step 3: Respect dependencies
Before: ResidueTheory.lean (3000 lines)
After:
ResidueTheory/
├── CauchyPrincipalValue.lean -- PV definitions & lemmas
├── Residue.lean -- Residue definitions & lemmas
└── ResidueTheorem.lean -- Main theorems (imports above)
We have a RAG (Retrieval Augmented Generation) system built from 4,600+ PR review comments. Use it to find relevant examples for the specific code you're working on.
Option 1: MCP Server (if configured in .mcp.json)
search_golf_examples(code="have h := foo; simp [h]") # Find similar examples
search_by_pattern(pattern="use_grind") # Find grind transformation examples
search_by_topic(topics=["continuity"]) # Find topic-specific examples
get_mathlib_quality_principles() # Get core quality rules
Option 2: Query Script
python3 scripts/query_rag.py --code "simp only [foo]; exact bar" --limit 5
python3 scripts/query_rag.py --pattern use_grind --limit 5
python3 scripts/query_rag.py --tactics simp have exact --limit 5
python3 scripts/query_rag.py --topic continuity --limit 5
simp_to_simpa - Converting simp to simpause_grind - Using grind tactic (50 examples)use_fun_prop - Using fun_prop (22 examples)use_aesop - Using aesop (31 examples)use_omega - Using omega (3 examples)term_mode - Converting to term mode (16 examples)remove_redundant - Removing unnecessary code (24 examples)Key document:
references/mathlib-quality-principles.md - Comprehensive quality guide from PR analysisCurated examples:
data/pr_feedback/curated_examples.md - Best before/after examples with principlesdata/pr_feedback/rag_index_focused.json - Focused index with 891 golf examplesRaw data (4,600+ items):
data/pr_feedback/rag_index.json - Full searchable index (1,905 useful examples)data/pr_feedback/proof_golf_feedback.json - All proof golf suggestions (2,786 items)