Lean math foundations

Skill r-irbe/proof-skills/skills/lean-math-foundations

APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.

Install

npx -y skills add r-irbe/proof-skills --skill lean-math-foundations

Assembled from the repository path, not quoted from the project. Check it against their README if it does not work.

One thing to look at

2 stars2 stars. Stars are a popularity signal and not a quality one, but at this level it is likely that nobody has read this closely except its author, and you would be relying on your own review.

What its author says it does

Copied from the file, not written here

USE FOR: foundational mathematics in Lean 4 — Lean's type system (Prop / Type / universes), classical vs constructive choices, Mathlib's algebraic typeclass hierarchy (Group / Ring / Order / Lattice / Module / Algebra), category theory basics, and any proof that needs foundational reasoning about types, propositions, or universes. DO NOT USE FOR: applied lattice instances such as severity / quality-gate lattices (use @lean-math-discrete); analysis-flavoured algebra such as normed-space structure (use @lean-math-analysis); writing a specific proof (use @lean-proof); reviewing a finished proof (use @lean-proof-review). TRIGGERS: type universe, Prop vs Type, classical reasoning, Classical.choice, algebraic typeclass, Mathlib hierarchy, category theory, propext, funext.

SKILL.md

8.1 KB, as published. Nobody here has run it

Lean 4 Mathematical Foundations

Guide to formalizing foundational mathematics in Lean 4, covering the structures and patterns that underpin all domain-specific formalization work.

Routing

USE FOR: foundational mathematics in Lean 4 — Lean's type system (Prop / Type / universes), classical vs constructive choices, Mathlib's algebraic typeclass hierarchy (Group / Ring / Order / Lattice / Module / Algebra), category theory basics, and any proof that needs foundational reasoning about types, propositions, or universes.
DO NOT USE FOR: applied lattice instances such as severity / quality-gate lattices (delegate to @lean-math-discrete); analysis-flavoured algebra such as normed-space structure (delegate to @lean-math-analysis); writing a specific proof (delegate to @lean-proof); reviewing a finished proof (delegate to @lean-proof-review).
TRIGGERS: type universe, Prop vs Type, classical reasoning, Classical.choice, algebraic typeclass, Mathlib hierarchy, category theory, propext, funext.

Workflow

Identify whether the question is about Lean's logical foundation (Part 1), Mathlib's typeclass hierarchy (Parts 2–5), or a category-theoretic construction (later parts).
Locate the relevant Part below and read the project-relevance callouts before applying any pattern.
If the answer is a specific proof, handoff to @lean-proof; if it is a soundness-affecting choice (e.g., adding a new Classical import), handoff to @lean-proof-review and @lean-enforcement.

Recovery & STOP

STOP if a foundational choice silently introduces a new axiom — #print axioms must show only propext, Classical.choice, Quot.sound (and funext is a theorem, not an axiom). Escalate to @lean-review-council if uncertain.
STOP and handoff to @lean-research if the question is about a result not present in Mathlib at the current pin (e.g., a new universe-polymorphism API).

Handoffs

Predecessors: agent:gateway, skill:lean-proof (mid-proof typeclass synthesis failure), skill:lean-research (when a survey turns up a foundational construct).
Successors: skill:lean-proof (apply the foundational pattern in a concrete proof), skill:lean-proof-review (verify axiom impact), skill:lean-enforcement (run native-decide / #print axioms checks after the change).

Detailed reference

Full encyclopaedia content (Parts 1 through 6) lives in references/lean4-math-foundations.md. Load that file when authoring; the SKILL.md only carries the dispatch contract and the high-frequency pitfalls / recipes (kept inline below).

Part	Topic	Covers
Part 1	Lean's Logical Foundations	type universes, classical vs constructive, Prop vs Decidable, equality variants
Part 2	Set Theory in Mathlib	Set vs Finset, set operations, well-founded recursion, choice principles
Part 3	Algebraic Hierarchies	Monoid → Group → Ring → Field, Order typeclasses, instance discovery
Part 4	Order Theory	Preorder, PartialOrder, LinearOrder, Lattice, Galois connections
Part 5	Logic and Proof Techniques	classical reasoning, decidability, choice, propositional extensionality
Part 6	Category Theory Basics	Mathlib's CategoryTheory namespace; when to use it (rarely)

Part 7 — Research Council Integration

Consolidated into the single canonical routing matrix: references/research-council-skill-map.md (see the "Foundations" section). When dispatching a question to a council member, cite that table rather than restating the rows here.

Part 8 — Common Pitfalls & Anti-Patterns

Pitfall	Symptom	Recovery
Decidable-instance synthesis loop	`failed to synthesize Decidable` + stack-depth warning	Replace `infer_instance` with `Classical.dec _`; mark the surrounding def `noncomputable` if needed
Universe-polymorphism mismatch	`type mismatch` involving `.{u}` arguments in elaboration	Annotate universes explicitly (`@F.{u, v}`); prefer `Type _` over `Type 0` in generic positions
`simp` set explosion via algebraic typeclasses	Trivial goal hangs `simp`	Switch to `simp only [...]` with a hand-picked list; drop `Algebra.*` lemmas when working over `Nat`
Unintended `Classical.choice` leak	`#print axioms` shows `Classical.choice` on a supposedly constructive proof	Search for `Classical.byContradiction` / `decide`-via-`Decidable.decide` coercions; localise the `open Classical`
`Prop` ↔ `Bool` confusion	`simp` won't reduce a `decide`-based goal	`Decidable.decide_eq_true_iff` bridges them; or rewrite via `Bool.decide` lemmas
`funext` on dependent functions	`funext_iff` doesn't fire	`funext_iff` is non-dependent only; for `Π x, ...` unfold and apply `funext` directly

Anti-patterns

Do not redeclare a Group / Ring instance that already exists in Mathlib — it triggers diamond / overlap issues. Search Mathlib.Algebra.Group.Defs first.
Do not open Classical at file scope — it pollutes every decide downstream. Open it only inside the proof that needs it.
Do not reach for Mathlib.CategoryTheory.* if the same statement can be phrased in Mathlib.Order.* or Mathlib.Algebra.Order.*; the category-theoretic phrasing is correct but harder to automate against.

Part 9 — Recovery Recipes

Situation	First-line recipe
Typeclass synthesis stuck on an instance you believe exists	`set_option synthInstance.maxHeartbeats 40000` temporarily, then `exact?` to confirm the instance Mathlib expects
`simp` loops on an algebraic rewrite	`simp only [list]`; replace `add_comm` with `Nat.add_comm` etc. (qualified names cut through diamond confusion)
`decide` can't see a `Decidable` instance	`classical decide` (uses `Classical.dec`); or rewrite the predicate to one with a `Decidable` instance you can locate via `#check`
Universe issue blocks elaboration	Annotate universes explicitly (`@F.{u, v}`) at the call site
Need a foundational lemma absent from Mathlib at the pin	Author it locally in a host-repository `Foundation/Helpers.lean` (mirroring the Mathlib namespace) and open a Lean/Mathlib PR via `@lean-pr`
Want to suppress an instance for one section	`attribute [-instance] foo in section` — preferable to deleting the instance entirely