LeanAutoformalizationSkills

In the author's own words, from each skill's SKILL.md.

• 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 orche…

  skills/build-proof-dependency-graph/SKILL.md on GitHub (opens in a new tab)

• 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,…

  skills/lean-elaboration-test/SKILL.md on GitHub (opens in a new tab)

• 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 blow…

  skills/lean-elaboration/SKILL.md on GitHub (opens in a new tab)

• 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.

  skills/lean-learnings/SKILL.md on GitHub (opens in a new tab)

• lean-naming-style

  Use when naming Lean declarations, organizing files, adding docstrings, or cleaning code so it matches Mathlib conventions and review expectations.

  skills/lean-naming-style/SKILL.md on GitHub (opens in a new tab)

• 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.

  skills/lean-orchestrator/SKILL.md on GitHub (opens in a new tab)

• 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.

  skills/lean-project-architecture/SKILL.md on GitHub (opens in a new tab)

• 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.

  skills/lean-proof-patterns/SKILL.md on GitHub (opens in a new tab)

• 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.

  skills/lean-public-release/SKILL.md on GitHub (opens in a new tab)

• lean-search-discovery

  Use when searching Mathlib for existing declarations, likely theorem names, relevant files, or proof ingredients before attempting a new Lean proof.

  skills/lean-search-discovery/SKILL.md on GitHub (opens in a new tab)

• 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.

  skills/lean-statement-audit/SKILL.md on GitHub (opens in a new tab)

• 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.

  skills/lean-workflow/SKILL.md on GitHub (opens in a new tab)

No skill matches that filter.

Similar skills

• ECCby affaan-m The agent harness performance optimization system. Skills, instincts, memory, security, and research-first development for Claude Code, Cod… 280k stars · 30 skills
• reaby morluto Reverse engineer anything with agents, from app behavior down to native binaries. 270k stars · 1 skill
• andrej-karpathy-skillsby multica-ai A single CLAUDE.md file to improve Claude Code behavior, derived from Andrej Karpathy's observations on LLM coding pitfalls. 220k stars · 1 skill
• ponytailby DietrichGebert Makes your AI agent think like the laziest senior dev in the room. The best code is the code you never wrote. 164k stars · 6 skills
• ui-ux-pro-max-skillby nextlevelbuilder An AI skill that provides design intelligence for building professional UI/UX across multiple platforms. 136k stars · 7 skills
• graphifyby Graphify-Labs Turn any codebase, with its docs, SQL schemas, configs, and PDFs, into a queryable knowledge graph. A /graphify skill for Claude Code, Curs… 127k stars · 1 skill