scottnarmstrong/leanautoformalizationskills/lean-learnings

Lean Learnings

Use these empirical lessons as hypotheses to test, not as universal policy. Check the repository's own instructions, inspect the definitions and imports in the current version of Mathlib, profile before changing architecture, and A/B any performance intervention.

Reference map

Working principles

• Treat the dependency set and quantifier order of every public constant as part

of the theorem. Audit types and instance arguments as well as named binders.

• Keep source statements, source dependency topology, Lean declarations, and

Lean proof status distinct. A source dependency graph records source topology; it does not certify a Lean proof.

• Do not add axioms, placeholders, or proof-step hypotheses to make a theorem

elaborate. Preserve the mathematical statement and change the proof or API.

• Profile the dominant phase before restructuring. Narrow imports, helper

extraction, explicit arguments, local instance caches, and carrier changes address different causes.

• Treat EuclideanSpace, direct Pi types, bundled Lp, and bare functions as

design choices with different APIs and elaboration costs. Change carriers only after checking the mathematics, downstream API, and measured cost.

• Keep nonlinear and transcendental expressions opaque while proving small

algebraic side lemmas. Prefer controlled rewriting and minimal automation.

• Preserve dependency build artifacts according to the current repository's

build policy. Never turn a project-specific cache rule into a general Lake command.

• Record a reproducible lesson: Lean/Mathlib version, minimal trigger, measured

symptom, intervention, and an A/B check.

Related skills

• lean-workflow — router for choosing the appropriate Lean workflow
• lean-project-architecture — declarations, module boundaries, and reusable APIs
• lean-proof-patterns — stable translations from mathematics to Lean proofs
• lean-search-discovery — finding existing Mathlib declarations
• lean-elaboration — profiling and improving elaboration performance
• lean-statement-audit — source, binder, semantics, consumption, and axiom checks
• build-proof-dependency-graph — source-level dependency topology