Mathlib Pr
REDIRECT — Mathlib PR workflow has been merged into the agnostic `lean-pr` SKILL, with Mathlib-specific conventions extracted to `references/upstream/mathlib4-pr.md` (W4 Wave 2 / move A1 of lab/design/07-cluster-workflow.md). This stub preserves the slug for Ctrl-F discoverability and incoming cross-references (per the zero-deletions Chesterton protocol).
Install
$ agentstack add skill-r-irbe-proof-skills-mathlib-pr ✓ scanned · ✓ verified — works with Claude Code, Cursor, and more.
Security review
✓ PassedNo issues found. Passed automated security review. · v0.1.0 How review works →
- ✓ Prompt-injection patterns
- ✓ Secret / credential exfiltration
- ✓ Dangerous shell & filesystem operations
- ✓ Untrusted network calls
- ✓ Known-malicious package signatures
What it can access
- ✓ Network access No
- ✓ Filesystem access No
- ✓ Shell / process execution No
- ✓ Environment & secrets No
- ✓ Dynamic code execution No
From automated source analysis of v0.1.0. “Used” means the capability is present in the source — more access means more to trust, not that it’s unsafe.
About
SK-30: Mathlib PR (REDIRECT)
This skill no longer hosts content. The generic PR workflow and the Mathlib-specific conventions are now separated cleanly: the agnostic workflow lives in [lean-pr](../lean-pr/SKILL.md), and the Mathlib-only deltas (commit format with (), labels, merge process via bors, lake exe mk_all) live in the upstream reference.
| Old section | New home | |---|---| | Commit message format ((): ) | [references/upstream/mathlib4-pr.md](../../../references/upstream/mathlib4-pr.md) §Commit message format | | Workflow (forks, mk_all, depends-on, !bench) | Same reference §Workflow | | Labels (author-managed / topic / downstream / automated) | Same reference §Labels | | Merge process (maintainer-merge → ready-to-merge → bors) | Same reference §Merge process | | Style and naming URLs | Same reference §Style and naming | | Generic agnostic PR workflow (dispatch, title shape, common ecosystem rules) | [../lean-pr/SKILL.md](../lean-pr/SKILL.md) |
Existing inbound links to "SK-30 / mathlib-pr" should resolve here and then follow the table above. lean-gateway/REFERENCE.md registry row continues to resolve to this stub. Do not add new content to this file — author it in references/upstream/mathlib4-pr.md (Mathlib- specific) or _overrides/lean-pr/SKILL.md (generic) instead.
See also
- [
../lean-pr/SKILL.md](../lean-pr/SKILL.md) — agnostic Lean-ecosystem PR SKILL (parent) - [
../../../references/upstream/mathlib4-pr.md](../../../references/upstream/mathlib4-pr.md) — full Mathlib-specific content - [
../../../references/upstream/lean4-pr.md](../../../references/upstream/lean4-pr.md) — Lean 4 core sister reference - [
../../../references/upstream/mathlib4-review.md](../../../references/upstream/mathlib4-review.md) — Mathlib PR review standards (sister W4 Wave 1)
Source & license
This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.
- Author: r-irbe
- Source: r-irbe/proof-skills
- License: Apache-2.0
- Homepage: https://github.com/r-irbe/proof-skills
Install and usage instructions live in the source repository linked above.
Reviews
No reviews yet — be the first.
Write a review
Versions
- v0.1.0 Imported from the upstream source.