leanprover
- 9 skills
- 0 followers
- 8 hours ago last updated
- ▌ Code Review · leanproverPerforms thorough code reviews of individual human-eval problems. Use when asked explicity to review code or analyze code quality.
- ▌ Restructure Solutions · leanproverRestructures a Lean file with one or many solution implementations so that each solution is self-contained with its own Implementation, Tests, and Verification sections.
- ▌ Lean Beam · leanprover bundleUse this when an AI should work on an external Lean project through the installed `lean-beam` wrapper, giving it direct efficient access to Lean's proof engine to avoid repeated inner-loop rebuilds through cheap speculative checks and zero-build module checkpoints.
- ▌ Rocq Beam · leanprover bundleUse this when an AI needs the optional Rocq goal-probe surface exposed through the installed `lean-beam` wrapper while porting Rocq developments to Lean.
- ▌
- ▌ Verso Blueprint · leanprover bundleWork with Verso Blueprint Lean projects. Use when Codex needs to build or serve Blueprint HTML, query Blueprint labels/dependencies/owners/tags/work queues, debug generated graph/summary/preview data, inspect or edit Blueprint source modules, add conservative Blueprint nodes or metadata, or reason about `lake exe vbp` workflows in repositories using `VersoBlueprint`.
- ▌ Profiling · leanproverProfile Lean programs with demangled names using samply and Firefox Profiler. Use when the user asks to profile a Lean binary or investigate performance.
- ▌ Stage2 Olean Test · leanproverDiagnose a spurious stage1 test failure caused by olean-persisted compiler changes. Use when a stage1 test fails unexpectedly and the change adds or modifies an environment extension or other information persisted into .olean files.
- ▌ Release Highlights · leanproverWrite the Highlights section for Lean 4 release notes. Use when asked to write, draft, or update release highlights for a Lean version.