Skills
12 skills · index.json
-
build-proof-dependency-graph
Build an independently reviewed, source-level dependency database anchored to exact author-frozen Lean declarations. Use after source-first approval of one-declaration anchor files, when an orchestrator must trace roots through LaTeX, Markdown, or other line-addressable proof sources, expose substantive proof steps and external inputs, and produce a structurally checked graph for later Lean orchestration. Do not use this skill to inspect implementation Lean code or decide whether any theorem is proved.
-
lean-elaboration
Diagnose and improve Lean 4 elaboration performance in a repo — locate genuine hot spots, route by profile phase, apply the proven levers (consumer import narrowing, nlinarith elimination, targeted simp-only, head-class caches, leaf splits, folding hypothesis types to the abbrev their consumer expects, naming the function in congr), and A/B every change. Use when a repo builds slowly, a file blows past heartbeats, before landing perf edits, or when planning an elaboration campaign.
-
lean-elaboration-test
Run a repeatable elaboration test of ONE Lean 4 repo and write a dated report — snapshot size (date, commit, lines excluding comment-only files), clean project-only rebuild with wall/CPU/parallelism/RSS, heavy-tail and per-namespace breakdown, warm own-file profiles of the worst files with likely causes, and improvement suggestions. Use when asked to run an elaboration test, profile a repo build, or track elaboration health over time.
-
lean-learnings
Reusable Lean 4 and Mathlib lessons for analysis formalizations. Use when choosing an ambient carrier or repository layout, debugging elaboration and typeclass costs, preserving constant dependencies, or looking for recurring proof and API patterns.
-
lean-naming-style
Use when naming Lean declarations, organizing files, adding docstrings, or cleaning code so it matches Mathlib conventions and review expectations.
-
lean-orchestrator
Coordinate a large multi-agent Lean 4 formalization around exact author-approved declarations, source-level dependency graphs, independent statement audits, bounded proof tasks, and safe landings. Use when planning or running parallel Lean work, reviewing proof status, landing integrated results, or repairing a campaign affected by statement drift or hypothesis smuggling.
-
lean-project-architecture
Use when planning a Lean formalization, selecting and freezing author-approved declarations, choosing module boundaries, designing reusable APIs, or staging a large proof project into stable phases.
-
lean-proof-patterns
Use when writing, refactoring, or debugging Lean proofs and you need a stable translation from mathematical reasoning into explicit tactics, controlled rewriting, or maintainable proof structure.
-
lean-public-release
Prepare and verify a private Lean repository for public release. Use for source scrubbing, selective syncs, clean history, proof-status and license review, fresh-checkout builds, optional registry or comparator intake, independent review, and an explicit publication gate.
-
lean-search-discovery
Use when searching Mathlib for existing declarations, likely theorem names, relevant files, or proof ingredients before attempting a new Lean proof.
-
lean-statement-audit
Audit an exact manifest-bound Lean theorem or definition against its pinned mathematical source, with fail-closed binder, carrier, definition-body, characterization, consumption, and axiom checks. Use before approving a frozen declaration, after any frozen version change, before marking a source node proved, and before a theorem or section closure claim.
-
lean-workflow
Route Lean 4 work through a repository's Mathlib/Lake conventions. Use when editing Lean files, checking source fidelity or axioms, searching dependencies, validating focused targets, or protecting dependency build artifacts.
No matching skills