r-irbe 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 newClassicalimport), handoff to@lean-proof-reviewand@lean-enforcement.
Recovery & STOP
- STOP if a foundational choice silently introduces a new axiom —
#print axiomsmust show onlypropext,Classical.choice,Quot.sound(andfunextis a theorem, not an axiom). Escalate to@lean-review-councilif uncertain. - STOP and handoff to
@lean-researchif 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 axiomschecks 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/Ringinstance that already exists in Mathlib — it triggers diamond / overlap issues. SearchMathlib.Algebra.Group.Defsfirst. - Do not
open Classicalat file scope — it pollutes everydecidedownstream. Open it only inside the proof that needs it. - Do not reach for
Mathlib.CategoryTheory.*if the same statement can be phrased inMathlib.Order.*orMathlib.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 |
See also
../../references/lean4-math-foundations.md— Foundational Mathematics Encyclopaedia (full encyclopaedia, extracted from this skill)../../templates/Template_Foundation.md— Template: Foundation modules (types, structures, decidable preds)../../references/lean4-proof-strategy.md— Proof strategy & error priority../../references/mathlib4-conventions.md— Mathlib4 naming and file conventions