Source-mapped help for proving and tooling
An installable agent skill for Lean programming, theorem proving, Mathlib, Lake, Elan, and editor workflows, mapped back to official sources.
The Lean 4 skill packages practical guidance for agents working across programs, proofs, formalization, package management, and editor tooling.
Its source snapshot is mapped to official Lean and Mathlib material so instructions can be audited and refreshed instead of becoming unattributed folklore.
It installs directly from the public repository through skills.sh and keeps the main skill concise by routing deeper questions to focused references.
where the effort went
the numbers
built with
delivery record
I kept repeating the same setup, proof-debugging, and source-verification steps across formalization projects, so I turned that working method into a reusable skill.
Installable Lean 4 skill with scoped activation rules
Twenty focused Markdown guides and references
Coverage for proving, programming, Mathlib, Lake, Elan, and VS Code
Source map to the official documentation snapshot
Progressive routing that keeps routine tasks compact
The constraints mattered as much as the finished interface.
after shipping
Reusable agent instructions need provenance and update boundaries just as much as code dependencies do.
The best context is the smallest source-backed slice that can answer the current proof state.